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

Theorem prmreclem6 16801
Description: Lemma for prmrec 16802. 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 16800 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 12814 . . . . . . . . 9 β„• = (β„€β‰₯β€˜1)
2 1zzd 12542 . . . . . . . . 9 (⊀ β†’ 1 ∈ β„€)
3 nnrecre 12203 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ (1 / 𝑛) ∈ ℝ)
43adantl 483 . . . . . . . . . . . 12 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (1 / 𝑛) ∈ ℝ)
5 0re 11165 . . . . . . . . . . . 12 0 ∈ ℝ
6 ifcl 4535 . . . . . . . . . . . 12 (((1 / 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) β†’ if(𝑛 ∈ β„™, (1 / 𝑛), 0) ∈ ℝ)
74, 5, 6sylancl 587 . . . . . . . . . . 11 ((⊀ ∧ 𝑛 ∈ β„•) β†’ if(𝑛 ∈ β„™, (1 / 𝑛), 0) ∈ ℝ)
8 prmrec.1 . . . . . . . . . . 11 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (1 / 𝑛), 0))
97, 8fmptd 7066 . . . . . . . . . 10 (⊀ β†’ 𝐹:β„•βŸΆβ„)
109ffvelcdmda 7039 . . . . . . . . 9 ((⊀ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ ℝ)
111, 2, 10serfre 13946 . . . . . . . 8 (⊀ β†’ seq1( + , 𝐹):β„•βŸΆβ„)
1211mptru 1549 . . . . . . 7 seq1( + , 𝐹):β„•βŸΆβ„
13 frn 6679 . . . . . . 7 (seq1( + , 𝐹):β„•βŸΆβ„ β†’ ran seq1( + , 𝐹) βŠ† ℝ)
1412, 13mp1i 13 . . . . . 6 (seq1( + , 𝐹) ∈ dom ⇝ β†’ ran seq1( + , 𝐹) βŠ† ℝ)
15 1nn 12172 . . . . . . . 8 1 ∈ β„•
1612fdmi 6684 . . . . . . . 8 dom seq1( + , 𝐹) = β„•
1715, 16eleqtrri 2833 . . . . . . 7 1 ∈ dom seq1( + , 𝐹)
18 ne0i 4298 . . . . . . . 8 (1 ∈ dom seq1( + , 𝐹) β†’ dom seq1( + , 𝐹) β‰  βˆ…)
19 dm0rn0 5884 . . . . . . . . 9 (dom seq1( + , 𝐹) = βˆ… ↔ ran seq1( + , 𝐹) = βˆ…)
2019necon3bii 2993 . . . . . . . 8 (dom seq1( + , 𝐹) β‰  βˆ… ↔ ran seq1( + , 𝐹) β‰  βˆ…)
2118, 20sylib 217 . . . . . . 7 (1 ∈ dom seq1( + , 𝐹) β†’ ran seq1( + , 𝐹) β‰  βˆ…)
2217, 21mp1i 13 . . . . . 6 (seq1( + , 𝐹) ∈ dom ⇝ β†’ ran seq1( + , 𝐹) β‰  βˆ…)
23 1zzd 12542 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ β†’ 1 ∈ β„€)
24 climdm 15445 . . . . . . . . . 10 (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
2524biimpi 215 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ β†’ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
2612a1i 11 . . . . . . . . . 10 (seq1( + , 𝐹) ∈ dom ⇝ β†’ seq1( + , 𝐹):β„•βŸΆβ„)
2726ffvelcdmda 7039 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) ∈ ℝ)
281, 23, 25, 27climrecl 15474 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ β†’ ( ⇝ β€˜seq1( + , 𝐹)) ∈ ℝ)
29 simpr 486 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
3025adantr 482 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
31 eleq1w 2817 . . . . . . . . . . . . . . 15 (𝑛 = 𝑗 β†’ (𝑛 ∈ β„™ ↔ 𝑗 ∈ β„™))
32 oveq2 7369 . . . . . . . . . . . . . . 15 (𝑛 = 𝑗 β†’ (1 / 𝑛) = (1 / 𝑗))
3331, 32ifbieq1d 4514 . . . . . . . . . . . . . 14 (𝑛 = 𝑗 β†’ if(𝑛 ∈ β„™, (1 / 𝑛), 0) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
34 prmnn 16558 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„™ β†’ 𝑗 ∈ β„•)
3534adantl 483 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ 𝑗 ∈ β„™) β†’ 𝑗 ∈ β„•)
3635nnrecred 12212 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ 𝑗 ∈ β„™) β†’ (1 / 𝑗) ∈ ℝ)
375a1i 11 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ Β¬ 𝑗 ∈ β„™) β†’ 0 ∈ ℝ)
3836, 37ifclda 4525 . . . . . . . . . . . . . . . 16 (⊀ β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
3938mptru 1549 . . . . . . . . . . . . . . 15 if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ
4039elexi 3466 . . . . . . . . . . . . . 14 if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ V
4133, 8, 40fvmpt 6952 . . . . . . . . . . . . 13 (𝑗 ∈ β„• β†’ (πΉβ€˜π‘—) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
4241adantl 483 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
4339a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
4442, 43eqeltrd 2834 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ ℝ)
4544adantlr 714 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ ℝ)
46 nnrp 12934 . . . . . . . . . . . . . . . 16 (𝑗 ∈ β„• β†’ 𝑗 ∈ ℝ+)
4746adantl 483 . . . . . . . . . . . . . . 15 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ ℝ+)
4847rpreccld 12975 . . . . . . . . . . . . . 14 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ (1 / 𝑗) ∈ ℝ+)
4948rpge0d 12969 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (1 / 𝑗))
50 0le0 12262 . . . . . . . . . . . . 13 0 ≀ 0
51 breq2 5113 . . . . . . . . . . . . . 14 ((1 / 𝑗) = if(𝑗 ∈ β„™, (1 / 𝑗), 0) β†’ (0 ≀ (1 / 𝑗) ↔ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
52 breq2 5113 . . . . . . . . . . . . . 14 (0 = if(𝑗 ∈ β„™, (1 / 𝑗), 0) β†’ (0 ≀ 0 ↔ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
5351, 52ifboth 4529 . . . . . . . . . . . . 13 ((0 ≀ (1 / 𝑗) ∧ 0 ≀ 0) β†’ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0))
5449, 50, 53sylancl 587 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0))
5554, 42breqtrrd 5137 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (πΉβ€˜π‘—))
5655adantlr 714 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (πΉβ€˜π‘—))
571, 29, 30, 45, 56climserle 15556 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) ≀ ( ⇝ β€˜seq1( + , 𝐹)))
5857ralrimiva 3140 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ β†’ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ ( ⇝ β€˜seq1( + , 𝐹)))
59 brralrspcev 5169 . . . . . . . 8 ((( ⇝ β€˜seq1( + , 𝐹)) ∈ ℝ ∧ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ ( ⇝ β€˜seq1( + , 𝐹))) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯)
6028, 58, 59syl2anc 585 . . . . . . 7 (seq1( + , 𝐹) ∈ dom ⇝ β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯)
61 ffn 6672 . . . . . . . . 9 (seq1( + , 𝐹):β„•βŸΆβ„ β†’ seq1( + , 𝐹) Fn β„•)
62 breq1 5112 . . . . . . . . . 10 (𝑧 = (seq1( + , 𝐹)β€˜π‘˜) β†’ (𝑧 ≀ π‘₯ ↔ (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯))
6362ralrn 7042 . . . . . . . . 9 (seq1( + , 𝐹) Fn β„• β†’ (βˆ€π‘§ ∈ ran seq1( + , 𝐹)𝑧 ≀ π‘₯ ↔ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯))
6412, 61, 63mp2b 10 . . . . . . . 8 (βˆ€π‘§ ∈ ran seq1( + , 𝐹)𝑧 ≀ π‘₯ ↔ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯)
6564rexbii 3094 . . . . . . 7 (βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran seq1( + , 𝐹)𝑧 ≀ π‘₯ ↔ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯)
6660, 65sylibr 233 . . . . . 6 (seq1( + , 𝐹) ∈ dom ⇝ β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran seq1( + , 𝐹)𝑧 ≀ π‘₯)
6714, 22, 66suprcld 12126 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ β†’ sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
68 2rp 12928 . . . . . 6 2 ∈ ℝ+
69 rpreccl 12949 . . . . . 6 (2 ∈ ℝ+ β†’ (1 / 2) ∈ ℝ+)
7068, 69ax-mp 5 . . . . 5 (1 / 2) ∈ ℝ+
71 ltsubrp 12959 . . . . 5 ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ+) β†’ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
7267, 70, 71sylancl 587 . . . 4 (seq1( + , 𝐹) ∈ dom ⇝ β†’ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
73 halfre 12375 . . . . . 6 (1 / 2) ∈ ℝ
74 resubcl 11473 . . . . . 6 ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ) β†’ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) ∈ ℝ)
7567, 73, 74sylancl 587 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ β†’ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) ∈ ℝ)
76 suprlub 12127 . . . . 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)) < 𝑦))
7714, 22, 66, 75, 76syl31anc 1374 . . . 4 (seq1( + , 𝐹) ∈ dom ⇝ β†’ ((sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ) ↔ βˆƒπ‘¦ ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < 𝑦))
7872, 77mpbid 231 . . 3 (seq1( + , 𝐹) ∈ dom ⇝ β†’ βˆƒπ‘¦ ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < 𝑦)
79 breq2 5113 . . . . 5 (𝑦 = (seq1( + , 𝐹)β€˜π‘˜) β†’ ((sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < 𝑦 ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜)))
8079rexrn 7041 . . . 4 (seq1( + , 𝐹) Fn β„• β†’ (βˆƒπ‘¦ ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < 𝑦 ↔ βˆƒπ‘˜ ∈ β„• (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜)))
8112, 61, 80mp2b 10 . . 3 (βˆƒπ‘¦ ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < 𝑦 ↔ βˆƒπ‘˜ ∈ β„• (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜))
8278, 81sylib 217 . 2 (seq1( + , 𝐹) ∈ dom ⇝ β†’ βˆƒπ‘˜ ∈ β„• (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜))
83 2re 12235 . . . . . 6 2 ∈ ℝ
84 2nn 12234 . . . . . . . . 9 2 ∈ β„•
85 nnmulcl 12185 . . . . . . . . 9 ((2 ∈ β„• ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„•)
8684, 29, 85sylancr 588 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„•)
8786peano2nnd 12178 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
8887nnnn0d 12481 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
89 reexpcl 13993 . . . . . 6 ((2 ∈ ℝ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ ℝ)
9083, 88, 89sylancr 588 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ ℝ)
9190ltnrd 11297 . . . 4 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Β¬ (2↑((2 Β· π‘˜) + 1)) < (2↑((2 Β· π‘˜) + 1)))
9229adantr 482 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ π‘˜ ∈ β„•)
93 peano2nn 12173 . . . . . . . . . . . 12 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
9493adantl 483 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„•)
9594nnnn0d 12481 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„•0)
96 nnexpcl 13989 . . . . . . . . . 10 ((2 ∈ β„• ∧ (π‘˜ + 1) ∈ β„•0) β†’ (2↑(π‘˜ + 1)) ∈ β„•)
9784, 95, 96sylancr 588 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(π‘˜ + 1)) ∈ β„•)
9897nnsqcld 14156 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2↑(π‘˜ + 1))↑2) ∈ β„•)
9998adantr 482 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ ((2↑(π‘˜ + 1))↑2) ∈ β„•)
100 breq1 5112 . . . . . . . . . . 11 (𝑝 = 𝑀 β†’ (𝑝 βˆ₯ π‘Ÿ ↔ 𝑀 βˆ₯ π‘Ÿ))
101100notbid 318 . . . . . . . . . 10 (𝑝 = 𝑀 β†’ (Β¬ 𝑝 βˆ₯ π‘Ÿ ↔ Β¬ 𝑀 βˆ₯ π‘Ÿ))
102101cbvralvw 3224 . . . . . . . . 9 (βˆ€π‘ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑝 βˆ₯ π‘Ÿ ↔ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ π‘Ÿ)
103 breq2 5113 . . . . . . . . . . 11 (π‘Ÿ = 𝑛 β†’ (𝑀 βˆ₯ π‘Ÿ ↔ 𝑀 βˆ₯ 𝑛))
104103notbid 318 . . . . . . . . . 10 (π‘Ÿ = 𝑛 β†’ (Β¬ 𝑀 βˆ₯ π‘Ÿ ↔ Β¬ 𝑀 βˆ₯ 𝑛))
105104ralbidv 3171 . . . . . . . . 9 (π‘Ÿ = 𝑛 β†’ (βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ π‘Ÿ ↔ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ 𝑛))
106102, 105bitrid 283 . . . . . . . 8 (π‘Ÿ = 𝑛 β†’ (βˆ€π‘ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑝 βˆ₯ π‘Ÿ ↔ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ 𝑛))
107106cbvrabv 3416 . . . . . . 7 {π‘Ÿ ∈ (1...((2↑(π‘˜ + 1))↑2)) ∣ βˆ€π‘ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑝 βˆ₯ π‘Ÿ} = {𝑛 ∈ (1...((2↑(π‘˜ + 1))↑2)) ∣ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ 𝑛}
108 simpll 766 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ seq1( + , 𝐹) ∈ dom ⇝ )
109 eleq1w 2817 . . . . . . . . . 10 (π‘š = 𝑗 β†’ (π‘š ∈ β„™ ↔ 𝑗 ∈ β„™))
110 oveq2 7369 . . . . . . . . . 10 (π‘š = 𝑗 β†’ (1 / π‘š) = (1 / 𝑗))
111109, 110ifbieq1d 4514 . . . . . . . . 9 (π‘š = 𝑗 β†’ if(π‘š ∈ β„™, (1 / π‘š), 0) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
112111cbvsumv 15589 . . . . . . . 8 Ξ£π‘š ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(π‘š ∈ β„™, (1 / π‘š), 0) = Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)
113 simpr 486 . . . . . . . 8 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2))
114112, 113eqbrtrid 5144 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ Ξ£π‘š ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(π‘š ∈ β„™, (1 / π‘š), 0) < (1 / 2))
115 eqid 2733 . . . . . . 7 (𝑀 ∈ β„• ↦ {𝑛 ∈ (1...((2↑(π‘˜ + 1))↑2)) ∣ (𝑀 ∈ β„™ ∧ 𝑀 βˆ₯ 𝑛)}) = (𝑀 ∈ β„• ↦ {𝑛 ∈ (1...((2↑(π‘˜ + 1))↑2)) ∣ (𝑀 ∈ β„™ ∧ 𝑀 βˆ₯ 𝑛)})
1168, 92, 99, 107, 108, 114, 115prmreclem5 16800 . . . . . 6 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ (((2↑(π‘˜ + 1))↑2) / 2) < ((2β†‘π‘˜) Β· (βˆšβ€˜((2↑(π‘˜ + 1))↑2))))
117116ex 414 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2) β†’ (((2↑(π‘˜ + 1))↑2) / 2) < ((2β†‘π‘˜) Β· (βˆšβ€˜((2↑(π‘˜ + 1))↑2)))))
118 eqid 2733 . . . . . . . . 9 (β„€β‰₯β€˜(π‘˜ + 1)) = (β„€β‰₯β€˜(π‘˜ + 1))
11994nnzd 12534 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„€)
120 eluznn 12851 . . . . . . . . . . 11 (((π‘˜ + 1) ∈ β„• ∧ 𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))) β†’ 𝑗 ∈ β„•)
12194, 120sylan 581 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))) β†’ 𝑗 ∈ β„•)
122121, 41syl 17 . . . . . . . . 9 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))) β†’ (πΉβ€˜π‘—) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
12339a1i 11 . . . . . . . . 9 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))) β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
124 simpl 484 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ seq1( + , 𝐹) ∈ dom ⇝ )
12541adantl 483 . . . . . . . . . . . 12 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
12639recni 11177 . . . . . . . . . . . . 13 if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ β„‚
127126a1i 11 . . . . . . . . . . . 12 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ β„‚)
128125, 127eqeltrd 2834 . . . . . . . . . . 11 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ β„‚)
1291, 94, 128iserex 15550 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(π‘˜ + 1)( + , 𝐹) ∈ dom ⇝ ))
130124, 129mpbid 231 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ seq(π‘˜ + 1)( + , 𝐹) ∈ dom ⇝ )
131118, 119, 122, 123, 130isumrecl 15658 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
13273a1i 11 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (1 / 2) ∈ ℝ)
133 elfznn 13479 . . . . . . . . . . . 12 (𝑗 ∈ (1...π‘˜) β†’ 𝑗 ∈ β„•)
134133adantl 483 . . . . . . . . . . 11 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...π‘˜)) β†’ 𝑗 ∈ β„•)
135134, 41syl 17 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...π‘˜)) β†’ (πΉβ€˜π‘—) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
13629, 1eleqtrdi 2844 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
137126a1i 11 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...π‘˜)) β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ β„‚)
138135, 136, 137fsumser 15623 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) = (seq1( + , 𝐹)β€˜π‘˜))
139138, 27eqeltrd 2834 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
140131, 132, 139ltadd2d 11319 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2) ↔ (Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) + Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)) < (Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) + (1 / 2))))
1411, 118, 94, 125, 127, 124isumsplit 15733 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...((π‘˜ + 1) βˆ’ 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) + Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
142 nncn 12169 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
143142adantl 483 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„‚)
144 ax-1cn 11117 . . . . . . . . . . . . 13 1 ∈ β„‚
145 pncan 11415 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
146143, 144, 145sylancl 587 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
147146oveq2d 7377 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (1...((π‘˜ + 1) βˆ’ 1)) = (1...π‘˜))
148147sumeq1d 15594 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...((π‘˜ + 1) βˆ’ 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) = Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0))
149148oveq1d 7376 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ (1...((π‘˜ + 1) βˆ’ 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) + Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)) = (Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) + Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
150141, 149eqtrd 2773 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) + Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
151150breq1d 5119 . . . . . . 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))))
152140, 151bitr4d 282 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2) ↔ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) + (1 / 2))))
153 eqid 2733 . . . . . . . . . 10 seq1( + , 𝐹) = seq1( + , 𝐹)
1541, 153, 23, 42, 43, 54, 60isumsup 15740 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
155154, 67eqeltrd 2834 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
156155adantr 482 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
157156, 132, 139ltsubaddd 11759 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) βˆ’ (1 / 2)) < Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) ↔ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) + (1 / 2))))
158154adantr 482 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
159158oveq1d 7376 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) βˆ’ (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)))
160159, 138breq12d 5122 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) βˆ’ (1 / 2)) < Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜)))
161152, 157, 1603bitr2d 307 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜)))
162 2cn 12236 . . . . . . . . . . . . 13 2 ∈ β„‚
163162a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ 2 ∈ β„‚)
164144a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ 1 ∈ β„‚)
165163, 143, 164adddid 11187 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (π‘˜ + 1)) = ((2 Β· π‘˜) + (2 Β· 1)))
16694nncnd 12177 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„‚)
167 mulcom 11145 . . . . . . . . . . . 12 (((π‘˜ + 1) ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((π‘˜ + 1) Β· 2) = (2 Β· (π‘˜ + 1)))
168166, 162, 167sylancl 587 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) Β· 2) = (2 Β· (π‘˜ + 1)))
16986nncnd 12177 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„‚)
170169, 164, 164addassd 11185 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2 Β· π‘˜) + 1) + 1) = ((2 Β· π‘˜) + (1 + 1)))
1711442timesi 12299 . . . . . . . . . . . . 13 (2 Β· 1) = (1 + 1)
172171oveq2i 7372 . . . . . . . . . . . 12 ((2 Β· π‘˜) + (2 Β· 1)) = ((2 Β· π‘˜) + (1 + 1))
173170, 172eqtr4di 2791 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2 Β· π‘˜) + 1) + 1) = ((2 Β· π‘˜) + (2 Β· 1)))
174165, 168, 1733eqtr4d 2783 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) Β· 2) = (((2 Β· π‘˜) + 1) + 1))
175174oveq2d 7377 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((π‘˜ + 1) Β· 2)) = (2↑(((2 Β· π‘˜) + 1) + 1)))
176 2nn0 12438 . . . . . . . . . . 11 2 ∈ β„•0
177176a1i 11 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ 2 ∈ β„•0)
178163, 177, 95expmuld 14063 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((π‘˜ + 1) Β· 2)) = ((2↑(π‘˜ + 1))↑2))
179 expp1 13983 . . . . . . . . . 10 ((2 ∈ β„‚ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (2↑(((2 Β· π‘˜) + 1) + 1)) = ((2↑((2 Β· π‘˜) + 1)) Β· 2))
180162, 88, 179sylancr 588 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(((2 Β· π‘˜) + 1) + 1)) = ((2↑((2 Β· π‘˜) + 1)) Β· 2))
181175, 178, 1803eqtr3d 2781 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2↑(π‘˜ + 1))↑2) = ((2↑((2 Β· π‘˜) + 1)) Β· 2))
182181oveq1d 7376 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2↑(π‘˜ + 1))↑2) / 2) = (((2↑((2 Β· π‘˜) + 1)) Β· 2) / 2))
183 expcl 13994 . . . . . . . . 9 ((2 ∈ β„‚ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ β„‚)
184162, 88, 183sylancr 588 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ β„‚)
185 2ne0 12265 . . . . . . . . 9 2 β‰  0
186 divcan4 11848 . . . . . . . . 9 (((2↑((2 Β· π‘˜) + 1)) ∈ β„‚ ∧ 2 ∈ β„‚ ∧ 2 β‰  0) β†’ (((2↑((2 Β· π‘˜) + 1)) Β· 2) / 2) = (2↑((2 Β· π‘˜) + 1)))
187162, 185, 186mp3an23 1454 . . . . . . . 8 ((2↑((2 Β· π‘˜) + 1)) ∈ β„‚ β†’ (((2↑((2 Β· π‘˜) + 1)) Β· 2) / 2) = (2↑((2 Β· π‘˜) + 1)))
188184, 187syl 17 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2↑((2 Β· π‘˜) + 1)) Β· 2) / 2) = (2↑((2 Β· π‘˜) + 1)))
189182, 188eqtrd 2773 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2↑(π‘˜ + 1))↑2) / 2) = (2↑((2 Β· π‘˜) + 1)))
190 nnnn0 12428 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0)
191190adantl 483 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•0)
192163, 95, 191expaddd 14062 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(π‘˜ + (π‘˜ + 1))) = ((2β†‘π‘˜) Β· (2↑(π‘˜ + 1))))
1931432timesd 12404 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) = (π‘˜ + π‘˜))
194193oveq1d 7376 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) = ((π‘˜ + π‘˜) + 1))
195143, 143, 164addassd 11185 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + π‘˜) + 1) = (π‘˜ + (π‘˜ + 1)))
196194, 195eqtrd 2773 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) = (π‘˜ + (π‘˜ + 1)))
197196oveq2d 7377 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((2 Β· π‘˜) + 1)) = (2↑(π‘˜ + (π‘˜ + 1))))
19897nnrpd 12963 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(π‘˜ + 1)) ∈ ℝ+)
199198rprege0d 12972 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2↑(π‘˜ + 1)) ∈ ℝ ∧ 0 ≀ (2↑(π‘˜ + 1))))
200 sqrtsq 15163 . . . . . . . . 9 (((2↑(π‘˜ + 1)) ∈ ℝ ∧ 0 ≀ (2↑(π‘˜ + 1))) β†’ (βˆšβ€˜((2↑(π‘˜ + 1))↑2)) = (2↑(π‘˜ + 1)))
201199, 200syl 17 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (βˆšβ€˜((2↑(π‘˜ + 1))↑2)) = (2↑(π‘˜ + 1)))
202201oveq2d 7377 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2β†‘π‘˜) Β· (βˆšβ€˜((2↑(π‘˜ + 1))↑2))) = ((2β†‘π‘˜) Β· (2↑(π‘˜ + 1))))
203192, 197, 2023eqtr4rd 2784 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2β†‘π‘˜) Β· (βˆšβ€˜((2↑(π‘˜ + 1))↑2))) = (2↑((2 Β· π‘˜) + 1)))
204189, 203breq12d 5122 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((((2↑(π‘˜ + 1))↑2) / 2) < ((2β†‘π‘˜) Β· (βˆšβ€˜((2↑(π‘˜ + 1))↑2))) ↔ (2↑((2 Β· π‘˜) + 1)) < (2↑((2 Β· π‘˜) + 1))))
205117, 161, 2043imtr3d 293 . . . 4 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜) β†’ (2↑((2 Β· π‘˜) + 1)) < (2↑((2 Β· π‘˜) + 1))))
20691, 205mtod 197 . . 3 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Β¬ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜))
207206nrexdv 3143 . 2 (seq1( + , 𝐹) ∈ dom ⇝ β†’ Β¬ βˆƒπ‘˜ ∈ β„• (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜))
20882, 207pm2.65i 193 1 Β¬ seq1( + , 𝐹) ∈ dom ⇝
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   ↔ wb 205   ∧ wa 397   = wceq 1542  βŠ€wtru 1543   ∈ wcel 2107   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3406   βˆ– cdif 3911   βŠ† wss 3914  βˆ…c0 4286  ifcif 4490   class class class wbr 5109   ↦ cmpt 5192  dom cdm 5637  ran crn 5638   Fn wfn 6495  βŸΆwf 6496  β€˜cfv 6500  (class class class)co 7361  supcsup 9384  β„‚cc 11057  β„cr 11058  0cc0 11059  1c1 11060   + caddc 11062   Β· cmul 11064   < clt 11197   ≀ cle 11198   βˆ’ cmin 11393   / cdiv 11820  β„•cn 12161  2c2 12216  β„•0cn0 12421  β„€β‰₯cuz 12771  β„+crp 12923  ...cfz 13433  seqcseq 13915  β†‘cexp 13976  βˆšcsqrt 15127   ⇝ cli 15375  Ξ£csu 15579   βˆ₯ cdvds 16144  β„™cprime 16555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5246  ax-sep 5260  ax-nul 5267  ax-pow 5324  ax-pr 5388  ax-un 7676  ax-inf2 9585  ax-cnex 11115  ax-resscn 11116  ax-1cn 11117  ax-icn 11118  ax-addcl 11119  ax-addrcl 11120  ax-mulcl 11121  ax-mulrcl 11122  ax-mulcom 11123  ax-addass 11124  ax-mulass 11125  ax-distr 11126  ax-i2m1 11127  ax-1ne0 11128  ax-1rid 11129  ax-rnegex 11130  ax-rrecex 11131  ax-cnre 11132  ax-pre-lttri 11133  ax-pre-lttrn 11134  ax-pre-ltadd 11135  ax-pre-mulgt0 11136  ax-pre-sup 11137
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3449  df-sbc 3744  df-csb 3860  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3933  df-nul 4287  df-if 4491  df-pw 4566  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4870  df-int 4912  df-iun 4960  df-br 5110  df-opab 5172  df-mpt 5193  df-tr 5227  df-id 5535  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5592  df-se 5593  df-we 5594  df-xp 5643  df-rel 5644  df-cnv 5645  df-co 5646  df-dm 5647  df-rn 5648  df-res 5649  df-ima 5650  df-pred 6257  df-ord 6324  df-on 6325  df-lim 6326  df-suc 6327  df-iota 6452  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-isom 6509  df-riota 7317  df-ov 7364  df-oprab 7365  df-mpo 7366  df-om 7807  df-1st 7925  df-2nd 7926  df-frecs 8216  df-wrecs 8247  df-recs 8321  df-rdg 8360  df-1o 8416  df-2o 8417  df-oadd 8420  df-er 8654  df-map 8773  df-pm 8774  df-en 8890  df-dom 8891  df-sdom 8892  df-fin 8893  df-sup 9386  df-inf 9387  df-oi 9454  df-dju 9845  df-card 9883  df-pnf 11199  df-mnf 11200  df-xr 11201  df-ltxr 11202  df-le 11203  df-sub 11395  df-neg 11396  df-div 11821  df-nn 12162  df-2 12224  df-3 12225  df-n0 12422  df-xnn0 12494  df-z 12508  df-uz 12772  df-q 12882  df-rp 12924  df-fz 13434  df-fzo 13577  df-fl 13706  df-mod 13784  df-seq 13916  df-exp 13977  df-hash 14240  df-cj 14993  df-re 14994  df-im 14995  df-sqrt 15129  df-abs 15130  df-clim 15379  df-rlim 15380  df-sum 15580  df-dvds 16145  df-gcd 16383  df-prm 16556  df-pc 16717
This theorem is referenced by:  prmrec  16802
  Copyright terms: Public domain W3C validator