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

Theorem prmreclem6 16854
Description: Lemma for prmrec 16855. 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 16853 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 12865 . . . . . . . . 9 β„• = (β„€β‰₯β€˜1)
2 1zzd 12593 . . . . . . . . 9 (⊀ β†’ 1 ∈ β„€)
3 nnrecre 12254 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ (1 / 𝑛) ∈ ℝ)
43adantl 483 . . . . . . . . . . . 12 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (1 / 𝑛) ∈ ℝ)
5 0re 11216 . . . . . . . . . . . 12 0 ∈ ℝ
6 ifcl 4574 . . . . . . . . . . . 12 (((1 / 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) β†’ if(𝑛 ∈ β„™, (1 / 𝑛), 0) ∈ ℝ)
74, 5, 6sylancl 587 . . . . . . . . . . 11 ((⊀ ∧ 𝑛 ∈ β„•) β†’ if(𝑛 ∈ β„™, (1 / 𝑛), 0) ∈ ℝ)
8 prmrec.1 . . . . . . . . . . 11 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (1 / 𝑛), 0))
97, 8fmptd 7114 . . . . . . . . . 10 (⊀ β†’ 𝐹:β„•βŸΆβ„)
109ffvelcdmda 7087 . . . . . . . . 9 ((⊀ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ ℝ)
111, 2, 10serfre 13997 . . . . . . . 8 (⊀ β†’ seq1( + , 𝐹):β„•βŸΆβ„)
1211mptru 1549 . . . . . . 7 seq1( + , 𝐹):β„•βŸΆβ„
13 frn 6725 . . . . . . 7 (seq1( + , 𝐹):β„•βŸΆβ„ β†’ ran seq1( + , 𝐹) βŠ† ℝ)
1412, 13mp1i 13 . . . . . 6 (seq1( + , 𝐹) ∈ dom ⇝ β†’ ran seq1( + , 𝐹) βŠ† ℝ)
15 1nn 12223 . . . . . . . 8 1 ∈ β„•
1612fdmi 6730 . . . . . . . 8 dom seq1( + , 𝐹) = β„•
1715, 16eleqtrri 2833 . . . . . . 7 1 ∈ dom seq1( + , 𝐹)
18 ne0i 4335 . . . . . . . 8 (1 ∈ dom seq1( + , 𝐹) β†’ dom seq1( + , 𝐹) β‰  βˆ…)
19 dm0rn0 5925 . . . . . . . . 9 (dom seq1( + , 𝐹) = βˆ… ↔ ran seq1( + , 𝐹) = βˆ…)
2019necon3bii 2994 . . . . . . . 8 (dom seq1( + , 𝐹) β‰  βˆ… ↔ ran seq1( + , 𝐹) β‰  βˆ…)
2118, 20sylib 217 . . . . . . 7 (1 ∈ dom seq1( + , 𝐹) β†’ ran seq1( + , 𝐹) β‰  βˆ…)
2217, 21mp1i 13 . . . . . 6 (seq1( + , 𝐹) ∈ dom ⇝ β†’ ran seq1( + , 𝐹) β‰  βˆ…)
23 1zzd 12593 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ β†’ 1 ∈ β„€)
24 climdm 15498 . . . . . . . . . 10 (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
2524biimpi 215 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ β†’ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
2612a1i 11 . . . . . . . . . 10 (seq1( + , 𝐹) ∈ dom ⇝ β†’ seq1( + , 𝐹):β„•βŸΆβ„)
2726ffvelcdmda 7087 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) ∈ ℝ)
281, 23, 25, 27climrecl 15527 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ β†’ ( ⇝ β€˜seq1( + , 𝐹)) ∈ ℝ)
29 simpr 486 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
3025adantr 482 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
31 eleq1w 2817 . . . . . . . . . . . . . . 15 (𝑛 = 𝑗 β†’ (𝑛 ∈ β„™ ↔ 𝑗 ∈ β„™))
32 oveq2 7417 . . . . . . . . . . . . . . 15 (𝑛 = 𝑗 β†’ (1 / 𝑛) = (1 / 𝑗))
3331, 32ifbieq1d 4553 . . . . . . . . . . . . . 14 (𝑛 = 𝑗 β†’ if(𝑛 ∈ β„™, (1 / 𝑛), 0) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
34 prmnn 16611 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„™ β†’ 𝑗 ∈ β„•)
3534adantl 483 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ 𝑗 ∈ β„™) β†’ 𝑗 ∈ β„•)
3635nnrecred 12263 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ 𝑗 ∈ β„™) β†’ (1 / 𝑗) ∈ ℝ)
375a1i 11 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ Β¬ 𝑗 ∈ β„™) β†’ 0 ∈ ℝ)
3836, 37ifclda 4564 . . . . . . . . . . . . . . . 16 (⊀ β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
3938mptru 1549 . . . . . . . . . . . . . . 15 if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ
4039elexi 3494 . . . . . . . . . . . . . 14 if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ V
4133, 8, 40fvmpt 6999 . . . . . . . . . . . . 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 12985 . . . . . . . . . . . . . . . 16 (𝑗 ∈ β„• β†’ 𝑗 ∈ ℝ+)
4746adantl 483 . . . . . . . . . . . . . . 15 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ ℝ+)
4847rpreccld 13026 . . . . . . . . . . . . . 14 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ (1 / 𝑗) ∈ ℝ+)
4948rpge0d 13020 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (1 / 𝑗))
50 0le0 12313 . . . . . . . . . . . . 13 0 ≀ 0
51 breq2 5153 . . . . . . . . . . . . . 14 ((1 / 𝑗) = if(𝑗 ∈ β„™, (1 / 𝑗), 0) β†’ (0 ≀ (1 / 𝑗) ↔ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
52 breq2 5153 . . . . . . . . . . . . . 14 (0 = if(𝑗 ∈ β„™, (1 / 𝑗), 0) β†’ (0 ≀ 0 ↔ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
5351, 52ifboth 4568 . . . . . . . . . . . . 13 ((0 ≀ (1 / 𝑗) ∧ 0 ≀ 0) β†’ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0))
5449, 50, 53sylancl 587 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0))
5554, 42breqtrrd 5177 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (πΉβ€˜π‘—))
5655adantlr 714 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (πΉβ€˜π‘—))
571, 29, 30, 45, 56climserle 15609 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) ≀ ( ⇝ β€˜seq1( + , 𝐹)))
5857ralrimiva 3147 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ β†’ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ ( ⇝ β€˜seq1( + , 𝐹)))
59 brralrspcev 5209 . . . . . . . 8 ((( ⇝ β€˜seq1( + , 𝐹)) ∈ ℝ ∧ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ ( ⇝ β€˜seq1( + , 𝐹))) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯)
6028, 58, 59syl2anc 585 . . . . . . 7 (seq1( + , 𝐹) ∈ dom ⇝ β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯)
61 ffn 6718 . . . . . . . . 9 (seq1( + , 𝐹):β„•βŸΆβ„ β†’ seq1( + , 𝐹) Fn β„•)
62 breq1 5152 . . . . . . . . . 10 (𝑧 = (seq1( + , 𝐹)β€˜π‘˜) β†’ (𝑧 ≀ π‘₯ ↔ (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯))
6362ralrn 7090 . . . . . . . . 9 (seq1( + , 𝐹) Fn β„• β†’ (βˆ€π‘§ ∈ ran seq1( + , 𝐹)𝑧 ≀ π‘₯ ↔ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯))
6412, 61, 63mp2b 10 . . . . . . . 8 (βˆ€π‘§ ∈ ran seq1( + , 𝐹)𝑧 ≀ π‘₯ ↔ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯)
6564rexbii 3095 . . . . . . 7 (βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran seq1( + , 𝐹)𝑧 ≀ π‘₯ ↔ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯)
6660, 65sylibr 233 . . . . . 6 (seq1( + , 𝐹) ∈ dom ⇝ β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘§ ∈ ran seq1( + , 𝐹)𝑧 ≀ π‘₯)
6714, 22, 66suprcld 12177 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ β†’ sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
68 2rp 12979 . . . . . 6 2 ∈ ℝ+
69 rpreccl 13000 . . . . . 6 (2 ∈ ℝ+ β†’ (1 / 2) ∈ ℝ+)
7068, 69ax-mp 5 . . . . 5 (1 / 2) ∈ ℝ+
71 ltsubrp 13010 . . . . 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 12426 . . . . . 6 (1 / 2) ∈ ℝ
74 resubcl 11524 . . . . . 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 12178 . . . . 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 5153 . . . . 5 (𝑦 = (seq1( + , 𝐹)β€˜π‘˜) β†’ ((sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < 𝑦 ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜)))
8079rexrn 7089 . . . 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 12286 . . . . . 6 2 ∈ ℝ
84 2nn 12285 . . . . . . . . 9 2 ∈ β„•
85 nnmulcl 12236 . . . . . . . . 9 ((2 ∈ β„• ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„•)
8684, 29, 85sylancr 588 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„•)
8786peano2nnd 12229 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
8887nnnn0d 12532 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
89 reexpcl 14044 . . . . . 6 ((2 ∈ ℝ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ ℝ)
9083, 88, 89sylancr 588 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ ℝ)
9190ltnrd 11348 . . . 4 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Β¬ (2↑((2 Β· π‘˜) + 1)) < (2↑((2 Β· π‘˜) + 1)))
9229adantr 482 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ π‘˜ ∈ β„•)
93 peano2nn 12224 . . . . . . . . . . . 12 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
9493adantl 483 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„•)
9594nnnn0d 12532 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„•0)
96 nnexpcl 14040 . . . . . . . . . 10 ((2 ∈ β„• ∧ (π‘˜ + 1) ∈ β„•0) β†’ (2↑(π‘˜ + 1)) ∈ β„•)
9784, 95, 96sylancr 588 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(π‘˜ + 1)) ∈ β„•)
9897nnsqcld 14207 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2↑(π‘˜ + 1))↑2) ∈ β„•)
9998adantr 482 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ ((2↑(π‘˜ + 1))↑2) ∈ β„•)
100 breq1 5152 . . . . . . . . . . 11 (𝑝 = 𝑀 β†’ (𝑝 βˆ₯ π‘Ÿ ↔ 𝑀 βˆ₯ π‘Ÿ))
101100notbid 318 . . . . . . . . . 10 (𝑝 = 𝑀 β†’ (Β¬ 𝑝 βˆ₯ π‘Ÿ ↔ Β¬ 𝑀 βˆ₯ π‘Ÿ))
102101cbvralvw 3235 . . . . . . . . 9 (βˆ€π‘ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑝 βˆ₯ π‘Ÿ ↔ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ π‘Ÿ)
103 breq2 5153 . . . . . . . . . . 11 (π‘Ÿ = 𝑛 β†’ (𝑀 βˆ₯ π‘Ÿ ↔ 𝑀 βˆ₯ 𝑛))
104103notbid 318 . . . . . . . . . 10 (π‘Ÿ = 𝑛 β†’ (Β¬ 𝑀 βˆ₯ π‘Ÿ ↔ Β¬ 𝑀 βˆ₯ 𝑛))
105104ralbidv 3178 . . . . . . . . 9 (π‘Ÿ = 𝑛 β†’ (βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ π‘Ÿ ↔ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ 𝑛))
106102, 105bitrid 283 . . . . . . . 8 (π‘Ÿ = 𝑛 β†’ (βˆ€π‘ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑝 βˆ₯ π‘Ÿ ↔ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ 𝑛))
107106cbvrabv 3443 . . . . . . 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 7417 . . . . . . . . . 10 (π‘š = 𝑗 β†’ (1 / π‘š) = (1 / 𝑗))
111109, 110ifbieq1d 4553 . . . . . . . . 9 (π‘š = 𝑗 β†’ if(π‘š ∈ β„™, (1 / π‘š), 0) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
112111cbvsumv 15642 . . . . . . . 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 5184 . . . . . . 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 16853 . . . . . 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 12585 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„€)
120 eluznn 12902 . . . . . . . . . . 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 11228 . . . . . . . . . . . . 13 if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ β„‚
127126a1i 11 . . . . . . . . . . . 12 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ β„‚)
128125, 127eqeltrd 2834 . . . . . . . . . . 11 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ β„‚)
1291, 94, 128iserex 15603 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(π‘˜ + 1)( + , 𝐹) ∈ dom ⇝ ))
130124, 129mpbid 231 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ seq(π‘˜ + 1)( + , 𝐹) ∈ dom ⇝ )
131118, 119, 122, 123, 130isumrecl 15711 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
13273a1i 11 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (1 / 2) ∈ ℝ)
133 elfznn 13530 . . . . . . . . . . . 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 15676 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) = (seq1( + , 𝐹)β€˜π‘˜))
139138, 27eqeltrd 2834 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
140131, 132, 139ltadd2d 11370 . . . . . . 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 15786 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...((π‘˜ + 1) βˆ’ 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) + Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
142 nncn 12220 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
143142adantl 483 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„‚)
144 ax-1cn 11168 . . . . . . . . . . . . 13 1 ∈ β„‚
145 pncan 11466 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
146143, 144, 145sylancl 587 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
147146oveq2d 7425 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (1...((π‘˜ + 1) βˆ’ 1)) = (1...π‘˜))
148147sumeq1d 15647 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...((π‘˜ + 1) βˆ’ 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) = Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0))
149148oveq1d 7424 . . . . . . . . 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 5159 . . . . . . 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 15793 . . . . . . . . 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 11810 . . . . . 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 7424 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) βˆ’ (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)))
160159, 138breq12d 5162 . . . . . 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 12287 . . . . . . . . . . . . 13 2 ∈ β„‚
163162a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ 2 ∈ β„‚)
164144a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ 1 ∈ β„‚)
165163, 143, 164adddid 11238 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (π‘˜ + 1)) = ((2 Β· π‘˜) + (2 Β· 1)))
16694nncnd 12228 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„‚)
167 mulcom 11196 . . . . . . . . . . . 12 (((π‘˜ + 1) ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((π‘˜ + 1) Β· 2) = (2 Β· (π‘˜ + 1)))
168166, 162, 167sylancl 587 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) Β· 2) = (2 Β· (π‘˜ + 1)))
16986nncnd 12228 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„‚)
170169, 164, 164addassd 11236 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2 Β· π‘˜) + 1) + 1) = ((2 Β· π‘˜) + (1 + 1)))
1711442timesi 12350 . . . . . . . . . . . . 13 (2 Β· 1) = (1 + 1)
172171oveq2i 7420 . . . . . . . . . . . 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 7425 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((π‘˜ + 1) Β· 2)) = (2↑(((2 Β· π‘˜) + 1) + 1)))
176 2nn0 12489 . . . . . . . . . . 11 2 ∈ β„•0
177176a1i 11 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ 2 ∈ β„•0)
178163, 177, 95expmuld 14114 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((π‘˜ + 1) Β· 2)) = ((2↑(π‘˜ + 1))↑2))
179 expp1 14034 . . . . . . . . . 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 7424 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2↑(π‘˜ + 1))↑2) / 2) = (((2↑((2 Β· π‘˜) + 1)) Β· 2) / 2))
183 expcl 14045 . . . . . . . . 9 ((2 ∈ β„‚ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ β„‚)
184162, 88, 183sylancr 588 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ β„‚)
185 2ne0 12316 . . . . . . . . 9 2 β‰  0
186 divcan4 11899 . . . . . . . . 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 12479 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0)
191190adantl 483 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•0)
192163, 95, 191expaddd 14113 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(π‘˜ + (π‘˜ + 1))) = ((2β†‘π‘˜) Β· (2↑(π‘˜ + 1))))
1931432timesd 12455 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) = (π‘˜ + π‘˜))
194193oveq1d 7424 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) = ((π‘˜ + π‘˜) + 1))
195143, 143, 164addassd 11236 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + π‘˜) + 1) = (π‘˜ + (π‘˜ + 1)))
196194, 195eqtrd 2773 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) = (π‘˜ + (π‘˜ + 1)))
197196oveq2d 7425 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((2 Β· π‘˜) + 1)) = (2↑(π‘˜ + (π‘˜ + 1))))
19897nnrpd 13014 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(π‘˜ + 1)) ∈ ℝ+)
199198rprege0d 13023 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2↑(π‘˜ + 1)) ∈ ℝ ∧ 0 ≀ (2↑(π‘˜ + 1))))
200 sqrtsq 15216 . . . . . . . . 9 (((2↑(π‘˜ + 1)) ∈ ℝ ∧ 0 ≀ (2↑(π‘˜ + 1))) β†’ (βˆšβ€˜((2↑(π‘˜ + 1))↑2)) = (2↑(π‘˜ + 1)))
201199, 200syl 17 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (βˆšβ€˜((2↑(π‘˜ + 1))↑2)) = (2↑(π‘˜ + 1)))
202201oveq2d 7425 . . . . . . 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 5162 . . . . 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 3150 . 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 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433   βˆ– cdif 3946   βŠ† wss 3949  βˆ…c0 4323  ifcif 4529   class class class wbr 5149   ↦ cmpt 5232  dom cdm 5677  ran crn 5678   Fn wfn 6539  βŸΆwf 6540  β€˜cfv 6544  (class class class)co 7409  supcsup 9435  β„‚cc 11108  β„cr 11109  0cc0 11110  1c1 11111   + caddc 11113   Β· cmul 11115   < clt 11248   ≀ cle 11249   βˆ’ cmin 11444   / cdiv 11871  β„•cn 12212  2c2 12267  β„•0cn0 12472  β„€β‰₯cuz 12822  β„+crp 12974  ...cfz 13484  seqcseq 13966  β†‘cexp 14027  βˆšcsqrt 15180   ⇝ cli 15428  Ξ£csu 15632   βˆ₯ cdvds 16197  β„™cprime 16608
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 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
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 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-2o 8467  df-oadd 8470  df-er 8703  df-map 8822  df-pm 8823  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-inf 9438  df-oi 9505  df-dju 9896  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-n0 12473  df-xnn0 12545  df-z 12559  df-uz 12823  df-q 12933  df-rp 12975  df-fz 13485  df-fzo 13628  df-fl 13757  df-mod 13835  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-rlim 15433  df-sum 15633  df-dvds 16198  df-gcd 16436  df-prm 16609  df-pc 16770
This theorem is referenced by:  prmrec  16855
  Copyright terms: Public domain W3C validator