[STATEMENT]
lemma regularAmicPairExample: "regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have a: "220 Amic 284"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
using Amicable_Example_Pythagoras
[PROOF STATE]
proof (prove)
using this:
220 Amic 284

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

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have b: "gcd (220::nat) (284::nat) = 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd 220 284 = 4
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
gcd 220 284 = 4

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have c: "(220::nat) = 55*4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 220 = 55 * 4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
220 = 55 * 4

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have d: "(284::nat) = 71*4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 284 = 71 * 4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
284 = 71 * 4

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have e: "squarefree (55::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. squarefree 55
[PROOF STEP]
using squarefree_def
[PROOF STATE]
proof (prove)
using this:
squarefree ?n = (\<forall>x. x\<^sup>2 dvd ?n \<longrightarrow> x dvd (1::?'a))

goal (1 subgoal):
 1. squarefree 55
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
squarefree 55

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have f: "squarefree (71::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. squarefree 71
[PROOF STEP]
using squarefree_def
[PROOF STATE]
proof (prove)
using this:
squarefree ?n = (\<forall>x. x\<^sup>2 dvd ?n \<longrightarrow> x dvd (1::?'a))

goal (1 subgoal):
 1. squarefree 71
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
squarefree 71

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have g: "gcd (4::nat) (55::nat) =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd 4 55 = 1
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
gcd 4 55 = 1

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have h: "gcd (4::nat) (71::nat) =1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. gcd 4 71 = 1
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
gcd 4 71 = 1

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have A: "regularAmicPair 220 284"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regularAmicPair 220 284
[PROOF STEP]
by (simp add: a b e g f h gcd.commute regularAmicPair_def)
[PROOF STATE]
proof (state)
this:
regularAmicPair 220 284

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have B: "(card {i.\<exists> N. ( 220::nat) = N*(4::nat) \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4}) = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
obtain N::nat where N: "(220::nat) = N* 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. 220 = N * 4 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis  c)
[PROOF STATE]
proof (state)
this:
220 = N * 4

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have NN:"N=55"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N = 55
[PROOF STEP]
using N
[PROOF STATE]
proof (prove)
using this:
220 = N * 4

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

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K1: "prime(5::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 5
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 5

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K2: "prime(11::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. prime 11
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
prime 11

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have KK2: " \<not> prime (55::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> prime 55
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> prime 55

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have KK3: " \<not> prime (1::nat)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> prime 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> prime 1

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K: "set(divisors_nat 55 ) = {1, 5, 11, 55}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 55) = {1, 5, 11, 55}
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
set (divisors_nat 55) = {1, 5, 11, 55}

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have KK: "{i. i dvd (55::nat)} = {1, 5, 11, 55}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i dvd 55} = {1, 5, 11, 55}
[PROOF STEP]
using K divisors_nat  divisors_nat_def
[PROOF STATE]
proof (prove)
using this:
set (divisors_nat 55) = {1, 5, 11, 55}
?n \<noteq> 0 \<Longrightarrow> set (divisors_nat ?n) = {p. p dvd ?n}
distinct (divisors_nat ?n)
divisors_nat 0 = []
divisors_nat ?n \<equiv> if ?n = 0 then [] else remdups_adj (sort (map prod_list (subseqs (prime_factorization_nat ?n))))

goal (1 subgoal):
 1. {i. i dvd 55} = {1, 5, 11, 55}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i dvd 55} = {1, 5, 11, 55}

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K3 : "\<not> (5::nat) dvd 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 5 dvd 4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> 5 dvd 4

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K4 : "\<not> (11::nat) dvd 4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> 11 dvd 4
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<not> 11 dvd 4

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K55: "(1::nat) \<notin> {i. prime i \<and> i dvd 55}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<notin> {i. prime i \<and> i dvd 55}
[PROOF STEP]
using KK3
[PROOF STATE]
proof (prove)
using this:
\<not> prime 1

goal (1 subgoal):
 1. 1 \<notin> {i. prime i \<and> i dvd 55}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<notin> {i. prime i \<and> i dvd 55}

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K56: "(55::nat) \<notin> {i. prime i \<and> i dvd 55}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 55 \<notin> {i. prime i \<and> i dvd 55}
[PROOF STEP]
using KK2
[PROOF STATE]
proof (prove)
using this:
\<not> prime 55

goal (1 subgoal):
 1. 55 \<notin> {i. prime i \<and> i dvd 55}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
55 \<notin> {i. prime i \<and> i dvd 55}

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K57: "(5::nat) \<in> {i. prime i \<and> i dvd 55}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 5 \<in> {i. prime i \<and> i dvd 55}
[PROOF STEP]
using K1
[PROOF STATE]
proof (prove)
using this:
prime 5

goal (1 subgoal):
 1. 5 \<in> {i. prime i \<and> i dvd 55}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
5 \<in> {i. prime i \<and> i dvd 55}

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K58: "(11::nat) \<in> {i. prime i \<and> i dvd 55}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 11 \<in> {i. prime i \<and> i dvd 55}
[PROOF STEP]
using K2
[PROOF STATE]
proof (prove)
using this:
prime 11

goal (1 subgoal):
 1. 11 \<in> {i. prime i \<and> i dvd 55}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
11 \<in> {i. prime i \<and> i dvd 55}

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K5:  "{i.( prime i \<and> i dvd (55::nat) \<and> \<not> i dvd 4)} = {5, 11}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {5, 11}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {5, 11}
[PROOF STEP]
have K66: "{i.(prime i \<and> i dvd (55::nat) \<and> \<not> i dvd 4)}=
{i. prime i} \<inter> {i. i dvd 55} \<inter> { i. \<not> i dvd 4}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {i. prime i} \<inter> {i. i dvd 55} \<inter> {i. \<not> i dvd 4}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {i. prime i} \<inter> {i. i dvd 55} \<inter> {i. \<not> i dvd 4}

goal (1 subgoal):
 1. {i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {5, 11}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {5, 11}
[PROOF STEP]
using K66  K K1 K2 KK2 KK3  K3 K4 KK K55 K56 K57 K58 divisors_nat_def
          divisors_nat
[PROOF STATE]
proof (prove)
using this:
{i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {i. prime i} \<inter> {i. i dvd 55} \<inter> {i. \<not> i dvd 4}
set (divisors_nat 55) = {1, 5, 11, 55}
prime 5
prime 11
\<not> prime 55
\<not> prime 1
\<not> 5 dvd 4
\<not> 11 dvd 4
{i. i dvd 55} = {1, 5, 11, 55}
1 \<notin> {i. prime i \<and> i dvd 55}
55 \<notin> {i. prime i \<and> i dvd 55}
5 \<in> {i. prime i \<and> i dvd 55}
11 \<in> {i. prime i \<and> i dvd 55}
divisors_nat ?n \<equiv> if ?n = 0 then [] else remdups_adj (sort (map prod_list (subseqs (prime_factorization_nat ?n))))
?n \<noteq> 0 \<Longrightarrow> set (divisors_nat ?n) = {p. p dvd ?n}
distinct (divisors_nat ?n)
divisors_nat 0 = []

goal (1 subgoal):
 1. {i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {5, 11}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {5, 11}

goal:
No subgoals!
[PROOF STEP]
(*slow*)
[PROOF STATE]
proof (state)
this:
{i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {5, 11}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {5, 11}

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
have K6:  "card ({(5::nat), (11::nat)}) = 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {5, 11} = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {5, 11} = 2

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
using K5 K6
[PROOF STATE]
proof (prove)
using this:
{i. prime i \<and> i dvd 55 \<and> \<not> i dvd 4} = {5, 11}
card {5, 11} = 2

goal (1 subgoal):
 1. card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
have C: "(card {i. \<exists>N. (284::nat) = N*4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} ) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
obtain N::nat where N: "284 = N*4"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>N. 284 = N * 4 \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (metis d)
[PROOF STATE]
proof (state)
this:
284 = N * 4

goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
have NN: "N= 71"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. N = 71
[PROOF STEP]
using N
[PROOF STATE]
proof (prove)
using this:
284 = N * 4

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

goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
have K: "set(divisors_nat 71 ) = {1, 71 }"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (divisors_nat 71) = {1, 71}
[PROOF STEP]
by eval
[PROOF STATE]
proof (state)
this:
set (divisors_nat 71) = {1, 71}

goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
have KK: "{i. i dvd (71::nat)} = {1, 71}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. i dvd 71} = {1, 71}
[PROOF STEP]
using K divisors_nat  divisors_nat_def
[PROOF STATE]
proof (prove)
using this:
set (divisors_nat 71) = {1, 71}
?n \<noteq> 0 \<Longrightarrow> set (divisors_nat ?n) = {p. p dvd ?n}
distinct (divisors_nat ?n)
divisors_nat 0 = []
divisors_nat ?n \<equiv> if ?n = 0 then [] else remdups_adj (sort (map prod_list (subseqs (prime_factorization_nat ?n))))

goal (1 subgoal):
 1. {i. i dvd 71} = {1, 71}
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
{i. i dvd 71} = {1, 71}

goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
have K55:"(1::nat) \<notin> {i. prime i \<and> i dvd 71}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<notin> {i. prime i \<and> i dvd 71}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
1 \<notin> {i. prime i \<and> i dvd 71}

goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
have K58: "(71::nat) \<in> {i. prime i \<and> i dvd 71}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 71 \<in> {i. prime i \<and> i dvd 71}
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
71 \<in> {i. prime i \<and> i dvd 71}

goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
have K5: "{i. prime i \<and> i dvd 71 \<and> \<not> i dvd 4} = {(71::nat)}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. prime i \<and> i dvd 71 \<and> \<not> i dvd 4} = {71}
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. {i. prime i \<and> i dvd 71 \<and> \<not> i dvd 4} = {71}
[PROOF STEP]
have K66: "{i. prime i \<and> i dvd 71 \<and> \<not> i dvd 4}=
{i. prime i} \<inter> {i. i dvd 71} \<inter> { i. \<not> i dvd 4}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. prime i \<and> i dvd (71::'a) \<and> \<not> i dvd (4::'a)} = {i. prime i} \<inter> {i. i dvd (71::'a)} \<inter> {i. \<not> i dvd (4::'a)}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
{i. prime i \<and> i dvd (71::?'a1) \<and> \<not> i dvd (4::?'a1)} = {i. prime i} \<inter> {i. i dvd (71::?'a1)} \<inter> {i. \<not> i dvd (4::?'a1)}

goal (1 subgoal):
 1. {i. prime i \<and> i dvd 71 \<and> \<not> i dvd 4} = {71}
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. {i. prime i \<and> i dvd 71 \<and> \<not> i dvd 4} = {71}
[PROOF STEP]
using  K KK K55 K58
[PROOF STATE]
proof (prove)
using this:
set (divisors_nat 71) = {1, 71}
{i. i dvd 71} = {1, 71}
1 \<notin> {i. prime i \<and> i dvd 71}
71 \<in> {i. prime i \<and> i dvd 71}

goal (1 subgoal):
 1. {i. prime i \<and> i dvd 71 \<and> \<not> i dvd 4} = {71}
[PROOF STEP]
by (auto simp add: divisors_nat_def K66 divisors_nat)
[PROOF STATE]
proof (state)
this:
{i. prime i \<and> i dvd 71 \<and> \<not> i dvd 4} = {71}

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
{i. prime i \<and> i dvd 71 \<and> \<not> i dvd 4} = {71}

goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
have K6: "card ({(71::nat)}) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {71} = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {71} = 1

goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
using K5 K6
[PROOF STATE]
proof (prove)
using this:
{i. prime i \<and> i dvd 71 \<and> \<not> i dvd 4} = {71}
card {71} = 1

goal (1 subgoal):
 1. card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
using A B C
[PROOF STATE]
proof (prove)
using this:
regularAmicPair 220 284
card {i. \<exists>N. 220 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 2
card {i. \<exists>N. 284 = N * 4 \<and> prime i \<and> i dvd N \<and> \<not> i dvd 4} = 1

goal (1 subgoal):
 1. regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]
[PROOF STEP]
by (simp add: typeAmic_def b)
[PROOF STATE]
proof (state)
this:
regularAmicPair 220 284 \<and> typeAmic 220 284 = [2, 1]

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma abundant220ex: "abundant_number 220"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. abundant_number 220
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. abundant_number 220
[PROOF STEP]
have "220 Amic 284"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
using Amicable_Example_Pythagoras
[PROOF STATE]
proof (prove)
using this:
220 Amic 284

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

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

goal (1 subgoal):
 1. abundant_number 220
[PROOF STEP]
have "(220::nat) < 284"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 220 < 284
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
220 < 284

goal (1 subgoal):
 1. abundant_number 220
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
220 Amic 284
220 < 284
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
220 Amic 284
220 < 284

goal (1 subgoal):
 1. abundant_number 220
[PROOF STEP]
using Amicable_pair_abundant Amicable_pair_sym
[PROOF STATE]
proof (prove)
using this:
220 Amic 284
220 < 284
\<lbrakk>?n < ?m; ?m Amic ?n\<rbrakk> \<Longrightarrow> abundant_number ?n
?m Amic ?n \<Longrightarrow> ?n Amic ?m

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma deficient284ex: "deficient_number 284"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. deficient_number 284
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. deficient_number 284
[PROOF STEP]
have "220 Amic 284"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 220 Amic 284
[PROOF STEP]
using Amicable_Example_Pythagoras
[PROOF STATE]
proof (prove)
using this:
220 Amic 284

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

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

goal (1 subgoal):
 1. deficient_number 284
[PROOF STEP]
have "(220::nat) < 284"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 220 < 284
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
220 < 284

goal (1 subgoal):
 1. deficient_number 284
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
220 Amic 284
220 < 284
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
220 Amic 284
220 < 284

goal (1 subgoal):
 1. deficient_number 284
[PROOF STEP]
using Amicable_pair_deficient Amicable_pair_sym
[PROOF STATE]
proof (prove)
using this:
220 Amic 284
220 < 284
\<lbrakk>?n < ?m; ?m Amic ?n\<rbrakk> \<Longrightarrow> deficient_number ?m
?m Amic ?n \<Longrightarrow> ?n Amic ?m

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

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem teRiele_Rule_Amicable:
  fixes a u p r c q :: nat
  assumes "a \<ge> 1" and "u \<ge> 1"
      and "prime p" and "prime r" and "prime c" and "prime q" and "r \<noteq> c"
      and "\<not>(p dvd a)" and "(a*u) Amic (a*p)" and "gcd a (r*c)=1"
      and "q = r+c+u" and "gcd (a*u) q =1" and "r*c = p*(r +c+ u) + p+u"
  shows "(a*u*q) Amic (a*r*c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have "p+1 >0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < p + 1
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u

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

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have Z1: " r*c = p*q+p+u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. r * c = p * q + p + u
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u

goal (1 subgoal):
 1. r * c = p * q + p + u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
r * c = p * q + p + u

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have Z2: "(r+1)*(c+1) = (q+1)*(p+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r + 1) * (c + 1) = (q + 1) * (p + 1)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (r + 1) * (c + 1) = (q + 1) * (p + 1)
[PROOF STEP]
have y: "(q+1)*(p+1) = q*p + q+ p+1 "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (q + 1) * (p + 1) = q * p + q + p + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(q + 1) * (p + 1) = q * p + q + p + 1

goal (1 subgoal):
 1. (r + 1) * (c + 1) = (q + 1) * (p + 1)
[PROOF STEP]
have yy: "(r+1)*(c+1) = r*c + r+ c+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r + 1) * (c + 1) = r * c + r + c + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(r + 1) * (c + 1) = r * c + r + c + 1

goal (1 subgoal):
 1. (r + 1) * (c + 1) = (q + 1) * (p + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r + 1) * (c + 1) = (q + 1) * (p + 1)
[PROOF STEP]
using assms y Z1 yy
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
(q + 1) * (p + 1) = q * p + q + p + 1
r * c = p * q + p + u
(r + 1) * (c + 1) = r * c + r + c + 1

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

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

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have "Esigma(a) = (a*(u+p)/(p+1))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma a) = real (a * (u + p)) / real (p + 1)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. real (Esigma a) = real (a * (u + p)) / real (p + 1)
[PROOF STEP]
have d: "Esigma (a*p) = (Esigma a)*(Esigma p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * p) = Esigma a * Esigma p
[PROOF STEP]
using assms gcd_Esigma_mult \<open>prime p\<close> \<open>\<not> (p dvd a)\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n
prime p
\<not> p dvd a

goal (1 subgoal):
 1. Esigma (a * p) = Esigma a * Esigma p
[PROOF STEP]
by (metis gcd_unique_nat prime_nat_iff)
[PROOF STATE]
proof (state)
this:
Esigma (a * p) = Esigma a * Esigma p

goal (1 subgoal):
 1. real (Esigma a) = real (a * (u + p)) / real (p + 1)
[PROOF STEP]
have dd : "Esigma (a*p) =(Esigma a)*(p+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * p) = Esigma a * (p + 1)
[PROOF STEP]
using d assms  prime_sum_div
[PROOF STATE]
proof (prove)
using this:
Esigma (a * p) = Esigma a * Esigma p
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1

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

goal (1 subgoal):
 1. real (Esigma a) = real (a * (u + p)) / real (p + 1)
[PROOF STEP]
have ddd: "Esigma (a*p) = a*(u+p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * p) = a * (u + p)
[PROOF STEP]
using assms Amicable_pair_def
        Amicable_pair_equiv_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
?m Amic ?n \<equiv> ?m = aliquot_sum ?n \<and> ?n = aliquot_sum ?m
\<lbrakk>?m Amic ?n; 1 \<le> ?m; 1 \<le> ?n\<rbrakk> \<Longrightarrow> Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n

goal (1 subgoal):
 1. Esigma (a * p) = a * (u + p)
[PROOF STEP]
by (smt One_nat_def add_mult_distrib2 one_le_mult_iff prime_ge_1_nat)
[PROOF STATE]
proof (state)
this:
Esigma (a * p) = a * (u + p)

goal (1 subgoal):
 1. real (Esigma a) = real (a * (u + p)) / real (p + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma a) = real (a * (u + p)) / real (p + 1)
[PROOF STEP]
using d dd ddd Esigmanotzero assms(3) dvd_triv_right
        nonzero_mult_div_cancel_right prime_nat_iff prime_sum_div real_of_nat_div
[PROOF STATE]
proof (prove)
using this:
Esigma (a * p) = Esigma a * Esigma p
Esigma (a * p) = Esigma a * (p + 1)
Esigma (a * p) = a * (u + p)
1 \<le> ?n \<Longrightarrow> 1 \<le> Esigma ?n
prime p
?a dvd ?b * ?a
?b \<noteq> (0::?'a) \<Longrightarrow> ?a * ?b div ?b = ?a
prime ?n = (1 < ?n \<and> (\<forall>m. m dvd ?n \<longrightarrow> m = 1 \<or> m = ?n))
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1
?d dvd ?n \<Longrightarrow> real (?n div ?d) = real ?n / real ?d

goal (1 subgoal):
 1. real (Esigma a) = real (a * (u + p)) / real (p + 1)
[PROOF STEP]
by (metis \<open>0 < p + 1\<close> neq0_conv)
[PROOF STATE]
proof (state)
this:
real (Esigma a) = real (a * (u + p)) / real (p + 1)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
real (Esigma a) = real (a * (u + p)) / real (p + 1)

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have "Esigma(r) = (r+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma r = r + 1
[PROOF STEP]
using assms prime_sum_div
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1

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

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have "Esigma(c) = (c+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma c = c + 1
[PROOF STEP]
using assms prime_sum_div
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
prime ?n \<Longrightarrow> Esigma ?n = ?n + 1

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

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have "Esigma (a*r*c) = (Esigma a)*(Esigma r)*(Esigma c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * Esigma r * Esigma c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * Esigma r * Esigma c
[PROOF STEP]
have h: "Esigma (a*r*c) = (Esigma a)*(Esigma (r*c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * Esigma (r * c)
[PROOF STEP]
using assms gcd_Esigma_mult
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n

goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * Esigma (r * c)
[PROOF STEP]
by (metis mult.assoc mult.commute)
[PROOF STATE]
proof (state)
this:
Esigma (a * r * c) = Esigma a * Esigma (r * c)

goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * Esigma r * Esigma c
[PROOF STEP]
have hh: " Esigma (r*c) = (Esigma r)*(Esigma c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (r * c) = Esigma r * Esigma c
[PROOF STEP]
using assms prime_Esigma_mult
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
\<lbrakk>prime ?m; prime ?n; ?m \<noteq> ?n\<rbrakk> \<Longrightarrow> Esigma (?m * ?n) = Esigma ?n * Esigma ?m

goal (1 subgoal):
 1. Esigma (r * c) = Esigma r * Esigma c
[PROOF STEP]
by (metis semiring_normalization_rules(7))
[PROOF STATE]
proof (state)
this:
Esigma (r * c) = Esigma r * Esigma c

goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * Esigma r * Esigma c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * Esigma r * Esigma c
[PROOF STEP]
using h hh
[PROOF STATE]
proof (prove)
using this:
Esigma (a * r * c) = Esigma a * Esigma (r * c)
Esigma (r * c) = Esigma r * Esigma c

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

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

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have A: "Esigma (a*u*q) = Esigma (a*r*c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
have wk: "Esigma (a*u*q) = Esigma (a*u)*(q+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * u) * (q + 1)
[PROOF STEP]
using assms gcd_Esigma_mult
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n

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

goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
have wk1: "Esigma (a*u) = a*(u+p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u) = a * (u + p)
[PROOF STEP]
using assms Amicable_pair_equiv_def
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
\<lbrakk>?m Amic ?n; 1 \<le> ?m; 1 \<le> ?n\<rbrakk> \<Longrightarrow> Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n

goal (1 subgoal):
 1. Esigma (a * u) = a * (u + p)
[PROOF STEP]
by (smt One_nat_def add_mult_distrib2 one_le_mult_iff prime_ge_1_nat)
[PROOF STATE]
proof (state)
this:
Esigma (a * u) = a * (u + p)

goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
have w3: "Esigma (a*u*q) = a*(u+p)*(q+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = a * (u + p) * (q + 1)
[PROOF STEP]
using wk wk1
[PROOF STATE]
proof (prove)
using this:
Esigma (a * u * q) = Esigma (a * u) * (q + 1)
Esigma (a * u) = a * (u + p)

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

goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
have w4: "Esigma (a*r*c) =(Esigma a)*(r+1) * (c+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * (r + 1) * (c + 1)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u

goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * (r + 1) * (c + 1)
[PROOF STEP]
by (simp add: \<open>Esigma (a*r*c) = Esigma a * Esigma r * Esigma c\<close> \<open>Esigma c = c + 1\<close>
           \<open>Esigma r = r+1\<close>)
[PROOF STATE]
proof (state)
this:
Esigma (a * r * c) = Esigma a * (r + 1) * (c + 1)

goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
have we: "a*(u+p)*(q+1) = (Esigma a)*(r+1)*(c+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (u + p) * (q + 1) = Esigma a * (r + 1) * (c + 1)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. a * (u + p) * (q + 1) = Esigma a * (r + 1) * (c + 1)
[PROOF STEP]
have we1: "(Esigma a)*(r+1)*(c+1) = (a*(u+p)/(p+1))*(r+1)*(c+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma a * (r + 1) * (c + 1)) = real (a * (u + p)) / real (p + 1) * real (r + 1) * real (c + 1)
[PROOF STEP]
by (metis \<open>real (Esigma a) = real (a*(u+p))/real(p+1)\<close> of_nat_mult)
[PROOF STATE]
proof (state)
this:
real (Esigma a * (r + 1) * (c + 1)) = real (a * (u + p)) / real (p + 1) * real (r + 1) * real (c + 1)

goal (1 subgoal):
 1. a * (u + p) * (q + 1) = Esigma a * (r + 1) * (c + 1)
[PROOF STEP]
have we12: " (Esigma a)*(r+1)*(c+1) = (a*(u+p)/(p+1))*(q+1)*(p+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (Esigma a * (r + 1) * (c + 1)) = real (a * (u + p)) / real (p + 1) * real (q + 1) * real (p + 1)
[PROOF STEP]
using we1 Z2
[PROOF STATE]
proof (prove)
using this:
real (Esigma a * (r + 1) * (c + 1)) = real (a * (u + p)) / real (p + 1) * real (r + 1) * real (c + 1)
(r + 1) * (c + 1) = (q + 1) * (p + 1)

goal (1 subgoal):
 1. real (Esigma a * (r + 1) * (c + 1)) = real (a * (u + p)) / real (p + 1) * real (q + 1) * real (p + 1)
[PROOF STEP]
by (metis of_nat_mult semiring_normalization_rules(18))
[PROOF STATE]
proof (state)
this:
real (Esigma a * (r + 1) * (c + 1)) = real (a * (u + p)) / real (p + 1) * real (q + 1) * real (p + 1)

goal (1 subgoal):
 1. a * (u + p) * (q + 1) = Esigma a * (r + 1) * (c + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (u + p) * (q + 1) = Esigma a * (r + 1) * (c + 1)
[PROOF STEP]
using we12 assms
[PROOF STATE]
proof (prove)
using this:
real (Esigma a * (r + 1) * (c + 1)) = real (a * (u + p)) / real (p + 1) * real (q + 1) * real (p + 1)
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u

goal (1 subgoal):
 1. a * (u + p) * (q + 1) = Esigma a * (r + 1) * (c + 1)
[PROOF STEP]
by (smt  nonzero_mult_div_cancel_right of_nat_1  of_nat_add of_nat_eq_iff of_nat_le_iff
            of_nat_mult prime_ge_1_nat times_divide_eq_left)
[PROOF STATE]
proof (state)
this:
a * (u + p) * (q + 1) = Esigma a * (r + 1) * (c + 1)

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

goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
using we w3 w4
[PROOF STATE]
proof (prove)
using this:
a * (u + p) * (q + 1) = Esigma a * (r + 1) * (c + 1)
Esigma (a * u * q) = a * (u + p) * (q + 1)
Esigma (a * r * c) = Esigma a * (r + 1) * (c + 1)

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

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

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have B : "Esigma (a*r*c) = (a*u*q)+(a*r*c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
have a1: "(u+p)*(q+1) = (u*q+p*q+p+u)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u + p) * (q + 1) = u * q + p * q + p + u
[PROOF STEP]
using assms add_mult_distrib
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
(?m + ?n) * ?k = ?m * ?k + ?n * ?k

goal (1 subgoal):
 1. (u + p) * (q + 1) = u * q + p * q + p + u
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(u + p) * (q + 1) = u * q + p * q + p + u

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
have a2: "(u+p)*(q+1)*(p+1) = (u*q+p*q+p+u)*(p+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u + p) * (q + 1) * (p + 1) = (u * q + p * q + p + u) * (p + 1)
[PROOF STEP]
using a1 assms
[PROOF STATE]
proof (prove)
using this:
(u + p) * (q + 1) = u * q + p * q + p + u
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u

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

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
have a3: "(u+p)*(r+1)*(c+1) = (u*q+p*q+p+u)*(p+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (u + p) * (r + 1) * (c + 1) = (u * q + p * q + p + u) * (p + 1)
[PROOF STEP]
using assms a2 Z2
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
(u + p) * (q + 1) * (p + 1) = (u * q + p * q + p + u) * (p + 1)
(r + 1) * (c + 1) = (q + 1) * (p + 1)

goal (1 subgoal):
 1. (u + p) * (r + 1) * (c + 1) = (u * q + p * q + p + u) * (p + 1)
[PROOF STEP]
by (metis semiring_normalization_rules(18))
[PROOF STATE]
proof (state)
this:
(u + p) * (r + 1) * (c + 1) = (u * q + p * q + p + u) * (p + 1)

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
have a4: "a*(u+p)* (r+1)*(c+1) = a*(u*q+ p*q+p+u)*(p+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (u + p) * (r + 1) * (c + 1) = a * (u * q + p * q + p + u) * (p + 1)
[PROOF STEP]
using assms a3
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
(u + p) * (r + 1) * (c + 1) = (u * q + p * q + p + u) * (p + 1)

goal (1 subgoal):
 1. a * (u + p) * (r + 1) * (c + 1) = a * (u * q + p * q + p + u) * (p + 1)
[PROOF STEP]
by (metis semiring_normalization_rules(18))
[PROOF STATE]
proof (state)
this:
a * (u + p) * (r + 1) * (c + 1) = a * (u * q + p * q + p + u) * (p + 1)

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
have a5: "a*(u+p)*(r+1)*(c+1) = a*(u*q+r*c)*(p+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a * (u + p) * (r + 1) * (c + 1) = a * (u * q + r * c) * (p + 1)
[PROOF STEP]
using assms a4 Z1
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
a * (u + p) * (r + 1) * (c + 1) = a * (u * q + p * q + p + u) * (p + 1)
r * c = p * q + p + u

goal (1 subgoal):
 1. a * (u + p) * (r + 1) * (c + 1) = a * (u * q + r * c) * (p + 1)
[PROOF STEP]
by (simp add: semiring_normalization_rules(21))
[PROOF STATE]
proof (state)
this:
a * (u + p) * (r + 1) * (c + 1) = a * (u * q + r * c) * (p + 1)

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
have a6: "(a*(u+p)*(r+1)*(c+1))/(p+1) =(a*(u*q+ r*c)* (p+1))/(p+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (a * (u + p) * (r + 1) * (c + 1)) / real (p + 1) = real (a * (u * q + r * c) * (p + 1)) / real (p + 1)
[PROOF STEP]
using assms a5
        semiring_normalization_rules(21) \<open>p+1 >0\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
a * (u + p) * (r + 1) * (c + 1) = a * (u * q + r * c) * (p + 1)
?a + ?b + ?c = ?a + (?b + ?c)
0 < p + 1

goal (1 subgoal):
 1. real (a * (u + p) * (r + 1) * (c + 1)) / real (p + 1) = real (a * (u * q + r * c) * (p + 1)) / real (p + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
real (a * (u + p) * (r + 1) * (c + 1)) / real (p + 1) = real (a * (u * q + r * c) * (p + 1)) / real (p + 1)

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
have a7: "(a*(u+p)*(r+1)*(c+1))/(p+1) =(a*(u*q+ r*c))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (a * (u + p) * (r + 1) * (c + 1)) / real (p + 1) = real (a * (u * q + r * c))
[PROOF STEP]
using assms a6 \<open>p+1 >0\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
real (a * (u + p) * (r + 1) * (c + 1)) / real (p + 1) = real (a * (u * q + r * c) * (p + 1)) / real (p + 1)
0 < p + 1

goal (1 subgoal):
 1. real (a * (u + p) * (r + 1) * (c + 1)) / real (p + 1) = real (a * (u * q + r * c))
[PROOF STEP]
by (metis neq0_conv nonzero_mult_div_cancel_right of_nat_eq_0_iff of_nat_mult)
[PROOF STATE]
proof (state)
this:
real (a * (u + p) * (r + 1) * (c + 1)) / real (p + 1) = real (a * (u * q + r * c))

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
have a8:"(a*(u+p)/(p+1))*(r+1)*(c+1) = a*(u*q+r*c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. real (a * (u + p)) / real (p + 1) * real (r + 1) * real (c + 1) = real (a * (u * q + r * c))
[PROOF STEP]
using assms a7  \<open>p+1 >0\<close>
[PROOF STATE]
proof (prove)
using this:
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
real (a * (u + p) * (r + 1) * (c + 1)) / real (p + 1) = real (a * (u * q + r * c))
0 < p + 1

goal (1 subgoal):
 1. real (a * (u + p)) / real (p + 1) * real (r + 1) * real (c + 1) = real (a * (u * q + r * c))
[PROOF STEP]
by (metis of_nat_mult times_divide_eq_left)
[PROOF STATE]
proof (state)
this:
real (a * (u + p)) / real (p + 1) * real (r + 1) * real (c + 1) = real (a * (u * q + r * c))

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
have a9: "(Esigma a)* Esigma(r)* Esigma(c) = a*(u*q+ r*c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma a * Esigma r * Esigma c = a * (u * q + r * c)
[PROOF STEP]
using a8 assms
        \<open> Esigma(r) = (r+1)\<close> \<open> Esigma(c) = (c+1)\<close>
[PROOF STATE]
proof (prove)
using this:
real (a * (u + p)) / real (p + 1) * real (r + 1) * real (c + 1) = real (a * (u * q + r * c))
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
Esigma r = r + 1
Esigma c = c + 1

goal (1 subgoal):
 1. Esigma a * Esigma r * Esigma c = a * (u * q + r * c)
[PROOF STEP]
by (metis \<open>real (Esigma a) = real (a*(u + p))/real(p + 1)\<close> of_nat_eq_iff of_nat_mult)
[PROOF STATE]
proof (state)
this:
Esigma a * Esigma r * Esigma c = a * (u * q + r * c)

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
have a10: " Esigma(a*r*c) = a*(u*q+ r*c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * r * c) = a * (u * q + r * c)
[PROOF STEP]
using a9 assms
        \<open>Esigma (a*r*c) = (Esigma a)*(Esigma r)*(Esigma c)\<close>
[PROOF STATE]
proof (prove)
using this:
Esigma a * Esigma r * Esigma c = a * (u * q + r * c)
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
Esigma (a * r * c) = Esigma a * Esigma r * Esigma c

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

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
using a10 assms
[PROOF STATE]
proof (prove)
using this:
Esigma (a * r * c) = a * (u * q + r * c)
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u

goal (1 subgoal):
 1. Esigma (a * r * c) = a * u * q + a * r * c
[PROOF STEP]
by (simp add: add_mult_distrib2 mult.assoc)
[PROOF STATE]
proof (state)
this:
Esigma (a * r * c) = a * u * q + a * r * c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (a * r * c) = a * u * q + a * r * c

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
using A B  Amicable_pair_equiv_def_conv assms One_nat_def  one_le_mult_iff
[PROOF STATE]
proof (prove)
using this:
Esigma (a * u * q) = Esigma (a * r * c)
Esigma (a * r * c) = a * u * q + a * r * c
\<lbrakk>1 \<le> ?m; 1 \<le> ?n; Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n\<rbrakk> \<Longrightarrow> ?m Amic ?n
1 \<le> a
1 \<le> u
prime p
prime r
prime c
prime q
r \<noteq> c
\<not> p dvd a
(a * u) Amic (a * p)
gcd a (r * c) = 1
q = r + c + u
gcd (a * u) q = 1
r * c = p * (r + c + u) + p + u
1 = Suc 0
(Suc 0 \<le> ?m * ?n) = (Suc 0 \<le> ?m \<and> Suc 0 \<le> ?n)

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
by (smt prime_ge_1_nat)
[PROOF STATE]
proof (state)
this:
(a * u * q) Amic (a * r * c)

goal:
No subgoals!
[PROOF STEP]
qed


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

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

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have a1: "Esigma(a*r*c) = (Esigma a)*Esigma(r*c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * Esigma (r * c)
[PROOF STEP]
using assms gcd_Esigma_mult
[PROOF STATE]
proof (prove)
using this:
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u
gcd ?m ?n = 1 \<Longrightarrow> Esigma (?m * ?n) = Esigma ?m * Esigma ?n

goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * Esigma (r * c)
[PROOF STEP]
by (metis mult.assoc mult.commute)
[PROOF STATE]
proof (state)
this:
Esigma (a * r * c) = Esigma a * Esigma (r * c)

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have a2: "Esigma(a*r*c) = (Esigma a)*(r+1)*(c+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * (r + 1) * (c + 1)
[PROOF STEP]
using a1 assms
[PROOF STATE]
proof (prove)
using this:
Esigma (a * r * c) = Esigma a * Esigma (r * c)
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u

goal (1 subgoal):
 1. Esigma (a * r * c) = Esigma a * (r + 1) * (c + 1)
[PROOF STEP]
by (metis mult.commute mult.left_commute prime_Esigma_mult prime_sum_div)
[PROOF STATE]
proof (state)
this:
Esigma (a * r * c) = Esigma a * (r + 1) * (c + 1)

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have A: "Esigma (a*u*q) = Esigma(a*r*c)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
have d: "Esigma(a)*(r+1)*(c+1) = Esigma(a*u)*(q+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma a * (r + 1) * (c + 1) = Esigma (a * u) * (q + 1)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma a * (r + 1) * (c + 1) = Esigma (a * u) * (q + 1)
[PROOF STEP]
have d1: "(r+1)*(c+1) =(x+1)*(q+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r + 1) * (c + 1) = (x + 1) * (q + 1)
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (r + 1) * (c + 1) = (x + 1) * (q + 1)
[PROOF STEP]
have ce: "(r+1)*(c+1) = r*c+r+c+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r + 1) * (c + 1) = r * c + r + c + 1
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(r + 1) * (c + 1) = r * c + r + c + 1

goal (1 subgoal):
 1. (r + 1) * (c + 1) = (x + 1) * (q + 1)
[PROOF STEP]
have ce1: "(r+1)*(c+1) = x+u+x*u+r*x+x*c+r+c+1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r + 1) * (c + 1) = x + u + x * u + r * x + x * c + r + c + 1
[PROOF STEP]
using ce assms
[PROOF STATE]
proof (prove)
using this:
(r + 1) * (c + 1) = r * c + r + c + 1
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u

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

goal (1 subgoal):
 1. (r + 1) * (c + 1) = (x + 1) * (q + 1)
[PROOF STEP]
have de: "(x+1)*(q+1) = x*q +1+x+q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + 1) * (q + 1) = x * q + 1 + x + q
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x + 1) * (q + 1) = x * q + 1 + x + q

goal (1 subgoal):
 1. (r + 1) * (c + 1) = (x + 1) * (q + 1)
[PROOF STEP]
have de1: "(x+1)*(q+1) = x*(r+c+u)+1+x+ r+c+u"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (x + 1) * (q + 1) = x * (r + c + u) + 1 + x + r + c + u
[PROOF STEP]
using assms de
[PROOF STATE]
proof (prove)
using this:
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u
(x + 1) * (q + 1) = x * q + 1 + x + q

goal (1 subgoal):
 1. (x + 1) * (q + 1) = x * (r + c + u) + 1 + x + r + c + u
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(x + 1) * (q + 1) = x * (r + c + u) + 1 + x + r + c + u

goal (1 subgoal):
 1. (r + 1) * (c + 1) = (x + 1) * (q + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (r + 1) * (c + 1) = (x + 1) * (q + 1)
[PROOF STEP]
using de1 ce1 add_mult_distrib2
[PROOF STATE]
proof (prove)
using this:
(x + 1) * (q + 1) = x * (r + c + u) + 1 + x + r + c + u
(r + 1) * (c + 1) = x + u + x * u + r * x + x * c + r + c + 1
?k * (?m + ?n) = ?k * ?m + ?k * ?n

goal (1 subgoal):
 1. (r + 1) * (c + 1) = (x + 1) * (q + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(r + 1) * (c + 1) = (x + 1) * (q + 1)

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

goal (1 subgoal):
 1. Esigma a * (r + 1) * (c + 1) = Esigma (a * u) * (q + 1)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma a * (r + 1) * (c + 1) = Esigma (a * u) * (q + 1)
[PROOF STEP]
using d1 assms
[PROOF STATE]
proof (prove)
using this:
(r + 1) * (c + 1) = (x + 1) * (q + 1)
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u

goal (1 subgoal):
 1. Esigma a * (r + 1) * (c + 1) = Esigma (a * u) * (q + 1)
[PROOF STEP]
by (metis semiring_normalization_rules(18))
[PROOF STATE]
proof (state)
this:
Esigma a * (r + 1) * (c + 1) = Esigma (a * u) * (q + 1)

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

goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
using d a2
[PROOF STATE]
proof (prove)
using this:
Esigma a * (r + 1) * (c + 1) = Esigma (a * u) * (q + 1)
Esigma (a * r * c) = Esigma a * (r + 1) * (c + 1)

goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * r * c)
[PROOF STEP]
by (simp add: a assms(6) prime_sum_div)
[PROOF STATE]
proof (state)
this:
Esigma (a * u * q) = Esigma (a * r * c)

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

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
have B: "Esigma (a*u*q) = a*u*q + a*r*c"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = a * u * q + a * r * c
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. Esigma (a * u * q) = a * u * q + a * r * c
[PROOF STEP]
have i: "Esigma (a*u*q) = Esigma(a*u)*(q+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = Esigma (a * u) * (q + 1)
[PROOF STEP]
using a assms
[PROOF STATE]
proof (prove)
using this:
Esigma (a * u * q) = Esigma (a * u) * Esigma q
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u

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

goal (1 subgoal):
 1. Esigma (a * u * q) = a * u * q + a * r * c
[PROOF STEP]
have ii:"Esigma (a*u*q) = (a*u+ a*x)*(q+1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = (a * u + a * x) * (q + 1)
[PROOF STEP]
using assms i
[PROOF STATE]
proof (prove)
using this:
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u
Esigma (a * u * q) = Esigma (a * u) * (q + 1)

goal (1 subgoal):
 1. Esigma (a * u * q) = (a * u + a * x) * (q + 1)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
Esigma (a * u * q) = (a * u + a * x) * (q + 1)

goal (1 subgoal):
 1. Esigma (a * u * q) = a * u * q + a * r * c
[PROOF STEP]
have iii:"Esigma (a*u*q) = a*u*q +a*u+ a*x*q+ a*x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = a * u * q + a * u + a * x * q + a * x
[PROOF STEP]
using assms ii add_mult_distrib
[PROOF STATE]
proof (prove)
using this:
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u
Esigma (a * u * q) = (a * u + a * x) * (q + 1)
(?m + ?n) * ?k = ?m * ?k + ?n * ?k

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

goal (1 subgoal):
 1. Esigma (a * u * q) = a * u * q + a * r * c
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. Esigma (a * u * q) = a * u * q + a * r * c
[PROOF STEP]
using iii assms
[PROOF STATE]
proof (prove)
using this:
Esigma (a * u * q) = a * u * q + a * u + a * x * q + a * x
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u

goal (1 subgoal):
 1. Esigma (a * u * q) = a * u * q + a * r * c
[PROOF STEP]
by (smt distrib_left semiring_normalization_rules)
[PROOF STATE]
proof (state)
this:
Esigma (a * u * q) = a * u * q + a * r * c

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
Esigma (a * u * q) = a * u * q + a * r * c

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
using A B assms Amicable_pair_equiv_def_conv assms  One_nat_def one_le_mult_iff
[PROOF STATE]
proof (prove)
using this:
Esigma (a * u * q) = Esigma (a * r * c)
Esigma (a * u * q) = a * u * q + a * r * c
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u
\<lbrakk>1 \<le> ?m; 1 \<le> ?n; Esigma ?m = Esigma ?n \<and> Esigma ?m = ?m + ?n\<rbrakk> \<Longrightarrow> ?m Amic ?n
1 \<le> x
1 \<le> a
1 \<le> u
prime r
prime c
prime q
r \<noteq> c
Esigma (a * u) = a * u + a * x
Esigma (a * u) = Esigma a * (x + 1)
gcd a (r * c) = 1
gcd (a * u) q = 1
r * c = x + u + x * u + r * x + x * c
q = r + c + u
1 = Suc 0
(Suc 0 \<le> ?m * ?n) = (Suc 0 \<le> ?m \<and> Suc 0 \<le> ?n)

goal (1 subgoal):
 1. (a * u * q) Amic (a * r * c)
[PROOF STEP]
by (smt prime_ge_1_nat)
[PROOF STATE]
proof (state)
this:
(a * u * q) Amic (a * r * c)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma integral_nonneg:
  "a \<le> b \<Longrightarrow> integrable f a b \<Longrightarrow> (\<And>x. x \<in> {a..b} \<Longrightarrow> f x \<ge> 0) \<Longrightarrow> integral f a b \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> b; integrable f a b; \<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x\<rbrakk> \<Longrightarrow> 0 \<le> integral f a b
[PROOF STEP]
using integral_le[OF integrable_const[of 0], of f a b]
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>0 \<le> 0; integrable f a b; \<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x\<rbrakk> \<Longrightarrow> integral (\<lambda>_. 0) a b \<le> integral f a b

goal (1 subgoal):
 1. \<lbrakk>a \<le> b; integrable f a b; \<And>x. x \<in> {a..b} \<Longrightarrow> 0 \<le> f x\<rbrakk> \<Longrightarrow> 0 \<le> integral f a b
[PROOF STEP]
by (simp add: integral_const)


[STATEMENT]
lemma strict_mono_imp_ex1_real:
  fixes f :: "real \<Rightarrow> real"
  assumes lim_neg_inf: "LIM x at_bot. f x :> at_top"
  assumes lim_inf: "(f \<longlongrightarrow> z) at_top"
  assumes mono: "\<And>a b. a < b \<Longrightarrow> f b < f a"
  assumes cont: "\<And>x. isCont f x"
  assumes y_greater_z: "z < y"
  shows   "\<exists>!x. f x = y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!x. f x = y
[PROOF STEP]
proof (rule ex_ex1I)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x. f x = y
 2. \<And>x ya. \<lbrakk>f x = y; f ya = y\<rbrakk> \<Longrightarrow> x = ya
[PROOF STEP]
fix a b
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<exists>x. f x = y
 2. \<And>x ya. \<lbrakk>f x = y; f ya = y\<rbrakk> \<Longrightarrow> x = ya
[PROOF STEP]
assume "f a = y" "f b = y"
[PROOF STATE]
proof (state)
this:
f a = y
f b = y

goal (2 subgoals):
 1. \<exists>x. f x = y
 2. \<And>x ya. \<lbrakk>f x = y; f ya = y\<rbrakk> \<Longrightarrow> x = ya
[PROOF STEP]
thus "a = b"
[PROOF STATE]
proof (prove)
using this:
f a = y
f b = y

goal (1 subgoal):
 1. a = b
[PROOF STEP]
by (cases rule: linorder_cases[of a b]) (auto dest: mono)
[PROOF STATE]
proof (state)
this:
a = b

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
from lim_neg_inf
[PROOF STATE]
proof (chain)
picking this:
filterlim f at_top at_bot
[PROOF STEP]
have "eventually (\<lambda>x. y \<le> f x) at_bot"
[PROOF STATE]
proof (prove)
using this:
filterlim f at_top at_bot

goal (1 subgoal):
 1. \<forall>\<^sub>F x in at_bot. y \<le> f x
[PROOF STEP]
by (subst (asm) filterlim_at_top) simp
[PROOF STATE]
proof (state)
this:
\<forall>\<^sub>F x in at_bot. y \<le> f x

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in at_bot. y \<le> f x
[PROOF STEP]
obtain l where l: "\<And>x. x \<le> l \<Longrightarrow> y \<le> f x"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at_bot. y \<le> f x

goal (1 subgoal):
 1. (\<And>l. (\<And>x. x \<le> l \<Longrightarrow> y \<le> f x) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (subst (asm) eventually_at_bot_linorder) auto
[PROOF STATE]
proof (state)
this:
?x \<le> l \<Longrightarrow> y \<le> f ?x

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
from order_tendstoD(2)[OF lim_inf y_greater_z]
[PROOF STATE]
proof (chain)
picking this:
\<forall>\<^sub>F x in at_top. f x < y
[PROOF STEP]
obtain u where u: "\<And>x. x \<ge> u \<Longrightarrow> f x < y"
[PROOF STATE]
proof (prove)
using this:
\<forall>\<^sub>F x in at_top. f x < y

goal (1 subgoal):
 1. (\<And>u. (\<And>x. u \<le> x \<Longrightarrow> f x < y) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (subst (asm) eventually_at_top_linorder) auto
[PROOF STATE]
proof (state)
this:
u \<le> ?x \<Longrightarrow> f ?x < y

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
define a where "a = min l u"
[PROOF STATE]
proof (state)
this:
a = min l u

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
define b where "b = max l u"
[PROOF STATE]
proof (state)
this:
b = max l u

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
have a: "f a \<ge> y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> f a
[PROOF STEP]
unfolding a_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y \<le> f (min l u)
[PROOF STEP]
by (intro l) simp
[PROOF STATE]
proof (state)
this:
y \<le> f a

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
y \<le> f a

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
have b: "f b < y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f b < y
[PROOF STEP]
unfolding b_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. f (max l u) < y
[PROOF STEP]
by (intro u) simp
[PROOF STATE]
proof (state)
this:
f b < y

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
f b < y

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
have a_le_b: "a \<le> b"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. a \<le> b
[PROOF STEP]
by (simp add: a_def b_def)
[PROOF STATE]
proof (state)
this:
a \<le> b

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
y \<le> f a
f b < y
a \<le> b
[PROOF STEP]
have "\<exists>x\<ge>a. x \<le> b \<and> f x = y"
[PROOF STATE]
proof (prove)
using this:
y \<le> f a
f b < y
a \<le> b

goal (1 subgoal):
 1. \<exists>x\<ge>a. x \<le> b \<and> f x = y
[PROOF STEP]
using cont
[PROOF STATE]
proof (prove)
using this:
y \<le> f a
f b < y
a \<le> b
isCont f ?x

goal (1 subgoal):
 1. \<exists>x\<ge>a. x \<le> b \<and> f x = y
[PROOF STEP]
by (intro IVT2) auto
[PROOF STATE]
proof (state)
this:
\<exists>x\<ge>a. x \<le> b \<and> f x = y

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
thus "\<exists>x. f x = y"
[PROOF STATE]
proof (prove)
using this:
\<exists>x\<ge>a. x \<le> b \<and> f x = y

goal (1 subgoal):
 1. \<exists>x. f x = y
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>x. f x = y

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma p_def: "p = (THE p. (\<Sum>i<k. as!i * bs!i powr p) = 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. p = (THE p. (\<Sum>i<k. as ! i * bs ! i powr p) = 1)
[PROOF STEP]
by (simp add: akra_bazzi_exponent_def length_as)


[STATEMENT]
lemma b_pos: "b \<in> set bs \<Longrightarrow> b > 0" and b_less_1: "b \<in> set bs \<Longrightarrow> b < 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (b \<in> set bs \<Longrightarrow> 0 < b) &&& (b \<in> set bs \<Longrightarrow> b < 1)
[PROOF STEP]
using b_bounds
[PROOF STATE]
proof (prove)
using this:
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}

goal (1 subgoal):
 1. (b \<in> set bs \<Longrightarrow> 0 < b) &&& (b \<in> set bs \<Longrightarrow> b < 1)
[PROOF STEP]
by simp_all


[STATEMENT]
lemma as_nonempty [simp]: "as \<noteq> []" and bs_nonempty [simp]: "bs \<noteq> []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as \<noteq> [] &&& bs \<noteq> []
[PROOF STEP]
using length_as length_bs k_not_0
[PROOF STATE]
proof (prove)
using this:
length as = k
length bs = k
k \<noteq> 0

goal (1 subgoal):
 1. as \<noteq> [] &&& bs \<noteq> []
[PROOF STEP]
by auto


[STATEMENT]
lemma a_in_as[intro, simp]: "i < k \<Longrightarrow> as ! i \<in> set as"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < k \<Longrightarrow> as ! i \<in> set as
[PROOF STEP]
by (rule nth_mem) (simp add: length_as)


[STATEMENT]
lemma b_in_bs[intro, simp]: "i < k \<Longrightarrow> bs ! i \<in> set bs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < k \<Longrightarrow> bs ! i \<in> set bs
[PROOF STEP]
by (rule nth_mem) (simp add: length_bs)


[STATEMENT]
lemma akra_bazzi_p_strict_mono:
  assumes "x < y"
  shows "(\<Sum>i<k. as!i * bs!i powr y) < (\<Sum>i<k. as!i * bs!i powr x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr y) < (\<Sum>i<k. as ! i * bs ! i powr x)
[PROOF STEP]
proof (intro sum_strict_mono_ex1 ballI)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. finite {..<k}
 2. \<And>xa. xa \<in> {..<k} \<Longrightarrow> as ! xa * bs ! xa powr y \<le> as ! xa * bs ! xa powr x
 3. \<exists>a\<in>{..<k}. as ! a * bs ! a powr y < as ! a * bs ! a powr x
[PROOF STEP]
from ex_a_pos
[PROOF STATE]
proof (chain)
picking this:
\<exists>a\<in>set as. 0 < a
[PROOF STEP]
obtain a where "a \<in> set as" "a > 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>set as. 0 < a

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> set as; 0 < a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> set as
0 < a

goal (3 subgoals):
 1. finite {..<k}
 2. \<And>xa. xa \<in> {..<k} \<Longrightarrow> as ! xa * bs ! xa powr y \<le> as ! xa * bs ! xa powr x
 3. \<exists>a\<in>{..<k}. as ! a * bs ! a powr y < as ! a * bs ! a powr x
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set as
0 < a
[PROOF STEP]
obtain i where "i < k" "as!i > 0"
[PROOF STATE]
proof (prove)
using this:
a \<in> set as
0 < a

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < k; 0 < as ! i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp: in_set_conv_nth length_as)
[PROOF STATE]
proof (state)
this:
i < k
0 < as ! i

goal (3 subgoals):
 1. finite {..<k}
 2. \<And>xa. xa \<in> {..<k} \<Longrightarrow> as ! xa * bs ! xa powr y \<le> as ! xa * bs ! xa powr x
 3. \<exists>a\<in>{..<k}. as ! a * bs ! a powr y < as ! a * bs ! a powr x
[PROOF STEP]
with b_bounds \<open>x < y\<close>
[PROOF STATE]
proof (chain)
picking this:
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}
x < y
i < k
0 < as ! i
[PROOF STEP]
have "as!i * bs!i powr y < as!i * bs!i powr x"
[PROOF STATE]
proof (prove)
using this:
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}
x < y
i < k
0 < as ! i

goal (1 subgoal):
 1. as ! i * bs ! i powr y < as ! i * bs ! i powr x
[PROOF STEP]
by (intro mult_strict_left_mono powr_less_mono') auto
[PROOF STATE]
proof (state)
this:
as ! i * bs ! i powr y < as ! i * bs ! i powr x

goal (3 subgoals):
 1. finite {..<k}
 2. \<And>xa. xa \<in> {..<k} \<Longrightarrow> as ! xa * bs ! xa powr y \<le> as ! xa * bs ! xa powr x
 3. \<exists>a\<in>{..<k}. as ! a * bs ! a powr y < as ! a * bs ! a powr x
[PROOF STEP]
with \<open>i < k\<close>
[PROOF STATE]
proof (chain)
picking this:
i < k
as ! i * bs ! i powr y < as ! i * bs ! i powr x
[PROOF STEP]
show "\<exists>i\<in>{..<k}. as!i * bs!i powr y < as!i * bs!i powr x"
[PROOF STATE]
proof (prove)
using this:
i < k
as ! i * bs ! i powr y < as ! i * bs ! i powr x

goal (1 subgoal):
 1. \<exists>i\<in>{..<k}. as ! i * bs ! i powr y < as ! i * bs ! i powr x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>i\<in>{..<k}. as ! i * bs ! i powr y < as ! i * bs ! i powr x

goal (2 subgoals):
 1. finite {..<k}
 2. \<And>xa. xa \<in> {..<k} \<Longrightarrow> as ! xa * bs ! xa powr y \<le> as ! xa * bs ! xa powr x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite {..<k}
 2. \<And>xa. xa \<in> {..<k} \<Longrightarrow> as ! xa * bs ! xa powr y \<le> as ! xa * bs ! xa powr x
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. finite {..<k}
 2. \<And>xa. xa \<in> {..<k} \<Longrightarrow> as ! xa * bs ! xa powr y \<le> as ! xa * bs ! xa powr x
[PROOF STEP]
assume "i \<in> {..<k}"
[PROOF STATE]
proof (state)
this:
i \<in> {..<k}

goal (2 subgoals):
 1. finite {..<k}
 2. \<And>xa. xa \<in> {..<k} \<Longrightarrow> as ! xa * bs ! xa powr y \<le> as ! xa * bs ! xa powr x
[PROOF STEP]
with a_ge_0 b_bounds[of "bs!i"] \<open>x < y\<close>
[PROOF STATE]
proof (chain)
picking this:
?a \<in> set as \<Longrightarrow> 0 \<le> ?a
bs ! i \<in> set bs \<Longrightarrow> bs ! i \<in> {0<..<1}
x < y
i \<in> {..<k}
[PROOF STEP]
show "as!i * bs!i powr y \<le> as!i * bs!i powr x"
[PROOF STATE]
proof (prove)
using this:
?a \<in> set as \<Longrightarrow> 0 \<le> ?a
bs ! i \<in> set bs \<Longrightarrow> bs ! i \<in> {0<..<1}
x < y
i \<in> {..<k}

goal (1 subgoal):
 1. as ! i * bs ! i powr y \<le> as ! i * bs ! i powr x
[PROOF STEP]
by (intro mult_left_mono powr_mono') simp_all
[PROOF STATE]
proof (state)
this:
as ! i * bs ! i powr y \<le> as ! i * bs ! i powr x

goal (1 subgoal):
 1. finite {..<k}
[PROOF STEP]
qed simp_all


[STATEMENT]
lemma akra_bazzi_p_mono:
  assumes "x \<le> y"
  shows "(\<Sum>i<k. as!i * bs!i powr y) \<le> (\<Sum>i<k. as!i * bs!i powr x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr y) \<le> (\<Sum>i<k. as ! i * bs ! i powr x)
[PROOF STEP]
apply (cases "x < y")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. x < y \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr y) \<le> (\<Sum>i<k. as ! i * bs ! i powr x)
 2. \<not> x < y \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr y) \<le> (\<Sum>i<k. as ! i * bs ! i powr x)
[PROOF STEP]
using akra_bazzi_p_strict_mono[of x y] assms
[PROOF STATE]
proof (prove)
using this:
x < y \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr y) < (\<Sum>i<k. as ! i * bs ! i powr x)
x \<le> y

goal (2 subgoals):
 1. x < y \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr y) \<le> (\<Sum>i<k. as ! i * bs ! i powr x)
 2. \<not> x < y \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr y) \<le> (\<Sum>i<k. as ! i * bs ! i powr x)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma akra_bazzi_p_unique:
  "\<exists>!p. (\<Sum>i<k. as!i * bs!i powr p) = 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>!p. (\<Sum>i<k. as ! i * bs ! i powr p) = 1
[PROOF STEP]
proof (rule strict_mono_imp_ex1_real)
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top
 2. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> ?z) at_top
 3. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 4. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 5. ?z < 1
[PROOF STEP]
from as_nonempty
[PROOF STATE]
proof (chain)
picking this:
as \<noteq> []
[PROOF STEP]
have [simp]: "k > 0"
[PROOF STATE]
proof (prove)
using this:
as \<noteq> []

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

goal (5 subgoals):
 1. LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top
 2. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> ?z) at_top
 3. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 4. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 5. ?z < 1
[PROOF STEP]
have [simp]: "\<And>i. i < k \<Longrightarrow> as!i \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> 0 \<le> as ! i
[PROOF STEP]
by (rule a_ge_0) simp
[PROOF STATE]
proof (state)
this:
?i < k \<Longrightarrow> 0 \<le> as ! ?i

goal (5 subgoals):
 1. LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top
 2. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> ?z) at_top
 3. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 4. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 5. ?z < 1
[PROOF STEP]
from ex_a_pos
[PROOF STATE]
proof (chain)
picking this:
\<exists>a\<in>set as. 0 < a
[PROOF STEP]
obtain a where "a \<in> set as" "a > 0"
[PROOF STATE]
proof (prove)
using this:
\<exists>a\<in>set as. 0 < a

goal (1 subgoal):
 1. (\<And>a. \<lbrakk>a \<in> set as; 0 < a\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
a \<in> set as
0 < a

goal (5 subgoals):
 1. LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top
 2. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> ?z) at_top
 3. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 4. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 5. ?z < 1
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a \<in> set as
0 < a
[PROOF STEP]
obtain i where i: "i < k" "as!i > 0"
[PROOF STATE]
proof (prove)
using this:
a \<in> set as
0 < a

goal (1 subgoal):
 1. (\<And>i. \<lbrakk>i < k; 0 < as ! i\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (force simp: in_set_conv_nth length_as)
[PROOF STATE]
proof (state)
this:
i < k
0 < as ! i

goal (5 subgoals):
 1. LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top
 2. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> ?z) at_top
 3. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 4. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 5. ?z < 1
[PROOF STEP]
hence "LIM p at_bot. as!i * bs!i powr p :> at_top"
[PROOF STATE]
proof (prove)
using this:
i < k
0 < as ! i

goal (1 subgoal):
 1. LIM p at_bot. as ! i * bs ! i powr p :> at_top
[PROOF STEP]
using b_bounds i
[PROOF STATE]
proof (prove)
using this:
i < k
0 < as ! i
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}
i < k
0 < as ! i

goal (1 subgoal):
 1. LIM p at_bot. as ! i * bs ! i powr p :> at_top
[PROOF STEP]
by (intro filterlim_tendsto_pos_mult_at_top[OF tendsto_const] real_powr_at_bot_neg) simp_all
[PROOF STATE]
proof (state)
this:
LIM p at_bot. as ! i * bs ! i powr p :> at_top

goal (5 subgoals):
 1. LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top
 2. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> ?z) at_top
 3. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 4. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 5. ?z < 1
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
LIM p at_bot. as ! i * bs ! i powr p :> at_top

goal (5 subgoals):
 1. LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top
 2. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> ?z) at_top
 3. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 4. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 5. ?z < 1
[PROOF STEP]
have "\<forall>p. as!i*bs!i powr p \<le> (\<Sum>i\<in>{..<k}. as ! i * bs ! i powr p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
fix p :: real
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
from a_ge_0 b_bounds
[PROOF STATE]
proof (chain)
picking this:
?a \<in> set as \<Longrightarrow> 0 \<le> ?a
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}
[PROOF STEP]
have "(\<Sum>i\<in>{..<k}-{i}. as ! i * bs ! i powr p) \<ge> 0"
[PROOF STATE]
proof (prove)
using this:
?a \<in> set as \<Longrightarrow> 0 \<le> ?a
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}

goal (1 subgoal):
 1. 0 \<le> (\<Sum>i\<in>{..<k} - {i}. as ! i * bs ! i powr p)
[PROOF STEP]
by (intro sum_nonneg mult_nonneg_nonneg) simp_all
[PROOF STATE]
proof (state)
this:
0 \<le> (\<Sum>i\<in>{..<k} - {i}. as ! i * bs ! i powr p)

goal (1 subgoal):
 1. \<And>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
0 \<le> (\<Sum>i\<in>{..<k} - {i}. as ! i * bs ! i powr p)

goal (1 subgoal):
 1. \<And>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
have "as!i * bs!i powr p + ... = (\<Sum>i\<in>insert i {..<k}. as ! i * bs ! i powr p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. as ! i * bs ! i powr p + (\<Sum>i\<in>{..<k} - {i}. as ! i * bs ! i powr p) = (\<Sum>i\<in>insert i {..<k}. as ! i * bs ! i powr p)
[PROOF STEP]
by (simp add: sum.insert_remove)
[PROOF STATE]
proof (state)
this:
as ! i * bs ! i powr p + (\<Sum>i\<in>{..<k} - {i}. as ! i * bs ! i powr p) = (\<Sum>i\<in>insert i {..<k}. as ! i * bs ! i powr p)

goal (1 subgoal):
 1. \<And>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
as ! i * bs ! i powr p + (\<Sum>i\<in>{..<k} - {i}. as ! i * bs ! i powr p) = (\<Sum>i\<in>insert i {..<k}. as ! i * bs ! i powr p)

goal (1 subgoal):
 1. \<And>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
from i
[PROOF STATE]
proof (chain)
picking this:
i < k
0 < as ! i
[PROOF STEP]
have "insert i {..<k} = {..<k}"
[PROOF STATE]
proof (prove)
using this:
i < k
0 < as ! i

goal (1 subgoal):
 1. insert i {..<k} = {..<k}
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
insert i {..<k} = {..<k}

goal (1 subgoal):
 1. \<And>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<And>x y. x \<le> y \<Longrightarrow> as ! i * bs ! i powr p + x \<le> as ! i * bs ! i powr p + y) \<Longrightarrow> as ! i * bs ! i powr p + 0 \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
show "as!i*bs!i powr p \<le> (\<Sum>i\<in>{..<k}. as ! i * bs ! i powr p)"
[PROOF STATE]
proof (prove)
using this:
(\<And>x y. x \<le> y \<Longrightarrow> as ! i * bs ! i powr p + x \<le> as ! i * bs ! i powr p + y) \<Longrightarrow> as ! i * bs ! i powr p + 0 \<le> (\<Sum>i<k. as ! i * bs ! i powr p)

goal (1 subgoal):
 1. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<forall>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)

goal (5 subgoals):
 1. LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top
 2. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> ?z) at_top
 3. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 4. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 5. ?z < 1
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
LIM p at_bot. as ! i * bs ! i powr p :> at_top
\<forall>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)
[PROOF STEP]
show "LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top"
[PROOF STATE]
proof (prove)
using this:
LIM p at_bot. as ! i * bs ! i powr p :> at_top
\<forall>p. as ! i * bs ! i powr p \<le> (\<Sum>i<k. as ! i * bs ! i powr p)

goal (1 subgoal):
 1. LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top
[PROOF STEP]
by (rule filterlim_at_top_mono[OF _ always_eventually])
[PROOF STATE]
proof (state)
this:
LIM p at_bot. \<Sum>i<k. as ! i * bs ! i powr p :> at_top

goal (4 subgoals):
 1. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> ?z) at_top
 2. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 3. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 4. ?z < 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> ?z) at_top
 2. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 3. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 4. ?z < 1
[PROOF STEP]
from b_bounds
[PROOF STATE]
proof (chain)
picking this:
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}
[PROOF STEP]
show "((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> (\<Sum>i<k. 0)) at_top"
[PROOF STATE]
proof (prove)
using this:
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}

goal (1 subgoal):
 1. ((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> (\<Sum>i<k. 0)) at_top
[PROOF STEP]
by (intro tendsto_sum tendsto_mult_right_zero real_powr_at_top_neg) simp_all
[PROOF STATE]
proof (state)
this:
((\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) \<longlongrightarrow> (\<Sum>i<k. 0)) at_top

goal (3 subgoals):
 1. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 2. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 3. (\<Sum>i<k. 0) < 1
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 2. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 3. (\<Sum>i<k. 0) < 1
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 2. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 3. (\<Sum>i<k. 0) < 1
[PROOF STEP]
from b_bounds
[PROOF STATE]
proof (chain)
picking this:
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}
[PROOF STEP]
have A: "\<And>i. i < k \<Longrightarrow> bs ! i > 0"
[PROOF STATE]
proof (prove)
using this:
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}

goal (1 subgoal):
 1. \<And>i. i < k \<Longrightarrow> 0 < bs ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
?i < k \<Longrightarrow> 0 < bs ! ?i

goal (3 subgoals):
 1. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 2. \<And>p. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) p
 3. (\<Sum>i<k. 0) < 1
[PROOF STEP]
show "isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) x
[PROOF STEP]
using b_bounds[OF nth_mem]
[PROOF STATE]
proof (prove)
using this:
?n1 < length bs \<Longrightarrow> bs ! ?n1 \<in> {0<..<1}

goal (1 subgoal):
 1. isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) x
[PROOF STEP]
by (intro continuous_intros) (auto dest: A)
[PROOF STATE]
proof (state)
this:
isCont (\<lambda>x. \<Sum>i<k. as ! i * bs ! i powr x) x

goal (2 subgoals):
 1. \<And>a b. a < b \<Longrightarrow> (\<Sum>i<k. as ! i * bs ! i powr b) < (\<Sum>i<k. as ! i * bs ! i powr a)
 2. (\<Sum>i<k. 0) < 1
[PROOF STEP]
qed (simp_all add: akra_bazzi_p_strict_mono)


[STATEMENT]
lemma p_props:  "(\<Sum>i<k. as!i * bs!i powr p) = 1"
  and p_unique: "(\<Sum>i<k. as!i * bs!i powr p') = 1 \<Longrightarrow> p = p'"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr p) = 1 &&& ((\<Sum>i<k. as ! i * bs ! i powr p') = 1 \<Longrightarrow> p = p')
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. (\<Sum>i<k. as ! i * bs ! i powr p) = 1
 2. (\<Sum>i<k. as ! i * bs ! i powr p') = 1 \<Longrightarrow> p = p'
[PROOF STEP]
from theI'[OF akra_bazzi_p_unique] the1_equality[OF akra_bazzi_p_unique]
[PROOF STATE]
proof (chain)
picking this:
(\<Sum>i<k. as ! i * bs ! i powr (THE x. (\<Sum>i<k. as ! i * bs ! i powr x) = 1)) = 1
(\<Sum>i<k. as ! i * bs ! i powr ?a) = 1 \<Longrightarrow> (THE x. (\<Sum>i<k. as ! i * bs ! i powr x) = 1) = ?a
[PROOF STEP]
show "(\<Sum>i<k. as!i * bs!i powr p) = 1" "(\<Sum>i<k. as!i * bs!i powr p') = 1 \<Longrightarrow> p = p'"
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<k. as ! i * bs ! i powr (THE x. (\<Sum>i<k. as ! i * bs ! i powr x) = 1)) = 1
(\<Sum>i<k. as ! i * bs ! i powr ?a) = 1 \<Longrightarrow> (THE x. (\<Sum>i<k. as ! i * bs ! i powr x) = 1) = ?a

goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr p) = 1 &&& ((\<Sum>i<k. as ! i * bs ! i powr p') = 1 \<Longrightarrow> p = p')
[PROOF STEP]
unfolding p_def
[PROOF STATE]
proof (prove)
using this:
(\<Sum>i<k. as ! i * bs ! i powr (THE x. (\<Sum>i<k. as ! i * bs ! i powr x) = 1)) = 1
(\<Sum>i<k. as ! i * bs ! i powr ?a) = 1 \<Longrightarrow> (THE x. (\<Sum>i<k. as ! i * bs ! i powr x) = 1) = ?a

goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr (THE p. (\<Sum>i<k. as ! i * bs ! i powr p) = 1)) = 1 &&& ((\<Sum>i<k. as ! i * bs ! i powr p') = 1 \<Longrightarrow> (THE p. (\<Sum>i<k. as ! i * bs ! i powr p) = 1) = p')
[PROOF STEP]
by - blast+
[PROOF STATE]
proof (state)
this:
(\<Sum>i<k. as ! i * bs ! i powr p) = 1
(\<Sum>i<k. as ! i * bs ! i powr p') = 1 \<Longrightarrow> p = p'

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma p_greaterI: "1 < (\<Sum>i<k. as!i * bs!i powr p') \<Longrightarrow> p' < p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < (\<Sum>i<k. as ! i * bs ! i powr p') \<Longrightarrow> p' < p
[PROOF STEP]
by (rule disjE[OF le_less_linear, of p p'], drule akra_bazzi_p_mono, subst (asm) p_props, simp_all)


[STATEMENT]
lemma p_lessI: "1 > (\<Sum>i<k. as!i * bs!i powr p') \<Longrightarrow> p' > p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr p') < 1 \<Longrightarrow> p < p'
[PROOF STEP]
by (rule disjE[OF le_less_linear, of p' p], drule akra_bazzi_p_mono, subst (asm) p_props, simp_all)


[STATEMENT]
lemma p_geI: "1 \<le> (\<Sum>i<k. as!i * bs!i powr p') \<Longrightarrow> p' \<le> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr p') \<Longrightarrow> p' \<le> p
[PROOF STEP]
by (rule disjE[OF le_less_linear, of p' p], simp, drule akra_bazzi_p_strict_mono,
      subst (asm) p_props, simp_all)


[STATEMENT]
lemma p_leI: "1 \<ge> (\<Sum>i<k. as!i * bs!i powr p') \<Longrightarrow> p' \<ge> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr p') \<le> 1 \<Longrightarrow> p \<le> p'
[PROOF STEP]
by (rule disjE[OF le_less_linear, of p p'], simp, drule akra_bazzi_p_strict_mono,
      subst (asm) p_props, simp_all)


[STATEMENT]
lemma p_boundsI: "(\<Sum>i<k. as!i * bs!i powr x) \<le> 1 \<and> (\<Sum>i<k. as!i * bs!i powr y) \<ge> 1 \<Longrightarrow> p \<in> {y..x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr x) \<le> 1 \<and> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr y) \<Longrightarrow> p \<in> {y..x}
[PROOF STEP]
by (elim conjE, drule p_leI, drule p_geI, simp)


[STATEMENT]
lemma p_boundsI': "(\<Sum>i<k. as!i * bs!i powr x) < 1 \<and> (\<Sum>i<k. as!i * bs!i powr y) > 1 \<Longrightarrow> p \<in> {y<..<x}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<Sum>i<k. as ! i * bs ! i powr x) < 1 \<and> 1 < (\<Sum>i<k. as ! i * bs ! i powr y) \<Longrightarrow> p \<in> {y<..<x}
[PROOF STEP]
by (elim conjE, drule p_lessI, drule p_greaterI, simp)


[STATEMENT]
lemma p_nonneg: "sum_list as \<ge> 1 \<Longrightarrow> p \<ge> 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 0 \<le> p
[PROOF STEP]
proof (rule p_geI)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
assume "sum_list as \<ge> 1"
[PROOF STATE]
proof (state)
this:
1 \<le> sum_list as

goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 \<le> sum_list as

goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
have "... = (\<Sum>i<k. as!i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. sum_list as = sum ((!) as) {..<k}
[PROOF STEP]
by (simp add: sum_list_sum_nth length_as atLeast0LessThan)
[PROOF STATE]
proof (state)
this:
sum_list as = sum ((!) as) {..<k}

goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
sum_list as = sum ((!) as) {..<k}

goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
sum_list as = sum ((!) as) {..<k}

goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
fix i
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
assume "i < k"
[PROOF STATE]
proof (state)
this:
i < k

goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
with b_bounds
[PROOF STATE]
proof (chain)
picking this:
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}
i < k
[PROOF STEP]
have "bs!i > 0"
[PROOF STATE]
proof (prove)
using this:
?b \<in> set bs \<Longrightarrow> ?b \<in> {0<..<1}
i < k

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

goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
hence "as!i * bs!i powr 0 = as!i"
[PROOF STATE]
proof (prove)
using this:
0 < bs ! i

goal (1 subgoal):
 1. as ! i * bs ! i powr 0 = as ! i
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
as ! i * bs ! i powr 0 = as ! i

goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
?i2 < k \<Longrightarrow> as ! ?i2 * bs ! ?i2 powr 0 = as ! ?i2

goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
hence "(\<Sum>i<k. as!i) = (\<Sum>i<k. as!i * bs!i powr 0)"
[PROOF STATE]
proof (prove)
using this:
?i2 < k \<Longrightarrow> as ! ?i2 * bs ! ?i2 powr 0 = as ! ?i2

goal (1 subgoal):
 1. sum ((!) as) {..<k} = (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
by (intro sum.cong) simp_all
[PROOF STATE]
proof (state)
this:
sum ((!) as) {..<k} = (\<Sum>i<k. as ! i * bs ! i powr 0)

goal (1 subgoal):
 1. 1 \<le> sum_list as \<Longrightarrow> 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
show "1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)"
[PROOF STATE]
proof (prove)
using this:
1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)

goal (1 subgoal):
 1. 1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
1 \<le> (\<Sum>i<k. as ! i * bs ! i powr 0)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma h_in_hs[intro, simp]: "i < k \<Longrightarrow> hs ! i \<in> set hs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < k \<Longrightarrow> hs ! i \<in> set hs
[PROOF STEP]
by (rule nth_mem) (simp add: length_hs)


[STATEMENT]
lemma x1_gt_1: "x\<^sub>1 > 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 < x\<^sub>1
[PROOF STEP]
proof-
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. 1 < x\<^sub>1
[PROOF STEP]
from bs_nonempty
[PROOF STATE]
proof (chain)
picking this:
bs \<noteq> []
[PROOF STEP]
obtain b where "b \<in> set bs"
[PROOF STATE]
proof (prove)
using this:
bs \<noteq> []

goal (1 subgoal):
 1. (\<And>b. b \<in> set bs \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases bs) auto
[PROOF STATE]
proof (state)
this:
b \<in> set bs

goal (1 subgoal):
 1. 1 < x\<^sub>1
[PROOF STEP]
from b_pos[OF this] b_less_1[OF this] x0_ge_1
[PROOF STATE]
proof (chain)
picking this:
0 < b
b < 1
1 \<le> x\<^sub>0
[PROOF STEP]
have "1 < 2 * x\<^sub>0 * inverse b"
[PROOF STATE]
proof (prove)
using this:
0 < b
b < 1
1 \<le> x\<^sub>0

goal (1 subgoal):
 1. 1 < 2 * x\<^sub>0 * inverse b
[PROOF STEP]
by (simp add: field_simps)
[PROOF STATE]
proof (state)
this:
1 < 2 * x\<^sub>0 * inverse b

goal (1 subgoal):
 1. 1 < x\<^sub>1
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
1 < 2 * x\<^sub>0 * inverse b

goal (1 subgoal):
 1. 1 < x\<^sub>1
[PROOF STEP]
from x1_ge and \<open>b \<in> set bs\<close>
[PROOF STATE]
proof (chain)
picking this:
?b \<in> set bs \<Longrightarrow> 2 * x\<^sub>0 * inverse ?b \<le> x\<^sub>1
b \<in> set bs
[PROOF STEP]
have "... \<le> x\<^sub>1"
[PROOF STATE]
proof (prove)
using this:
?b \<in> set bs \<Longrightarrow> 2 * x\<^sub>0 * inverse ?b \<le> x\<^sub>1
b \<in> set bs

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

goal (1 subgoal):
 1. 1 < x\<^sub>1
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
1 < x\<^sub>1
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
1 < x\<^sub>1

goal (1 subgoal):
 1. 1 < x\<^sub>1
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
1 < x\<^sub>1

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma x1_ge_1: "x\<^sub>1 \<ge> 1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 1 \<le> x\<^sub>1
[PROOF STEP]
using x1_gt_1
[PROOF STATE]
proof (prove)
using this:
1 < x\<^sub>1

goal (1 subgoal):
 1. 1 \<le> x\<^sub>1
[PROOF STEP]
by simp


[STATEMENT]
lemma x1_pos: "x\<^sub>1 > 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 0 < x\<^sub>1
[PROOF STEP]
using x1_ge_1
[PROOF STATE]
proof (prove)
using this:
1 \<le> x\<^sub>1

goal (1 subgoal):
 1. 0 < x\<^sub>1
[PROOF STEP]
by simp