Metamath Proof Explorer

Theorem prmreclem6

Description: Lemma for prmrec . If the series F was convergent, there would be some k such that the sum starting from k + 1 sums to less than 1 / 2 ; this is a sufficient hypothesis for prmreclem5 to produce the contradictory bound N / 2 < ( 2 ^ k ) sqrt N , which is false for N = 2 ^ ( 2 k + 2 ) . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypothesis prmrec.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
Assertion prmreclem6 ¬ seq 1 ( + , 𝐹 ) ∈ dom ⇝

Proof

Step Hyp Ref Expression
1 prmrec.1 ⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
2 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
3 1zzd ⊢ ( ⊤ → 1 ∈ ℤ )
4 nnrecre ⊢ ( 𝑛 ∈ ℕ → ( 1 / 𝑛 ) ∈ ℝ )
5 4 adantl ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → ( 1 / 𝑛 ) ∈ ℝ )
6 0re ⊢ 0 ∈ ℝ
7 ifcl ⊢ ( ( ( 1 / 𝑛 ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) ∈ ℝ )
8 5 6 7 sylancl ⊢ ( ( ⊤ ∧ 𝑛 ∈ ℕ ) → if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) ∈ ℝ )
9 8 1 fmptd ⊢ ( ⊤ → 𝐹 : ℕ ⟶ ℝ )
10 9 ffvelcdmda ⊢ ( ( ⊤ ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
11 2 3 10 serfre ⊢ ( ⊤ → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ )
12 11 mptru ⊢ seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ
13 frn ⊢ ( seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ → ran seq 1 ( + , 𝐹 ) ⊆ ℝ )
14 12 13 mp1i ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ran seq 1 ( + , 𝐹 ) ⊆ ℝ )
15 1nn ⊢ 1 ∈ ℕ
16 12 fdmi ⊢ dom seq 1 ( + , 𝐹 ) = ℕ
17 15 16 eleqtrri ⊢ 1 ∈ dom seq 1 ( + , 𝐹 )
18 ne0i ⊢ ( 1 ∈ dom seq 1 ( + , 𝐹 ) → dom seq 1 ( + , 𝐹 ) ≠ ∅ )
19 dm0rn0 ⊢ ( dom seq 1 ( + , 𝐹 ) = ∅ ↔ ran seq 1 ( + , 𝐹 ) = ∅ )
20 19 necon3bii ⊢ ( dom seq 1 ( + , 𝐹 ) ≠ ∅ ↔ ran seq 1 ( + , 𝐹 ) ≠ ∅ )
21 18 20 sylib ⊢ ( 1 ∈ dom seq 1 ( + , 𝐹 ) → ran seq 1 ( + , 𝐹 ) ≠ ∅ )
22 17 21 mp1i ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ran seq 1 ( + , 𝐹 ) ≠ ∅ )
23 1zzd ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → 1 ∈ ℤ )
24 climdm ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
25 24 biimpi ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
26 12 a1i ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ )
27 26 ffvelcdmda ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ∈ ℝ )
28 2 23 25 27 climrecl ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ∈ ℝ )
29 simpr ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
30 25 adantr ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → seq 1 ( + , 𝐹 ) ⇝ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
31 eleq1w ⊢ ( 𝑛 = 𝑗 → ( 𝑛 ∈ ℙ ↔ 𝑗 ∈ ℙ ) )
32 oveq2 ⊢ ( 𝑛 = 𝑗 → ( 1 / 𝑛 ) = ( 1 / 𝑗 ) )
33 31 32 ifbieq1d ⊢ ( 𝑛 = 𝑗 → if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) = if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) )
34 prmnn ⊢ ( 𝑗 ∈ ℙ → 𝑗 ∈ ℕ )
35 34 adantl ⊢ ( ( ⊤ ∧ 𝑗 ∈ ℙ ) → 𝑗 ∈ ℕ )
36 35 nnrecred ⊢ ( ( ⊤ ∧ 𝑗 ∈ ℙ ) → ( 1 / 𝑗 ) ∈ ℝ )
37 6 a1i ⊢ ( ( ⊤ ∧ ¬ 𝑗 ∈ ℙ ) → 0 ∈ ℝ )
38 36 37 ifclda ⊢ ( ⊤ → if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℝ )
39 38 mptru ⊢ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℝ
40 39 elexi ⊢ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ V
41 33 1 40 fvmpt ⊢ ( 𝑗 ∈ ℕ → ( 𝐹 ‘ 𝑗 ) = if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) )
42 41 adantl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) )
43 39 a1i ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℝ )
44 42 43 eqeltrd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
45 44 adantlr ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
46 nnrp ⊢ ( 𝑗 ∈ ℕ → 𝑗 ∈ ℝ+ )
47 46 adantl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → 𝑗 ∈ ℝ+ )
48 47 rpreccld ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → ( 1 / 𝑗 ) ∈ ℝ+ )
49 48 rpge0d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( 1 / 𝑗 ) )
50 0le0 ⊢ 0 ≤ 0
51 breq2 ⊢ ( ( 1 / 𝑗 ) = if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) → ( 0 ≤ ( 1 / 𝑗 ) ↔ 0 ≤ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ) )
52 breq2 ⊢ ( 0 = if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) → ( 0 ≤ 0 ↔ 0 ≤ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ) )
53 51 52 ifboth ⊢ ( ( 0 ≤ ( 1 / 𝑗 ) ∧ 0 ≤ 0 ) → 0 ≤ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) )
54 49 50 53 sylancl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → 0 ≤ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) )
55 54 42 breqtrrd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑗 ) )
56 55 adantlr ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → 0 ≤ ( 𝐹 ‘ 𝑗 ) )
57 2 29 30 45 56 climserle ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
58 57 ralrimiva ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) )
59 brralrspcev ⊢ ( ( ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ∈ ℝ ∧ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ ( ⇝ ‘ seq 1 ( + , 𝐹 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 )
60 28 58 59 syl2anc ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 )
61 ffn ⊢ ( seq 1 ( + , 𝐹 ) : ℕ ⟶ ℝ → seq 1 ( + , 𝐹 ) Fn ℕ )
62 breq1 ⊢ ( 𝑧 = ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) → ( 𝑧 ≤ 𝑥 ↔ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
63 62 ralrn ⊢ ( seq 1 ( + , 𝐹 ) Fn ℕ → ( ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 ) )
64 12 61 63 mp2b ⊢ ( ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 )
65 64 rexbii ⊢ ( ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ↔ ∃ 𝑥 ∈ ℝ ∀ 𝑘 ∈ ℕ ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ≤ 𝑥 )
66 60 65 sylibr ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 )
67 14 22 66 suprcld ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) ∈ ℝ )
68 2rp ⊢ 2 ∈ ℝ+
69 rpreccl ⊢ ( 2 ∈ ℝ+ → ( 1 / 2 ) ∈ ℝ+ )
70 68 69 ax-mp ⊢ ( 1 / 2 ) ∈ ℝ+
71 ltsubrp ⊢ ( ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ+ ) → ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) )
72 67 70 71 sylancl ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) )
73 halfre ⊢ ( 1 / 2 ) ∈ ℝ
74 resubcl ⊢ ( ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) ∈ ℝ ∧ ( 1 / 2 ) ∈ ℝ ) → ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) ∈ ℝ )
75 67 73 74 sylancl ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) ∈ ℝ )
76 suprlub ⊢ ( ( ( ran seq 1 ( + , 𝐹 ) ⊆ ℝ ∧ ran seq 1 ( + , 𝐹 ) ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑧 ∈ ran seq 1 ( + , 𝐹 ) 𝑧 ≤ 𝑥 ) ∧ ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) ∈ ℝ ) → ( ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) ↔ ∃ 𝑦 ∈ ran seq 1 ( + , 𝐹 ) ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < 𝑦 ) )
77 14 22 66 75 76 syl31anc ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ( ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) ↔ ∃ 𝑦 ∈ ran seq 1 ( + , 𝐹 ) ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < 𝑦 ) )
78 72 77 mpbid ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ∃ 𝑦 ∈ ran seq 1 ( + , 𝐹 ) ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < 𝑦 )
79 breq2 ⊢ ( 𝑦 = ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) → ( ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < 𝑦 ↔ ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) )
80 79 rexrn ⊢ ( seq 1 ( + , 𝐹 ) Fn ℕ → ( ∃ 𝑦 ∈ ran seq 1 ( + , 𝐹 ) ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < 𝑦 ↔ ∃ 𝑘 ∈ ℕ ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) )
81 12 61 80 mp2b ⊢ ( ∃ 𝑦 ∈ ran seq 1 ( + , 𝐹 ) ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < 𝑦 ↔ ∃ 𝑘 ∈ ℕ ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) )
82 78 81 sylib ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ∃ 𝑘 ∈ ℕ ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) )
83 2re ⊢ 2 ∈ ℝ
84 2nn ⊢ 2 ∈ ℕ
85 nnmulcl ⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ℕ )
86 84 29 85 sylancr ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ℕ )
87 86 peano2nnd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ )
88 87 nnnn0d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ0 )
89 reexpcl ⊢ ( ( 2 ∈ ℝ ∧ ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℝ )
90 83 88 89 sylancr ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℝ )
91 90 ltnrd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ¬ ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) < ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) )
92 29 adantr ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) ) → 𝑘 ∈ ℕ )
93 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
94 93 adantl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
95 94 nnnn0d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ0 )
96 nnexpcl ⊢ ( ( 2 ∈ ℕ ∧ ( 𝑘 + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℕ )
97 84 95 96 sylancr ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℕ )
98 97 nnsqcld ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ∈ ℕ )
99 98 adantr ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) ) → ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ∈ ℕ )
100 breq1 ⊢ ( 𝑝 = 𝑤 → ( 𝑝 ∥ 𝑟 ↔ 𝑤 ∥ 𝑟 ) )
101 100 notbid ⊢ ( 𝑝 = 𝑤 → ( ¬ 𝑝 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑟 ) )
102 101 cbvralvw ⊢ ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝑘 ) ) ¬ 𝑝 ∥ 𝑟 ↔ ∀ 𝑤 ∈ ( ℙ ∖ ( 1 ... 𝑘 ) ) ¬ 𝑤 ∥ 𝑟 )
103 breq2 ⊢ ( 𝑟 = 𝑛 → ( 𝑤 ∥ 𝑟 ↔ 𝑤 ∥ 𝑛 ) )
104 103 notbid ⊢ ( 𝑟 = 𝑛 → ( ¬ 𝑤 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑛 ) )
105 104 ralbidv ⊢ ( 𝑟 = 𝑛 → ( ∀ 𝑤 ∈ ( ℙ ∖ ( 1 ... 𝑘 ) ) ¬ 𝑤 ∥ 𝑟 ↔ ∀ 𝑤 ∈ ( ℙ ∖ ( 1 ... 𝑘 ) ) ¬ 𝑤 ∥ 𝑛 ) )
106 102 105 bitrid ⊢ ( 𝑟 = 𝑛 → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝑘 ) ) ¬ 𝑝 ∥ 𝑟 ↔ ∀ 𝑤 ∈ ( ℙ ∖ ( 1 ... 𝑘 ) ) ¬ 𝑤 ∥ 𝑛 ) )
107 106 cbvrabv ⊢ { 𝑟 ∈ ( 1 ... ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝑘 ) ) ¬ 𝑝 ∥ 𝑟 } = { 𝑛 ∈ ( 1 ... ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) ∣ ∀ 𝑤 ∈ ( ℙ ∖ ( 1 ... 𝑘 ) ) ¬ 𝑤 ∥ 𝑛 }
108 simpll ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) ) → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
109 eleq1w ⊢ ( 𝑚 = 𝑗 → ( 𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ ) )
110 oveq2 ⊢ ( 𝑚 = 𝑗 → ( 1 / 𝑚 ) = ( 1 / 𝑗 ) )
111 109 110 ifbieq1d ⊢ ( 𝑚 = 𝑗 → if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) = if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) )
112 111 cbvsumv ⊢ Σ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) = Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 )
113 simpr ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) ) → Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) )
114 112 113 eqbrtrid ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) ) → Σ 𝑚 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑚 ∈ ℙ , ( 1 / 𝑚 ) , 0 ) < ( 1 / 2 ) )
115 eqid ⊢ ( 𝑤 ∈ ℕ ↦ { 𝑛 ∈ ( 1 ... ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) ∣ ( 𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛 ) } ) = ( 𝑤 ∈ ℕ ↦ { 𝑛 ∈ ( 1 ... ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) ∣ ( 𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛 ) } )
116 1 92 99 107 108 114 115 prmreclem5 ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) ) → ( ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) / 2 ) < ( ( 2 ↑ 𝑘 ) · ( √ ‘ ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) ) )
117 116 ex ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) → ( ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) / 2 ) < ( ( 2 ↑ 𝑘 ) · ( √ ‘ ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) ) ) )
118 eqid ⊢ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) = ( ℤ≥ ‘ ( 𝑘 + 1 ) )
119 94 nnzd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℤ )
120 eluznn ⊢ ( ( ( 𝑘 + 1 ) ∈ ℕ ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝑗 ∈ ℕ )
121 94 120 sylan ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → 𝑗 ∈ ℕ )
122 121 41 syl ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → ( 𝐹 ‘ 𝑗 ) = if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) )
123 39 a1i ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) ) → if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℝ )
124 simpl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → seq 1 ( + , 𝐹 ) ∈ dom ⇝ )
125 41 adantl ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) = if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) )
126 39 recni ⊢ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℂ
127 126 a1i ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℂ )
128 125 127 eqeltrd ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ℕ ) → ( 𝐹 ‘ 𝑗 ) ∈ ℂ )
129 2 94 128 iserex ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ↔ seq ( 𝑘 + 1 ) ( + , 𝐹 ) ∈ dom ⇝ ) )
130 124 129 mpbid ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → seq ( 𝑘 + 1 ) ( + , 𝐹 ) ∈ dom ⇝ )
131 118 119 122 123 130 isumrecl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℝ )
132 73 a1i ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 1 / 2 ) ∈ ℝ )
133 elfznn ⊢ ( 𝑗 ∈ ( 1 ... 𝑘 ) → 𝑗 ∈ ℕ )
134 133 adantl ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → 𝑗 ∈ ℕ )
135 134 41 syl ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → ( 𝐹 ‘ 𝑗 ) = if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) )
136 29 2 eleqtrdi ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ( ℤ≥ ‘ 1 ) )
137 126 a1i ⊢ ( ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑗 ∈ ( 1 ... 𝑘 ) ) → if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℂ )
138 135 136 137 fsumser ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) = ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) )
139 138 27 eqeltrd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℝ )
140 131 132 139 ltadd2d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) ↔ ( Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ) < ( Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + ( 1 / 2 ) ) ) )
141 2 118 94 125 127 124 isumsplit ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) = ( Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ) )
142 nncn ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℂ )
143 142 adantl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
144 ax-1cn ⊢ 1 ∈ ℂ
145 pncan ⊢ ( ( 𝑘 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
146 143 144 145 sylancl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 1 ) − 1 ) = 𝑘 )
147 146 oveq2d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) = ( 1 ... 𝑘 ) )
148 147 sumeq1d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) = Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) )
149 148 oveq1d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ( 1 ... ( ( 𝑘 + 1 ) − 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ) = ( Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ) )
150 141 149 eqtrd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) = ( Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ) )
151 150 breq1d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + ( 1 / 2 ) ) ↔ ( Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ) < ( Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + ( 1 / 2 ) ) ) )
152 140 151 bitr4d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) ↔ Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + ( 1 / 2 ) ) ) )
153 eqid ⊢ seq 1 ( + , 𝐹 ) = seq 1 ( + , 𝐹 )
154 2 153 23 42 43 54 60 isumsup ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) = sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) )
155 154 67 eqeltrd ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℝ )
156 155 adantr ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ∈ ℝ )
157 156 132 139 ltsubaddd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) − ( 1 / 2 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ↔ Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) + ( 1 / 2 ) ) ) )
158 154 adantr ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) = sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) )
159 158 oveq1d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) − ( 1 / 2 ) ) = ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) )
160 159 138 breq12d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( Σ 𝑗 ∈ ℕ if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) − ( 1 / 2 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑘 ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) ↔ ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) )
161 152 157 160 3bitr2d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( Σ 𝑗 ∈ ( ℤ≥ ‘ ( 𝑘 + 1 ) ) if ( 𝑗 ∈ ℙ , ( 1 / 𝑗 ) , 0 ) < ( 1 / 2 ) ↔ ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) ) )
162 2cn ⊢ 2 ∈ ℂ
163 162 a1i ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → 2 ∈ ℂ )
164 144 a1i ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℂ )
165 163 143 164 adddid ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 · ( 𝑘 + 1 ) ) = ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) )
166 94 nncnd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℂ )
167 mulcom ⊢ ( ( ( 𝑘 + 1 ) ∈ ℂ ∧ 2 ∈ ℂ ) → ( ( 𝑘 + 1 ) · 2 ) = ( 2 · ( 𝑘 + 1 ) ) )
168 166 162 167 sylancl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 1 ) · 2 ) = ( 2 · ( 𝑘 + 1 ) ) )
169 86 nncnd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ℂ )
170 169 164 164 addassd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) = ( ( 2 · 𝑘 ) + ( 1 + 1 ) ) )
171 144 2timesi ⊢ ( 2 · 1 ) = ( 1 + 1 )
172 171 oveq2i ⊢ ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) = ( ( 2 · 𝑘 ) + ( 1 + 1 ) )
173 170 172 eqtr4di ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) = ( ( 2 · 𝑘 ) + ( 2 · 1 ) ) )
174 165 168 173 3eqtr4d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 1 ) · 2 ) = ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) )
175 174 oveq2d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( ( 𝑘 + 1 ) · 2 ) ) = ( 2 ↑ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) )
176 2nn0 ⊢ 2 ∈ ℕ0
177 176 a1i ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → 2 ∈ ℕ0 )
178 163 177 95 expmuld ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( ( 𝑘 + 1 ) · 2 ) ) = ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) )
179 expp1 ⊢ ( ( 2 ∈ ℂ ∧ ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) · 2 ) )
180 162 88 179 sylancr ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( ( ( 2 · 𝑘 ) + 1 ) + 1 ) ) = ( ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) · 2 ) )
181 175 178 180 3eqtr3d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) = ( ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) · 2 ) )
182 181 oveq1d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) / 2 ) = ( ( ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) · 2 ) / 2 ) )
183 expcl ⊢ ( ( 2 ∈ ℂ ∧ ( ( 2 · 𝑘 ) + 1 ) ∈ ℕ0 ) → ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℂ )
184 162 88 183 sylancr ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℂ )
185 2ne0 ⊢ 2 ≠ 0
186 divcan4 ⊢ ( ( ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0 ) → ( ( ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) · 2 ) / 2 ) = ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) )
187 162 185 186 mp3an23 ⊢ ( ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ∈ ℂ → ( ( ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) · 2 ) / 2 ) = ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) )
188 184 187 syl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) · 2 ) / 2 ) = ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) )
189 182 188 eqtrd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) / 2 ) = ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) )
190 nnnn0 ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
191 190 adantl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
192 163 95 191 expaddd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( 𝑘 + ( 𝑘 + 1 ) ) ) = ( ( 2 ↑ 𝑘 ) · ( 2 ↑ ( 𝑘 + 1 ) ) ) )
193 143 2timesd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) = ( 𝑘 + 𝑘 ) )
194 193 oveq1d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) + 1 ) = ( ( 𝑘 + 𝑘 ) + 1 ) )
195 143 143 164 addassd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝑘 + 𝑘 ) + 1 ) = ( 𝑘 + ( 𝑘 + 1 ) ) )
196 194 195 eqtrd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) + 1 ) = ( 𝑘 + ( 𝑘 + 1 ) ) )
197 196 oveq2d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) = ( 2 ↑ ( 𝑘 + ( 𝑘 + 1 ) ) ) )
198 97 nnrpd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ+ )
199 198 rprege0d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ ( 𝑘 + 1 ) ) ) )
200 sqrtsq ⊢ ( ( ( 2 ↑ ( 𝑘 + 1 ) ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ ( 𝑘 + 1 ) ) ) → ( √ ‘ ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) = ( 2 ↑ ( 𝑘 + 1 ) ) )
201 199 200 syl ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( √ ‘ ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) = ( 2 ↑ ( 𝑘 + 1 ) ) )
202 201 oveq2d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 2 ↑ 𝑘 ) · ( √ ‘ ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) ) = ( ( 2 ↑ 𝑘 ) · ( 2 ↑ ( 𝑘 + 1 ) ) ) )
203 192 197 202 3eqtr4rd ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( 2 ↑ 𝑘 ) · ( √ ‘ ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) ) = ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) )
204 189 203 breq12d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) / 2 ) < ( ( 2 ↑ 𝑘 ) · ( √ ‘ ( ( 2 ↑ ( 𝑘 + 1 ) ) ↑ 2 ) ) ) ↔ ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) < ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) )
205 117 161 204 3imtr3d ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ( ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) → ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) < ( 2 ↑ ( ( 2 · 𝑘 ) + 1 ) ) ) )
206 91 205 mtod ⊢ ( ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ ) → ¬ ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) )
207 206 nrexdv ⊢ ( seq 1 ( + , 𝐹 ) ∈ dom ⇝ → ¬ ∃ 𝑘 ∈ ℕ ( sup ( ran seq 1 ( + , 𝐹 ) , ℝ , < ) − ( 1 / 2 ) ) < ( seq 1 ( + , 𝐹 ) ‘ 𝑘 ) )
208 82 207 pm2.65i ⊢ ¬ seq 1 ( + , 𝐹 ) ∈ dom ⇝