[STATEMENT]
theorem Euler_Rule_Amicable:
  fixes k l f p q r m n :: nat
  assumes "k > l" and "l \<ge> 1" and "f = 2^l+1"
      and "prime p" and "prime q" and "prime r"
      and "p = 2^(k-l) * f - 1" and "q = 2^k * f - 1" and "r = 2^(2*k-l) * f^2 - 1"
      and "m = 2^k * p * q" and "n = 2^k * r"
  shows "m Amic n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
note [[linarith_split_limit = 50]]
[PROOF STATE]
proof (state)
this:
TERM _

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
have A1: "(p+1)*(q+1) = (r+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p + 1) * (q + 1) = r + 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (p + 1) * (q + 1) = r + 1
[PROOF STEP]
have a: "p+1 = (2^(k-l))*f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p + 1 = 2 ^ (k - l) * f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. p + 1 = 2 ^ (k - l) * f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
p + 1 = 2 ^ (k - l) * f

goal (1 subgoal):
 1. (p + 1) * (q + 1) = r + 1
[PROOF STEP]
have b: "q+1 = (2^(k))*f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q + 1 = 2 ^ k * f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. q + 1 = 2 ^ k * f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
q + 1 = 2 ^ k * f

goal (1 subgoal):
 1. (p + 1) * (q + 1) = r + 1
[PROOF STEP]
have c: "r+1 = (2^(2*k-l))*(f^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r + 1 = 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. r + 1 = 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
r + 1 = 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. (p + 1) * (q + 1) = r + 1
[PROOF STEP]
have d: "(p+1)*(q+1) = (2^(k-l))*(2^(k))*f^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p + 1) * (q + 1) = 2 ^ (k - l) * 2 ^ k * f\<^sup>2
[PROOF STEP]
using a b
[PROOF STATE]
proof (prove)
using this:
p + 1 = 2 ^ (k - l) * f
q + 1 = 2 ^ k * f

goal (1 subgoal):
 1. (p + 1) * (q + 1) = 2 ^ (k - l) * 2 ^ k * f\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
(p + 1) * (q + 1) = 2 ^ (k - l) * 2 ^ k * f\<^sup>2

goal (1 subgoal):
 1. (p + 1) * (q + 1) = r + 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (p + 1) * (q + 1) = r + 1
[PROOF STEP]
using d c
[PROOF STATE]
proof (prove)
using this:
(p + 1) * (q + 1) = 2 ^ (k - l) * 2 ^ k * f\<^sup>2
r + 1 = 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. (p + 1) * (q + 1) = r + 1
[PROOF STEP]
by (metis Nat.add_diff_assoc add.commute assms(1) less_imp_le_nat mult_2 power_add)
[PROOF STATE]
proof (state)
this:
(p + 1) * (q + 1) = r + 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
(p + 1) * (q + 1) = r + 1

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
have aa: "Esigma p = p+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma p = p + 1
[PROOF STEP]
using assms \<open>prime p\<close> prime_sum_div
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
prime p
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1

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

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
have bb: "Esigma q = q+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma q = q + 1
[PROOF STEP]
using \<open>prime q\<close> prime_sum_div assms
[PROOF STATE]
proof (prove)
using this:
prime q
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

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

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
have cc: "Esigma r = r+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma r = r + 1
[PROOF STEP]
using \<open>prime r\<close> prime_sum_div assms
[PROOF STATE]
proof (prove)
using this:
prime r
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

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

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
have A2: "(Esigma p)*(Esigma q) = Esigma r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma p * Esigma q = Esigma r
[PROOF STEP]
using aa bb cc A1
[PROOF STATE]
proof (prove)
using this:
Esigma p = p + 1
Esigma q = q + 1
Esigma r = r + 1
(p + 1) * (q + 1) = r + 1

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

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
have A3: "Esigma (2^k)*(Esigma p)*(Esigma q) = Esigma(2^k)*(Esigma r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k) * Esigma p * Esigma q = Esigma (2 ^ k) * Esigma r
[PROOF STEP]
using A2
[PROOF STATE]
proof (prove)
using this:
Esigma p * Esigma q = Esigma r

goal (1 subgoal):
 1. Esigma (2 ^ k) * Esigma p * Esigma q = Esigma (2 ^ k) * Esigma r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k) * Esigma p * Esigma q = Esigma (2 ^ k) * Esigma r

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
have A4: "Esigma(( 2^k)*r) = (Esigma(2^k))*(Esigma r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * r) = Esigma (2 ^ k) * Esigma r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (2 ^ k * r) = Esigma (2 ^ k) * Esigma r
[PROOF STEP]
have Z0: "gcd ((2::nat)^k)r =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (2 ^ k) r = 1
[PROOF STEP]
using assms \<open>prime r\<close>
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
prime r

goal (1 subgoal):
 1. gcd (2 ^ k) r = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gcd (2 ^ k) r = 1

goal (1 subgoal):
 1. Esigma (2 ^ k * r) = Esigma (2 ^ k) * Esigma r
[PROOF STEP]
have A: "(2::nat)^k \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> 2 ^ k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 1 \<le> 2 ^ k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> 2 ^ k

goal (1 subgoal):
 1. Esigma (2 ^ k * r) = Esigma (2 ^ k) * Esigma r
[PROOF STEP]
have Ab: "(2::nat)^k \<noteq> r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k \<noteq> r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 2 ^ k \<noteq> r
[PROOF STEP]
by (metis gcd_nat.idem numeral_le_one_iff prime_ge_2_nat semiring_norm(69) Z0)
[PROOF STATE]
proof (state)
this:
2 ^ k \<noteq> r

goal (1 subgoal):
 1. Esigma (2 ^ k * r) = Esigma (2 ^ k) * Esigma r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * r) = Esigma (2 ^ k) * Esigma r
[PROOF STEP]
using Z0 gcd_Esigma_mult assms A Ab
[PROOF STATE]
proof (prove)
using this:
gcd (2 ^ k) r = 1
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
1 \<le> 2 ^ k
2 ^ k \<noteq> r

goal (1 subgoal):
 1. Esigma (2 ^ k * r) = Esigma (2 ^ k) * Esigma r
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * r) = Esigma (2 ^ k) * Esigma r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * r) = Esigma (2 ^ k) * Esigma r

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
have A5: "Esigma((2^k)*p*q) =(Esigma(2^k))*(Esigma p)*(Esigma q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
have "(2::nat)^k \<ge>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> 2 ^ k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 1 \<le> 2 ^ k
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<le> 2 ^ k

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
have A:  "gcd (2^k) p =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (2 ^ k) p = 1
[PROOF STEP]
using assms \<open>prime p\<close>
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
prime p

goal (1 subgoal):
 1. gcd (2 ^ k) p = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gcd (2 ^ k) p = 1

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
have B:  "gcd (2^k) q =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (2 ^ k) q = 1
[PROOF STEP]
using assms \<open>prime q\<close>
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
prime q

goal (1 subgoal):
 1. gcd (2 ^ k) q = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
gcd (2 ^ k) q = 1

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
have BB: "gcd (2^k) (p*q) =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd (2 ^ k) (p * q) = 1
[PROOF STEP]
using assms A B
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
gcd (2 ^ k) p = 1
gcd (2 ^ k) q = 1

goal (1 subgoal):
 1. gcd (2 ^ k) (p * q) = 1
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
gcd (2 ^ k) (p * q) = 1

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
have C:  "p*q \<ge>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> p * q
[PROOF STEP]
using assms One_nat_def one_le_mult_iff prime_ge_1_nat
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
1 = Suc 0
(Suc 0 \<le> ?m * ?n) = (Suc 0 \<le> ?m \<and> Suc 0 \<le> ?n)
prime ?p \<Longrightarrow> 1 \<le> ?p

goal (1 subgoal):
 1. 1 \<le> p * q
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
1 \<le> p * q

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
have A6: " Esigma((2^k)*(p*q))=( Esigma(2^k))*(Esigma(p*q))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * (p * q)) = Esigma (2 ^ k) * Esigma (p * q)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (2 ^ k * (p * q)) = Esigma (2 ^ k) * Esigma (p * q)
[PROOF STEP]
have "(( 2::nat)^k) \<noteq> (p*q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k \<noteq> p * q
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 2 ^ k \<noteq> p * q
[PROOF STEP]
by (metis BB Nat.add_0_right gcd_idem_nat less_add_eq_less
            not_add_less1 power_inject_exp prime_gt_1_nat semiring_normalization_rules(32)
            two_is_prime_nat )
[PROOF STATE]
proof (state)
this:
2 ^ k \<noteq> p * q

goal (1 subgoal):
 1. Esigma (2 ^ k * (p * q)) = Esigma (2 ^ k) * Esigma (p * q)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * (p * q)) = Esigma (2 ^ k) * Esigma (p * q)
[PROOF STEP]
using \<open>(( 2::nat)^k) \<noteq> (p*q)\<close>
          \<open>( 2::nat)^k \<ge>1\<close>  gcd_Esigma_mult assms C BB
[PROOF STATE]
proof (prove)
using this:
2 ^ k \<noteq> p * q
1 \<le> 2 ^ k
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
1 \<le> p * q
gcd (2 ^ k) (p * q) = 1

goal (1 subgoal):
 1. Esigma (2 ^ k * (p * q)) = Esigma (2 ^ k) * Esigma (p * q)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * (p * q)) = Esigma (2 ^ k) * Esigma (p * q)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * (p * q)) = Esigma (2 ^ k) * Esigma (p * q)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
have A7:"Esigma(p*q) = (Esigma p)*(Esigma q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (p * q) = Esigma p * Esigma q
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (p * q) = Esigma p * Esigma q
[PROOF STEP]
have "p \<noteq> q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p \<noteq> q
[PROOF STEP]
using assms One_nat_def Suc_pred add_gr_0 add_is_0 diff_commute diff_diff_cancel
          diff_is_0_eq nat_0_less_mult_iff nat_mult_eq_cancel_disj
          numeral_One prime_gt_1_nat power_inject_exp
          semiring_normalization_rules(7) two_is_prime_nat zero_less_numeral zero_less_power
zero_neq_numeral
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
1 = Suc 0
0 < ?n \<Longrightarrow> Suc (?n - Suc 0) = ?n
(0 < ?m + ?n) = (0 < ?m \<or> 0 < ?n)
(?m + ?n = 0) = (?m = 0 \<and> ?n = 0)
?i - ?j - ?k = ?i - ?k - ?j
?i \<le> ?n \<Longrightarrow> ?n - (?n - ?i) = ?i
(?m - ?n = 0) = (?m \<le> ?n)
(0 < ?m * ?n) = (0 < ?m \<and> 0 < ?n)
(?k * ?m = ?k * ?n) = (?k = 0 \<or> ?m = ?n)
Numeral1 = (1::?'a)
prime ?p \<Longrightarrow> 1 < ?p
(1::?'a) < ?a \<Longrightarrow> (?a ^ ?m = ?a ^ ?n) = (?m = ?n)
?a * ?b = ?b * ?a
prime 2
(0::?'a) < numeral ?n
(0::?'a) < ?a \<Longrightarrow> (0::?'a) < ?a ^ ?n
(0::?'a) \<noteq> numeral ?n

goal (1 subgoal):
 1. p \<noteq> q
[PROOF STEP]
by (smt less_imp_le_nat)
[PROOF STATE]
proof (state)
this:
p \<noteq> q

goal (1 subgoal):
 1. Esigma (p * q) = Esigma p * Esigma q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (p * q) = Esigma p * Esigma q
[PROOF STEP]
using \<open>p \<noteq> q\<close>
          \<open>prime p\<close>  \<open>prime q\<close> C  prime_Esigma_mult assms
[PROOF STATE]
proof (prove)
using this:
p \<noteq> q
prime p
prime q
1 \<le> p * q
\<lbrakk>prime ?m; prime ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> Esigma (?m * ?n) = Esigma ?n * Esigma ?m
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. Esigma (p * q) = Esigma p * Esigma q
[PROOF STEP]
by (metis mult.commute)
[PROOF STATE]
proof (state)
this:
Esigma (p * q) = Esigma p * Esigma q

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

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
have A8: "Esigma((2^k)*( p*q))=(Esigma(2^k))*(Esigma p)*(Esigma q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * (p * q)) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
by (simp add: A6 A7)
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * (p * q)) = Esigma (2 ^ k) * Esigma p * Esigma q

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
using A8
[PROOF STATE]
proof (prove)
using this:
Esigma (2 ^ k * (p * q)) = Esigma (2 ^ k) * Esigma p * Esigma q

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
by (simp add: mult.assoc)
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
have Z: "Esigma((2^k)*p*q) = Esigma ((2^k)*r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k * r)
[PROOF STEP]
using A1 A2 A3 A4 A5
[PROOF STATE]
proof (prove)
using this:
(p + 1) * (q + 1) = r + 1
Esigma p * Esigma q = Esigma r
Esigma (2 ^ k) * Esigma p * Esigma q = Esigma (2 ^ k) * Esigma r
Esigma (2 ^ k * r) = Esigma (2 ^ k) * Esigma r
Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k * r)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * p * q) = Esigma (2 ^ k * r)

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
have Z1: "Esigma ((2^k)*p*q) = 2^k *p*q + 2^k*r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have "prime (2::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have s: "Esigma (2^k) =((2::nat)^(k+1)-1)/(2-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma (2 ^ k)) = real (2 ^ (k + 1) - 1) / (2 - 1)
[PROOF STEP]
using  \<open>prime (2::nat)\<close> assms Esigma_prime_sum
[PROOF STATE]
proof (prove)
using this:
prime 2
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
\<lbrakk>prime ?m; 1 \<le> ?k\<rbrakk> \<Longrightarrow> real (Esigma (?m ^ ?k)) = real (?m ^ (?k + 1) - 1) / (real ?m - 1)

goal (1 subgoal):
 1. real (Esigma (2 ^ k)) = real (2 ^ (k + 1) - 1) / (2 - 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (Esigma (2 ^ k)) = real (2 ^ (k + 1) - 1) / (2 - 1)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have ss: "Esigma (2^k) =(2^(k+1)-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k) = 2 ^ (k + 1) - 1
[PROOF STEP]
using s
[PROOF STATE]
proof (prove)
using this:
real (Esigma (2 ^ k)) = real (2 ^ (k + 1) - 1) / (2 - 1)

goal (1 subgoal):
 1. Esigma (2 ^ k) = 2 ^ (k + 1) - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k) = 2 ^ (k + 1) - 1

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have J: "(k+1+k-l+k)= 3*k +1-l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. k + 1 + k - l + k = 3 * k + 1 - l
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. k + 1 + k - l + k = 3 * k + 1 - l
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
k + 1 + k - l + k = 3 * k + 1 - l

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have JJ: "(2^(k-l))*(2^k) = (2::nat)^(2*k-l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) * 2 ^ k = 2 ^ (2 * k - l)
[PROOF STEP]
apply (simp add: algebra_simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * 2 ^ (k - l) = 2 ^ (k * 2 - l)
[PROOF STEP]
by (metis Nat.add_diff_assoc assms(1) less_imp_le_nat mult_2_right power_add)
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) * 2 ^ k = 2 ^ (2 * k - l)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have "Esigma((2^k)*p*q)= (Esigma(2^k))*(Esigma p)*(Esigma q)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
using A5
[PROOF STATE]
proof (prove)
using this:
Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * p * q) = Esigma (2 ^ k) * Esigma p * Esigma q

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have "\<dots> = (2^(k+1)-1)*(p+1)*(q+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k) * Esigma p * Esigma q = (2 ^ (k + 1) - 1) * (p + 1) * (q + 1)
[PROOF STEP]
using assms ss aa bb
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
Esigma (2 ^ k) = 2 ^ (k + 1) - 1
Esigma p = p + 1
Esigma q = q + 1

goal (1 subgoal):
 1. Esigma (2 ^ k) * Esigma p * Esigma q = (2 ^ (k + 1) - 1) * (p + 1) * (q + 1)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k) * Esigma p * Esigma q = (2 ^ (k + 1) - 1) * (p + 1) * (q + 1)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k) * Esigma p * Esigma q = (2 ^ (k + 1) - 1) * (p + 1) * (q + 1)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have "\<dots> = (2^(k+1)-1)*((2^(k-l))*f)*((2^k)*f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 ^ (k + 1) - 1) * (p + 1) * (q + 1) = (2 ^ (k + 1) - 1) * (2 ^ (k - l) * f) * (2 ^ k * f)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. (2 ^ (k + 1) - 1) * (p + 1) * (q + 1) = (2 ^ (k + 1) - 1) * (2 ^ (k - l) * f) * (2 ^ k * f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(2 ^ (k + 1) - 1) * (p + 1) * (q + 1) = (2 ^ (k + 1) - 1) * (2 ^ (k - l) * f) * (2 ^ k * f)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(2 ^ (k + 1) - 1) * (p + 1) * (q + 1) = (2 ^ (k + 1) - 1) * (2 ^ (k - l) * f) * (2 ^ k * f)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have "\<dots> = (2^(k+1)-1)*(2^(k-l))*(2^k)*f^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 ^ (k + 1) - 1) * (2 ^ (k - l) * f) * (2 ^ k * f) = (2 ^ (k + 1) - 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2
[PROOF STEP]
by (simp add: power2_eq_square)
[PROOF STATE]
proof (state)
this:
(2 ^ (k + 1) - 1) * (2 ^ (k - l) * f) * (2 ^ k * f) = (2 ^ (k + 1) - 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(2 ^ (k + 1) - 1) * (2 ^ (k - l) * f) * (2 ^ k * f) = (2 ^ (k + 1) - 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have "\<dots> = (2^(k+1))*(2^(k-l))*(2^k)*f^2-(2^(k-l))*(2^k)*f^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 ^ (k + 1) - 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (k + 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2
[PROOF STEP]
by (smt left_diff_distrib' mult.commute mult_numeral_1_right numeral_One)
[PROOF STATE]
proof (state)
this:
(2 ^ (k + 1) - 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (k + 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(2 ^ (k + 1) - 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (k + 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have "\<dots> = (2^(k+1+k-l+k))*f^2-(2^(k-l))*(2^k)*f^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k + 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (k + 1 + k - l + k) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2
[PROOF STEP]
by (metis Nat.add_diff_assoc assms(1) less_imp_le_nat power_add)
[PROOF STATE]
proof (state)
this:
2 ^ (k + 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (k + 1 + k - l + k) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 ^ (k + 1) * 2 ^ (k - l) * 2 ^ k * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (k + 1 + k - l + k) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have "\<dots> = (2^(3*k+1-l))*f^2-(2^(k-l))*(2^k)*f^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k + 1 + k - l + k) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2
[PROOF STEP]
using J
[PROOF STATE]
proof (prove)
using this:
k + 1 + k - l + k = 3 * k + 1 - l

goal (1 subgoal):
 1. 2 ^ (k + 1 + k - l + k) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
2 ^ (k + 1 + k - l + k) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
2 ^ (k + 1 + k - l + k) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have "\<dots> = (2^(3*k+1-l))*f^2-(2^(2*k-l))*f^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
using JJ
[PROOF STATE]
proof (prove)
using this:
2 ^ (k - l) * 2 ^ k = 2 ^ (2 * k - l)

goal (1 subgoal):
 1. 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (k - l) * 2 ^ k * f\<^sup>2 = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
Esigma (2 ^ k * p * q) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have YY:" Esigma((2^k)*p*q)= (2^(3*k+1-l))*f^2-(2^(2*k-l))*f^2"
[PROOF STATE]
proof (prove)
using this:
Esigma (2 ^ k * p * q) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * p * q) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have auxicalc: "(2^(2*k-l))*(f^2)=(2^(2*k-l))*f +(2^(2*k))*f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
[PROOF STEP]
have i: "(2^(2*k-l))*f = (2^(2*k-l))*(2^l+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f = 2 ^ (2 * k - l) * (2 ^ l + 1)
[PROOF STEP]
using assms \<open>f = 2^l+1\<close>
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
f = 2 ^ l + 1

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f = 2 ^ (2 * k - l) * (2 ^ l + 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f = 2 ^ (2 * k - l) * (2 ^ l + 1)

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
[PROOF STEP]
have ii: "( 2^(2*k-l))*f = (2^(2*k-l))*( 2^l)+(2^(2*k-l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f = 2 ^ (2 * k - l) * 2 ^ l + 2 ^ (2 * k - l)
[PROOF STEP]
using i
[PROOF STATE]
proof (prove)
using this:
2 ^ (2 * k - l) * f = 2 ^ (2 * k - l) * (2 ^ l + 1)

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f = 2 ^ (2 * k - l) * 2 ^ l + 2 ^ (2 * k - l)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f = 2 ^ (2 * k - l) * 2 ^ l + 2 ^ (2 * k - l)

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
[PROOF STEP]
have iii: "(2^(2*k-l))*f = (2^(2*k-l+l))+(2^(2*k-l))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f = 2 ^ (2 * k - l + l) + 2 ^ (2 * k - l)
[PROOF STEP]
using ii
[PROOF STATE]
proof (prove)
using this:
2 ^ (2 * k - l) * f = 2 ^ (2 * k - l) * 2 ^ l + 2 ^ (2 * k - l)

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f = 2 ^ (2 * k - l + l) + 2 ^ (2 * k - l)
[PROOF STEP]
by (simp add: power_add)
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f = 2 ^ (2 * k - l + l) + 2 ^ (2 * k - l)

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
[PROOF STEP]
have iv: "( 2^(2*k-l))*f*f =(((2^(2*k))+(2^(2*k-l))))*f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f * f = (2 ^ (2 * k) + 2 ^ (2 * k - l)) * f
[PROOF STEP]
using iii assms
[PROOF STATE]
proof (prove)
using this:
2 ^ (2 * k - l) * f = 2 ^ (2 * k - l + l) + 2 ^ (2 * k - l)
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f * f = (2 ^ (2 * k) + 2 ^ (2 * k - l)) * f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f * f = (2 ^ (2 * k) + 2 ^ (2 * k - l)) * f

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
[PROOF STEP]
have v:  "(2^(2*k-l))*f *f =((2^(2*k)))*f+((2^(2*k-l)))*f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f * f = 2 ^ (2 * k) * f + 2 ^ (2 * k - l) * f
[PROOF STEP]
using iv assms comm_monoid_mult_axioms  power2_eq_square semiring_normalization_rules(18)
          semiring_normalization_rules
[PROOF STATE]
proof (prove)
using this:
2 ^ (2 * k - l) * f * f = (2 ^ (2 * k) + 2 ^ (2 * k - l)) * f
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
class.comm_monoid_mult (*) (1::?'a)
?a\<^sup>2 = ?a * ?a
?lx * (?rx * ?ry) = ?lx * ?rx * ?ry
?a * ?m + ?b * ?m = (?a + ?b) * ?m
?a * ?m + ?m = (?a + (1::?'a)) * ?m
?m + ?a * ?m = (?a + (1::?'a)) * ?m
?m + ?m = ((1::?'a) + (1::?'a)) * ?m
(0::?'a) + ?a = ?a
?a + (0::?'a) = ?a
?a * ?b = ?b * ?a
(?a + ?b) * ?c = ?a * ?c + ?b * ?c
(0::?'a) * ?a = (0::?'a)
?a * (0::?'a) = (0::?'a)
(1::?'a) * ?a = ?a
?a * (1::?'a) = ?a
?lx * ?ly * (?rx * ?ry) = ?lx * ?rx * (?ly * ?ry)
?lx * ?ly * (?rx * ?ry) = ?lx * (?ly * (?rx * ?ry))
?lx * ?ly * (?rx * ?ry) = ?rx * (?lx * ?ly * ?ry)
?lx * ?ly * ?rx = ?lx * ?rx * ?ly
?lx * ?ly * ?rx = ?lx * (?ly * ?rx)
?lx * (?rx * ?ry) = ?lx * ?rx * ?ry
?lx * (?rx * ?ry) = ?rx * (?lx * ?ry)
?a + ?b + (?c + ?d) = ?a + ?c + (?b + ?d)
?a + ?b + ?c = ?a + (?b + ?c)
?a + (?c + ?d) = ?c + (?a + ?d)
?a + ?b + ?c = ?a + ?c + ?b
?a + ?c = ?c + ?a
?a + (?c + ?d) = ?a + ?c + ?d
?x ^ ?p * ?x ^ ?q = ?x ^ (?p + ?q)
?x * ?x ^ ?q = ?x ^ Suc ?q
?x ^ ?q * ?x = ?x ^ Suc ?q
?x * ?x = ?x\<^sup>2
(?x * ?y) ^ ?q = ?x ^ ?q * ?y ^ ?q
(?x ^ ?p) ^ ?q = ?x ^ (?p * ?q)
?x ^ 0 = (1::?'a)
?x ^ 1 = ?x
?x * (?y + ?z) = ?x * ?y + ?x * ?z
?x ^ Suc ?q = ?x * ?x ^ ?q
?x ^ (2 * ?n) = ?x ^ ?n * ?x ^ ?n

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f * f = 2 ^ (2 * k) * f + 2 ^ (2 * k - l) * f
[PROOF STEP]
by (simp add: add_mult_distrib assms)
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f * f = 2 ^ (2 * k) * f + 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
[PROOF STEP]
(*slow*)
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f * f = 2 ^ (2 * k) * f + 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
[PROOF STEP]
using v
[PROOF STATE]
proof (prove)
using this:
2 ^ (2 * k - l) * f * f = 2 ^ (2 * k) * f + 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
[PROOF STEP]
by (simp add: power2_eq_square semiring_normalization_rules(18))
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have W1: "2^k*p*q + 2^k*r = 2^k *(p*q +r) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * p * q + 2 ^ k * r = 2 ^ k * (p * q + r)
[PROOF STEP]
by (simp add: add_mult_distrib2)
[PROOF STATE]
proof (state)
this:
2 ^ k * p * q + 2 ^ k * r = 2 ^ k * (p * q + r)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have W2: "2^k*(p*q +r)= 2^k *((2^(k-l)*f-1)*((2^k)*f-1)+(2^(2*k-l))*f^2-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (p * q + r) = 2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 2 ^ k * (p * q + r) = 2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ k * (p * q + r) = 2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have W3: "2^k*((2^(k-l)*f-1)*((2^k)*f-1)+(2^(2*k-l))*f^2-1)=
2^k*((2^(k-l)*f-1)*((2^k)*f)-(2^(k-l)*f-1)+(2^(2*k-l))*f^2-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f) - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
[PROOF STEP]
by (simp add: right_diff_distrib')
[PROOF STATE]
proof (state)
this:
2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f) - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have W4: "2^k*((2^(k-l)*f-1)*((2^k)*f)-(2^(k-l)*f-1)+(2^(2*k-l))*f^2-1) =
2^k*((2^(k-l)*f)*((2^k)*f)-((2^k)*f)-(2^(k-l)*f-1)+(2^(2*k-l))*f^2-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f) - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f) - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
[PROOF STEP]
by (simp add: diff_mult_distrib)
[PROOF STATE]
proof (state)
this:
2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f) - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have W5: " 2^k*((2^(k-l)*f)*((2^k)*f)-((2^k)*f)-(2^(k-l)*f-1)+(2^(2*k-l))*f^2-1) =
2^k *(( 2^(k-l)*f)*((2^k)*f)-((2^k)*f)-(2^(k-l)*f)+1 +(2^(2*k-l))*f^2-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 1 + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
[PROOF STEP]
using assms  less_imp_le_nat less_imp_le_nat  prime_ge_1_nat
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
?m < ?n \<Longrightarrow> ?m \<le> ?n
?m < ?n \<Longrightarrow> ?m \<le> ?n
prime ?p \<Longrightarrow> 1 \<le> ?p

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 1 + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
[PROOF STEP]
by (smt Nat.add_diff_assoc2 Nat.diff_diff_right One_nat_def Suc_leI Suc_pred W3 W4
          add_diff_cancel_right' add_gr_0 le_Suc_ex less_numeral_extra(1) mult_cancel1
          nat_0_less_mult_iff zero_less_diff zero_less_numeral zero_less_power)
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 1 + 2 ^ (2 * k - l) * f\<^sup>2 - 1)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have W6: "2^k*((2^(k-l)* f)*((2^k)*f)-((2^k)*f)-(2^(k-l)*f)+1+(2^(2*k-l))*f^2-1 ) =
 2^k*((2^(k-l)*f)*((2^k)*f)-((2^k )*f)-(2^(k-l)*f)+(2^(2*k-l))*f^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 1 + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 1 + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have W7: "2^k*((2^(k-l)*f)*((2^k)*f)-((2^k)*f)-(2^(k-l)*f)+(2^(2*k-l))*f^2) =
   2^k *((2^(2*k-l+1)*(f^2))-((2^k)*f)-(2^(k-l)* f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
have a: "(2^(k-l)*f)*(2^k * f) = (2^(k-l)*f*(f*(2^k))) "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) = 2 ^ (k - l) * f * (f * 2 ^ k)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) = 2 ^ (k - l) * f * (f * 2 ^ k)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) * f * (2 ^ k * f) = 2 ^ (k - l) * f * (f * 2 ^ k)

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
have b: "(2^(k-l)*f)*(f*(2^k)) = 2^(k-l)*(f*f)*(2^k)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) * f * (f * 2 ^ k) = 2 ^ (k - l) * (f * f) * 2 ^ k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 2 ^ (k - l) * f * (f * 2 ^ k) = 2 ^ (k - l) * (f * f) * 2 ^ k
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) * f * (f * 2 ^ k) = 2 ^ (k - l) * (f * f) * 2 ^ k

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
have c: "2^(k-l)*(f*f)*(2^k) = 2^(k-l+k)*(f^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) * (f * f) * 2 ^ k = 2 ^ (k - l + k) * f\<^sup>2
[PROOF STEP]
using Semiring_Normalization.comm_semiring_1_class.semiring_normalization_rules(16)
          Semiring_Normalization.comm_semiring_1_class.semiring_normalization_rules(29)
[PROOF STATE]
proof (prove)
using this:
?lx * ?ly * ?rx = ?lx * ?rx * ?ly
?x * ?x = ?x\<^sup>2

goal (1 subgoal):
 1. 2 ^ (k - l) * (f * f) * 2 ^ k = 2 ^ (k - l + k) * f\<^sup>2
[PROOF STEP]
by  (simp add:  power_add)
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) * (f * f) * 2 ^ k = 2 ^ (k - l + k) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
have d: "2^(k-l+k) *(f^2) = 2^(2*k-l) *(f^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l + k) * f\<^sup>2 = 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
by (simp add: JJ power_add)
[PROOF STATE]
proof (state)
this:
2 ^ (k - l + k) * f\<^sup>2 = 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
have e: "(2^(2*k-l))*f^2 + (2^(2*k-l))*f^2 =  2^(2*k-l +1)*(f^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f\<^sup>2 + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
have f1: "((2^(k-l)*f)*((2^k)*f)-((2^k)*f)-(2^(k-l)*f)+(2^(2*k-l))*f^2) =
    (2^(2*k-l)*(f^2)-((2^k)*f)-(2^(k-l)*f)+(2^(2*k-l))*f^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
using a b c d e
[PROOF STATE]
proof (prove)
using this:
2 ^ (k - l) * f * (2 ^ k * f) = 2 ^ (k - l) * f * (f * 2 ^ k)
2 ^ (k - l) * f * (f * 2 ^ k) = 2 ^ (k - l) * (f * f) * 2 ^ k
2 ^ (k - l) * (f * f) * 2 ^ k = 2 ^ (k - l + k) * f\<^sup>2
2 ^ (k - l + k) * f\<^sup>2 = 2 ^ (2 * k - l) * f\<^sup>2
2 ^ (2 * k - l) * f\<^sup>2 + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
have f2:"((2^(k-l)*f)*((2^k)*f)-((2^k)*f)-(2^(k-l)*f))+(2^(2*k-l))*f^2
       = ((2^(2*k-l+1)*(f^2))-((2^k)*f)-(2^(k-l)*f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f
[PROOF STEP]
have aa: "f > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < f
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

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

goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f
[PROOF STEP]
have a: "((2::nat)^(2*k-l))*f^2-((2::nat)^(k-l)*f)>0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f
[PROOF STEP]
have b: "(2::nat)^(2*k-l) > 2^(k-l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) < 2 ^ (2 * k - l)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 2 ^ (k - l) < 2 ^ (2 * k - l)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) < 2 ^ (2 * k - l)

goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f
[PROOF STEP]
have c: "(2::nat)^(2*k-l)*f > 2^(k-l)*f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) * f < 2 ^ (2 * k - l) * f
[PROOF STEP]
using a assms
[PROOF STATE]
proof (prove)
using this:
2 ^ (k - l) * f * (2 ^ k * f) = 2 ^ (k - l) * f * (f * 2 ^ k)
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 2 ^ (k - l) * f < 2 ^ (2 * k - l) * f
[PROOF STEP]
by (metis One_nat_def add_gr_0 b lessI mult_less_mono1)
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) * f < 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f
[PROOF STEP]
using c auxicalc
[PROOF STATE]
proof (prove)
using this:
2 ^ (k - l) * f < 2 ^ (2 * k - l) * f
2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f

goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f

goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f
[PROOF STEP]
have aaa: "(2^(2*k-l))*f^2 -(2^(k-l)*f)-((2^k)*f) >0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f - 2 ^ k * f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f - 2 ^ k * f
[PROOF STEP]
have A: "(2^(2*k-l))*f-(2^(k-l))-(( 2^k)) >0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f - 2 ^ (k - l) - 2 ^ k
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f - 2 ^ (k - l) - 2 ^ k
[PROOF STEP]
have A_1 : "(2^(2*k-l))*f  > (2^(k-l))+((2^k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
have A_2: "(2^(2*k-l))*f = 2^(k)*2^(k-l)*f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f = 2 ^ k * 2 ^ (k - l) * f
[PROOF STEP]
by (metis JJ semiring_normalization_rules(7))
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f = 2 ^ k * 2 ^ (k - l) * f

goal (1 subgoal):
 1. 2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
have df1: "(2^(k-l))+((2^k))< ((2::nat)^(2*k-l))+((2^k))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) + 2 ^ k
[PROOF STEP]
using \<open>l < k\<close>
[PROOF STATE]
proof (prove)
using this:
l < k

goal (1 subgoal):
 1. 2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) + 2 ^ k
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) + 2 ^ k

goal (1 subgoal):
 1. 2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
have df2: "((2::nat)^(2*k-l))+((2^k)) < ((2::nat)^(2*k-l))*f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
have "k >1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < k
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

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

goal (1 subgoal):
 1. 2 ^ (2 * k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
have df: "((2::nat)^(k-l))+(1::nat) < ((2::nat)^(k-l))*f"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * f
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * f
[PROOF STEP]
obtain x::nat where xx: "x=(2::nat)^(k-l)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. x = 2 ^ (k - l) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = 2 ^ (k - l)

goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * f
[PROOF STEP]
have xxx: "x \<ge>( 2::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<le> x
[PROOF STEP]
using assms xx
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
x = 2 ^ (k - l)

goal (1 subgoal):
 1. 2 \<le> x
[PROOF STEP]
by (metis One_nat_def Suc_leI one_le_numeral power_increasing
                        semiring_normalization_rules(33) zero_less_diff)
[PROOF STATE]
proof (state)
this:
2 \<le> x

goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * f
[PROOF STEP]
have c: "x*f \<ge> x*(2::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x * 2 \<le> x * f
[PROOF STEP]
using aa
[PROOF STATE]
proof (prove)
using this:
1 < f

goal (1 subgoal):
 1. x * 2 \<le> x * f
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x * 2 \<le> x * f

goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * f
[PROOF STEP]
have c1: "x+(1::nat) < x*(2::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x + 1 < x * 2
[PROOF STEP]
using auxiliary_ineq  xxx
[PROOF STATE]
proof (prove)
using this:
2 \<le> ?x \<Longrightarrow> ?x + 1 < 2 * ?x
2 \<le> x

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

goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * f
[PROOF STEP]
have c2: "((2::nat)^(k-l))+(1::nat) < ((2::nat)^(k-l))*(2::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * 2
[PROOF STEP]
using c1 xx
[PROOF STATE]
proof (prove)
using this:
x + 1 < x * 2
x = 2 ^ (k - l)

goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * 2
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) + 1 < 2 ^ (k - l) * 2

goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * f
[PROOF STEP]
using c2 c xx
[PROOF STATE]
proof (prove)
using this:
2 ^ (k - l) + 1 < 2 ^ (k - l) * 2
x * 2 \<le> x * f
x = 2 ^ (k - l)

goal (1 subgoal):
 1. 2 ^ (k - l) + 1 < 2 ^ (k - l) * f
[PROOF STEP]
by (metis diff_is_0_eq' le_trans nat_less_le zero_less_diff)
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) + 1 < 2 ^ (k - l) * f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) + 1 < 2 ^ (k - l) * f

goal (1 subgoal):
 1. 2 ^ (2 * k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
using df aa assms
[PROOF STATE]
proof (prove)
using this:
2 ^ (k - l) + 1 < 2 ^ (k - l) * f
1 < f
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 2 ^ (2 * k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
by (smt JJ add.commute mult_less_cancel2 semiring_normalization_rules
                      zero_less_numeral zero_less_power)
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) + 2 ^ k < 2 ^ (2 * k - l) * f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) + 2 ^ k < 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. 2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
using A_2 df1 df2
[PROOF STATE]
proof (prove)
using this:
2 ^ (2 * k - l) * f = 2 ^ k * 2 ^ (k - l) * f
2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) + 2 ^ k
2 ^ (2 * k - l) + 2 ^ k < 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. 2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f - 2 ^ (k - l) - 2 ^ k
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f - 2 ^ (k - l) - 2 ^ k
[PROOF STEP]
using assms A_1
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f - 2 ^ (k - l) - 2 ^ k
[PROOF STEP]
using diff_diff_left zero_less_diff
[PROOF STATE]
proof (prove)
using this:
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
2 ^ (k - l) + 2 ^ k < 2 ^ (2 * k - l) * f
?i - ?j - ?k = ?i - (?j + ?k)
(0 < ?n - ?m) = (?m < ?n)

goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f - 2 ^ (k - l) - 2 ^ k
[PROOF STEP]
by presburger
[PROOF STATE]
proof (state)
this:
0 < 2 ^ (2 * k - l) * f - 2 ^ (k - l) - 2 ^ k

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < 2 ^ (2 * k - l) * f - 2 ^ (k - l) - 2 ^ k

goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f - 2 ^ k * f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f - 2 ^ k * f
[PROOF STEP]
using A aa assms
[PROOF STATE]
proof (prove)
using this:
0 < 2 ^ (2 * k - l) * f - 2 ^ (k - l) - 2 ^ k
1 < f
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r

goal (1 subgoal):
 1. 0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f - 2 ^ k * f
[PROOF STEP]
by (metis (no_types, opaque_lifting)  a nat_0_less_mult_iff right_diff_distrib'
                semiring_normalization_rules(18) semiring_normalization_rules(29)
               semiring_normalization_rules(7))
[PROOF STATE]
proof (state)
this:
0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f - 2 ^ k * f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f - 2 ^ k * f

goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f
[PROOF STEP]
have b3: "((2^(2*k-l)*(f^2))-((2^k)*f)-(2^(k-l)*f)+(2^(2*k-l))*f^2) =
                  (2*(2^(2*k-l)*(f^2))-((2^k)*f)-(2^(k-l)*f))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 * (2 ^ (2 * k - l) * f\<^sup>2) - 2 ^ k * f - 2 ^ (k - l) * f
[PROOF STEP]
using a aa assms  minus_eq_nat_subst_order
[PROOF STATE]
proof (prove)
using this:
0 < 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ (k - l) * f
1 < f
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
\<lbrakk>0 < ?B - ?C - ?D; ?A = ?B - ?C - ?D + ?B\<rbrakk> \<Longrightarrow> ?A = 2 * ?B - ?C - ?D

goal (1 subgoal):
 1. 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 * (2 ^ (2 * k - l) * f\<^sup>2) - 2 ^ k * f - 2 ^ (k - l) * f
[PROOF STEP]
by (smt aaa diff_commute)
[PROOF STATE]
proof (state)
this:
2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 * (2 ^ (2 * k - l) * f\<^sup>2) - 2 ^ k * f - 2 ^ (k - l) * f

goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f
[PROOF STEP]
using f1
[PROOF STATE]
proof (prove)
using this:
2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f
[PROOF STEP]
by (metis b3 e mult_2)
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
using f2
[PROOF STATE]
proof (prove)
using this:
2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have W8: "2^k*((2^(2*k-l+1)*(f^2))-((2^k)*f)-(2^(k-l)*f)) = (2^(3*k+1-l))*f^2-(2^(2*k-l))*f^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have a: "2^k*(2^(2*k-l+1)*f^2-2^k*f-2^(k-l)*f) = 2^k*(2^(2*k-l+1)*f^2)-2^k*(2^k*f)-2^k*(2^(k-l)*f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have b: "2^k*(2^(2*k-l+1)*f^2)-2^k*(2^k*f)-2^k*(2^(k-l)*f) =
2^k*(2^(2*k-l+1)*f^2)-2^k*(2^k*f)-2^k*(2^(k-l)*f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)
[PROOF STEP]
by (simp add: algebra_simps)
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have c: "2^k*(2^(2*k-l+1)*f^2)-2^k*(2^k*f)-2^k*(2^(k-l)*f) =
2^(2*k+1-l+k)*f^2-2^k*(2^k*f)-2^k*(2^(k-l)*f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f) = 2 ^ (2 * k + 1 - l + k) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)
[PROOF STEP]
apply (simp add: algebra_simps power_add)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 * (f\<^sup>2 * (2 ^ k * 2 ^ (k * 2 - l))) - (f * (2 ^ k * 2 ^ k) + f * (2 ^ k * 2 ^ (k - l))) = f\<^sup>2 * (2 ^ k * 2 ^ (Suc (k * 2) - l)) - (f * (2 ^ k * 2 ^ k) + f * (2 ^ k * 2 ^ (k - l)))
[PROOF STEP]
by (smt Groups.mult_ac(1) Groups.mult_ac(2) Nat.diff_add_assoc assms(1) le_simps(1)
mult_2_right plus_nat.simps(2) power.simps(2))
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f) = 2 ^ (2 * k + 1 - l + k) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have d: "2^k*(2^(2*k-l+1)*(f^2))= (2^(3*k+1-l))*f^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) = 2 ^ (3 * k + 1 - l) * f\<^sup>2
[PROOF STEP]
using power_add   Nat.add_diff_assoc assms(1) less_imp_le_nat mult_2
          semiring_normalization_rules(18) semiring_normalization_rules(23)
[PROOF STATE]
proof (prove)
using this:
?a ^ (?m + ?n) = ?a ^ ?m * ?a ^ ?n
?k \<le> ?j \<Longrightarrow> ?i + (?j - ?k) = ?i + ?j - ?k
l < k
?m < ?n \<Longrightarrow> ?m \<le> ?n
(2::?'a) * ?z = ?z + ?z
?lx * (?rx * ?ry) = ?lx * ?rx * ?ry
?a + ?b + ?c = ?a + ?c + ?b

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) = 2 ^ (3 * k + 1 - l) * f\<^sup>2
[PROOF STEP]
by (smt J)
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) = 2 ^ (3 * k + 1 - l) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have e: "2^k*((2^(2*k-l+1)*(f^2))-((2^k)*f)-(2^(k-l)*f)) =
(2^(3*k+1-l))*f^2-(2^k)*((2^k)*f)-(2^k)*(2^(k-l)*f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)
[PROOF STEP]
using a b c d  One_nat_def  one_le_mult_iff
          Nat.add_diff_assoc assms(1) less_imp_le_nat
[PROOF STATE]
proof (prove)
using this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f) = 2 ^ (2 * k + 1 - l + k) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2) = 2 ^ (3 * k + 1 - l) * f\<^sup>2
1 = Suc 0
(Suc 0 \<le> ?m * ?n) = (Suc 0 \<le> ?m \<and> Suc 0 \<le> ?n)
?k \<le> ?j \<Longrightarrow> ?i + (?j - ?k) = ?i + ?j - ?k
l < k
?m < ?n \<Longrightarrow> ?m \<le> ?n

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have ee: "2^k*((2^(2*k-l+1)*(f^2))-((2^k)*f)-((2::nat)^(k-l)*f))
= (2^(3*k+1-l))*f^2-( 2^k)*((2^k)*f)-(2^(2*k-l)*f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ (2 * k - l) * f
[PROOF STEP]
using e  power_add  Nat.add_diff_assoc assms(1) less_imp_le_nat mult_2
          semiring_normalization_rules
[PROOF STATE]
proof (prove)
using this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ k * (2 ^ (k - l) * f)
?a ^ (?m + ?n) = ?a ^ ?m * ?a ^ ?n
?k \<le> ?j \<Longrightarrow> ?i + (?j - ?k) = ?i + ?j - ?k
l < k
?m < ?n \<Longrightarrow> ?m \<le> ?n
(2::?'a) * ?z = ?z + ?z
?a * ?m + ?b * ?m = (?a + ?b) * ?m
?a * ?m + ?m = (?a + (1::?'a)) * ?m
?m + ?a * ?m = (?a + (1::?'a)) * ?m
?m + ?m = ((1::?'a) + (1::?'a)) * ?m
(0::?'a) + ?a = ?a
?a + (0::?'a) = ?a
?a * ?b = ?b * ?a
(?a + ?b) * ?c = ?a * ?c + ?b * ?c
(0::?'a) * ?a = (0::?'a)
?a * (0::?'a) = (0::?'a)
(1::?'a) * ?a = ?a
?a * (1::?'a) = ?a
?lx * ?ly * (?rx * ?ry) = ?lx * ?rx * (?ly * ?ry)
?lx * ?ly * (?rx * ?ry) = ?lx * (?ly * (?rx * ?ry))
?lx * ?ly * (?rx * ?ry) = ?rx * (?lx * ?ly * ?ry)
?lx * ?ly * ?rx = ?lx * ?rx * ?ly
?lx * ?ly * ?rx = ?lx * (?ly * ?rx)
?lx * (?rx * ?ry) = ?lx * ?rx * ?ry
?lx * (?rx * ?ry) = ?rx * (?lx * ?ry)
?a + ?b + (?c + ?d) = ?a + ?c + (?b + ?d)
?a + ?b + ?c = ?a + (?b + ?c)
?a + (?c + ?d) = ?c + (?a + ?d)
?a + ?b + ?c = ?a + ?c + ?b
?a + ?c = ?c + ?a
?a + (?c + ?d) = ?a + ?c + ?d
?x ^ ?p * ?x ^ ?q = ?x ^ (?p + ?q)
?x * ?x ^ ?q = ?x ^ Suc ?q
?x ^ ?q * ?x = ?x ^ Suc ?q
?x * ?x = ?x\<^sup>2
(?x * ?y) ^ ?q = ?x ^ ?q * ?y ^ ?q
(?x ^ ?p) ^ ?q = ?x ^ (?p * ?q)
?x ^ 0 = (1::?'a)
?x ^ 1 = ?x
?x * (?y + ?z) = ?x * ?y + ?x * ?z
?x ^ Suc ?q = ?x * ?x ^ ?q
?x ^ (2 * ?n) = ?x ^ ?n * ?x ^ ?n

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ (2 * k - l) * f
[PROOF STEP]
by (smt J)
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have eee :
        "-(( 2::nat)^(2*k-l))*(f^(2::nat)) =(-(( 2::nat)^(2*k))*f-(( 2::nat)^(2*k-l))*f)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - int (2 ^ (2 * k - l)) * int (f\<^sup>2) = - int (2 ^ (2 * k)) * int f - int (2 ^ (2 * k - l) * f)
[PROOF STEP]
using auxicalc mult_minus_eq_nat mult_minus_left of_nat_mult
[PROOF STATE]
proof (prove)
using this:
2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f
?x + ?y = ?z \<Longrightarrow> - int ?x - int ?y = - int ?z
- ?a * ?b = - (?a * ?b)
of_nat (?m * ?n) = of_nat ?m * of_nat ?n

goal (1 subgoal):
 1. - int (2 ^ (2 * k - l)) * int (f\<^sup>2) = - int (2 ^ (2 * k)) * int f - int (2 ^ (2 * k - l) * f)
[PROOF STEP]
by smt
[PROOF STATE]
proof (state)
this:
- int (2 ^ (2 * k - l)) * int (f\<^sup>2) = - int (2 ^ (2 * k)) * int f - int (2 ^ (2 * k - l) * f)

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have e4: "2^k*((2^(2*k-l+1)*(f^2))-((2^k)*f)-(2^(k-l)*f))=(2^(3*k+1-l))*f^2-(2^(2*k-l))*(f^2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
define A where A: "A = 2^k*((2^(2*k-l+1)*(f^2))-((2^k)*f)-(2^(k-l)*f))"
[PROOF STATE]
proof (state)
this:
A = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
define B where B: "B = (2^(3*k+(1::nat)-l))*f^2"
[PROOF STATE]
proof (state)
this:
B = 2 ^ (3 * k + 1 - l) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
define C where C: "C = (2^k)*((2^k)*f)"
[PROOF STATE]
proof (state)
this:
C = 2 ^ k * (2 ^ k * f)

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
define D where D: "D = (2^(2*k-l)*f)"
[PROOF STATE]
proof (state)
this:
D = 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
define E where E: "E = (2^(2*k-l))*(f^2)"
[PROOF STATE]
proof (state)
this:
E = 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have wq: "A = B-C-D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B - C - D
[PROOF STEP]
using ee A B C D
[PROOF STATE]
proof (prove)
using this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ k * (2 ^ k * f) - 2 ^ (2 * k - l) * f
A = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
B = 2 ^ (3 * k + 1 - l) * f\<^sup>2
C = 2 ^ k * (2 ^ k * f)
D = 2 ^ (2 * k - l) * f

goal (1 subgoal):
 1. A = B - C - D
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
A = B - C - D

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have wq1: "-E = -C-D"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. - int E = - int C - int D
[PROOF STEP]
using eee C D E
[PROOF STATE]
proof (prove)
using this:
- int (2 ^ (2 * k - l)) * int (f\<^sup>2) = - int (2 ^ (2 * k)) * int f - int (2 ^ (2 * k - l) * f)
C = 2 ^ k * (2 ^ k * f)
D = 2 ^ (2 * k - l) * f
E = 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. - int E = - int C - int D
[PROOF STEP]
by (simp add: semiring_normalization_rules(36))
[PROOF STATE]
proof (state)
this:
- int E = - int C - int D

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
have wq2: "A = B-E"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. A = B - E
[PROOF STEP]
using wq wq1  minus_eq_nat_subst
[PROOF STATE]
proof (prove)
using this:
A = B - C - D
- int E = - int C - int D
\<lbrakk>?A = ?B - ?C - ?D; - int ?E = - int ?C - int ?D\<rbrakk> \<Longrightarrow> ?A = ?B - ?E

goal (1 subgoal):
 1. A = B - E
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
A = B - E

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
using wq2 A B E
[PROOF STATE]
proof (prove)
using this:
A = B - E
A = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
B = 2 ^ (3 * k + 1 - l) * f\<^sup>2
E = 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
using e4
[PROOF STATE]
proof (prove)
using this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
have Y: "2^k*p*q+2^k*r = (2^(3*k+1-l))*f^2-(2^(2*k-l))*f^2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ k * p * q + 2 ^ k * r = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
using W1 W2 W3 W4 W5 W6 W7 W8
[PROOF STATE]
proof (prove)
using this:
2 ^ k * p * q + 2 ^ k * r = 2 ^ k * (p * q + r)
2 ^ k * (p * q + r) = 2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f) - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
2 ^ k * ((2 ^ (k - l) * f - 1) * (2 ^ k * f) - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - (2 ^ (k - l) * f - 1) + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 1 + 2 ^ (2 * k - l) * f\<^sup>2 - 1)
2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 1 + 2 ^ (2 * k - l) * f\<^sup>2 - 1) = 2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2)
2 ^ k * (2 ^ (k - l) * f * (2 ^ k * f) - 2 ^ k * f - 2 ^ (k - l) * f + 2 ^ (2 * k - l) * f\<^sup>2) = 2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f)
2 ^ k * (2 ^ (2 * k - l + 1) * f\<^sup>2 - 2 ^ k * f - 2 ^ (k - l) * f) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. 2 ^ k * p * q + 2 ^ k * r = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
[PROOF STEP]
by linarith
[PROOF STATE]
proof (state)
this:
2 ^ k * p * q + 2 ^ k * r = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
using Y YY  auxicalc
[PROOF STATE]
proof (prove)
using this:
2 ^ k * p * q + 2 ^ k * r = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
Esigma (2 ^ k * p * q) = 2 ^ (3 * k + 1 - l) * f\<^sup>2 - 2 ^ (2 * k - l) * f\<^sup>2
2 ^ (2 * k - l) * f\<^sup>2 = 2 ^ (2 * k - l) * f + 2 ^ (2 * k) * f

goal (1 subgoal):
 1. Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r

goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. m Amic n
[PROOF STEP]
using Z Z1 Amicable_pair_equiv_def_conv assms One_nat_def  one_le_mult_iff
         one_le_numeral less_imp_le_nat one_le_power
[PROOF STATE]
proof (prove)
using this:
Esigma (2 ^ k * p * q) = Esigma (2 ^ k * r)
Esigma (2 ^ k * p * q) = 2 ^ k * p * q + 2 ^ k * r
\<lbrakk>1 \<le> ?m; 1 \<le> ?n; Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n\<rbrakk> \<Longrightarrow> ?m Amic ?n
l < k
1 \<le> l
f = 2 ^ l + 1
prime p
prime q
prime r
p = 2 ^ (k - l) * f - 1
q = 2 ^ k * f - 1
r = 2 ^ (2 * k - l) * f\<^sup>2 - 1
m = 2 ^ k * p * q
n = 2 ^ k * r
1 = Suc 0
(Suc 0 \<le> ?m * ?n) = (Suc 0 \<le> ?m \<and> Suc 0 \<le> ?n)
(1::?'a) \<le> numeral ?n
?m < ?n \<Longrightarrow> ?m \<le> ?n
(1::?'a) \<le> ?a \<Longrightarrow> (1::?'a) \<le> ?a ^ ?n

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem Euler_Rule_Amicable_1:
  fixes m n a :: nat
  assumes "m \<ge> 1" and "n \<ge> 1" and "a \<ge> 1"
      and "Esigma m = Esigma n" and "Esigma a * Esigma m = a*(m+n)"
      and "gcd a m =1" and "gcd a n =1"
      shows "(a*m) Amic (a*n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * m) Amic (a * n)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a * m) Amic (a * n)
[PROOF STEP]
have a: "Esigma (a*m) =(Esigma a)*(Esigma m)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * m) = Esigma a * Esigma m
[PROOF STEP]
using assms  gcd_Esigma_mult
[PROOF STATE]
proof (prove)
using this:
1 \<le> m
1 \<le> n
1 \<le> a
Esigma m = Esigma n
Esigma a * Esigma m = a * (m + n)
gcd a m = 1
gcd a n = 1
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n

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

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

goal (1 subgoal):
 1. Esigma (a * n) = Esigma a * Esigma n
[PROOF STEP]
by (metis assms(4) a )
[PROOF STATE]
proof (state)
this:
Esigma (a * n) = Esigma a * Esigma n

goal (1 subgoal):
 1. Esigma (a * m) = Esigma (a * n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * m) = Esigma (a * n)
[PROOF STEP]
using c a assms
[PROOF STATE]
proof (prove)
using this:
Esigma (a * n) = Esigma a * Esigma n
Esigma (a * m) = Esigma a * Esigma m
1 \<le> m
1 \<le> n
1 \<le> a
Esigma m = Esigma n
Esigma a * Esigma m = a * (m + n)
gcd a m = 1
gcd a n = 1

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

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

goal (1 subgoal):
 1. (a * m) Amic (a * n)
[PROOF STEP]
have d: " Esigma (a*m) = a*m + a*n "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * m) = a * m + a * n
[PROOF STEP]
using a assms
[PROOF STATE]
proof (prove)
using this:
Esigma (a * m) = Esigma a * Esigma m
1 \<le> m
1 \<le> n
1 \<le> a
Esigma m = Esigma n
Esigma a * Esigma m = a * (m + n)
gcd a m = 1
gcd a n = 1

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

goal (1 subgoal):
 1. (a * m) Amic (a * n)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * m) Amic (a * n)
[PROOF STEP]
using a b d Amicable_pair_equiv_def_conv assms
[PROOF STATE]
proof (prove)
using this:
Esigma (a * m) = Esigma a * Esigma m
Esigma (a * m) = Esigma (a * n)
Esigma (a * m) = a * m + a * n
\<lbrakk>1 \<le> ?m; 1 \<le> ?n; Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n\<rbrakk> \<Longrightarrow> ?m Amic ?n
1 \<le> m
1 \<le> n
1 \<le> a
Esigma m = Esigma n
Esigma a * Esigma m = a * (m + n)
gcd a m = 1
gcd a n = 1

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Amicable_Example_Pythagoras:
  shows "220 Amic 284"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
have a: "(2::nat)>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < 2

goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
have b: "prime((3::nat)*(2^(2-1))-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (3 * 2 ^ (2 - 1) - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime (3 * 2 ^ (2 - 1) - 1)

goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
have c: "prime((3::nat)*(2^2)-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (3 * 2\<^sup>2 - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime (3 * 2\<^sup>2 - 1)

goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
have d: "prime((9::nat)*(2^(2*2-1))-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (9 * 2 ^ (2 * 2 - 1) - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime (9 * 2 ^ (2 * 2 - 1) - 1)

goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
have e: "((2^2)*(3*(2^(2-1))-1)*(3*(2^2)-1))Amic((2^2)*(9*(2^(2*2-1))-1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2\<^sup>2 * (3 * 2 ^ (2 - 1) - 1) * (3 * 2\<^sup>2 - 1)) Amic (2\<^sup>2 * (9 * 2 ^ (2 * 2 - 1) - 1))
[PROOF STEP]
using Thabit_ibn_Qurra_Rule_Amicable a b c d
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 < ?k; prime ?p; prime ?q; prime ?r; ?p = 2 ^ (?k - 1) * 3 - 1; ?q = 2 ^ ?k * 3 - 1; ?r = 2 ^ (2 * ?k - 1) * 9 - 1\<rbrakk> \<Longrightarrow> (2 ^ ?k * ?p * ?q) Amic (2 ^ ?k * ?r)
1 < 2
prime (3 * 2 ^ (2 - 1) - 1)
prime (3 * 2\<^sup>2 - 1)
prime (9 * 2 ^ (2 * 2 - 1) - 1)

goal (1 subgoal):
 1. (2\<^sup>2 * (3 * 2 ^ (2 - 1) - 1) * (3 * 2\<^sup>2 - 1)) Amic (2\<^sup>2 * (9 * 2 ^ (2 * 2 - 1) - 1))
[PROOF STEP]
by (metis mult.commute)
[PROOF STATE]
proof (state)
this:
(2\<^sup>2 * (3 * 2 ^ (2 - 1) - 1) * (3 * 2\<^sup>2 - 1)) Amic (2\<^sup>2 * (9 * 2 ^ (2 * 2 - 1) - 1))

goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
have f: "((2::nat)^2)*5*11 = 220"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2\<^sup>2 * 5 * 11 = 220
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2\<^sup>2 * 5 * 11 = 220

goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
have g: "((2::nat)^2)*71 = 284"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2\<^sup>2 * 71 = 284
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2\<^sup>2 * 71 = 284

goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
using  e f g
[PROOF STATE]
proof (prove)
using this:
(2\<^sup>2 * (3 * 2 ^ (2 - 1) - 1) * (3 * 2\<^sup>2 - 1)) Amic (2\<^sup>2 * (9 * 2 ^ (2 * 2 - 1) - 1))
2\<^sup>2 * 5 * 11 = 220
2\<^sup>2 * 71 = 284

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Amicable_Example_Fermat:
  shows  "17296 Amic 18416"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
have a: "(4::nat)>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < 4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < 4

goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
have b: "prime((3::nat)*(2^(4-1))-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (3 * 2 ^ (4 - 1) - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime (3 * 2 ^ (4 - 1) - 1)

goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
have c: "prime((3::nat)*(2^4)-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (3 * 2 ^ 4 - 1)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime (3 * 2 ^ 4 - 1)

goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
have d: "prime (1151::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 1151
[PROOF STEP]
by (pratt (code))
[PROOF STATE]
proof (state)
this:
prime 1151

goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
have e: "(1151::nat) = 9*(2^(2*4-1))-1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1151 = 9 * 2 ^ (2 * 4 - 1) - 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1151 = 9 * 2 ^ (2 * 4 - 1) - 1

goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
have f: "prime((9::nat)*(2^(2*4-1))-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (9 * 2 ^ (2 * 4 - 1) - 1)
[PROOF STEP]
using d e
[PROOF STATE]
proof (prove)
using this:
prime 1151
1151 = 9 * 2 ^ (2 * 4 - 1) - 1

goal (1 subgoal):
 1. prime (9 * 2 ^ (2 * 4 - 1) - 1)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
prime (9 * 2 ^ (2 * 4 - 1) - 1)

goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
have g: "((2^4)*(3*(2^(4-1))-1)*(3*(2^4)-1)) Amic((2^4)*(9*(2^(2*4-1))-1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 ^ 4 * (3 * 2 ^ (4 - 1) - 1) * (3 * 2 ^ 4 - 1)) Amic (2 ^ 4 * (9 * 2 ^ (2 * 4 - 1) - 1))
[PROOF STEP]
using  Thabit_ibn_Qurra_Rule_Amicable a b c f
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 < ?k; prime ?p; prime ?q; prime ?r; ?p = 2 ^ (?k - 1) * 3 - 1; ?q = 2 ^ ?k * 3 - 1; ?r = 2 ^ (2 * ?k - 1) * 9 - 1\<rbrakk> \<Longrightarrow> (2 ^ ?k * ?p * ?q) Amic (2 ^ ?k * ?r)
1 < 4
prime (3 * 2 ^ (4 - 1) - 1)
prime (3 * 2 ^ 4 - 1)
prime (9 * 2 ^ (2 * 4 - 1) - 1)

goal (1 subgoal):
 1. (2 ^ 4 * (3 * 2 ^ (4 - 1) - 1) * (3 * 2 ^ 4 - 1)) Amic (2 ^ 4 * (9 * 2 ^ (2 * 4 - 1) - 1))
[PROOF STEP]
by (metis mult.commute)
[PROOF STATE]
proof (state)
this:
(2 ^ 4 * (3 * 2 ^ (4 - 1) - 1) * (3 * 2 ^ 4 - 1)) Amic (2 ^ 4 * (9 * 2 ^ (2 * 4 - 1) - 1))

goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
have h: "((2::nat)^4)*23*47 = 17296"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ 4 * 23 * 47 = 17296
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ 4 * 23 * 47 = 17296

goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
have i: "(((2::nat)^4)*1151) = 18416"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ 4 * 1151 = 18416
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ 4 * 1151 = 18416

goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 17296 Amic 18416
[PROOF STEP]
using g h i
[PROOF STATE]
proof (prove)
using this:
(2 ^ 4 * (3 * 2 ^ (4 - 1) - 1) * (3 * 2 ^ 4 - 1)) Amic (2 ^ 4 * (9 * 2 ^ (2 * 4 - 1) - 1))
2 ^ 4 * 23 * 47 = 17296
2 ^ 4 * 1151 = 18416

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Amicable_Example_Descartes:
  shows "9363584 Amic 9437056"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have a: "(7::nat)>1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < 7
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 < 7

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have b: "prime (191::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 191
[PROOF STEP]
by (pratt (code))
[PROOF STATE]
proof (state)
this:
prime 191

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have c: "((3::nat)* (2^(7-1))-1) =191"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 * 2 ^ (7 - 1) - 1 = 191
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
3 * 2 ^ (7 - 1) - 1 = 191

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have d: "prime((3::nat)* (2^(7-1))-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (3 * 2 ^ (7 - 1) - 1)
[PROOF STEP]
using b c
[PROOF STATE]
proof (prove)
using this:
prime 191
3 * 2 ^ (7 - 1) - 1 = 191

goal (1 subgoal):
 1. prime (3 * 2 ^ (7 - 1) - 1)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
prime (3 * 2 ^ (7 - 1) - 1)

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have e: "prime (383::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 383
[PROOF STEP]
by (pratt (code))
[PROOF STATE]
proof (state)
this:
prime 383

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have f: "(3::nat)*(2^7)-1 = 383"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 3 * 2 ^ 7 - 1 = 383
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
3 * 2 ^ 7 - 1 = 383

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have g: "prime ((3::nat)*(2^7)-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (3 * 2 ^ 7 - 1)
[PROOF STEP]
using e f
[PROOF STATE]
proof (prove)
using this:
prime 383
3 * 2 ^ 7 - 1 = 383

goal (1 subgoal):
 1. prime (3 * 2 ^ 7 - 1)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
prime (3 * 2 ^ 7 - 1)

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have h: "prime (73727::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 73727
[PROOF STEP]
by (pratt (code))
[PROOF STATE]
proof (state)
this:
prime 73727

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have i: "(9::nat)*(2^(2*7-1))-1 = 73727"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 9 * 2 ^ (2 * 7 - 1) - 1 = 73727
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
9 * 2 ^ (2 * 7 - 1) - 1 = 73727

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have j: "prime ((9::nat)*(2^(2*7-1))-1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime (9 * 2 ^ (2 * 7 - 1) - 1)
[PROOF STEP]
using i h
[PROOF STATE]
proof (prove)
using this:
9 * 2 ^ (2 * 7 - 1) - 1 = 73727
prime 73727

goal (1 subgoal):
 1. prime (9 * 2 ^ (2 * 7 - 1) - 1)
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
prime (9 * 2 ^ (2 * 7 - 1) - 1)

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have k: "((2^7)*(3*(2^(7-1))-1)*(3*(2^7)-1))Amic((2^7)*(9*(2^(2*7-1))-1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (2 ^ 7 * (3 * 2 ^ (7 - 1) - 1) * (3 * 2 ^ 7 - 1)) Amic (2 ^ 7 * (9 * 2 ^ (2 * 7 - 1) - 1))
[PROOF STEP]
using  Thabit_ibn_Qurra_Rule_Amicable a d g j
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>1 < ?k; prime ?p; prime ?q; prime ?r; ?p = 2 ^ (?k - 1) * 3 - 1; ?q = 2 ^ ?k * 3 - 1; ?r = 2 ^ (2 * ?k - 1) * 9 - 1\<rbrakk> \<Longrightarrow> (2 ^ ?k * ?p * ?q) Amic (2 ^ ?k * ?r)
1 < 7
prime (3 * 2 ^ (7 - 1) - 1)
prime (3 * 2 ^ 7 - 1)
prime (9 * 2 ^ (2 * 7 - 1) - 1)

goal (1 subgoal):
 1. (2 ^ 7 * (3 * 2 ^ (7 - 1) - 1) * (3 * 2 ^ 7 - 1)) Amic (2 ^ 7 * (9 * 2 ^ (2 * 7 - 1) - 1))
[PROOF STEP]
by (metis mult.commute)
[PROOF STATE]
proof (state)
this:
(2 ^ 7 * (3 * 2 ^ (7 - 1) - 1) * (3 * 2 ^ 7 - 1)) Amic (2 ^ 7 * (9 * 2 ^ (2 * 7 - 1) - 1))

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have l: "((2::nat)^7)* 191* 383 = 9363584"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ 7 * 191 * 383 = 9363584
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ 7 * 191 * 383 = 9363584

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
have m: "(((2::nat)^7)* 73727) = 9437056"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 ^ 7 * 73727 = 9437056
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
2 ^ 7 * 73727 = 9437056

goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 9363584 Amic 9437056
[PROOF STEP]
using a k l
[PROOF STATE]
proof (prove)
using this:
1 < 7
(2 ^ 7 * (3 * 2 ^ (7 - 1) - 1) * (3 * 2 ^ 7 - 1)) Amic (2 ^ 7 * (9 * 2 ^ (2 * 7 - 1) - 1))
2 ^ 7 * 191 * 383 = 9363584

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

goal:
No subgoals!
[PROOF STEP]
qed