[STATEMENT]
lemma isotopic_pair_example1:
  assumes "(3^3*5*11*17*227) Amic (3^3*5*23*37*53)"
  shows  "(3^2*7*13*11*17*227) Amic (3^2*7*13*23*37*53)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
obtain m where o1: "m = (3::nat)^3*5*11*17*227"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>m. m = 3 ^ 3 * 5 * 11 * 17 * 227 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
m = 3 ^ 3 * 5 * 11 * 17 * 227

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
obtain n where o2: "n = (3::nat)^3*5*23*37*53"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>n. n = 3 ^ 3 * 5 * 23 * 37 * 53 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
n = 3 ^ 3 * 5 * 23 * 37 * 53

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
obtain g where o3: "g = (3::nat)^3*5"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>g. g = 3 ^ 3 * 5 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g = 3 ^ 3 * 5

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
obtain h where o4: "h = (3::nat)^2*7*13"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>h. h = 3\<^sup>2 * 7 * 13 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h = 3\<^sup>2 * 7 * 13

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
obtain M where o5: "M = (11::nat)*17*227"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>M. M = 11 * 17 * 227 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
M = 11 * 17 * 227

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
obtain N where o6: "N = (23::nat)*37*53"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. N = 23 * 37 * 53 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
N = 23 * 37 * 53

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have "prime(3::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 3
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 3

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have "prime(5::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 5
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 5

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have "prime(7::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 7
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 7

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have "prime(13::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 13
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 13

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have v: "m Amic n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
using o1 o2 assms
[PROOF STATE]
proof (prove)
using this:
m = 3 ^ 3 * 5 * 11 * 17 * 227
n = 3 ^ 3 * 5 * 23 * 37 * 53
(3 ^ 3 * 5 * 11 * 17 * 227) Amic (3 ^ 3 * 5 * 23 * 37 * 53)

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

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have v1: "m = g*M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m = g * M
[PROOF STEP]
using o1 o3 o5
[PROOF STATE]
proof (prove)
using this:
m = 3 ^ 3 * 5 * 11 * 17 * 227
g = 3 ^ 3 * 5
M = 11 * 17 * 227

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

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have v2: "n = g*N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n = g * N
[PROOF STEP]
using o2 o3 o6
[PROOF STATE]
proof (prove)
using this:
n = 3 ^ 3 * 5 * 23 * 37 * 53
g = 3 ^ 3 * 5
N = 23 * 37 * 53

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

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have v3: "h >0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < h
[PROOF STEP]
using o4
[PROOF STATE]
proof (prove)
using this:
h = 3\<^sup>2 * 7 * 13

goal (1 subgoal):
 1. 0 < h
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < h

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have w: "g >0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < g
[PROOF STEP]
using o3
[PROOF STATE]
proof (prove)
using this:
g = 3 ^ 3 * 5

goal (1 subgoal):
 1. 0 < g
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
0 < g

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have w1: "h \<noteq> g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<noteq> g
[PROOF STEP]
using o4 o3
[PROOF STATE]
proof (prove)
using this:
h = 3\<^sup>2 * 7 * 13
g = 3 ^ 3 * 5

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

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have "h = 819"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h = 819
[PROOF STEP]
using o4
[PROOF STATE]
proof (prove)
using this:
h = 3\<^sup>2 * 7 * 13

goal (1 subgoal):
 1. h = 819
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
h = 819

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have "g = 135"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. g = 135
[PROOF STEP]
using o3
[PROOF STATE]
proof (prove)
using this:
g = 3 ^ 3 * 5

goal (1 subgoal):
 1. g = 135
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
g = 135

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have w2: "Esigma h = (h/g)*Esigma g"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma h) = real h / real g * real (Esigma g)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real (Esigma h) = real h / real g * real (Esigma g)
[PROOF STEP]
have B: "Esigma h = 1456"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma h = 1456
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma h = 1456
[PROOF STEP]
have R: "set(divisors_nat 819) ={1, 3, 7, 9, 13, 21, 39, 63, 91, 117, 273, 819}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 819) = {1, 3, 7, 9, 13, 21, 39, 63, 91, 117, 273, 819}
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
set (divisors_nat 819) = {1, 3, 7, 9, 13, 21, 39, 63, 91, 117, 273, 819}

goal (1 subgoal):
 1. Esigma h = 1456
[PROOF STEP]
have RR: "set( divisors_nat(819)) = divisor_set (819)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 819) = divisor_set 819
[PROOF STEP]
using def_equiv_divisor_set
[PROOF STATE]
proof (prove)
using this:
divisor_set ?n = set (divisors_nat ?n)

goal (1 subgoal):
 1. set (divisors_nat 819) = divisor_set 819
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (divisors_nat 819) = divisor_set 819

goal (1 subgoal):
 1. Esigma h = 1456
[PROOF STEP]
show?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma h = 1456
[PROOF STEP]
using Esigma_def RR R \<open> h = 819\<close> divisor_def divisors_nat divisors_nat_def
[PROOF STATE]
proof (prove)
using this:
Esigma ?n \<equiv> \<Sum> (divisor_set ?n)
set (divisors_nat 819) = divisor_set 819
set (divisors_nat 819) = {1, 3, 7, 9, 13, 21, 39, 63, 91, 117, 273, 819}
h = 819
?n divisor ?m \<equiv> 1 \<le> ?n \<and> ?n \<le> ?m \<and> ?n dvd ?m
?n \<noteq> 0 \<Longrightarrow> set (divisors_nat ?n) = {p. p dvd ?n}
distinct (divisors_nat ?n)
divisors_nat 0 = []
divisors_nat ?n \<equiv> if ?n = 0 then [] else remdups_adj (sort (map prod_list (subseqs (prime_factorization_nat ?n))))

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

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

goal (1 subgoal):
 1. real (Esigma h) = real h / real g * real (Esigma g)
[PROOF STEP]
have C: "Esigma g = 240"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma g = 240
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma g = 240
[PROOF STEP]
have G: "set(divisors_nat 135) = {1, 3, 5, 9, 15, 27, 45, 135}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 135) = {1, 3, 5, 9, 15, 27, 45, 135}
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
set (divisors_nat 135) = {1, 3, 5, 9, 15, 27, 45, 135}

goal (1 subgoal):
 1. Esigma g = 240
[PROOF STEP]
have GG:  "set(divisors_nat 135) = divisor_set 135"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 135) = divisor_set 135
[PROOF STEP]
using  def_equiv_divisor_set
[PROOF STATE]
proof (prove)
using this:
divisor_set ?n = set (divisors_nat ?n)

goal (1 subgoal):
 1. set (divisors_nat 135) = divisor_set 135
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (divisors_nat 135) = divisor_set 135

goal (1 subgoal):
 1. Esigma g = 240
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma g = 240
[PROOF STEP]
using G GG Esigma_def  \<open> g = 135\<close>
      properdiv_set proper_divisor_def
[PROOF STATE]
proof (prove)
using this:
set (divisors_nat 135) = {1, 3, 5, 9, 15, 27, 45, 135}
set (divisors_nat 135) = divisor_set 135
Esigma ?n \<equiv> \<Sum> (divisor_set ?n)
g = 135
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. Esigma g = 240
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma g = 240

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

goal (1 subgoal):
 1. real (Esigma h) = real h / real g * real (Esigma g)
[PROOF STEP]
have D: "(Esigma h) * g = (Esigma g) * h"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma h * g = Esigma g * h
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma h * g = Esigma g * h
[PROOF STEP]
have A: "(Esigma h) * g = 196560"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma h * g = 196560
[PROOF STEP]
using B o3
[PROOF STATE]
proof (prove)
using this:
Esigma h = 1456
g = 3 ^ 3 * 5

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

goal (1 subgoal):
 1. Esigma h * g = Esigma g * h
[PROOF STEP]
have AA: "(Esigma g) * h = 196560"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma g * h = 196560
[PROOF STEP]
using C o4
[PROOF STATE]
proof (prove)
using this:
Esigma g = 240
h = 3\<^sup>2 * 7 * 13

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

goal (1 subgoal):
 1. Esigma h * g = Esigma g * h
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma h * g = Esigma g * h
[PROOF STEP]
using A AA
[PROOF STATE]
proof (prove)
using this:
Esigma h * g = 196560
Esigma g * h = 196560

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

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

goal (1 subgoal):
 1. real (Esigma h) = real h / real g * real (Esigma g)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma h) = real h / real g * real (Esigma g)
[PROOF STEP]
using D
[PROOF STATE]
proof (prove)
using this:
Esigma h * g = Esigma g * h

goal (1 subgoal):
 1. real (Esigma h) = real h / real g * real (Esigma g)
[PROOF STEP]
by (metis mult.commute nat_neq_iff nonzero_mult_div_cancel_right
of_nat_eq_0_iff of_nat_mult times_divide_eq_left w)
[PROOF STATE]
proof (state)
this:
real (Esigma h) = real h / real g * real (Esigma g)

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

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have w4: "gcd g M =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd g M = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gcd g M = 1
[PROOF STEP]
have "coprime g M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime g M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coprime g M
[PROOF STEP]
have "\<not> g dvd M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> g dvd M
[PROOF STEP]
using o3 o5
[PROOF STATE]
proof (prove)
using this:
g = 3 ^ 3 * 5
M = 11 * 17 * 227

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

goal (1 subgoal):
 1. coprime g M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> g dvd M

goal (1 subgoal):
 1. coprime g M
[PROOF STEP]
have  "\<not> 3 dvd M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 3 dvd M
[PROOF STEP]
using o5
[PROOF STATE]
proof (prove)
using this:
M = 11 * 17 * 227

goal (1 subgoal):
 1. \<not> 3 dvd M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> 3 dvd M

goal (1 subgoal):
 1. coprime g M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> 3 dvd M

goal (1 subgoal):
 1. coprime g M
[PROOF STEP]
have  "\<not> 5 dvd M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 5 dvd M
[PROOF STEP]
using o5
[PROOF STATE]
proof (prove)
using this:
M = 11 * 17 * 227

goal (1 subgoal):
 1. \<not> 5 dvd M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> 5 dvd M

goal (1 subgoal):
 1. coprime g M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> g dvd M
\<not> 3 dvd M
\<not> 5 dvd M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> g dvd M
\<not> 3 dvd M
\<not> 5 dvd M

goal (1 subgoal):
 1. coprime g M
[PROOF STEP]
using o5 o3
     gcd_nat.absorb_iff2 prime_nat_iff \<open> prime(3::nat)\<close> \<open> prime(5::nat)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> g dvd M
\<not> 3 dvd M
\<not> 5 dvd M
M = 11 * 17 * 227
g = 3 ^ 3 * 5
(?b dvd ?a) = (gcd ?a ?b = ?b)
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))
prime 3
prime 5

goal (1 subgoal):
 1. coprime g M
[PROOF STEP]
by (metis coprime_commute
coprime_mult_left_iff prime_imp_coprime_nat prime_imp_power_coprime_nat)
[PROOF STATE]
proof (state)
this:
coprime g M

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

goal (1 subgoal):
 1. gcd g M = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd g M = 1
[PROOF STEP]
using \<open>coprime g M\<close>
[PROOF STATE]
proof (prove)
using this:
coprime g M

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

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

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have s: " gcd g N =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd g N = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gcd g N = 1
[PROOF STEP]
have "coprime g N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime g N
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coprime g N
[PROOF STEP]
have "\<not> g dvd N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> g dvd N
[PROOF STEP]
using o3 o6
[PROOF STATE]
proof (prove)
using this:
g = 3 ^ 3 * 5
N = 23 * 37 * 53

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

goal (1 subgoal):
 1. coprime g N
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> g dvd N

goal (1 subgoal):
 1. coprime g N
[PROOF STEP]
have "\<not> 3 dvd N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 3 dvd N
[PROOF STEP]
using o6
[PROOF STATE]
proof (prove)
using this:
N = 23 * 37 * 53

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

goal (1 subgoal):
 1. coprime g N
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> 3 dvd N

goal (1 subgoal):
 1. coprime g N
[PROOF STEP]
have "\<not> 5 dvd N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 5 dvd N
[PROOF STEP]
using o6
[PROOF STATE]
proof (prove)
using this:
N = 23 * 37 * 53

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

goal (1 subgoal):
 1. coprime g N
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> g dvd N
\<not> 3 dvd N
\<not> 5 dvd N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> g dvd N
\<not> 3 dvd N
\<not> 5 dvd N

goal (1 subgoal):
 1. coprime g N
[PROOF STEP]
using o3 gcd_nat.absorb_iff2 prime_nat_iff \<open> prime(3::nat)\<close>
 \<open> prime(5::nat)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> g dvd N
\<not> 3 dvd N
\<not> 5 dvd N
g = 3 ^ 3 * 5
(?b dvd ?a) = (gcd ?a ?b = ?b)
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))
prime 3
prime 5

goal (1 subgoal):
 1. coprime g N
[PROOF STEP]
by (metis coprime_commute
coprime_mult_left_iff prime_imp_coprime_nat prime_imp_power_coprime_nat)
[PROOF STATE]
proof (state)
this:
coprime g N

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

goal (1 subgoal):
 1. gcd g N = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd g N = 1
[PROOF STEP]
using \<open>coprime g N\<close>
[PROOF STATE]
proof (prove)
using this:
coprime g N

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

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

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have s1: "gcd h M =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd h M = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gcd h M = 1
[PROOF STEP]
have "coprime h M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
have "\<not> h dvd M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> h dvd M
[PROOF STEP]
using o4 o5
[PROOF STATE]
proof (prove)
using this:
h = 3\<^sup>2 * 7 * 13
M = 11 * 17 * 227

goal (1 subgoal):
 1. \<not> h dvd M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> h dvd M

goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> h dvd M

goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
have "\<not> 3 dvd M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 3 dvd M
[PROOF STEP]
using o5
[PROOF STATE]
proof (prove)
using this:
M = 11 * 17 * 227

goal (1 subgoal):
 1. \<not> 3 dvd M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> 3 dvd M

goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> 3 dvd M

goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
have "\<not> 7 dvd M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 7 dvd M
[PROOF STEP]
using o5
[PROOF STATE]
proof (prove)
using this:
M = 11 * 17 * 227

goal (1 subgoal):
 1. \<not> 7 dvd M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> 7 dvd M

goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> 7 dvd M

goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
have "\<not> 13 dvd M"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 13 dvd M
[PROOF STEP]
using o5
[PROOF STATE]
proof (prove)
using this:
M = 11 * 17 * 227

goal (1 subgoal):
 1. \<not> 13 dvd M
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> 13 dvd M

goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> h dvd M
\<not> 3 dvd M
\<not> 7 dvd M
\<not> 13 dvd M
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> h dvd M
\<not> 3 dvd M
\<not> 7 dvd M
\<not> 13 dvd M

goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
using o4  gcd_nat.absorb_iff2 prime_nat_iff \<open> prime(3::nat)\<close>
\<open> prime(13::nat)\<close> \<open> prime(7::nat)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> h dvd M
\<not> 3 dvd M
\<not> 7 dvd M
\<not> 13 dvd M
h = 3\<^sup>2 * 7 * 13
(?b dvd ?a) = (gcd ?a ?b = ?b)
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))
prime 3
prime 13
prime 7

goal (1 subgoal):
 1. coprime h M
[PROOF STEP]
by (metis coprime_commute
coprime_mult_left_iff prime_imp_coprime_nat prime_imp_power_coprime_nat)
[PROOF STATE]
proof (state)
this:
coprime h M

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

goal (1 subgoal):
 1. gcd h M = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd h M = 1
[PROOF STEP]
using \<open>coprime h M\<close>
[PROOF STATE]
proof (prove)
using this:
coprime h M

goal (1 subgoal):
 1. gcd h M = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gcd h M = 1

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

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have s2: "gcd h N =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd h N = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. gcd h N = 1
[PROOF STEP]
have "coprime h N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
have "\<not> h dvd N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> h dvd N
[PROOF STEP]
using o4 o6
[PROOF STATE]
proof (prove)
using this:
h = 3\<^sup>2 * 7 * 13
N = 23 * 37 * 53

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

goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> h dvd N

goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
have "\<not> 3 dvd N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 3 dvd N
[PROOF STEP]
using o6
[PROOF STATE]
proof (prove)
using this:
N = 23 * 37 * 53

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

goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> 3 dvd N

goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
have "\<not> 7 dvd N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 7 dvd N
[PROOF STEP]
using o6
[PROOF STATE]
proof (prove)
using this:
N = 23 * 37 * 53

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

goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
\<not> 7 dvd N

goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
have "\<not> 13 dvd N"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 13 dvd N
[PROOF STEP]
using o6
[PROOF STATE]
proof (prove)
using this:
N = 23 * 37 * 53

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

goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
\<not> h dvd N
\<not> 3 dvd N
\<not> 7 dvd N
\<not> 13 dvd N
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> h dvd N
\<not> 3 dvd N
\<not> 7 dvd N
\<not> 13 dvd N

goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
using o4
     gcd_nat.absorb_iff2 prime_nat_iff \<open> prime(3::nat)\<close>\<open> prime(13::nat)\<close> \<open> prime(7::nat)\<close>
[PROOF STATE]
proof (prove)
using this:
\<not> h dvd N
\<not> 3 dvd N
\<not> 7 dvd N
\<not> 13 dvd N
h = 3\<^sup>2 * 7 * 13
(?b dvd ?a) = (gcd ?a ?b = ?b)
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))
prime 3
prime 13
prime 7

goal (1 subgoal):
 1. coprime h N
[PROOF STEP]
by (metis coprime_commute
coprime_mult_left_iff prime_imp_coprime_nat prime_imp_power_coprime_nat)
[PROOF STATE]
proof (state)
this:
coprime h N

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

goal (1 subgoal):
 1. gcd h N = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd h N = 1
[PROOF STEP]
using \<open>coprime h N\<close>
[PROOF STATE]
proof (prove)
using this:
coprime h N

goal (1 subgoal):
 1. gcd h N = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gcd h N = 1

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

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
have s4: "(h*M) Amic (h*N)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
using isotopic_amicable_pair v v1 v2 v3 w4 s s1 s2 w w1 w2
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?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\<rbrakk> \<Longrightarrow> (?h * ?M) Amic (?h * ?N)
m Amic n
m = g * M
n = g * N
0 < h
gcd g M = 1
gcd g N = 1
gcd h M = 1
gcd h N = 1
0 < g
h \<noteq> g
real (Esigma h) = real h / real g * real (Esigma g)

goal (1 subgoal):
 1. (h * M) Amic (h * N)
[PROOF STEP]
by (metis One_nat_def Suc_leI le_eq_less_or_eq nat_1_eq_mult_iff
num.distinct(3) numeral_eq_one_iff one_le_mult_iff one_le_numeral o3 o4 o5 o6)
[PROOF STATE]
proof (state)
this:
(h * M) Amic (h * N)

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
using s4 o4 o5 o6
[PROOF STATE]
proof (prove)
using this:
(h * M) Amic (h * N)
h = 3\<^sup>2 * 7 * 13
M = 11 * 17 * 227
N = 23 * 37 * 53

goal (1 subgoal):
 1. (3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(3\<^sup>2 * 7 * 13 * 11 * 17 * 227) Amic (3\<^sup>2 * 7 * 13 * 23 * 37 * 53)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma QuasiAmicable_pair_sym :
  assumes "m QAmic n " shows "n QAmic m "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n QAmic m
[PROOF STEP]
using  QuasiAmicable_pair_def assms
[PROOF STATE]
proof (prove)
using this:
?m QAmic ?n = (?m + 1 = aliquot_sum ?n \<and> ?n + 1 = aliquot_sum ?m)
m QAmic n

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


[STATEMENT]
lemma QuasiAmicable_example:
  shows "48 QAmic 75"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
have a: "set(divisors_nat 48) = {1, 2, 3, 4, 6, 8, 12, 16, 24, 48}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 48) = {1, 2, 3, 4, 6, 8, 12, 16, 24, 48}
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
set (divisors_nat 48) = {1, 2, 3, 4, 6, 8, 12, 16, 24, 48}

goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
have b: "divisor_set (48) = {1, 2, 3, 4, 6, 8, 12, 16, 24, 48}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set 48 = {1, 2, 3, 4, 6, 8, 12, 16, 24, 48}
[PROOF STEP]
using a  def_equiv_divisor_set
[PROOF STATE]
proof (prove)
using this:
set (divisors_nat 48) = {1, 2, 3, 4, 6, 8, 12, 16, 24, 48}
divisor_set ?n = set (divisors_nat ?n)

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

goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
have c: "properdiv_set (48) = {1, 2, 3, 4, 6, 8, 12, 16, 24}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. properdiv_set 48 = {1, 2, 3, 4, 6, 8, 12, 16, 24}
[PROOF STEP]
using b union_properdiv_set properdiv_set proper_divisor_def
[PROOF STATE]
proof (prove)
using this:
divisor_set 48 = {1, 2, 3, 4, 6, 8, 12, 16, 24, 48}
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 48 = {1, 2, 3, 4, 6, 8, 12, 16, 24}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
properdiv_set 48 = {1, 2, 3, 4, 6, 8, 12, 16, 24}

goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
have e: "aliquot_sum (48) = 75+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aliquot_sum 48 = 75 + 1
[PROOF STEP]
using aliquot_sum_def c
[PROOF STATE]
proof (prove)
using this:
aliquot_sum ?n \<equiv> \<Sum> (properdiv_set ?n)
properdiv_set 48 = {1, 2, 3, 4, 6, 8, 12, 16, 24}

goal (1 subgoal):
 1. aliquot_sum 48 = 75 + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aliquot_sum 48 = 75 + 1

goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
have i: "set(divisors_nat 75) = {1, 3, 5, 15, 25, 75}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 75) = {1, 3, 5, 15, 25, 75}
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
set (divisors_nat 75) = {1, 3, 5, 15, 25, 75}

goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
have ii: "divisor_set (75) = {1, 3, 5, 15, 25, 75}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set 75 = {1, 3, 5, 15, 25, 75}
[PROOF STEP]
using i  def_equiv_divisor_set
[PROOF STATE]
proof (prove)
using this:
set (divisors_nat 75) = {1, 3, 5, 15, 25, 75}
divisor_set ?n = set (divisors_nat ?n)

goal (1 subgoal):
 1. divisor_set 75 = {1, 3, 5, 15, 25, 75}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
divisor_set 75 = {1, 3, 5, 15, 25, 75}

goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
have iii: "properdiv_set (75) = {1, 3, 5, 15, 25}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. properdiv_set 75 = {1, 3, 5, 15, 25}
[PROOF STEP]
using ii union_properdiv_set properdiv_set proper_divisor_def
[PROOF STATE]
proof (prove)
using this:
divisor_set 75 = {1, 3, 5, 15, 25, 75}
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 75 = {1, 3, 5, 15, 25}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
properdiv_set 75 = {1, 3, 5, 15, 25}

goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
have iv: "aliquot_sum (75) = 48+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. aliquot_sum 75 = 48 + 1
[PROOF STEP]
using aliquot_sum_def iii
[PROOF STATE]
proof (prove)
using this:
aliquot_sum ?n \<equiv> \<Sum> (properdiv_set ?n)
properdiv_set 75 = {1, 3, 5, 15, 25}

goal (1 subgoal):
 1. aliquot_sum 75 = 48 + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
aliquot_sum 75 = 48 + 1

goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
using e iv QuasiAmicable_pair_def
[PROOF STATE]
proof (prove)
using this:
aliquot_sum 48 = 75 + 1
aliquot_sum 75 = 48 + 1
?m QAmic ?n = (?m + 1 = aliquot_sum ?n \<and> ?n + 1 = aliquot_sum ?m)

goal (1 subgoal):
 1. 48 QAmic 75
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
48 QAmic 75

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma breederAmic:
  fixes x :: nat
  assumes "x > 0" and "Esigma n = n + m*x" and "Esigma n = Esigma m * (x+1)"
      and "prime x" and "\<not>( x dvd m)"
  shows " n Amic (m*x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n Amic (m * x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. n Amic (m * x)
[PROOF STEP]
have A: "Esigma n = Esigma (m*x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma n = Esigma (m * x)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma n = Esigma (m * x)
[PROOF STEP]
have "gcd m x =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd m x = 1
[PROOF STEP]
using assms  gcd_nat.absorb_iff2 prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
0 < x
Esigma n = n + m * x
Esigma n = Esigma m * (x + 1)
prime x
\<not> x dvd m
(?b dvd ?a) = (gcd ?a ?b = ?b)
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))

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

goal (1 subgoal):
 1. Esigma n = Esigma (m * x)
[PROOF STEP]
have A1: "Esigma (m*x) = (Esigma m)*(Esigma x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (m * x) = Esigma m * Esigma x
[PROOF STEP]
using \<open>gcd m x =1\<close> gcd_Esigma_mult
[PROOF STATE]
proof (prove)
using this:
gcd m x = 1
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n

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

goal (1 subgoal):
 1. Esigma n = Esigma (m * x)
[PROOF STEP]
have A2: "Esigma (m*x) = (Esigma m)*(x+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (m * x) = Esigma m * (x + 1)
[PROOF STEP]
using \<open>prime x\<close>  prime_Esigma_mult A1
[PROOF STATE]
proof (prove)
using this:
prime x
\<lbrakk>prime ?m; prime ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> Esigma (?m * ?n) = Esigma ?n * Esigma ?m
Esigma (m * x) = Esigma m * Esigma x

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

goal (1 subgoal):
 1. Esigma n = Esigma (m * x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma n = Esigma (m * x)
[PROOF STEP]
using A2 assms
[PROOF STATE]
proof (prove)
using this:
Esigma (m * x) = Esigma m * (x + 1)
0 < x
Esigma n = n + m * x
Esigma n = Esigma m * (x + 1)
prime x
\<not> x dvd m

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma n = Esigma (m * x)

goal (1 subgoal):
 1. n Amic (m * x)
[PROOF STEP]
have B: "Esigma n = n+m*x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma n = n + m * x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
0 < x
Esigma n = n + m * x
Esigma n = Esigma m * (x + 1)
prime x
\<not> x dvd m

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

goal (1 subgoal):
 1. n Amic (m * x)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. n Amic (m * x)
[PROOF STEP]
using A B Amicable_pair_equiv_def
[PROOF STATE]
proof (prove)
using this:
Esigma n = Esigma (m * x)
Esigma n = n + m * x
\<lbrakk>?m Amic ?n; 1 \<le> ?m; 1 \<le> ?n\<rbrakk> \<Longrightarrow> Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n

goal (1 subgoal):
 1. n Amic (m * x)
[PROOF STEP]
by (smt Amicable_pair_equiv_def_conv Esigma_properdiv_set
One_nat_def Suc_leI add_cancel_left_left add_le_same_cancel1 add_mult_distrib2 assms
 dvd_triv_right le_add2 nat_0_less_mult_iff not_gr_zero not_le semiring_normalization_rules(1))
[PROOF STATE]
proof (state)
this:
n Amic (m * x)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma odd_odd_amicable_Euler: "69615 Amic 87633"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "prime(5::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 5
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 5

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "prime(17::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 17
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 17

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "\<not> (5*17)dvd((3::nat)^2*7*13)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 5 * 17 dvd 3\<^sup>2 * 7 * 13
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> 5 * 17 dvd 3\<^sup>2 * 7 * 13

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "\<not> 5 dvd((3::nat)^2*7*13)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 5 dvd 3\<^sup>2 * 7 * 13
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> 5 dvd 3\<^sup>2 * 7 * 13

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "\<not> 17 dvd((3::nat)^2*7*13)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 17 dvd 3\<^sup>2 * 7 * 13
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> 17 dvd 3\<^sup>2 * 7 * 13

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A1: "Esigma(69615) = Esigma(3^2*7*13*5*17)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 69615 = Esigma (3\<^sup>2 * 7 * 13 * 5 * 17)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma 69615 = Esigma (3\<^sup>2 * 7 * 13 * 5 * 17)

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A2: "Esigma(3^2*7*13*5*17) =  Esigma(3^2*7*13)*Esigma(5*17)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 5 * 17) = Esigma (3\<^sup>2 * 7 * 13) * Esigma (5 * 17)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 5 * 17) = Esigma (3\<^sup>2 * 7 * 13) * Esigma (5 * 17)
[PROOF STEP]
have A111: "coprime  ((3::nat)^2*7*13) ((5::nat)*17)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. coprime (3\<^sup>2 * 7 * 13) (5 * 17)
[PROOF STEP]
using \<open>\<not> 17 dvd((3::nat)^2*7*13)\<close> \<open>\<not> 5 dvd((3::nat)^2*7*13)\<close> \<open>prime (17::nat)\<close>
        \<open>prime (5::nat)\<close> coprime_commute coprime_mult_left_iff prime_imp_coprime_nat
[PROOF STATE]
proof (prove)
using this:
\<not> 17 dvd 3\<^sup>2 * 7 * 13
\<not> 5 dvd 3\<^sup>2 * 7 * 13
prime 17
prime 5
coprime ?b ?a = coprime ?a ?b
coprime (?a * ?b) ?c = (coprime ?a ?c \<and> coprime ?b ?c)
\<lbrakk>prime ?p; \<not> ?p dvd ?n\<rbrakk> \<Longrightarrow> coprime ?p ?n

goal (1 subgoal):
 1. coprime (3\<^sup>2 * 7 * 13) (5 * 17)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
coprime (3\<^sup>2 * 7 * 13) (5 * 17)

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 5 * 17) = Esigma (3\<^sup>2 * 7 * 13) * Esigma (5 * 17)
[PROOF STEP]
have "gcd (3^2*7*13)((5::nat)*17) =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (3\<^sup>2 * 7 * 13) (5 * 17) = 1
[PROOF STEP]
using A111  coprime_imp_gcd_eq_1
[PROOF STATE]
proof (prove)
using this:
coprime (3\<^sup>2 * 7 * 13) (5 * 17)
coprime ?a ?b \<Longrightarrow> gcd ?a ?b = (1::?'a)

goal (1 subgoal):
 1. gcd (3\<^sup>2 * 7 * 13) (5 * 17) = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
gcd (3\<^sup>2 * 7 * 13) (5 * 17) = 1

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 5 * 17) = Esigma (3\<^sup>2 * 7 * 13) * Esigma (5 * 17)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 5 * 17) = Esigma (3\<^sup>2 * 7 * 13) * Esigma (5 * 17)
[PROOF STEP]
using \<open>gcd (3^2*7*13)((5::nat)*17) =1 \<close>
        gcd_Esigma_mult
[PROOF STATE]
proof (prove)
using this:
gcd (3\<^sup>2 * 7 * 13) (5 * 17) = 1
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 5 * 17) = Esigma (3\<^sup>2 * 7 * 13) * Esigma (5 * 17)
[PROOF STEP]
by (smt semiring_normalization_rules(18) semiring_normalization_rules(7))
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2 * 7 * 13 * 5 * 17) = Esigma (3\<^sup>2 * 7 * 13) * Esigma (5 * 17)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2 * 7 * 13 * 5 * 17) = Esigma (3\<^sup>2 * 7 * 13) * Esigma (5 * 17)

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "prime (7::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 7
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 7

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "\<not> 7 dvd ((3::nat)^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 7 dvd 3\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> 7 dvd 3\<^sup>2

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "prime (13::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 13
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 13

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have " \<not> 13 dvd ((3::nat)^2*7)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 13 dvd 3\<^sup>2 * 7
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> 13 dvd 3\<^sup>2 * 7

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have  "gcd ((3::nat)^2*7) 13 =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (3\<^sup>2 * 7) 13 = 1
[PROOF STEP]
using \<open>prime (13::nat)\<close> \<open>\<not> 13 dvd ((3::nat)^2*7)\<close> gcd_nat.absorb_iff2 prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
prime 13
\<not> 13 dvd 3\<^sup>2 * 7
(?b dvd ?a) = (gcd ?a ?b = ?b)
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))

goal (1 subgoal):
 1. gcd (3\<^sup>2 * 7) 13 = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
gcd (3\<^sup>2 * 7) 13 = 1

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A3: " Esigma(3^2 * 7*13) = Esigma(3^2*7)*Esigma(13)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13) = Esigma (3\<^sup>2 * 7) * Esigma 13
[PROOF STEP]
using  \<open>gcd  (3^2 *7) 13 =1\<close>  gcd_Esigma_mult
[PROOF STATE]
proof (prove)
using this:
gcd (3\<^sup>2 * 7) 13 = 1
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13) = Esigma (3\<^sup>2 * 7) * Esigma 13
[PROOF STEP]
by (smt semiring_normalization_rules(18) semiring_normalization_rules(7))
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2 * 7 * 13) = Esigma (3\<^sup>2 * 7) * Esigma 13

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have  "gcd ((3::nat)^2) 7 = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (3\<^sup>2) 7 = 1
[PROOF STEP]
using \<open>prime (7::nat)\<close> \<open> \<not> 7 dvd ((3::nat)^2 )\<close> gcd_nat.absorb_iff2 prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
prime 7
\<not> 7 dvd 3\<^sup>2
(?b dvd ?a) = (gcd ?a ?b = ?b)
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))

goal (1 subgoal):
 1. gcd (3\<^sup>2) 7 = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
gcd (3\<^sup>2) 7 = 1

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A4: " Esigma(3^2*7) = Esigma(3^2)* Esigma (7)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7) = Esigma (3\<^sup>2) * Esigma 7
[PROOF STEP]
using  \<open>gcd ((3::nat)^2) 7 =1\<close>  gcd_Esigma_mult
[PROOF STATE]
proof (prove)
using this:
gcd (3\<^sup>2) 7 = 1
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7) = Esigma (3\<^sup>2) * Esigma 7
[PROOF STEP]
by (smt semiring_normalization_rules(18) semiring_normalization_rules(7))
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2 * 7) = Esigma (3\<^sup>2) * Esigma 7

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A5: "Esigma(3^2) = 13"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2) = 13
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (3\<^sup>2) = 13
[PROOF STEP]
have  "(3::nat)^2 =9"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3\<^sup>2 = 9
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
3\<^sup>2 = 9

goal (1 subgoal):
 1. Esigma (3\<^sup>2) = 13
[PROOF STEP]
have A55:"divisor_set 9 = {1, 3, 9}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set 9 = {1, 3, 9}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. divisor_set 9 = {1, 3, 9}
[PROOF STEP]
have A555: "set(divisors_nat (9)) = {1, 3, 9}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 9) = {1, 3, 9}
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
set (divisors_nat 9) = {1, 3, 9}

goal (1 subgoal):
 1. divisor_set 9 = {1, 3, 9}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. divisor_set 9 = {1, 3, 9}
[PROOF STEP]
using def_equiv_divisor_set A555
[PROOF STATE]
proof (prove)
using this:
divisor_set ?n = set (divisors_nat ?n)
set (divisors_nat 9) = {1, 3, 9}

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

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
divisor_set 9 = {1, 3, 9}

goal (1 subgoal):
 1. Esigma (3\<^sup>2) = 13
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2) = 13
[PROOF STEP]
using A55 \<open>(3::nat)^2 =9\<close> Esigma_def
[PROOF STATE]
proof (prove)
using this:
divisor_set 9 = {1, 3, 9}
3\<^sup>2 = 9
Esigma ?n \<equiv> \<Sum> (divisor_set ?n)

goal (1 subgoal):
 1. Esigma (3\<^sup>2) = 13
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2) = 13

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2) = 13

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "prime( 13::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 13
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 13

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A6: "Esigma (13) = 14"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 13 = 14
[PROOF STEP]
using prime_sum_div \<open>prime( 13::nat)\<close>
[PROOF STATE]
proof (prove)
using this:
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1
prime 13

goal (1 subgoal):
 1. Esigma 13 = 14
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma 13 = 14

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "prime( 7::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 7
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 7

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A7: "Esigma (7) = 8"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 7 = 8
[PROOF STEP]
using prime_sum_div \<open>prime( 7::nat)\<close>
[PROOF STATE]
proof (prove)
using this:
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1
prime 7

goal (1 subgoal):
 1. Esigma 7 = 8
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma 7 = 8

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "prime (5::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 5
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 5

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "prime (17::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 17
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 17

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A8: "Esigma(5*17) = Esigma(5) * Esigma (17)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (5 * 17) = Esigma 5 * Esigma 17
[PROOF STEP]
using prime_Esigma_mult \<open>prime (5::nat)\<close> \<open>prime (17::nat)\<close>
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>prime ?m; prime ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> Esigma (?m * ?n) = Esigma ?n * Esigma ?m
prime 5
prime 17

goal (1 subgoal):
 1. Esigma (5 * 17) = Esigma 5 * Esigma 17
[PROOF STEP]
by (metis arith_simps(2) mult.commute num.inject(2) numeral_eq_iff semiring_norm(83))
[PROOF STATE]
proof (state)
this:
Esigma (5 * 17) = Esigma 5 * Esigma 17

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A9: "Esigma(69615) = Esigma(3^2)*Esigma (7) *Esigma (13) * Esigma(5) * Esigma (17)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 69615 = Esigma (3\<^sup>2) * Esigma 7 * Esigma 13 * Esigma 5 * Esigma 17
[PROOF STEP]
using A1 A2 A3 A4 A5 A6 A7 A8
[PROOF STATE]
proof (prove)
using this:
Esigma 69615 = Esigma (3\<^sup>2 * 7 * 13 * 5 * 17)
Esigma (3\<^sup>2 * 7 * 13 * 5 * 17) = Esigma (3\<^sup>2 * 7 * 13) * Esigma (5 * 17)
Esigma (3\<^sup>2 * 7 * 13) = Esigma (3\<^sup>2 * 7) * Esigma 13
Esigma (3\<^sup>2 * 7) = Esigma (3\<^sup>2) * Esigma 7
Esigma (3\<^sup>2) = 13
Esigma 13 = 14
Esigma 7 = 8
Esigma (5 * 17) = Esigma 5 * Esigma 17

goal (1 subgoal):
 1. Esigma 69615 = Esigma (3\<^sup>2) * Esigma 7 * Esigma 13 * Esigma 5 * Esigma 17
[PROOF STEP]
by (metis mult.assoc)
[PROOF STATE]
proof (state)
this:
Esigma 69615 = Esigma (3\<^sup>2) * Esigma 7 * Esigma 13 * Esigma 5 * Esigma 17

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A10: "Esigma (5)=6"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 5 = 6
[PROOF STEP]
using prime_sum_div \<open>prime(5::nat)\<close>
[PROOF STATE]
proof (prove)
using this:
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1
prime 5

goal (1 subgoal):
 1. Esigma 5 = 6
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma 5 = 6

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A11: "Esigma (17)=18"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 17 = 18
[PROOF STEP]
using prime_sum_div \<open>prime(17::nat)\<close>
[PROOF STATE]
proof (prove)
using this:
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1
prime 17

goal (1 subgoal):
 1. Esigma 17 = 18
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma 17 = 18

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have AA:  "Esigma(69615)=13*8*14*6*18"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 69615 = 13 * 8 * 14 * 6 * 18
[PROOF STEP]
using A1 A2 A3 A4 A5 A6 A7 A8 A9 A10 A11
[PROOF STATE]
proof (prove)
using this:
Esigma 69615 = Esigma (3\<^sup>2 * 7 * 13 * 5 * 17)
Esigma (3\<^sup>2 * 7 * 13 * 5 * 17) = Esigma (3\<^sup>2 * 7 * 13) * Esigma (5 * 17)
Esigma (3\<^sup>2 * 7 * 13) = Esigma (3\<^sup>2 * 7) * Esigma 13
Esigma (3\<^sup>2 * 7) = Esigma (3\<^sup>2) * Esigma 7
Esigma (3\<^sup>2) = 13
Esigma 13 = 14
Esigma 7 = 8
Esigma (5 * 17) = Esigma 5 * Esigma 17
Esigma 69615 = Esigma (3\<^sup>2) * Esigma 7 * Esigma 13 * Esigma 5 * Esigma 17
Esigma 5 = 6
Esigma 17 = 18

goal (1 subgoal):
 1. Esigma 69615 = 13 * 8 * 14 * 6 * 18
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma 69615 = 13 * 8 * 14 * 6 * 18

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have AAA: "Esigma(69615) =157248"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 69615 = 157248
[PROOF STEP]
using AA
[PROOF STATE]
proof (prove)
using this:
Esigma 69615 = 13 * 8 * 14 * 6 * 18

goal (1 subgoal):
 1. Esigma 69615 = 157248
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma 69615 = 157248

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have AA1: "Esigma(87633) = Esigma (3^2*7*13*107)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 87633 = Esigma (3\<^sup>2 * 7 * 13 * 107)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma 87633 = Esigma (3\<^sup>2 * 7 * 13 * 107)

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have "prime (107::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 107
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 107

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have AA2: "Esigma (3^2*7*13*107) = Esigma (3^2*7*13)*Esigma(107)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 107) = Esigma (3\<^sup>2 * 7 * 13) * Esigma 107
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 107) = Esigma (3\<^sup>2 * 7 * 13) * Esigma 107
[PROOF STEP]
have "\<not> (107::nat) dvd  (3^2*7*13)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 107 dvd 3\<^sup>2 * 7 * 13
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> 107 dvd 3\<^sup>2 * 7 * 13

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 107) = Esigma (3\<^sup>2 * 7 * 13) * Esigma 107
[PROOF STEP]
have "gcd  ((3::nat)^2*7*13) 107 =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (3\<^sup>2 * 7 * 13) 107 = 1
[PROOF STEP]
using \<open>prime (107::nat)\<close>
        \<open> \<not> (107::nat) dvd  (3^2*7*13)\<close>
[PROOF STATE]
proof (prove)
using this:
prime 107
\<not> 107 dvd 3\<^sup>2 * 7 * 13

goal (1 subgoal):
 1. gcd (3\<^sup>2 * 7 * 13) 107 = 1
[PROOF STEP]
using gcd_nat.absorb_iff2 prime_nat_iff
[PROOF STATE]
proof (prove)
using this:
prime 107
\<not> 107 dvd 3\<^sup>2 * 7 * 13
(?b dvd ?a) = (gcd ?a ?b = ?b)
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))

goal (1 subgoal):
 1. gcd (3\<^sup>2 * 7 * 13) 107 = 1
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
gcd (3\<^sup>2 * 7 * 13) 107 = 1

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 107) = Esigma (3\<^sup>2 * 7 * 13) * Esigma 107
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 107) = Esigma (3\<^sup>2 * 7 * 13) * Esigma 107
[PROOF STEP]
using \<open>gcd  (3^2 *7*13) 107 =1\<close> gcd_Esigma_mult
[PROOF STATE]
proof (prove)
using this:
gcd (3\<^sup>2 * 7 * 13) 107 = 1
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 107) = Esigma (3\<^sup>2 * 7 * 13) * Esigma 107
[PROOF STEP]
by (smt mult.commute)
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2 * 7 * 13 * 107) = Esigma (3\<^sup>2 * 7 * 13) * Esigma 107

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2 * 7 * 13 * 107) = Esigma (3\<^sup>2 * 7 * 13) * Esigma 107

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have AA3:  "Esigma (107) =108"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 107 = 108
[PROOF STEP]
using prime_sum_div \<open>prime(107::nat)\<close>
[PROOF STATE]
proof (prove)
using this:
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1
prime 107

goal (1 subgoal):
 1. Esigma 107 = 108
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma 107 = 108

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have AA4: "Esigma(3^2*7*13) = 13*8*14"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13) = 13 * 8 * 14
[PROOF STEP]
using A3 A4 A5 A6 A7
[PROOF STATE]
proof (prove)
using this:
Esigma (3\<^sup>2 * 7 * 13) = Esigma (3\<^sup>2 * 7) * Esigma 13
Esigma (3\<^sup>2 * 7) = Esigma (3\<^sup>2) * Esigma 7
Esigma (3\<^sup>2) = 13
Esigma 13 = 14
Esigma 7 = 8

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13) = 13 * 8 * 14
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2 * 7 * 13) = 13 * 8 * 14

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have AA5 : "Esigma (3^2*7*13*107) = 13*8*14*108"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 107) = 13 * 8 * 14 * 108
[PROOF STEP]
using AA2 AA3 AA4
[PROOF STATE]
proof (prove)
using this:
Esigma (3\<^sup>2 * 7 * 13 * 107) = Esigma (3\<^sup>2 * 7 * 13) * Esigma 107
Esigma 107 = 108
Esigma (3\<^sup>2 * 7 * 13) = 13 * 8 * 14

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 107) = 13 * 8 * 14 * 108
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2 * 7 * 13 * 107) = 13 * 8 * 14 * 108

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have AA6: "Esigma (3^2*7*13*107) = 157248"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 107) = 157248
[PROOF STEP]
using AA5
[PROOF STATE]
proof (prove)
using this:
Esigma (3\<^sup>2 * 7 * 13 * 107) = 13 * 8 * 14 * 108

goal (1 subgoal):
 1. Esigma (3\<^sup>2 * 7 * 13 * 107) = 157248
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma (3\<^sup>2 * 7 * 13 * 107) = 157248

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have A:"Esigma(69615) = Esigma(87633)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 69615 = Esigma 87633
[PROOF STEP]
using  AAA AA6 AA5 AA1
[PROOF STATE]
proof (prove)
using this:
Esigma 69615 = 157248
Esigma (3\<^sup>2 * 7 * 13 * 107) = 157248
Esigma (3\<^sup>2 * 7 * 13 * 107) = 13 * 8 * 14 * 108
Esigma 87633 = Esigma (3\<^sup>2 * 7 * 13 * 107)

goal (1 subgoal):
 1. Esigma 69615 = Esigma 87633
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
Esigma 69615 = Esigma 87633

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
have B: " Esigma(87633) = 69615 + 87633"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 87633 = 69615 + 87633
[PROOF STEP]
using AAA \<open>Esigma 69615 = Esigma 87633\<close>
[PROOF STATE]
proof (prove)
using this:
Esigma 69615 = 157248
Esigma 69615 = Esigma 87633

goal (1 subgoal):
 1. Esigma 87633 = 69615 + 87633
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
Esigma 87633 = 69615 + 87633

goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 69615 Amic 87633
[PROOF STEP]
using A B Amicable_pair_def Amicable_pair_equiv_def_conv
[PROOF STATE]
proof (prove)
using this:
Esigma 69615 = Esigma 87633
Esigma 87633 = 69615 + 87633
?m Amic ?n \<equiv> ?m = aliquot_sum ?n \<and> ?n = aliquot_sum ?m
\<lbrakk>1 \<le> ?m; 1 \<le> ?n; Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n\<rbrakk> \<Longrightarrow> ?m Amic ?n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Amicable_pair_example_smallest_odd_odd: "12285 Amic 14595"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
have A: "set(divisors_nat (12285)) = {1, 3, 5, 7, 9, 13, 15, 21, 27, 35, 39, 45, 63, 65, 91,
105, 117, 135, 189, 195, 273, 315, 351, 455, 585, 819, 945, 1365, 1755, 2457, 4095, 12285}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 12285) = {1, 3, 5, 7, 9, 13, 15, 21, 27, 35, 39, 45, 63, 65, 91, 105, 117, 135, 189, 195, 273, 315, 351, 455, 585, 819, 945, 1365, 1755, 2457, 4095, 12285}
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
set (divisors_nat 12285) = {1, 3, 5, 7, 9, 13, 15, 21, 27, 35, 39, 45, 63, 65, 91, 105, 117, 135, 189, 195, 273, 315, 351, 455, 585, 819, 945, 1365, 1755, 2457, 4095, 12285}

goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
have A1: "set(divisors_nat (12285)) = divisor_set 12285"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 12285) = divisor_set 12285
[PROOF STEP]
using def_equiv_divisor_set
[PROOF STATE]
proof (prove)
using this:
divisor_set ?n = set (divisors_nat ?n)

goal (1 subgoal):
 1. set (divisors_nat 12285) = divisor_set 12285
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (divisors_nat 12285) = divisor_set 12285

goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
have A2: "\<Sum>{1, 3, 5, 7, 9, 13, 15, 21, 27, 35, 39, 45, 63, 65, 91, 105, 117, 135, 189, 195, 273,
315, 351, 455, 585, 819, 945, 1365, 1755, 2457, 4095, 12285} = (26880::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum> {1, 3, 5, 7, 9, 13, 15, 21, 27, 35, 39, 45, 63, 65, 91, 105, 117, 135, 189, 195, 273, 315, 351, 455, 585, 819, 945, 1365, 1755, 2457, 4095, 12285} = 26880
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
\<Sum> {1, 3, 5, 7, 9, 13, 15, 21, 27, 35, 39, 45, 63, 65, 91, 105, 117, 135, 189, 195, 273, 315, 351, 455, 585, 819, 945, 1365, 1755, 2457, 4095, 12285} = 26880

goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
have  A3: "Esigma 12285 = 26880"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 12285 = 26880
[PROOF STEP]
using A A1 A2 Esigma_def
[PROOF STATE]
proof (prove)
using this:
set (divisors_nat 12285) = {1, 3, 5, 7, 9, 13, 15, 21, 27, 35, 39, 45, 63, 65, 91, 105, 117, 135, 189, 195, 273, 315, 351, 455, 585, 819, 945, 1365, 1755, 2457, 4095, 12285}
set (divisors_nat 12285) = divisor_set 12285
\<Sum> {1, 3, 5, 7, 9, 13, 15, 21, 27, 35, 39, 45, 63, 65, 91, 105, 117, 135, 189, 195, 273, 315, 351, 455, 585, 819, 945, 1365, 1755, 2457, 4095, 12285} = 26880
Esigma ?n \<equiv> \<Sum> (divisor_set ?n)

goal (1 subgoal):
 1. Esigma 12285 = 26880
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma 12285 = 26880

goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
have Q:"Esigma 12285 = Esigma 14595"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 12285 = Esigma 14595
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma 12285 = Esigma 14595
[PROOF STEP]
have N: "set(divisors_nat (14595)) =
               { 1, 3, 5, 7, 15, 21, 35, 105, 139, 417, 695, 973, 2085, 2919, 4865, 14595}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 14595) = {1, 3, 5, 7, 15, 21, 35, 105, 139, 417, 695, 973, 2085, 2919, 4865, 14595}
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
set (divisors_nat 14595) = {1, 3, 5, 7, 15, 21, 35, 105, 139, 417, 695, 973, 2085, 2919, 4865, 14595}

goal (1 subgoal):
 1. Esigma 12285 = Esigma 14595
[PROOF STEP]
have N1: "set(divisors_nat (14595)) = divisor_set 14595"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 14595) = divisor_set 14595
[PROOF STEP]
using def_equiv_divisor_set
[PROOF STATE]
proof (prove)
using this:
divisor_set ?n = set (divisors_nat ?n)

goal (1 subgoal):
 1. set (divisors_nat 14595) = divisor_set 14595
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
set (divisors_nat 14595) = divisor_set 14595

goal (1 subgoal):
 1. Esigma 12285 = Esigma 14595
[PROOF STEP]
have N2:
      "\<Sum>{ 1, 3, 5, 7, 15, 21, 35, 105, 139, 417, 695, 973, 2085, 2919, 4865, 14595} = (26880::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<Sum> {1, 3, 5, 7, 15, 21, 35, 105, 139, 417, 695, 973, 2085, 2919, 4865, 14595} = 26880
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
\<Sum> {1, 3, 5, 7, 15, 21, 35, 105, 139, 417, 695, 973, 2085, 2919, 4865, 14595} = 26880

goal (1 subgoal):
 1. Esigma 12285 = Esigma 14595
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 12285 = Esigma 14595
[PROOF STEP]
using A3 N N1 N2 Esigma_def
[PROOF STATE]
proof (prove)
using this:
Esigma 12285 = 26880
set (divisors_nat 14595) = {1, 3, 5, 7, 15, 21, 35, 105, 139, 417, 695, 973, 2085, 2919, 4865, 14595}
set (divisors_nat 14595) = divisor_set 14595
\<Sum> {1, 3, 5, 7, 15, 21, 35, 105, 139, 417, 695, 973, 2085, 2919, 4865, 14595} = 26880
Esigma ?n \<equiv> \<Sum> (divisor_set ?n)

goal (1 subgoal):
 1. Esigma 12285 = Esigma 14595
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma 12285 = Esigma 14595

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma 12285 = Esigma 14595

goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
have B:"Esigma (12285) = 12285 + 14595"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma 12285 = 12285 + 14595
[PROOF STEP]
using A3
[PROOF STATE]
proof (prove)
using this:
Esigma 12285 = 26880

goal (1 subgoal):
 1. Esigma 12285 = 12285 + 14595
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma 12285 = 12285 + 14595

goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
using B Q Amicable_pair_def
[PROOF STATE]
proof (prove)
using this:
Esigma 12285 = 12285 + 14595
Esigma 12285 = Esigma 14595
?m Amic ?n \<equiv> ?m = aliquot_sum ?n \<and> ?n = aliquot_sum ?m

goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
using Amicable_pair_equiv_def_conv one_le_numeral
[PROOF STATE]
proof (prove)
using this:
Esigma 12285 = 12285 + 14595
Esigma 12285 = Esigma 14595
?m Amic ?n \<equiv> ?m = aliquot_sum ?n \<and> ?n = aliquot_sum ?m
\<lbrakk>1 \<le> ?m; 1 \<le> ?n; Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n\<rbrakk> \<Longrightarrow> ?m Amic ?n
(1::?'a) \<le> numeral ?n

goal (1 subgoal):
 1. 12285 Amic 14595
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
12285 Amic 14595

goal:
No subgoals!
[PROOF STEP]
qed