MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmreclem6 Structured version   Visualization version   GIF version

Theorem prmreclem6 15836
Description: Lemma for prmrec 15837. If the series 𝐹 was convergent, there would be some 𝑘 such that the sum starting from 𝑘 + 1 sums to less than 1 / 2; this is a sufficient hypothesis for prmreclem5 15835 to produce the contradictory bound 𝑁 / 2 < (2↑𝑘)√𝑁, which is false for 𝑁 = 2↑(2𝑘 + 2). (Contributed by Mario Carneiro, 6-Aug-2014.)
Hypothesis
Ref Expression
prmrec.1 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
Assertion
Ref Expression
prmreclem6 ¬ seq1( + , 𝐹) ∈ dom ⇝
Distinct variable group:   𝑛,𝐹

Proof of Theorem prmreclem6
Dummy variables 𝑗 𝑘 𝑚 𝑝 𝑟 𝑤 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nnuz 11935 . . . . . . . . 9 ℕ = (ℤ‘1)
2 1zzd 11668 . . . . . . . . 9 (⊤ → 1 ∈ ℤ)
3 nnrecre 11337 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
43adantl 469 . . . . . . . . . . . 12 ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
5 0re 10321 . . . . . . . . . . . 12 0 ∈ ℝ
6 ifcl 4317 . . . . . . . . . . . 12 (((1 / 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) ∈ ℝ)
74, 5, 6sylancl 576 . . . . . . . . . . 11 ((⊤ ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) ∈ ℝ)
8 prmrec.1 . . . . . . . . . . 11 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
97, 8fmptd 6600 . . . . . . . . . 10 (⊤ → 𝐹:ℕ⟶ℝ)
109ffvelrnda 6575 . . . . . . . . 9 ((⊤ ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ∈ ℝ)
111, 2, 10serfre 13047 . . . . . . . 8 (⊤ → seq1( + , 𝐹):ℕ⟶ℝ)
1211mptru 1645 . . . . . . 7 seq1( + , 𝐹):ℕ⟶ℝ
13 frn 6256 . . . . . . 7 (seq1( + , 𝐹):ℕ⟶ℝ → ran seq1( + , 𝐹) ⊆ ℝ)
1412, 13mp1i 13 . . . . . 6 (seq1( + , 𝐹) ∈ dom ⇝ → ran seq1( + , 𝐹) ⊆ ℝ)
15 1nn 11310 . . . . . . . 8 1 ∈ ℕ
1612fdmi 6260 . . . . . . . 8 dom seq1( + , 𝐹) = ℕ
1715, 16eleqtrri 2880 . . . . . . 7 1 ∈ dom seq1( + , 𝐹)
18 ne0i 4116 . . . . . . . 8 (1 ∈ dom seq1( + , 𝐹) → dom seq1( + , 𝐹) ≠ ∅)
19 dm0rn0 5537 . . . . . . . . 9 (dom seq1( + , 𝐹) = ∅ ↔ ran seq1( + , 𝐹) = ∅)
2019necon3bii 3026 . . . . . . . 8 (dom seq1( + , 𝐹) ≠ ∅ ↔ ran seq1( + , 𝐹) ≠ ∅)
2118, 20sylib 209 . . . . . . 7 (1 ∈ dom seq1( + , 𝐹) → ran seq1( + , 𝐹) ≠ ∅)
2217, 21mp1i 13 . . . . . 6 (seq1( + , 𝐹) ∈ dom ⇝ → ran seq1( + , 𝐹) ≠ ∅)
23 1zzd 11668 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ → 1 ∈ ℤ)
24 climdm 14502 . . . . . . . . . 10 (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
2524biimpi 207 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
2612a1i 11 . . . . . . . . . 10 (seq1( + , 𝐹) ∈ dom ⇝ → seq1( + , 𝐹):ℕ⟶ℝ)
2726ffvelrnda 6575 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℝ)
281, 23, 25, 27climrecl 14531 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ → ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ)
29 simpr 473 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
3025adantr 468 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
31 eleq1w 2864 . . . . . . . . . . . . . . 15 (𝑛 = 𝑗 → (𝑛 ∈ ℙ ↔ 𝑗 ∈ ℙ))
32 oveq2 6876 . . . . . . . . . . . . . . 15 (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗))
3331, 32ifbieq1d 4296 . . . . . . . . . . . . . 14 (𝑛 = 𝑗 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
34 prmnn 15600 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ ℙ → 𝑗 ∈ ℕ)
3534adantl 469 . . . . . . . . . . . . . . . . . 18 ((⊤ ∧ 𝑗 ∈ ℙ) → 𝑗 ∈ ℕ)
3635nnrecred 11346 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ 𝑗 ∈ ℙ) → (1 / 𝑗) ∈ ℝ)
375a1i 11 . . . . . . . . . . . . . . . . 17 ((⊤ ∧ ¬ 𝑗 ∈ ℙ) → 0 ∈ ℝ)
3836, 37ifclda 4307 . . . . . . . . . . . . . . . 16 (⊤ → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
3938mptru 1645 . . . . . . . . . . . . . . 15 if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ
4039elexi 3403 . . . . . . . . . . . . . 14 if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ V
4133, 8, 40fvmpt 6497 . . . . . . . . . . . . 13 (𝑗 ∈ ℕ → (𝐹𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
4241adantl 469 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
4339a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
4442, 43eqeltrd 2881 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ∈ ℝ)
4544adantlr 697 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ∈ ℝ)
46 nnrp 12050 . . . . . . . . . . . . . . . 16 (𝑗 ∈ ℕ → 𝑗 ∈ ℝ+)
4746adantl 469 . . . . . . . . . . . . . . 15 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℝ+)
4847rpreccld 12090 . . . . . . . . . . . . . 14 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (1 / 𝑗) ∈ ℝ+)
4948rpge0d 12084 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (1 / 𝑗))
50 0le0 11387 . . . . . . . . . . . . 13 0 ≤ 0
51 breq2 4841 . . . . . . . . . . . . . 14 ((1 / 𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ (1 / 𝑗) ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
52 breq2 4841 . . . . . . . . . . . . . 14 (0 = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
5351, 52ifboth 4311 . . . . . . . . . . . . 13 ((0 ≤ (1 / 𝑗) ∧ 0 ≤ 0) → 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
5449, 50, 53sylancl 576 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
5554, 42breqtrrd 4865 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹𝑗))
5655adantlr 697 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹𝑗))
571, 29, 30, 45, 56climserle 14610 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
5857ralrimiva 3150 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ → ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
59 brralrspcev 4897 . . . . . . . 8 ((( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
6028, 58, 59syl2anc 575 . . . . . . 7 (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
61 ffn 6250 . . . . . . . . 9 (seq1( + , 𝐹):ℕ⟶ℝ → seq1( + , 𝐹) Fn ℕ)
62 breq1 4840 . . . . . . . . . 10 (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
6362ralrn 6578 . . . . . . . . 9 (seq1( + , 𝐹) Fn ℕ → (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
6412, 61, 63mp2b 10 . . . . . . . 8 (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
6564rexbii 3225 . . . . . . 7 (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
6660, 65sylibr 225 . . . . . 6 (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧𝑥)
67 suprcl 11262 . . . . . 6 ((ran seq1( + , 𝐹) ⊆ ℝ ∧ ran seq1( + , 𝐹) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧𝑥) → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
6814, 22, 66, 67syl3anc 1483 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
69 2rp 12045 . . . . . 6 2 ∈ ℝ+
70 rpreccl 12065 . . . . . 6 (2 ∈ ℝ+ → (1 / 2) ∈ ℝ+)
7169, 70ax-mp 5 . . . . 5 (1 / 2) ∈ ℝ+
72 ltsubrp 12074 . . . . 5 ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ+) → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
7368, 71, 72sylancl 576 . . . 4 (seq1( + , 𝐹) ∈ dom ⇝ → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
74 halfre 11507 . . . . . 6 (1 / 2) ∈ ℝ
75 resubcl 10624 . . . . . 6 ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈ ℝ)
7668, 74, 75sylancl 576 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈ ℝ)
77 suprlub 11266 . . . . 5 (((ran seq1( + , 𝐹) ⊆ ℝ ∧ ran seq1( + , 𝐹) ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧𝑥) ∧ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈ ℝ) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦))
7814, 22, 66, 76, 77syl31anc 1485 . . . 4 (seq1( + , 𝐹) ∈ dom ⇝ → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦))
7973, 78mpbid 223 . . 3 (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦)
80 breq2 4841 . . . . 5 (𝑦 = (seq1( + , 𝐹)‘𝑘) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦 ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
8180rexrn 6577 . . . 4 (seq1( + , 𝐹) Fn ℕ → (∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦 ↔ ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
8212, 61, 81mp2b 10 . . 3 (∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦 ↔ ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
8379, 82sylib 209 . 2 (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
84 2re 11368 . . . . . 6 2 ∈ ℝ
85 2nn 11456 . . . . . . . . 9 2 ∈ ℕ
86 nnmulcl 11322 . . . . . . . . 9 ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
8785, 29, 86sylancr 577 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
8887peano2nnd 11316 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
8988nnnn0d 11611 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ0)
90 reexpcl 13094 . . . . . 6 ((2 ∈ ℝ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
9184, 89, 90sylancr 577 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
9291ltnrd 10450 . . . 4 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ¬ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1)))
9329adantr 468 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → 𝑘 ∈ ℕ)
94 peano2nn 11311 . . . . . . . . . . . 12 (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
9594adantl 469 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
9695nnnn0d 11611 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ0)
97 nnexpcl 13090 . . . . . . . . . 10 ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ0) → (2↑(𝑘 + 1)) ∈ ℕ)
9885, 96, 97sylancr 577 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℕ)
9998nnsqcld 13246 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
10099adantr 468 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
101 breq1 4840 . . . . . . . . . . 11 (𝑝 = 𝑤 → (𝑝𝑟𝑤𝑟))
102101notbid 309 . . . . . . . . . 10 (𝑝 = 𝑤 → (¬ 𝑝𝑟 ↔ ¬ 𝑤𝑟))
103102cbvralv 3356 . . . . . . . . 9 (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤𝑟)
104 breq2 4841 . . . . . . . . . . 11 (𝑟 = 𝑛 → (𝑤𝑟𝑤𝑛))
105104notbid 309 . . . . . . . . . 10 (𝑟 = 𝑛 → (¬ 𝑤𝑟 ↔ ¬ 𝑤𝑛))
106105ralbidv 3170 . . . . . . . . 9 (𝑟 = 𝑛 → (∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤𝑛))
107103, 106syl5bb 274 . . . . . . . 8 (𝑟 = 𝑛 → (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤𝑛))
108107cbvrabv 3385 . . . . . . 7 {𝑟 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝𝑟} = {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤𝑛}
109 simpll 774 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → seq1( + , 𝐹) ∈ dom ⇝ )
110 eleq1w 2864 . . . . . . . . . 10 (𝑚 = 𝑗 → (𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ))
111 oveq2 6876 . . . . . . . . . 10 (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
112110, 111ifbieq1d 4296 . . . . . . . . 9 (𝑚 = 𝑗 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
113112cbvsumv 14643 . . . . . . . 8 Σ𝑚 ∈ (ℤ‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)
114 simpr 473 . . . . . . . 8 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2))
115113, 114syl5eqbr 4872 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑚 ∈ (ℤ‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) < (1 / 2))
116 eqid 2802 . . . . . . 7 (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤𝑛)}) = (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤𝑛)})
1178, 93, 100, 108, 109, 115, 116prmreclem5 15835 . . . . . 6 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → (((2↑(𝑘 + 1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))))
118117ex 399 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) → (((2↑(𝑘 + 1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2)))))
119 eqid 2802 . . . . . . . . 9 (ℤ‘(𝑘 + 1)) = (ℤ‘(𝑘 + 1))
12095nnzd 11741 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℤ)
121 eluznn 11971 . . . . . . . . . . 11 (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
12295, 121sylan 571 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (ℤ‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
123122, 41syl 17 . . . . . . . . 9 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (ℤ‘(𝑘 + 1))) → (𝐹𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
12439a1i 11 . . . . . . . . 9 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (ℤ‘(𝑘 + 1))) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
125 simpl 470 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq1( + , 𝐹) ∈ dom ⇝ )
12641adantl 469 . . . . . . . . . . . 12 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
12739recni 10333 . . . . . . . . . . . . 13 if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ
128127a1i 11 . . . . . . . . . . . 12 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
129126, 128eqeltrd 2881 . . . . . . . . . . 11 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹𝑗) ∈ ℂ)
1301, 95, 129iserex 14604 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝑘 + 1)( + , 𝐹) ∈ dom ⇝ ))
131125, 130mpbid 223 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq(𝑘 + 1)( + , 𝐹) ∈ dom ⇝ )
132119, 120, 123, 124, 131isumrecl 14713 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
13374a1i 11 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1 / 2) ∈ ℝ)
134 elfznn 12587 . . . . . . . . . . . 12 (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ)
135134adantl 469 . . . . . . . . . . 11 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ)
136135, 41syl 17 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → (𝐹𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
13729, 1syl6eleq 2891 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ‘1))
138127a1i 11 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
139136, 137, 138fsumser 14678 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (seq1( + , 𝐹)‘𝑘))
140139, 27eqeltrd 2881 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
141132, 133, 140ltadd2d 10472 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2))))
1421, 119, 95, 126, 128, 125isumsplit 14788 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
143 nncn 11307 . . . . . . . . . . . . . 14 (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
144143adantl 469 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
145 ax-1cn 10273 . . . . . . . . . . . . 13 1 ∈ ℂ
146 pncan 10566 . . . . . . . . . . . . 13 ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
147144, 145, 146sylancl 576 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) − 1) = 𝑘)
148147oveq2d 6884 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
149148sumeq1d 14648 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
150149oveq1d 6883 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) = (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
151142, 150eqtrd 2836 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
152151breq1d 4847 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2)) ↔ (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2))))
153141, 152bitr4d 273 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2))))
154 eqid 2802 . . . . . . . . . 10 seq1( + , 𝐹) = seq1( + , 𝐹)
1551, 154, 23, 42, 43, 54, 60isumsup 14795 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
156155, 68eqeltrd 2881 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
157156adantr 468 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
158157, 133, 140ltsubaddd 10902 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2))))
159155adantr 468 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
160159oveq1d 6883 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)))
161160, 139breq12d 4850 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
162153, 158, 1613bitr2d 298 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
163 2cn 11369 . . . . . . . . . . . . 13 2 ∈ ℂ
164163a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
165145a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
166164, 144, 165adddid 10343 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
16795nncnd 11315 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
168 mulcom 10301 . . . . . . . . . . . 12 (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
169167, 163, 168sylancl 576 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
17087nncnd 11315 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
171170, 165, 165addassd 10341 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
1721452timesi 11424 . . . . . . . . . . . . 13 (2 · 1) = (1 + 1)
173172oveq2i 6879 . . . . . . . . . . . 12 ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
174171, 173syl6eqr 2854 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (2 · 1)))
175166, 169, 1743eqtr4d 2846 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (((2 · 𝑘) + 1) + 1))
176175oveq2d 6884 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = (2↑(((2 · 𝑘) + 1) + 1)))
177 2nn0 11570 . . . . . . . . . . 11 2 ∈ ℕ0
178177a1i 11 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℕ0)
179164, 178, 96expmuld 13228 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = ((2↑(𝑘 + 1))↑2))
180 expp1 13084 . . . . . . . . . 10 ((2 ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) → (2↑(((2 · 𝑘) + 1) + 1)) = ((2↑((2 · 𝑘) + 1)) · 2))
181163, 89, 180sylancr 577 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(((2 · 𝑘) + 1) + 1)) = ((2↑((2 · 𝑘) + 1)) · 2))
182176, 179, 1813eqtr3d 2844 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) = ((2↑((2 · 𝑘) + 1)) · 2))
183182oveq1d 6883 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (((2↑((2 · 𝑘) + 1)) · 2) / 2))
184 expcl 13095 . . . . . . . . 9 ((2 ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ0) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
185163, 89, 184sylancr 577 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
186 2ne0 11390 . . . . . . . . 9 2 ≠ 0
187 divcan4 10991 . . . . . . . . 9 (((2↑((2 · 𝑘) + 1)) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
188163, 186, 187mp3an23 1570 . . . . . . . 8 ((2↑((2 · 𝑘) + 1)) ∈ ℂ → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
189185, 188syl 17 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
190183, 189eqtrd 2836 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (2↑((2 · 𝑘) + 1)))
191 nnnn0 11560 . . . . . . . . 9 (𝑘 ∈ ℕ → 𝑘 ∈ ℕ0)
192191adantl 469 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ0)
193164, 96, 192expaddd 13227 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + (𝑘 + 1))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
1941442timesd 11536 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) = (𝑘 + 𝑘))
195194oveq1d 6883 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = ((𝑘 + 𝑘) + 1))
196144, 144, 165addassd 10341 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
197195, 196eqtrd 2836 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
198197oveq2d 6884 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) = (2↑(𝑘 + (𝑘 + 1))))
19998nnrpd 12078 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℝ+)
200199rprege0d 12087 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1)) ∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))))
201 sqrtsq 14227 . . . . . . . . 9 (((2↑(𝑘 + 1)) ∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))) → (√‘((2↑(𝑘 + 1))↑2)) = (2↑(𝑘 + 1)))
202200, 201syl 17 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (√‘((2↑(𝑘 + 1))↑2)) = (2↑(𝑘 + 1)))
203202oveq2d 6884 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
204193, 198, 2033eqtr4rd 2847 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = (2↑((2 · 𝑘) + 1)))
205190, 204breq12d 4850 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((((2↑(𝑘 + 1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) ↔ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))))
206118, 162, 2053imtr3d 284 . . . 4 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘) → (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))))
20792, 206mtod 189 . . 3 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ¬ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
208207nrexdv 3184 . 2 (seq1( + , 𝐹) ∈ dom ⇝ → ¬ ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
20983, 208pm2.65i 185 1 ¬ seq1( + , 𝐹) ∈ dom ⇝
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wa 384   = wceq 1637  wtru 1638  wcel 2155  wne 2974  wral 3092  wrex 3093  {crab 3096  cdif 3760  wss 3763  c0 4110  ifcif 4273   class class class wbr 4837  cmpt 4916  dom cdm 5305  ran crn 5306   Fn wfn 6090  wf 6091  cfv 6095  (class class class)co 6868  supcsup 8579  cc 10213  cr 10214  0cc0 10215  1c1 10216   + caddc 10218   · cmul 10220   < clt 10353  cle 10354  cmin 10545   / cdiv 10963  cn 11299  2c2 11350  0cn0 11553  cuz 11898  +crp 12040  ...cfz 12543  seqcseq 13018  cexp 13077  csqrt 14190  cli 14432  Σcsu 14633  cdvds 15197  cprime 15597
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-8 2157  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-13 2419  ax-ext 2781  ax-rep 4957  ax-sep 4968  ax-nul 4977  ax-pow 5029  ax-pr 5090  ax-un 7173  ax-inf2 8779  ax-cnex 10271  ax-resscn 10272  ax-1cn 10273  ax-icn 10274  ax-addcl 10275  ax-addrcl 10276  ax-mulcl 10277  ax-mulrcl 10278  ax-mulcom 10279  ax-addass 10280  ax-mulass 10281  ax-distr 10282  ax-i2m1 10283  ax-1ne0 10284  ax-1rid 10285  ax-rnegex 10286  ax-rrecex 10287  ax-cnre 10288  ax-pre-lttri 10289  ax-pre-lttrn 10290  ax-pre-ltadd 10291  ax-pre-mulgt0 10292  ax-pre-sup 10293
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2060  df-eu 2633  df-mo 2634  df-clab 2789  df-cleq 2795  df-clel 2798  df-nfc 2933  df-ne 2975  df-nel 3078  df-ral 3097  df-rex 3098  df-reu 3099  df-rmo 3100  df-rab 3101  df-v 3389  df-sbc 3628  df-csb 3723  df-dif 3766  df-un 3768  df-in 3770  df-ss 3777  df-pss 3779  df-nul 4111  df-if 4274  df-pw 4347  df-sn 4365  df-pr 4367  df-tp 4369  df-op 4371  df-uni 4624  df-int 4663  df-iun 4707  df-br 4838  df-opab 4900  df-mpt 4917  df-tr 4940  df-id 5213  df-eprel 5218  df-po 5226  df-so 5227  df-fr 5264  df-se 5265  df-we 5266  df-xp 5311  df-rel 5312  df-cnv 5313  df-co 5314  df-dm 5315  df-rn 5316  df-res 5317  df-ima 5318  df-pred 5887  df-ord 5933  df-on 5934  df-lim 5935  df-suc 5936  df-iota 6058  df-fun 6097  df-fn 6098  df-f 6099  df-f1 6100  df-fo 6101  df-f1o 6102  df-fv 6103  df-isom 6104  df-riota 6829  df-ov 6871  df-oprab 6872  df-mpt2 6873  df-om 7290  df-1st 7392  df-2nd 7393  df-wrecs 7636  df-recs 7698  df-rdg 7736  df-1o 7790  df-2o 7791  df-oadd 7794  df-er 7973  df-map 8088  df-pm 8089  df-en 8187  df-dom 8188  df-sdom 8189  df-fin 8190  df-sup 8581  df-inf 8582  df-oi 8648  df-card 9042  df-cda 9269  df-pnf 10355  df-mnf 10356  df-xr 10357  df-ltxr 10358  df-le 10359  df-sub 10547  df-neg 10548  df-div 10964  df-nn 11300  df-2 11358  df-3 11359  df-n0 11554  df-xnn0 11624  df-z 11638  df-uz 11899  df-q 12002  df-rp 12041  df-fz 12544  df-fzo 12684  df-fl 12811  df-mod 12887  df-seq 13019  df-exp 13078  df-hash 13332  df-cj 14056  df-re 14057  df-im 14058  df-sqrt 14192  df-abs 14193  df-clim 14436  df-rlim 14437  df-sum 14634  df-dvds 15198  df-gcd 15430  df-prm 15598  df-pc 15753
This theorem is referenced by:  prmrec  15837
  Copyright terms: Public domain W3C validator