[STATEMENT]
lemma reachable_node_impl_wt_instr:
  assumes "(P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, nt)"
  and "C \<noteq> ClassMain P"
  shows "\<exists>T mxs mpc xt. PROG P,T,mxs,mpc,xt \<turnstile> (instrs_of (PROG P) C M ! pc),pc :: TYPING P C M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>T mxs mpc xt. PROG P,T,mxs,mpc,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>T mxs mpc xt. PROG P,T,mxs,mpc,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M
[PROOF STEP]
from \<open>C \<noteq> ClassMain P\<close> \<open>(P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, nt)\<close>
    method_of_reachable_node_exists [of P C0 Main C M "\<lfloor>pc\<rfloor>" nt]
    instr_of_reachable_node_typable [of P C0 Main C M "\<lfloor>pc\<rfloor>" nt]
[PROOF STATE]
proof (chain)
picking this:
C \<noteq> ClassMain P
 (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, nt)
\<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, nt); C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C
\<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, nt); C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> case \<lfloor>pc\<rfloor> of None \<Rightarrow> True | \<lfloor>pc''\<rfloor> \<Rightarrow> TYPING P C M ! pc'' \<noteq> None \<and> pc'' < length (instrs_of (PROG P) C M)
[PROOF STEP]
obtain Ts T mxs mxl\<^sub>0 "is" xt
    where "PROG P \<turnstile> C sees M:Ts\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in C"
    and "TYPING P C M ! pc \<noteq> None"
    and "pc < length (instrs_of (PROG P) C M)"
[PROOF STATE]
proof (prove)
using this:
C \<noteq> ClassMain P
 (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, nt)
\<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, nt); C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> \<exists>Ts T mb. PROG P \<turnstile> C sees M: Ts\<rightarrow>T = mb in C
\<lbrakk> (P, C0, Main) \<turnstile> \<Rightarrow>(C, M, \<lfloor>pc\<rfloor>, nt); C \<noteq> ClassMain P\<rbrakk> \<Longrightarrow> case \<lfloor>pc\<rfloor> of None \<Rightarrow> True | \<lfloor>pc''\<rfloor> \<Rightarrow> TYPING P C M ! pc'' \<noteq> None \<and> pc'' < length (instrs_of (PROG P) C M)

goal (1 subgoal):
 1. (\<And>Ts T mxs mxl\<^sub>0 is xt. \<lbrakk>PROG P \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in C; TYPING P C M ! pc \<noteq> None; pc < length (instrs_of (PROG P) C M)\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by fastforce+
[PROOF STATE]
proof (state)
this:
PROG P \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in C
TYPING P C M ! pc \<noteq> None
pc < length (instrs_of (PROG P) C M)

goal (1 subgoal):
 1. \<exists>T mxs mpc xt. PROG P,T,mxs,mpc,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M
[PROOF STEP]
with wf_jvmprog_is_wf_typ [of P]
[PROOF STATE]
proof (chain)
picking this:
wf_jvm_prog\<^bsub>TYPING P\<^esub> (PROG P)
PROG P \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in C
TYPING P C M ! pc \<noteq> None
pc < length (instrs_of (PROG P) C M)
[PROOF STEP]
have "PROG P,T,mxs,length is,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M"
[PROOF STATE]
proof (prove)
using this:
wf_jvm_prog\<^bsub>TYPING P\<^esub> (PROG P)
PROG P \<turnstile> C sees M: Ts\<rightarrow>T = (mxs, mxl\<^sub>0, is, xt) in C
TYPING P C M ! pc \<noteq> None
pc < length (instrs_of (PROG P) C M)

goal (1 subgoal):
 1. PROG P,T,mxs,length is,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M
[PROOF STEP]
by (fastforce dest!: wt_jvm_prog_impl_wt_instr)
[PROOF STATE]
proof (state)
this:
PROG P,T,mxs,length is,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M

goal (1 subgoal):
 1. \<exists>T mxs mpc xt. PROG P,T,mxs,mpc,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
PROG P,T,mxs,length is,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M

goal (1 subgoal):
 1. \<exists>T mxs mpc xt. PROG P,T,mxs,mpc,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>T mxs mpc xt. PROG P,T,mxs,mpc,xt \<turnstile> instrs_of (PROG P) C M ! pc,pc :: TYPING P C M

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma [simp]:
  "size_exp' (Mat e pes) = Suc (size_exp' e + size_list (size_prod size size_exp') pes)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size_exp' (Mat e pes) = Suc (size_exp' e + size_list (size_prod size size_exp') pes)
[PROOF STEP]
apply (simp add: size_exp'.simps size_list_conv_sum_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map ((\<lambda>(p, es). Suc (size p + es)) \<circ> map_prod id size_exp') pes) = sum_list (map (size_prod size size_exp') pes)
[PROOF STEP]
apply (rule arg_cong[where f = sum_list])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((\<lambda>(p, es). Suc (size p + es)) \<circ> map_prod id size_exp') pes = map (size_prod size size_exp') pes
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]:
  "size_exp' (Handle e pes) = Suc (size_exp' e + size_list (size_prod size size_exp') pes)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size_exp' (Handle e pes) = Suc (size_exp' e + size_list (size_prod size size_exp') pes)
[PROOF STEP]
apply (simp add: size_exp'.simps size_list_conv_sum_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map ((\<lambda>(p, es). Suc (size p + es)) \<circ> map_prod id size_exp') pes) = sum_list (map (size_prod size size_exp') pes)
[PROOF STEP]
apply (rule arg_cong[where f = sum_list])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((\<lambda>(p, es). Suc (size p + es)) \<circ> map_prod id size_exp') pes = map (size_prod size size_exp') pes
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [simp]:
  "size_exp' (Letrec defs e) = Suc (size_exp' e + size_list (size_prod (\<lambda>_. 0) (size_prod (\<lambda>_. 0) size_exp')) defs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. size_exp' (Letrec defs e) = Suc (size_exp' e + size_list (size_prod (\<lambda>_. 0) (size_prod (\<lambda>_. 0) size_exp')) defs)
[PROOF STEP]
apply (simp add: size_exp'.simps size_list_conv_sum_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list (map ((\<lambda>(uu_, uu_, es). Suc (Suc es)) \<circ> map_prod id (map_prod id size_exp')) defs) = sum_list (map (size_prod (\<lambda>_. 0) (size_prod (\<lambda>_. 0) size_exp')) defs)
[PROOF STEP]
apply (rule arg_cong[where f = sum_list])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map ((\<lambda>(uu_, uu_, es). Suc (Suc es)) \<circ> map_prod id (map_prod id size_exp')) defs = map (size_prod (\<lambda>_. 0) (size_prod (\<lambda>_. 0) size_exp')) defs
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma mult_minus_eq_nat:
  fixes  x::nat and y ::nat and z::nat
  assumes " x+y = z"
  shows " -x-y = -z "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - int x - int y = - int z
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x + y = z

goal (1 subgoal):
 1. - int x - int y = - int z
[PROOF STEP]
by linarith


[STATEMENT]
lemma minus_eq_nat_subst: fixes A::nat and B::nat and  C::nat and  D::nat and  E::nat
  assumes "A = B-C-D" and " -E = -C-D"
  shows " A = B-E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B - E
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
A = B - C - D
- int E = - int C - int D

goal (1 subgoal):
 1. A = B - E
[PROOF STEP]
by linarith


[STATEMENT]
lemma minus_eq_nat_subst_order:  fixes  A::nat and  B::nat  and  C::nat  and  D::nat  and   E::nat
  assumes "B-C-D > 0" and "A = B-C-D+B"  shows "A = 2*B-C-D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = 2 * B - C - D
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < B - C - D
A = B - C - D + B

goal (1 subgoal):
 1. A = 2 * B - C - D
[PROOF STEP]
by auto


[STATEMENT]
lemma auxiliary_ineq: fixes x::nat assumes "x \<ge> (2::nat)"
  shows " x+1 < (2::nat)*x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + 1 < 2 * x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
2 \<le> x

goal (1 subgoal):
 1. x + 1 < 2 * x
[PROOF STEP]
by linarith


[STATEMENT]
lemma sum_strict_mono:
  fixes A :: "nat set"
  assumes "finite B" "A \<subset> B" "0 \<notin> B"
  shows "\<Sum> A < \<Sum> B"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum> A < \<Sum> B
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Sum> A < \<Sum> B
[PROOF STEP]
have "B - A \<noteq> {}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. B - A \<noteq> {}
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
A \<subset> B

goal (1 subgoal):
 1. B - A \<noteq> {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
B - A \<noteq> {}

goal (1 subgoal):
 1. \<Sum> A < \<Sum> B
[PROOF STEP]
with assms DiffE
[PROOF STATE]
proof (chain)
picking this:
finite B
A \<subset> B
0 \<notin> B
\<lbrakk>?c \<in> ?A - ?B; \<lbrakk>?c \<in> ?A; ?c \<notin> ?B\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
B - A \<noteq> {}
[PROOF STEP]
have "\<Sum> (B-A) > 0"
[PROOF STATE]
proof (prove)
using this:
finite B
A \<subset> B
0 \<notin> B
\<lbrakk>?c \<in> ?A - ?B; \<lbrakk>?c \<in> ?A; ?c \<notin> ?B\<rbrakk> \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P
B - A \<noteq> {}

goal (1 subgoal):
 1. 0 < \<Sum> (B - A)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
0 < \<Sum> (B - A)

goal (1 subgoal):
 1. \<Sum> A < \<Sum> B
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
0 < \<Sum> (B - A)

goal (1 subgoal):
 1. \<Sum> A < \<Sum> B
[PROOF STEP]
have "\<Sum> B = \<Sum> A + \<Sum> (B-A)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum> B = \<Sum> A + \<Sum> (B - A)
[PROOF STEP]
by (metis add.commute assms(1) assms(2) psubsetE sum.subset_diff)
[PROOF STATE]
proof (state)
this:
\<Sum> B = \<Sum> A + \<Sum> (B - A)

goal (1 subgoal):
 1. \<Sum> A < \<Sum> B
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
0 < \<Sum> (B - A)
\<Sum> B = \<Sum> A + \<Sum> (B - A)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
0 < \<Sum> (B - A)
\<Sum> B = \<Sum> A + \<Sum> (B - A)

goal (1 subgoal):
 1. \<Sum> A < \<Sum> B
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
\<Sum> A < \<Sum> B

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_image_eq:
  assumes "inj_on f A"
  shows "\<Sum> (f ` A) = (\<Sum> i \<in> A. f i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum> (f ` A) = sum f A
[PROOF STEP]
using assms sum.reindex_cong
[PROOF STATE]
proof (prove)
using this:
inj_on f A
\<lbrakk>inj_on ?l ?B; ?A = ?l ` ?B; \<And>x. x \<in> ?B \<Longrightarrow> ?g (?l x) = ?h x\<rbrakk> \<Longrightarrow> sum ?g ?A = sum ?h ?B

goal (1 subgoal):
 1. \<Sum> (f ` A) = sum f A
[PROOF STEP]
by fastforce


[STATEMENT]
lemma coprime_dvd_aux:
  assumes "gcd m n = Suc 0" "na dvd n" "ma dvd m" "mb dvd m" "nb dvd n" and eq: "ma * na = mb * nb"
  shows "ma = mb"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ma = mb
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. ma = mb
[PROOF STEP]
have "gcd na mb = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd na mb = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gcd m n = Suc 0
na dvd n
ma dvd m
mb dvd m
nb dvd n
ma * na = mb * nb

goal (1 subgoal):
 1. gcd na mb = 1
[PROOF STEP]
by (metis One_nat_def gcd.commute gcd_nat.mono is_unit_gcd_iff)
[PROOF STATE]
proof (state)
this:
gcd na mb = 1

goal (1 subgoal):
 1. ma = mb
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
gcd na mb = 1

goal (1 subgoal):
 1. ma = mb
[PROOF STEP]
have "gcd nb ma = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd nb ma = 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gcd m n = Suc 0
na dvd n
ma dvd m
mb dvd m
nb dvd n
ma * na = mb * nb

goal (1 subgoal):
 1. gcd nb ma = 1
[PROOF STEP]
by (metis One_nat_def gcd.commute gcd_nat.mono is_unit_gcd_iff)
[PROOF STATE]
proof (state)
this:
gcd nb ma = 1

goal (1 subgoal):
 1. ma = mb
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
gcd na mb = 1
gcd nb ma = 1
[PROOF STEP]
show "ma = mb"
[PROOF STATE]
proof (prove)
using this:
gcd na mb = 1
gcd nb ma = 1

goal (1 subgoal):
 1. ma = mb
[PROOF STEP]
by (metis eq gcd_mult_distrib_nat mult.commute nat_mult_1_right)
[PROOF STATE]
proof (state)
this:
ma = mb

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma def_equiv_divisor_set: "divisor_set (n::nat) = set(divisors_nat n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set n = set (divisors_nat n)
[PROOF STEP]
using  divisors_nat_def divisors_nat divisor_set divisor_def
[PROOF STATE]
proof (prove)
using this:
divisors_nat ?n \<equiv> if ?n = 0 then [] else remdups_adj (sort (map prod_list (subseqs (prime_factorization_nat ?n))))
?n \<noteq> 0 \<Longrightarrow> set (divisors_nat ?n) = {p. p dvd ?n}
distinct (divisors_nat ?n)
divisors_nat 0 = []
divisor_set ?m = {n. n divisor ?m}
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. divisor_set n = set (divisors_nat n)
[PROOF STEP]
by auto


[STATEMENT]
lemma example1_divisor: shows "(2::nat) \<in> divisor_set (4::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<in> divisor_set 4
[PROOF STEP]
using  divisor_set divisor_def
[PROOF STATE]
proof (prove)
using this:
divisor_set ?m = {n. n divisor ?m}
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. 2 \<in> divisor_set 4
[PROOF STEP]
by force


[STATEMENT]
lemma example2_properdiv_set: "properdiv_set (Suc (Suc (Suc 0))) = {(1::nat)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. properdiv_set (Suc (Suc (Suc 0))) = {1}
[PROOF STEP]
by (auto simp: properdiv_set proper_divisor_def less_Suc_eq dvd_def; presburger)


[STATEMENT]
lemma divisor_set_not_empty: fixes m::nat assumes "m \<ge>1"
  shows "m \<in> divisor_set m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m \<in> divisor_set m
[PROOF STEP]
using assms divisor_set divisor_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> m
divisor_set ?m = {n. n divisor ?m}
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. m \<in> divisor_set m
[PROOF STEP]
by force


[STATEMENT]
lemma finite_divisor_set [simp]: "finite(divisor_set n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (divisor_set n)
[PROOF STEP]
using divisor_def divisor_set
[PROOF STATE]
proof (prove)
using this:
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m
divisor_set ?m = {n. n divisor ?m}

goal (1 subgoal):
 1. finite (divisor_set n)
[PROOF STEP]
by simp


[STATEMENT]
lemma finite_properdiv_set[simp]: shows "finite(properdiv_set m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. finite (properdiv_set m)
[PROOF STEP]
using  properdiv_set proper_divisor_def
[PROOF STATE]
proof (prove)
using this:
properdiv_set ?m = {n. n properdiv ?m}
?n properdiv ?m \<equiv> 1 \<le> ?n \<and> ?n < ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. finite (properdiv_set m)
[PROOF STEP]
by simp


[STATEMENT]
lemma divisor_set_mult:
  "divisor_set  (m*n) = {i*j| i j. (i \<in> divisor_set m)\<and>(j \<in> divisor_set n)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set (m * n) = {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n}
[PROOF STEP]
using divisor_set divisor_def
[PROOF STATE]
proof (prove)
using this:
divisor_set ?m = {n. n divisor ?m}
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. divisor_set (m * n) = {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n}
[PROOF STEP]
by (fastforce simp add: divisor_set divisor_def dest: division_decomp)


[STATEMENT]
lemma divisor_set_1 [simp]: "divisor_set (Suc 0) = {Suc 0}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set (Suc 0) = {Suc 0}
[PROOF STEP]
by (simp add: divisor_set divisor_def cong: conj_cong)


[STATEMENT]
lemma divisor_set_one: shows "divisor_set 1 ={1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set 1 = {1}
[PROOF STEP]
using divisor_set  divisor_def
[PROOF STATE]
proof (prove)
using this:
divisor_set ?m = {n. n divisor ?m}
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. divisor_set 1 = {1}
[PROOF STEP]
by auto


[STATEMENT]
lemma union_properdiv_set: assumes "n\<ge>1" shows "divisor_set n =(properdiv_set n)\<union>{n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set n = properdiv_set n \<union> {n}
[PROOF STEP]
using divisor_set properdiv_set  proper_divisor_def assms  divisor_def
[PROOF STATE]
proof (prove)
using this:
divisor_set ?m = {n. n divisor ?m}
properdiv_set ?m = {n. n properdiv ?m}
?n properdiv ?m \<equiv> 1 \<le> ?n \<and> ?n < ?m \<and> ?n dvd ?m
1 \<le> n
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. divisor_set n = properdiv_set n \<union> {n}
[PROOF STEP]
by auto


[STATEMENT]
lemma prime_div_set: assumes "prime n" shows "divisor_set n = {n, 1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set n = {n, 1}
[PROOF STEP]
using divisor_def assms divisor_set  prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m
prime n
divisor_set ?m = {n. n divisor ?m}
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))

goal (1 subgoal):
 1. divisor_set n = {n, 1}
[PROOF STEP]
by auto


[STATEMENT]
lemma div_set_prime:
  assumes "prime n"
  shows "properdiv_set n = {1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. properdiv_set n = {1}
[PROOF STEP]
using assms properdiv_set prime_nat_iff proper_divisor_def
[PROOF STATE]
proof (prove)
using this:
prime n
properdiv_set ?m = {n. n properdiv ?m}
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))
?n properdiv ?m \<equiv> 1 \<le> ?n \<and> ?n < ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. properdiv_set n = {1}
[PROOF STEP]
by (metis (no_types, lifting) Collect_cong One_nat_def divisor_def divisor_set divisor_set_one
 dvd_1_left empty_iff insert_iff mem_Collect_eq order_less_irrefl)


[STATEMENT]
lemma prime_gcd: fixes m::nat and n::nat assumes "prime m" and "prime n"
and "m \<noteq> n" shows "gcd m n =1 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd m n = 1
[PROOF STEP]
using prime_def
[PROOF STATE]
proof (prove)
using this:
prime ?p = (prime_elem ?p \<and> normalize ?p = ?p)

goal (1 subgoal):
 1. gcd m n = 1
[PROOF STEP]
by (simp add: assms primes_coprime)


[STATEMENT]
lemma example_perfect_6: shows "perfect_number 6"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perfect_number 6
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. perfect_number 6
[PROOF STEP]
have a: "set(divisors_nat 6) = {1, 2, 3, 6}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 6) = {1, 2, 3, 6}
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
set (divisors_nat 6) = {1, 2, 3, 6}

goal (1 subgoal):
 1. perfect_number 6
[PROOF STEP]
have b: "divisor_set (6) = {1, 2, 3, 6}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set 6 = {1, 2, 3, 6}
[PROOF STEP]
using a  def_equiv_divisor_set
[PROOF STATE]
proof (prove)
using this:
set (divisors_nat 6) = {1, 2, 3, 6}
divisor_set ?n = set (divisors_nat ?n)

goal (1 subgoal):
 1. divisor_set 6 = {1, 2, 3, 6}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
divisor_set 6 = {1, 2, 3, 6}

goal (1 subgoal):
 1. perfect_number 6
[PROOF STEP]
have  c: "properdiv_set (6) = {1, 2, 3}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. properdiv_set 6 = {1, 2, 3}
[PROOF STEP]
using b union_properdiv_set properdiv_set proper_divisor_def
[PROOF STATE]
proof (prove)
using this:
divisor_set 6 = {1, 2, 3, 6}
1 \<le> ?n \<Longrightarrow> divisor_set ?n = properdiv_set ?n \<union> {?n}
properdiv_set ?m = {n. n properdiv ?m}
?n properdiv ?m \<equiv> 1 \<le> ?n \<and> ?n < ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. properdiv_set 6 = {1, 2, 3}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
properdiv_set 6 = {1, 2, 3}

goal (1 subgoal):
 1. perfect_number 6
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perfect_number 6
[PROOF STEP]
using aliquot_sum_def c
[PROOF STATE]
proof (prove)
using this:
aliquot_sum ?n \<equiv> \<Sum> (properdiv_set ?n)
properdiv_set 6 = {1, 2, 3}

goal (1 subgoal):
 1. perfect_number 6
[PROOF STEP]
by (simp add: numeral_3_eq_3 perfect_number_def)
[PROOF STATE]
proof (state)
this:
perfect_number 6

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Esigma_properdiv_set:
  assumes "m \<ge> 1"
  shows "Esigma m = (aliquot_sum m) + m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma m = aliquot_sum m + m
[PROOF STEP]
using assms divisor_set properdiv_set proper_divisor_def union_properdiv_set  Esigma_def
        aliquot_sum_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> m
divisor_set ?m = {n. n divisor ?m}
properdiv_set ?m = {n. n properdiv ?m}
?n properdiv ?m \<equiv> 1 \<le> ?n \<and> ?n < ?m \<and> ?n dvd ?m
1 \<le> ?n \<Longrightarrow> divisor_set ?n = properdiv_set ?n \<union> {?n}
Esigma ?n \<equiv> \<Sum> (divisor_set ?n)
aliquot_sum ?n \<equiv> \<Sum> (properdiv_set ?n)

goal (1 subgoal):
 1. Esigma m = aliquot_sum m + m
[PROOF STEP]
by fastforce


[STATEMENT]
lemma Esigmanotzero:
  assumes "n \<ge> 1"
  shows "Esigma n \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> Esigma n
[PROOF STEP]
using Esigma_def assms Esigma_properdiv_set
[PROOF STATE]
proof (prove)
using this:
Esigma ?n \<equiv> \<Sum> (divisor_set ?n)
1 \<le> n
1 \<le> ?m \<Longrightarrow> Esigma ?m = aliquot_sum ?m + ?m

goal (1 subgoal):
 1. 1 \<le> Esigma n
[PROOF STEP]
by auto


[STATEMENT]
lemma prime_sum_div:
  assumes "prime n"
  shows " Esigma n = n +(1::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma n = n + 1
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma n = n + 1
[PROOF STEP]
have "1 \<le> n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> n
[PROOF STEP]
using assms prime_ge_1_nat
[PROOF STATE]
proof (prove)
using this:
prime n
prime ?p \<Longrightarrow> 1 \<le> ?p

goal (1 subgoal):
 1. 1 \<le> n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
1 \<le> n

goal (1 subgoal):
 1. Esigma n = n + 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
1 \<le> n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 \<le> n

goal (1 subgoal):
 1. Esigma n = n + 1
[PROOF STEP]
using Esigma_properdiv_set assms div_set_prime
[PROOF STATE]
proof (prove)
using this:
1 \<le> n
1 \<le> ?m \<Longrightarrow> Esigma ?m = aliquot_sum ?m + ?m
prime n
prime ?n \<Longrightarrow> properdiv_set ?n = {1}

goal (1 subgoal):
 1. Esigma n = n + 1
[PROOF STEP]
by (simp add: Esigma_properdiv_set aliquot_sum_def assms div_set_prime)
[PROOF STATE]
proof (state)
this:
Esigma n = n + 1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma sum_div_is_prime:
  assumes "Esigma n = n +(1::nat)" and "n \<ge>1"
  shows "prime n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime n
[PROOF STEP]
proof (rule ccontr)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> prime n \<Longrightarrow> False
[PROOF STEP]
assume F: " \<not> (prime n)"
[PROOF STATE]
proof (state)
this:
\<not> prime n

goal (1 subgoal):
 1. \<not> prime n \<Longrightarrow> False
[PROOF STEP]
have " n divisor n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n divisor n
[PROOF STEP]
using assms divisor_def
[PROOF STATE]
proof (prove)
using this:
Esigma n = n + 1
1 \<le> n
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. n divisor n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n divisor n

goal (1 subgoal):
 1. \<not> prime n \<Longrightarrow> False
[PROOF STEP]
have " (1::nat) divisor n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 divisor n
[PROOF STEP]
using assms divisor_def
[PROOF STATE]
proof (prove)
using this:
Esigma n = n + 1
1 \<le> n
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. 1 divisor n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 divisor n

goal (1 subgoal):
 1. \<not> prime n \<Longrightarrow> False
[PROOF STEP]
have "n \<noteq> Suc 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n \<noteq> Suc 0
[PROOF STEP]
using Esigma_def assms(1)
[PROOF STATE]
proof (prove)
using this:
Esigma ?n \<equiv> \<Sum> (divisor_set ?n)
Esigma n = n + 1

goal (1 subgoal):
 1. n \<noteq> Suc 0
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
n \<noteq> Suc 0

goal (1 subgoal):
 1. \<not> prime n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
n \<noteq> Suc 0
[PROOF STEP]
have r: " \<exists>( m::nat). m \<in> divisor_set n \<and> m\<noteq> (1::nat) \<and> m \<noteq> n"
[PROOF STATE]
proof (prove)
using this:
n \<noteq> Suc 0

goal (1 subgoal):
 1. \<exists>m. m \<in> divisor_set n \<and> m \<noteq> 1 \<and> m \<noteq> n
[PROOF STEP]
using assms F
[PROOF STATE]
proof (prove)
using this:
n \<noteq> Suc 0
Esigma n = n + 1
1 \<le> n
\<not> prime n

goal (1 subgoal):
 1. \<exists>m. m \<in> divisor_set n \<and> m \<noteq> 1 \<and> m \<noteq> n
[PROOF STEP]
apply (clarsimp simp add: Esigma_def divisor_set divisor_def prime_nat_iff)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>m. \<lbrakk>n \<noteq> Suc 0; \<Sum> {na. Suc 0 \<le> na \<and> na \<le> n \<and> na dvd n} = Suc n; Suc 0 \<le> n; m dvd n; m \<noteq> Suc 0; m \<noteq> n\<rbrakk> \<Longrightarrow> \<exists>m\<ge>Suc 0. m \<le> n \<and> m dvd n \<and> m \<noteq> Suc 0 \<and> m \<noteq> n
[PROOF STEP]
by (meson Suc_le_eq dvd_imp_le dvd_pos_nat)
[PROOF STATE]
proof (state)
this:
\<exists>m. m \<in> divisor_set n \<and> m \<noteq> 1 \<and> m \<noteq> n

goal (1 subgoal):
 1. \<not> prime n \<Longrightarrow> False
[PROOF STEP]
have "Suc n = \<Sum>{n,1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Suc n = \<Sum> {n, 1}
[PROOF STEP]
by (simp add: \<open>n \<noteq> Suc 0\<close>)
[PROOF STATE]
proof (state)
this:
Suc n = \<Sum> {n, 1}

goal (1 subgoal):
 1. \<not> prime n \<Longrightarrow> False
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
Suc n = \<Sum> {n, 1}

goal (1 subgoal):
 1. \<not> prime n \<Longrightarrow> False
[PROOF STEP]
have "divisor_set n \<supset> {n,1}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {n, 1} \<subset> divisor_set n
[PROOF STEP]
using assms divisor_set r \<open>1 divisor n\<close> divisor_set_not_empty
[PROOF STATE]
proof (prove)
using this:
Esigma n = n + 1
1 \<le> n
divisor_set ?m = {n. n divisor ?m}
\<exists>m. m \<in> divisor_set n \<and> m \<noteq> 1 \<and> m \<noteq> n
1 divisor n
1 \<le> ?m \<Longrightarrow> ?m \<in> divisor_set ?m

goal (1 subgoal):
 1. {n, 1} \<subset> divisor_set n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{n, 1} \<subset> divisor_set n

goal (1 subgoal):
 1. \<not> prime n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
{n, 1} \<subset> divisor_set n
[PROOF STEP]
have "\<Sum>(divisor_set n) > \<Sum>{n,1}"
[PROOF STATE]
proof (prove)
using this:
{n, 1} \<subset> divisor_set n

goal (1 subgoal):
 1. \<Sum> {n, 1} < \<Sum> (divisor_set n)
[PROOF STEP]
apply (rule sum_strict_mono [OF finite_divisor_set])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 \<notin> divisor_set n
[PROOF STEP]
by (simp add: divisor_def divisor_set)
[PROOF STATE]
proof (state)
this:
\<Sum> {n, 1} < \<Sum> (divisor_set n)

goal (1 subgoal):
 1. \<not> prime n \<Longrightarrow> False
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
Suc n = \<Sum> {n, 1}
\<Sum> {n, 1} < \<Sum> (divisor_set n)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Suc n = \<Sum> {n, 1}
\<Sum> {n, 1} < \<Sum> (divisor_set n)

goal (1 subgoal):
 1. False
[PROOF STEP]
using Esigma_def assms(1)
[PROOF STATE]
proof (prove)
using this:
Suc n = \<Sum> {n, 1}
\<Sum> {n, 1} < \<Sum> (divisor_set n)
Esigma ?n \<equiv> \<Sum> (divisor_set ?n)
Esigma n = n + 1

goal (1 subgoal):
 1. False
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Esigma_prime_sum:
  fixes k:: nat assumes "prime m" "k \<ge>1"
  shows "Esigma (m^k) =( m^(k+(1::nat)) -(1::nat)) /(m-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma (m ^ k)) = real (m ^ (k + 1) - 1) / (real m - 1)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real (Esigma (m ^ k)) = real (m ^ (k + 1) - 1) / (real m - 1)
[PROOF STEP]
have "m > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < m
[PROOF STEP]
using \<open>prime m\<close> prime_gt_1_nat
[PROOF STATE]
proof (prove)
using this:
prime m
prime ?p \<Longrightarrow> 1 < ?p

goal (1 subgoal):
 1. 1 < m
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
1 < m

goal (1 subgoal):
 1. real (Esigma (m ^ k)) = real (m ^ (k + 1) - 1) / (real m - 1)
[PROOF STEP]
have A: " Esigma (m^k) =( \<Sum> j= 0..k.( m^j)) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (m ^ k) = sum ((^) m) {0..k}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (m ^ k) = sum ((^) m) {0..k}
[PROOF STEP]
have AA: "divisor_set (m^k) = (\<lambda>j. m ^ j) ` {0..k}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set (m ^ k) = (^) m ` {0..k}
[PROOF STEP]
using assms prime_ge_1_nat
[PROOF STATE]
proof (prove)
using this:
prime m
1 \<le> k
prime ?p \<Longrightarrow> 1 \<le> ?p

goal (1 subgoal):
 1. divisor_set (m ^ k) = (^) m ` {0..k}
[PROOF STEP]
by (auto simp add: power_increasing prime_ge_Suc_0_nat divisor_set divisor_def image_iff
 divides_primepow_nat)
[PROOF STATE]
proof (state)
this:
divisor_set (m ^ k) = (^) m ` {0..k}

goal (1 subgoal):
 1. Esigma (m ^ k) = sum ((^) m) {0..k}
[PROOF STEP]
have \<section>: "\<Sum> ((\<lambda>j. m ^ j) ` {..k}) = sum (\<lambda>j. m ^ j) {0..k}"  for k
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum> ((^) m ` {..k}) = sum ((^) m) {0..k}
[PROOF STEP]
proof (induction k)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<Sum> ((^) m ` {..0}) = sum ((^) m) {0..0}
 2. \<And>k. \<Sum> ((^) m ` {..k}) = sum ((^) m) {0..k} \<Longrightarrow> \<Sum> ((^) m ` {..Suc k}) = sum ((^) m) {0..Suc k}
[PROOF STEP]
case (Suc k)
[PROOF STATE]
proof (state)
this:
\<Sum> ((^) m ` {..k}) = sum ((^) m) {0..k}

goal (2 subgoals):
 1. \<Sum> ((^) m ` {..0}) = sum ((^) m) {0..0}
 2. \<And>k. \<Sum> ((^) m ` {..k}) = sum ((^) m) {0..k} \<Longrightarrow> \<Sum> ((^) m ` {..Suc k}) = sum ((^) m) {0..Suc k}
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<Sum> ((^) m ` {..k}) = sum ((^) m) {0..k}
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
\<Sum> ((^) m ` {..k}) = sum ((^) m) {0..k}

goal (1 subgoal):
 1. \<Sum> ((^) m ` {..Suc k}) = sum ((^) m) {0..Suc k}
[PROOF STEP]
apply (clarsimp simp: atMost_Suc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum> ((^) m ` {..k}) = sum ((^) m) {0..k} \<Longrightarrow> \<Sum> (insert (m * m ^ k) ((^) m ` {..k})) = sum ((^) m) {0..k} + m * m ^ k
[PROOF STEP]
by (smt add.commute add_le_same_cancel1 assms(1) atMost_iff finite_atMost finite_imageI
image_iff le_zero_eq power_add power_one_right prime_power_inj sum.insert zero_neq_one)
[PROOF STATE]
proof (state)
this:
\<Sum> ((^) m ` {..Suc k}) = sum ((^) m) {0..Suc k}

goal (1 subgoal):
 1. \<Sum> ((^) m ` {..0}) = sum ((^) m) {0..0}
[PROOF STEP]
qed auto
[PROOF STATE]
proof (state)
this:
\<Sum> ((^) m ` {..?k}) = sum ((^) m) {0..?k}

goal (1 subgoal):
 1. Esigma (m ^ k) = sum ((^) m) {0..k}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (m ^ k) = sum ((^) m) {0..k}
[PROOF STEP]
by (metis "\<section>" AA Esigma_def atMost_atLeast0)
[PROOF STATE]
proof (state)
this:
Esigma (m ^ k) = sum ((^) m) {0..k}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (m ^ k) = sum ((^) m) {0..k}

goal (1 subgoal):
 1. real (Esigma (m ^ k)) = real (m ^ (k + 1) - 1) / (real m - 1)
[PROOF STEP]
have B: "(\<Sum> i\<le>k.( m^i)) = ( m^Suc k -(1::nat)) /(m-(1::nat))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (sum ((^) m) {..k}) = real (m ^ Suc k - 1) / real (m - 1)
[PROOF STEP]
using assms \<open>m > 1\<close> Set_Interval.geometric_sum  [of m "Suc k"]
[PROOF STATE]
proof (prove)
using this:
prime m
1 \<le> k
1 < m
real m \<noteq> 1 \<Longrightarrow> sum ((^) (real m)) {..<Suc k} = (real m ^ Suc k - 1) / (real m - 1)

goal (1 subgoal):
 1. real (sum ((^) m) {..k}) = real (m ^ Suc k - 1) / real (m - 1)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>prime m; Suc 0 \<le> k; Suc 0 < m; sum ((^) (real m)) {..<k} + real m ^ k = (real m * real m ^ k - 1) / (real m - 1)\<rbrakk> \<Longrightarrow> sum ((^) (real m)) {..k} = real (m * m ^ k - Suc 0) / real (m - Suc 0)
[PROOF STEP]
by (metis One_nat_def lessThan_Suc_atMost nat_one_le_power of_nat_1 of_nat_diff of_nat_mult
of_nat_power one_le_mult_iff prime_ge_Suc_0_nat sum.lessThan_Suc)
[PROOF STATE]
proof (state)
this:
real (sum ((^) m) {..k}) = real (m ^ Suc k - 1) / real (m - 1)

goal (1 subgoal):
 1. real (Esigma (m ^ k)) = real (m ^ (k + 1) - 1) / (real m - 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma (m ^ k)) = real (m ^ (k + 1) - 1) / (real m - 1)
[PROOF STEP]
using A B assms
[PROOF STATE]
proof (prove)
using this:
Esigma (m ^ k) = sum ((^) m) {0..k}
real (sum ((^) m) {..k}) = real (m ^ Suc k - 1) / real (m - 1)
prime m
1 \<le> k

goal (1 subgoal):
 1. real (Esigma (m ^ k)) = real (m ^ (k + 1) - 1) / (real m - 1)
[PROOF STEP]
by (metis Suc_eq_plus1 atMost_atLeast0 of_nat_1 of_nat_diff prime_ge_1_nat)
[PROOF STATE]
proof (state)
this:
real (Esigma (m ^ k)) = real (m ^ (k + 1) - 1) / (real m - 1)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma prime_Esigma_mult: assumes "prime m" and "prime n" and "m \<noteq> n"
  shows "Esigma (m*n) = (Esigma n)*(Esigma m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (m * n) = Esigma n * Esigma m
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (m * n) = Esigma n * Esigma m
[PROOF STEP]
have "m divisor (m*n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m divisor (m * n)
[PROOF STEP]
using divisor_def assms
[PROOF STATE]
proof (prove)
using this:
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m
prime m
prime n
m \<noteq> n

goal (1 subgoal):
 1. m divisor (m * n)
[PROOF STEP]
by (simp add: dvd_imp_le prime_gt_0_nat)
[PROOF STATE]
proof (state)
this:
m divisor (m * n)

goal (1 subgoal):
 1. Esigma (m * n) = Esigma n * Esigma m
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
m divisor (m * n)

goal (1 subgoal):
 1. Esigma (m * n) = Esigma n * Esigma m
[PROOF STEP]
have "\<not>(\<exists> k::nat. k divisor (m*n) \<and> k\<noteq>(1::nat)\<and> k \<noteq> m \<and> k \<noteq> n \<and> k\<noteq> m*n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<nexists>k. k divisor (m * n) \<and> k \<noteq> 1 \<and> k \<noteq> m \<and> k \<noteq> n \<and> k \<noteq> m * n
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
prime m
prime n
m \<noteq> n

goal (1 subgoal):
 1. \<nexists>k. k divisor (m * n) \<and> k \<noteq> 1 \<and> k \<noteq> m \<and> k \<noteq> n \<and> k \<noteq> m * n
[PROOF STEP]
unfolding divisor_def
[PROOF STATE]
proof (prove)
using this:
prime m
prime n
m \<noteq> n

goal (1 subgoal):
 1. \<nexists>k. (1 \<le> k \<and> k \<le> m * n \<and> k dvd m * n) \<and> k \<noteq> 1 \<and> k \<noteq> m \<and> k \<noteq> n \<and> k \<noteq> m * n
[PROOF STEP]
by (metis One_nat_def division_decomp nat_mult_1 nat_mult_1_right prime_nat_iff)
[PROOF STATE]
proof (state)
this:
\<nexists>k. k divisor (m * n) \<and> k \<noteq> 1 \<and> k \<noteq> m \<and> k \<noteq> n \<and> k \<noteq> m * n

goal (1 subgoal):
 1. Esigma (m * n) = Esigma n * Esigma m
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
m divisor (m * n)
\<nexists>k. k divisor (m * n) \<and> k \<noteq> 1 \<and> k \<noteq> m \<and> k \<noteq> n \<and> k \<noteq> m * n
[PROOF STEP]
have c: "divisor_set (m*n) = {m, n, m*n, 1}"
[PROOF STATE]
proof (prove)
using this:
m divisor (m * n)
\<nexists>k. k divisor (m * n) \<and> k \<noteq> 1 \<and> k \<noteq> m \<and> k \<noteq> n \<and> k \<noteq> m * n

goal (1 subgoal):
 1. divisor_set (m * n) = {m, n, m * n, 1}
[PROOF STEP]
using divisor_set assms  divisor_def
[PROOF STATE]
proof (prove)
using this:
m divisor (m * n)
\<nexists>k. k divisor (m * n) \<and> k \<noteq> 1 \<and> k \<noteq> m \<and> k \<noteq> n \<and> k \<noteq> m * n
divisor_set ?m = {n. n divisor ?m}
prime m
prime n
m \<noteq> n
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. divisor_set (m * n) = {m, n, m * n, 1}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
divisor_set (m * n) = {m, n, m * n, 1}

goal (1 subgoal):
 1. Esigma (m * n) = Esigma n * Esigma m
[PROOF STEP]
obtain "m\<noteq>1" "n\<noteq>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>m \<noteq> 1; n \<noteq> 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms not_prime_1
[PROOF STATE]
proof (prove)
using this:
prime m
prime n
m \<noteq> n
\<not> prime (1::?'a)

goal (1 subgoal):
 1. (\<lbrakk>m \<noteq> 1; n \<noteq> 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
m \<noteq> 1
n \<noteq> 1

goal (1 subgoal):
 1. Esigma (m * n) = Esigma n * Esigma m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
m \<noteq> 1
n \<noteq> 1
[PROOF STEP]
have dd: "Esigma (m*n) = m + n +m *n +1"
[PROOF STATE]
proof (prove)
using this:
m \<noteq> 1
n \<noteq> 1

goal (1 subgoal):
 1. Esigma (m * n) = m + n + m * n + 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m \<noteq> 1
n \<noteq> 1
prime m
prime n
m \<noteq> n

goal (1 subgoal):
 1. Esigma (m * n) = m + n + m * n + 1
[PROOF STEP]
by (simp add: Esigma_def c)
[PROOF STATE]
proof (state)
this:
Esigma (m * n) = m + n + m * n + 1

goal (1 subgoal):
 1. Esigma (m * n) = Esigma n * Esigma m
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Esigma (m * n) = m + n + m * n + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Esigma (m * n) = m + n + m * n + 1

goal (1 subgoal):
 1. Esigma (m * n) = Esigma n * Esigma m
[PROOF STEP]
using prime_sum_div assms
[PROOF STATE]
proof (prove)
using this:
Esigma (m * n) = m + n + m * n + 1
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1
prime m
prime n
m \<noteq> n

goal (1 subgoal):
 1. Esigma (m * n) = Esigma n * Esigma m
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma (m * n) = Esigma n * Esigma m

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma gcd_Esigma_mult:
  assumes "gcd m n = 1"
  shows "Esigma (m*n) = (Esigma m)*(Esigma n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
have "Esigma (m*n) = \<Sum> {i*j| i j. i \<in> divisor_set m \<and> j \<in> divisor_set n}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (m * n) = \<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n}
[PROOF STEP]
by (simp add: divisor_set_mult Esigma_def)
[PROOF STATE]
proof (state)
this:
Esigma (m * n) = \<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n}

goal (1 subgoal):
 1. Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Esigma (m * n) = \<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n}

goal (1 subgoal):
 1. Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
have "... = (\<Sum>i \<in> divisor_set m. \<Sum>j \<in> divisor_set n. i*j)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n))
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n))
[PROOF STEP]
have "inj_on (\<lambda>(i,j). i*j) (divisor_set m \<times> divisor_set n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. inj_on (\<lambda>(i, j). i * j) (divisor_set m \<times> divisor_set n)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
gcd m n = 1

goal (1 subgoal):
 1. inj_on (\<lambda>(i, j). i * j) (divisor_set m \<times> divisor_set n)
[PROOF STEP]
apply (simp add: inj_on_def divisor_set divisor_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd m n = Suc 0 \<Longrightarrow> \<forall>x. Suc 0 \<le> x \<and> x \<le> m \<and> x dvd m \<longrightarrow> (\<forall>y. Suc 0 \<le> y \<and> y \<le> n \<and> y dvd n \<longrightarrow> (\<forall>xa. Suc 0 \<le> xa \<and> xa \<le> m \<and> xa dvd m \<longrightarrow> (\<forall>ya. Suc 0 \<le> ya \<and> ya \<le> n \<and> ya dvd n \<longrightarrow> x * y = xa * ya \<longrightarrow> x = xa \<and> y = ya)))
[PROOF STEP]
by (metis assms coprime_dvd_aux mult_left_cancel not_one_le_zero)
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>(i, j). i * j) (divisor_set m \<times> divisor_set n)

goal (1 subgoal):
 1. \<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n))
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
inj_on (\<lambda>(i, j). i * j) (divisor_set m \<times> divisor_set n)

goal (1 subgoal):
 1. \<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n))
[PROOF STEP]
have
"{i*j| i j. i \<in> divisor_set m \<and> j \<in> divisor_set n}= (\<lambda>(i,j). i*j)`(divisor_set m \<times> divisor_set n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<lambda>(i, j). i * j) ` (divisor_set m \<times> divisor_set n)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<lambda>(i, j). i * j) ` (divisor_set m \<times> divisor_set n)

goal (1 subgoal):
 1. \<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n))
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
inj_on (\<lambda>(i, j). i * j) (divisor_set m \<times> divisor_set n)
{i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<lambda>(i, j). i * j) ` (divisor_set m \<times> divisor_set n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
inj_on (\<lambda>(i, j). i * j) (divisor_set m \<times> divisor_set n)
{i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<lambda>(i, j). i * j) ` (divisor_set m \<times> divisor_set n)

goal (1 subgoal):
 1. \<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n))
[PROOF STEP]
by (simp add: sum.cartesian_product sum_image_eq)
[PROOF STATE]
proof (state)
this:
\<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n))

goal (1 subgoal):
 1. Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
\<Sum> {i * j |i j. i \<in> divisor_set m \<and> j \<in> divisor_set n} = (\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n))

goal (1 subgoal):
 1. Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
have "... = \<Sum>( divisor_set m)* \<Sum>( divisor_set n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n)) = \<Sum> (divisor_set m) * \<Sum> (divisor_set n)
[PROOF STEP]
by (simp add: sum_product)
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n)) = \<Sum> (divisor_set m) * \<Sum> (divisor_set n)

goal (1 subgoal):
 1. Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<Sum>i\<in>divisor_set m. sum ((*) i) (divisor_set n)) = \<Sum> (divisor_set m) * \<Sum> (divisor_set n)

goal (1 subgoal):
 1. Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
have "... = Esigma m * Esigma n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum> (divisor_set m) * \<Sum> (divisor_set n) = Esigma m * Esigma n
[PROOF STEP]
by (simp add: Esigma_def)
[PROOF STATE]
proof (state)
this:
\<Sum> (divisor_set m) * \<Sum> (divisor_set n) = Esigma m * Esigma n

goal (1 subgoal):
 1. Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
Esigma (m * n) = Esigma m * Esigma n

goal (1 subgoal):
 1. Esigma (m * n) = Esigma m * Esigma n
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Esigma (m * n) = Esigma m * Esigma n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deficient_Esigma:
  assumes "Esigma m < 2*m" and "m \<ge>1"
  shows "deficient_number m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deficient_number m
[PROOF STEP]
using Esigma_properdiv_set assms deficient_number_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?m \<Longrightarrow> Esigma ?m = aliquot_sum ?m + ?m
Esigma m < 2 * m
1 \<le> m
deficient_number ?n \<equiv> aliquot_sum ?n < ?n

goal (1 subgoal):
 1. deficient_number m
[PROOF STEP]
by auto


[STATEMENT]
lemma abundant_Esigma:
  assumes "Esigma m > 2*m" and "m \<ge>1"
  shows "abundant_number m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abundant_number m
[PROOF STEP]
using Esigma_properdiv_set assms abundant_number_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?m \<Longrightarrow> Esigma ?m = aliquot_sum ?m + ?m
2 * m < Esigma m
1 \<le> m
abundant_number ?n \<equiv> ?n < aliquot_sum ?n

goal (1 subgoal):
 1. abundant_number m
[PROOF STEP]
by auto


[STATEMENT]
lemma perfect_Esigma:
  assumes "Esigma m = 2*m" and "m \<ge>1"
  shows "perfect_number m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perfect_number m
[PROOF STEP]
using Esigma_properdiv_set assms perfect_number_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> ?m \<Longrightarrow> Esigma ?m = aliquot_sum ?m + ?m
Esigma m = 2 * m
1 \<le> m
perfect_number ?n \<equiv> ?n = aliquot_sum ?n

goal (1 subgoal):
 1. perfect_number m
[PROOF STEP]
by auto


[STATEMENT]
lemma Amicable_pair_sym: fixes m::nat and n ::nat
  assumes "m Amic n " shows "n Amic m "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n Amic m
[PROOF STEP]
using  Amicable_pair_def assms
[PROOF STATE]
proof (prove)
using this:
?m Amic ?n \<equiv> ?m = aliquot_sum ?n \<and> ?n = aliquot_sum ?m
m Amic n

goal (1 subgoal):
 1. n Amic m
[PROOF STEP]
by blast


[STATEMENT]
lemma Amicable_pair_equiv_def:
  assumes "(m Amic n)" and "m \<ge>1" and "n \<ge>1"
  shows   "(Esigma m = Esigma n)\<and>(Esigma m = m+n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma m = Esigma n \<and> Esigma m = m + n
[PROOF STEP]
using assms Amicable_pair_def
[PROOF STATE]
proof (prove)
using this:
m Amic n
1 \<le> m
1 \<le> n
?m Amic ?n \<equiv> ?m = aliquot_sum ?n \<and> ?n = aliquot_sum ?m

goal (1 subgoal):
 1. Esigma m = Esigma n \<and> Esigma m = m + n
[PROOF STEP]
by (metis Esigma_properdiv_set add.commute)


[STATEMENT]
lemma Amicable_pair_equiv_def_conv:
  assumes "m\<ge>1" and "n\<ge>1" and "(Esigma m = Esigma n)\<and>(Esigma m = m+n)"
  shows  "(m Amic n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
using assms Amicable_pair_def Esigma_properdiv_set
[PROOF STATE]
proof (prove)
using this:
1 \<le> m
1 \<le> n
Esigma m = Esigma n \<and> Esigma m = m + n
?m Amic ?n \<equiv> ?m = aliquot_sum ?n \<and> ?n = aliquot_sum ?m
1 \<le> ?m \<Longrightarrow> Esigma ?m = aliquot_sum ?m + ?m

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
by (metis add_right_imp_eq add.commute )


[STATEMENT]
lemma Amicable_pair_deficient: assumes "m > n" and  "m Amic n"
  shows "deficient_number m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deficient_number m
[PROOF STEP]
using assms deficient_number_def Amicable_pair_def
[PROOF STATE]
proof (prove)
using this:
n < m
m Amic n
deficient_number ?n \<equiv> aliquot_sum ?n < ?n
?m Amic ?n \<equiv> ?m = aliquot_sum ?n \<and> ?n = aliquot_sum ?m

goal (1 subgoal):
 1. deficient_number m
[PROOF STEP]
by metis


[STATEMENT]
lemma Amicable_pair_abundant: assumes "m > n" and  "m Amic n"
  shows "abundant_number n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abundant_number n
[PROOF STEP]
using assms abundant_number_def Amicable_pair_def
[PROOF STATE]
proof (prove)
using this:
n < m
m Amic n
abundant_number ?n \<equiv> ?n < aliquot_sum ?n
?m Amic ?n \<equiv> ?m = aliquot_sum ?n \<and> ?n = aliquot_sum ?m

goal (1 subgoal):
 1. abundant_number n
[PROOF STEP]
by metis


[STATEMENT]
lemma even_even_amicable: assumes  "m Amic n" and "m \<ge>1" and "n \<ge>1" and "even m" and "even n"
  shows "(2*m \<noteq> n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * m \<noteq> n
[PROOF STEP]
proof( rule ccontr )
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> 2 * m \<noteq> n \<Longrightarrow> False
[PROOF STEP]
have a: "Esigma m  = Esigma n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma m = Esigma n
[PROOF STEP]
using \<open>m Amic n\<close> Amicable_pair_equiv_def Amicable_pair_def
     assms
[PROOF STATE]
proof (prove)
using this:
m Amic n
\<lbrakk>?m Amic ?n; 1 \<le> ?m; 1 \<le> ?n\<rbrakk> \<Longrightarrow> Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n
?m Amic ?n \<equiv> ?m = aliquot_sum ?n \<and> ?n = aliquot_sum ?m
m Amic n
1 \<le> m
1 \<le> n
even m
even n

goal (1 subgoal):
 1. Esigma m = Esigma n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Esigma m = Esigma n

goal (1 subgoal):
 1. \<not> 2 * m \<noteq> n \<Longrightarrow> False
[PROOF STEP]
assume "\<not> (2*m \<noteq> n)"
[PROOF STATE]
proof (state)
this:
\<not> 2 * m \<noteq> n

goal (1 subgoal):
 1. \<not> 2 * m \<noteq> n \<Longrightarrow> False
[PROOF STEP]
have "(2*m = n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * m = n
[PROOF STEP]
using \<open>\<not> (2*m \<noteq> n)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 2 * m \<noteq> n

goal (1 subgoal):
 1. 2 * m = n
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 * m = n

goal (1 subgoal):
 1. \<not> 2 * m \<noteq> n \<Longrightarrow> False
[PROOF STEP]
have d:"Esigma n = Esigma (2*m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma n = Esigma (2 * m)
[PROOF STEP]
using  \<open>\<not> (2*m \<noteq> n)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> 2 * m \<noteq> n

goal (1 subgoal):
 1. Esigma n = Esigma (2 * m)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma n = Esigma (2 * m)

goal (1 subgoal):
 1. \<not> 2 * m \<noteq> n \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Esigma n = Esigma (2 * m)
[PROOF STEP]
show False
[PROOF STATE]
proof (prove)
using this:
Esigma n = Esigma (2 * m)

goal (1 subgoal):
 1. False
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma n = Esigma (2 * m) \<Longrightarrow> False
[PROOF STEP]
have w: "2*m \<in> divisor_set (2*m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * m \<in> divisor_set (2 * m)
[PROOF STEP]
using divisor_set assms divisor_set_not_empty
[PROOF STATE]
proof (prove)
using this:
divisor_set ?m = {n. n divisor ?m}
m Amic n
1 \<le> m
1 \<le> n
even m
even n
1 \<le> ?m \<Longrightarrow> ?m \<in> divisor_set ?m

goal (1 subgoal):
 1. 2 * m \<in> divisor_set (2 * m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 * m \<in> divisor_set (2 * m)

goal (1 subgoal):
 1. Esigma n = Esigma (2 * m) \<Longrightarrow> False
[PROOF STEP]
have w1: "2*m \<notin> divisor_set (m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * m \<notin> divisor_set m
[PROOF STEP]
using divisor_set assms
[PROOF STATE]
proof (prove)
using this:
divisor_set ?m = {n. n divisor ?m}
m Amic n
1 \<le> m
1 \<le> n
even m
even n

goal (1 subgoal):
 1. 2 * m \<notin> divisor_set m
[PROOF STEP]
by (simp add: divisor_def)
[PROOF STATE]
proof (state)
this:
2 * m \<notin> divisor_set m

goal (1 subgoal):
 1. Esigma n = Esigma (2 * m) \<Longrightarrow> False
[PROOF STEP]
have w2: "\<forall> n::nat. n divisor m \<longrightarrow> n divisor (2*m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>n. n divisor m \<longrightarrow> n divisor (2 * m)
[PROOF STEP]
using assms divisor_def
[PROOF STATE]
proof (prove)
using this:
m Amic n
1 \<le> m
1 \<le> n
even m
even n
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m

goal (1 subgoal):
 1. \<forall>n. n divisor m \<longrightarrow> n divisor (2 * m)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>n. n divisor m \<longrightarrow> n divisor (2 * m)

goal (1 subgoal):
 1. Esigma n = Esigma (2 * m) \<Longrightarrow> False
[PROOF STEP]
have w3: "divisor_set (2*m) \<supset> divisor_set m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set m \<subset> divisor_set (2 * m)
[PROOF STEP]
using divisor_set divisor_def assms w w1 w2
[PROOF STATE]
proof (prove)
using this:
divisor_set ?m = {n. n divisor ?m}
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m
m Amic n
1 \<le> m
1 \<le> n
even m
even n
2 * m \<in> divisor_set (2 * m)
2 * m \<notin> divisor_set m
\<forall>n. n divisor m \<longrightarrow> n divisor (2 * m)

goal (1 subgoal):
 1. divisor_set m \<subset> divisor_set (2 * m)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
divisor_set m \<subset> divisor_set (2 * m)

goal (1 subgoal):
 1. Esigma n = Esigma (2 * m) \<Longrightarrow> False
[PROOF STEP]
have v: "( \<Sum> i \<in> ( divisor_set (2*m)).i)> ( \<Sum> i \<in> ( divisor_set m).i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum> (divisor_set m) < \<Sum> (divisor_set (2 * m))
[PROOF STEP]
using w3  sum_strict_mono
[PROOF STATE]
proof (prove)
using this:
divisor_set m \<subset> divisor_set (2 * m)
\<lbrakk>finite ?B; ?A \<subset> ?B; 0 \<notin> ?B\<rbrakk> \<Longrightarrow> \<Sum> ?A < \<Sum> ?B

goal (1 subgoal):
 1. \<Sum> (divisor_set m) < \<Sum> (divisor_set (2 * m))
[PROOF STEP]
by (simp add: divisor_def divisor_set)
[PROOF STATE]
proof (state)
this:
\<Sum> (divisor_set m) < \<Sum> (divisor_set (2 * m))

goal (1 subgoal):
 1. Esigma n = Esigma (2 * m) \<Longrightarrow> False
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. False
[PROOF STEP]
using v d Esigma_def a
[PROOF STATE]
proof (prove)
using this:
\<Sum> (divisor_set m) < \<Sum> (divisor_set (2 * m))
Esigma n = Esigma (2 * m)
Esigma ?n \<equiv> \<Sum> (divisor_set ?n)
Esigma m = Esigma n

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma regularAmicPair_sym:
  assumes "regularAmicPair n m" shows "regularAmicPair m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regularAmicPair m n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. regularAmicPair m n
[PROOF STEP]
have "gcd m n = gcd n m"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd m n = gcd n m
[PROOF STEP]
by (metis (no_types) gcd.commute)
[PROOF STATE]
proof (state)
this:
gcd m n = gcd n m

goal (1 subgoal):
 1. regularAmicPair m n
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
gcd m n = gcd n m
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
gcd m n = gcd n m

goal (1 subgoal):
 1. regularAmicPair m n
[PROOF STEP]
using Amicable_pair_sym assms regularAmicPair_def
[PROOF STATE]
proof (prove)
using this:
gcd m n = gcd n m
?m Amic ?n \<Longrightarrow> ?n Amic ?m
regularAmicPair n m
regularAmicPair ?n ?m = (?n Amic ?m \<and> (\<exists>M N g. g = gcd ?m ?n \<and> ?m = M * g \<and> ?n = N * g \<and> squarefree M \<and> squarefree N \<and> gcd g M = 1 \<and> gcd g N = 1))

goal (1 subgoal):
 1. regularAmicPair m n
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
regularAmicPair m n

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma irregularAmicPair_sym:
  assumes "irregularAmicPair n m"
  shows "irregularAmicPair m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. irregularAmicPair m n
[PROOF STEP]
using  irregularAmicPair_def regularAmicPair_sym Amicable_pair_sym assms
[PROOF STATE]
proof (prove)
using this:
irregularAmicPair ?n ?m = (?n Amic ?m \<and> \<not> regularAmicPair ?n ?m)
regularAmicPair ?n ?m \<Longrightarrow> regularAmicPair ?m ?n
?m Amic ?n \<Longrightarrow> ?n Amic ?m
irregularAmicPair n m

goal (1 subgoal):
 1. irregularAmicPair m n
[PROOF STEP]
by blast


[STATEMENT]
lemma twinAmicPair_sym:
  assumes "twinAmicPair n m"
  shows "twinAmicPair m n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. twinAmicPair m n
[PROOF STEP]
using assms twinAmicPair_def Amicable_pair_sym assms
[PROOF STATE]
proof (prove)
using this:
twinAmicPair n m
twinAmicPair ?n ?m = (?n Amic ?m \<and> (\<nexists>k l. Min {?n, ?m} < k \<and> k < Max {?n, ?m} \<and> k Amic l))
?m Amic ?n \<Longrightarrow> ?n Amic ?m
twinAmicPair n m

goal (1 subgoal):
 1. twinAmicPair m n
[PROOF STEP]
by auto


[STATEMENT]
lemma isotopic_amicable_pair:
  fixes m n g h M N :: nat
  assumes "m Amic n" and "m \<ge> 1" and "n \<ge> 1"and "m= g*M" and "n = g*N"
      and "Esigma h = (h/g) * Esigma g" and "h \<noteq> g" and "h > 1" and "g > 1"
      and "gcd g M = 1" and "gcd g N = 1" and "gcd h M = 1" and "gcd h N = 1"
    shows "(h*M) Amic (h*N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
have a: "Esigma m = Esigma n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma m = Esigma n
[PROOF STEP]
using \<open> m Amic n\<close>  Amicable_pair_equiv_def assms
[PROOF STATE]
proof (prove)
using this:
m Amic n
\<lbrakk>?m Amic ?n; 1 \<le> ?m; 1 \<le> ?n\<rbrakk> \<Longrightarrow> Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. Esigma m = Esigma n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Esigma m = Esigma n

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
have b: "Esigma m = m + n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma m = m + n
[PROOF STEP]
using \<open> m Amic n\<close> Amicable_pair_equiv_def assms
[PROOF STATE]
proof (prove)
using this:
m Amic n
\<lbrakk>?m Amic ?n; 1 \<le> ?m; 1 \<le> ?n\<rbrakk> \<Longrightarrow> Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. Esigma m = m + n
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
Esigma m = m + n

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
have c: "Esigma (h*M) = (Esigma h)*(Esigma M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (h * M) = Esigma h * Esigma M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (h * M) = Esigma h * Esigma M
[PROOF STEP]
have  "h \<noteq> M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<noteq> M
[PROOF STEP]
using assms Esigmanotzero gcd_Esigma_mult gcd_nat.idem b mult_eq_self_implies_10
[PROOF STATE]
proof (prove)
using this:
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1
1 \<le> ?n \<Longrightarrow> 1 \<le> Esigma ?n
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n
gcd ?a ?a = ?a
Esigma m = m + n
?m = ?m * ?n \<Longrightarrow> ?n = 1 \<or> ?m = 0

goal (1 subgoal):
 1. h \<noteq> M
[PROOF STEP]
by (metis less_irrefl)
[PROOF STATE]
proof (state)
this:
h \<noteq> M

goal (1 subgoal):
 1. Esigma (h * M) = Esigma h * Esigma M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (h * M) = Esigma h * Esigma M
[PROOF STEP]
using  \<open>h \<noteq> M\<close>  gcd_Esigma_mult assms
[PROOF STATE]
proof (prove)
using this:
h \<noteq> M
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. Esigma (h * M) = Esigma h * Esigma M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma (h * M) = Esigma h * Esigma M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (h * M) = Esigma h * Esigma M

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
have d: "Esigma (g*M) = (Esigma g)*(Esigma M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (g * M) = Esigma g * Esigma M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (g * M) = Esigma g * Esigma M
[PROOF STEP]
have  "g\<noteq>M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<noteq> M
[PROOF STEP]
using assms gcd_nat.idem
[PROOF STATE]
proof (prove)
using this:
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1
gcd ?a ?a = ?a

goal (1 subgoal):
 1. g \<noteq> M
[PROOF STEP]
by (metis less_irrefl)
[PROOF STATE]
proof (state)
this:
g \<noteq> M

goal (1 subgoal):
 1. Esigma (g * M) = Esigma g * Esigma M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (g * M) = Esigma g * Esigma M
[PROOF STEP]
using  \<open>g\<noteq>M\<close>  gcd_Esigma_mult assms
[PROOF STATE]
proof (prove)
using this:
g \<noteq> M
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. Esigma (g * M) = Esigma g * Esigma M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma (g * M) = Esigma g * Esigma M

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (g * M) = Esigma g * Esigma M

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
have e: "Esigma (g*N) = (Esigma g)*(Esigma N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (g * N) = Esigma g * Esigma N
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (g * N) = Esigma g * Esigma N
[PROOF STEP]
have  "g\<noteq>N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g \<noteq> N
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. g \<noteq> N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
g \<noteq> N

goal (1 subgoal):
 1. Esigma (g * N) = Esigma g * Esigma N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (g * N) = Esigma g * Esigma N
[PROOF STEP]
using  \<open>g\<noteq>N\<close>  gcd_Esigma_mult assms
[PROOF STATE]
proof (prove)
using this:
g \<noteq> N
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. Esigma (g * N) = Esigma g * Esigma N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma (g * N) = Esigma g * Esigma N

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (g * N) = Esigma g * Esigma N

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
have p1: "Esigma m = (Esigma g)*(Esigma M)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma m = Esigma g * Esigma M
[PROOF STEP]
using assms d
[PROOF STATE]
proof (prove)
using this:
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1
Esigma (g * M) = Esigma g * Esigma M

goal (1 subgoal):
 1. Esigma m = Esigma g * Esigma M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma m = Esigma g * Esigma M

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
have p2: "Esigma n = (Esigma g)*(Esigma N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma n = Esigma g * Esigma N
[PROOF STEP]
using assms e
[PROOF STATE]
proof (prove)
using this:
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1
Esigma (g * N) = Esigma g * Esigma N

goal (1 subgoal):
 1. Esigma n = Esigma g * Esigma N
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma n = Esigma g * Esigma N

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
have p3: "Esigma (h*N) = (Esigma h)*(Esigma N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (h * N) = Esigma h * Esigma N
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (h * N) = Esigma h * Esigma N
[PROOF STEP]
have  "h\<noteq>N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<noteq> N
[PROOF STEP]
using assms \<open> gcd h N =1\<close>  a b p2
[PROOF STATE]
proof (prove)
using this:
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1
gcd h N = 1
Esigma m = Esigma n
Esigma m = m + n
Esigma n = Esigma g * Esigma N

goal (1 subgoal):
 1. h \<noteq> N
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
h \<noteq> N

goal (1 subgoal):
 1. Esigma (h * N) = Esigma h * Esigma N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (h * N) = Esigma h * Esigma N
[PROOF STEP]
using  \<open>h \<noteq> N\<close>  gcd_Esigma_mult  assms
[PROOF STATE]
proof (prove)
using this:
h \<noteq> N
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. Esigma (h * N) = Esigma h * Esigma N
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma (h * N) = Esigma h * Esigma N

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (h * N) = Esigma h * Esigma N

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
have A: "Esigma (h*M) = Esigma (h*N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (h * M) = Esigma (h * N)
[PROOF STEP]
using c p3 d e p1 p2 a assms Esigmanotzero
[PROOF STATE]
proof (prove)
using this:
Esigma (h * M) = Esigma h * Esigma M
Esigma (h * N) = Esigma h * Esigma N
Esigma (g * M) = Esigma g * Esigma M
Esigma (g * N) = Esigma g * Esigma N
Esigma m = Esigma g * Esigma M
Esigma n = Esigma g * Esigma N
Esigma m = Esigma n
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1
1 \<le> ?n \<Longrightarrow> 1 \<le> Esigma ?n

goal (1 subgoal):
 1. Esigma (h * M) = Esigma (h * N)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Esigma (h * M) = Esigma (h * N)

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
have B:  "Esigma (h*M)=(h*M)+(h*N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (h * M) = h * M + h * N
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (h * M) = h * M + h * N
[PROOF STEP]
have s: "Esigma (h*M) = (h/g)*(m+n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma (h * M)) = real h / real g * real (m + n)
[PROOF STEP]
using b c p1 Esigmanotzero assms
[PROOF STATE]
proof (prove)
using this:
Esigma m = m + n
Esigma (h * M) = Esigma h * Esigma M
Esigma m = Esigma g * Esigma M
1 \<le> ?n \<Longrightarrow> 1 \<le> Esigma ?n
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. real (Esigma (h * M)) = real h / real g * real (m + n)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real (Esigma (h * M)) = real h / real g * real (m + n)

goal (1 subgoal):
 1. Esigma (h * M) = h * M + h * N
[PROOF STEP]
have s1: "Esigma (h*M) = h*(m/g+n/g)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma (h * M)) = real h * (real m / real g + real n / real g)
[PROOF STEP]
using  s assms
[PROOF STATE]
proof (prove)
using this:
real (Esigma (h * M)) = real h / real g * real (m + n)
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. real (Esigma (h * M)) = real h * (real m / real g + real n / real g)
[PROOF STEP]
by (metis add_divide_distrib b of_nat_add semiring_normalization_rules(7)
 times_divide_eq_left times_divide_eq_right)
[PROOF STATE]
proof (state)
this:
real (Esigma (h * M)) = real h * (real m / real g + real n / real g)

goal (1 subgoal):
 1. Esigma (h * M) = h * M + h * N
[PROOF STEP]
have s2: " Esigma (h*M) = h*(M+N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (h * M) = h * (M + N)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (h * M) = h * (M + N)
[PROOF STEP]
have v: "m/g = M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real m / real g = real M
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. real m / real g = real M
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real m / real g = real M

goal (1 subgoal):
 1. Esigma (h * M) = h * (M + N)
[PROOF STEP]
have v1:"n/g = N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real n / real g = real N
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. real n / real g = real N
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
real n / real g = real N

goal (1 subgoal):
 1. Esigma (h * M) = h * (M + N)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (h * M) = h * (M + N)
[PROOF STEP]
using s1 v v1 assms
[PROOF STATE]
proof (prove)
using this:
real (Esigma (h * M)) = real h * (real m / real g + real n / real g)
real m / real g = real M
real n / real g = real N
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. Esigma (h * M) = h * (M + N)
[PROOF STEP]
using of_nat_eq_iff
[PROOF STATE]
proof (prove)
using this:
real (Esigma (h * M)) = real h * (real m / real g + real n / real g)
real m / real g = real M
real n / real g = real N
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1
(of_nat ?m = of_nat ?n) = (?m = ?n)

goal (1 subgoal):
 1. Esigma (h * M) = h * (M + N)
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
Esigma (h * M) = h * (M + N)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (h * M) = h * (M + N)

goal (1 subgoal):
 1. Esigma (h * M) = h * M + h * N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (h * M) = h * M + h * N
[PROOF STEP]
using s2 assms
[PROOF STATE]
proof (prove)
using this:
Esigma (h * M) = h * (M + N)
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1

goal (1 subgoal):
 1. Esigma (h * M) = h * M + h * N
[PROOF STEP]
by (simp add: add_mult_distrib2)
[PROOF STATE]
proof (state)
this:
Esigma (h * M) = h * M + h * N

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (h * M) = h * M + h * N

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
using Amicable_pair_equiv_def_conv A B assms one_le_mult_iff  One_nat_def Suc_leI
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 \<le> ?m; 1 \<le> ?n; Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n\<rbrakk> \<Longrightarrow> ?m Amic ?n
Esigma (h * M) = Esigma (h * N)
Esigma (h * M) = h * M + h * N
m Amic n
1 \<le> m
1 \<le> n
m = g * M
n = g * N
real (Esigma h) = real h / real g * real (Esigma g)
h \<noteq> g
1 < h
1 < g
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1
(Suc 0 \<le> ?m * ?n) = (Suc 0 \<le> ?m \<and> Suc 0 \<le> ?n)
1 = Suc 0
?m < ?n \<Longrightarrow> Suc ?m \<le> ?n

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
by (metis (no_types, opaque_lifting)  nat_less_le)
[PROOF STATE]
proof (state)
this:
(h * M) Amic (h * N)

goal:
No subgoals!
[PROOF STEP]
qed