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

Theorem prmreclem6 16853
Description: Lemma for prmrec 16854. 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 16852 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 12864 . . . . . . . . 9 β„• = (β„€β‰₯β€˜1)
2 1zzd 12592 . . . . . . . . 9 (⊀ β†’ 1 ∈ β„€)
3 nnrecre 12253 . . . . . . . . . . . . 13 (𝑛 ∈ β„• β†’ (1 / 𝑛) ∈ ℝ)
43adantl 482 . . . . . . . . . . . 12 ((⊀ ∧ 𝑛 ∈ β„•) β†’ (1 / 𝑛) ∈ ℝ)
5 0re 11215 . . . . . . . . . . . 12 0 ∈ ℝ
6 ifcl 4573 . . . . . . . . . . . 12 (((1 / 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) β†’ if(𝑛 ∈ β„™, (1 / 𝑛), 0) ∈ ℝ)
74, 5, 6sylancl 586 . . . . . . . . . . 11 ((⊀ ∧ 𝑛 ∈ β„•) β†’ if(𝑛 ∈ β„™, (1 / 𝑛), 0) ∈ ℝ)
8 prmrec.1 . . . . . . . . . . 11 𝐹 = (𝑛 ∈ β„• ↦ if(𝑛 ∈ β„™, (1 / 𝑛), 0))
97, 8fmptd 7113 . . . . . . . . . 10 (⊀ β†’ 𝐹:β„•βŸΆβ„)
109ffvelcdmda 7086 . . . . . . . . 9 ((⊀ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ ℝ)
111, 2, 10serfre 13996 . . . . . . . 8 (⊀ β†’ seq1( + , 𝐹):β„•βŸΆβ„)
1211mptru 1548 . . . . . . 7 seq1( + , 𝐹):β„•βŸΆβ„
13 frn 6724 . . . . . . 7 (seq1( + , 𝐹):β„•βŸΆβ„ β†’ ran seq1( + , 𝐹) βŠ† ℝ)
1412, 13mp1i 13 . . . . . 6 (seq1( + , 𝐹) ∈ dom ⇝ β†’ ran seq1( + , 𝐹) βŠ† ℝ)
15 1nn 12222 . . . . . . . 8 1 ∈ β„•
1612fdmi 6729 . . . . . . . 8 dom seq1( + , 𝐹) = β„•
1715, 16eleqtrri 2832 . . . . . . 7 1 ∈ dom seq1( + , 𝐹)
18 ne0i 4334 . . . . . . . 8 (1 ∈ dom seq1( + , 𝐹) β†’ dom seq1( + , 𝐹) β‰  βˆ…)
19 dm0rn0 5924 . . . . . . . . 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 12592 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ β†’ 1 ∈ β„€)
24 climdm 15497 . . . . . . . . . 10 (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
2524biimpi 215 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ β†’ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
2612a1i 11 . . . . . . . . . 10 (seq1( + , 𝐹) ∈ dom ⇝ β†’ seq1( + , 𝐹):β„•βŸΆβ„)
2726ffvelcdmda 7086 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) ∈ ℝ)
281, 23, 25, 27climrecl 15526 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ β†’ ( ⇝ β€˜seq1( + , 𝐹)) ∈ ℝ)
29 simpr 485 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•)
3025adantr 481 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ seq1( + , 𝐹) ⇝ ( ⇝ β€˜seq1( + , 𝐹)))
31 eleq1w 2816 . . . . . . . . . . . . . . 15 (𝑛 = 𝑗 β†’ (𝑛 ∈ β„™ ↔ 𝑗 ∈ β„™))
32 oveq2 7416 . . . . . . . . . . . . . . 15 (𝑛 = 𝑗 β†’ (1 / 𝑛) = (1 / 𝑗))
3331, 32ifbieq1d 4552 . . . . . . . . . . . . . 14 (𝑛 = 𝑗 β†’ if(𝑛 ∈ β„™, (1 / 𝑛), 0) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
34 prmnn 16610 . . . . . . . . . . . . . . . . . . 19 (𝑗 ∈ β„™ β†’ 𝑗 ∈ β„•)
3534adantl 482 . . . . . . . . . . . . . . . . . 18 ((⊀ ∧ 𝑗 ∈ β„™) β†’ 𝑗 ∈ β„•)
3635nnrecred 12262 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ 𝑗 ∈ β„™) β†’ (1 / 𝑗) ∈ ℝ)
375a1i 11 . . . . . . . . . . . . . . . . 17 ((⊀ ∧ Β¬ 𝑗 ∈ β„™) β†’ 0 ∈ ℝ)
3836, 37ifclda 4563 . . . . . . . . . . . . . . . 16 (⊀ β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
3938mptru 1548 . . . . . . . . . . . . . . 15 if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ
4039elexi 3493 . . . . . . . . . . . . . 14 if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ V
4133, 8, 40fvmpt 6998 . . . . . . . . . . . . 13 (𝑗 ∈ β„• β†’ (πΉβ€˜π‘—) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
4241adantl 482 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
4339a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
4442, 43eqeltrd 2833 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ ℝ)
4544adantlr 713 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ ℝ)
46 nnrp 12984 . . . . . . . . . . . . . . . 16 (𝑗 ∈ β„• β†’ 𝑗 ∈ ℝ+)
4746adantl 482 . . . . . . . . . . . . . . 15 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 𝑗 ∈ ℝ+)
4847rpreccld 13025 . . . . . . . . . . . . . 14 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ (1 / 𝑗) ∈ ℝ+)
4948rpge0d 13019 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (1 / 𝑗))
50 0le0 12312 . . . . . . . . . . . . 13 0 ≀ 0
51 breq2 5152 . . . . . . . . . . . . . 14 ((1 / 𝑗) = if(𝑗 ∈ β„™, (1 / 𝑗), 0) β†’ (0 ≀ (1 / 𝑗) ↔ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
52 breq2 5152 . . . . . . . . . . . . . 14 (0 = if(𝑗 ∈ β„™, (1 / 𝑗), 0) β†’ (0 ≀ 0 ↔ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
5351, 52ifboth 4567 . . . . . . . . . . . . 13 ((0 ≀ (1 / 𝑗) ∧ 0 ≀ 0) β†’ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0))
5449, 50, 53sylancl 586 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 0 ≀ if(𝑗 ∈ β„™, (1 / 𝑗), 0))
5554, 42breqtrrd 5176 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (πΉβ€˜π‘—))
5655adantlr 713 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ 0 ≀ (πΉβ€˜π‘—))
571, 29, 30, 45, 56climserle 15608 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹)β€˜π‘˜) ≀ ( ⇝ β€˜seq1( + , 𝐹)))
5857ralrimiva 3146 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ β†’ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ ( ⇝ β€˜seq1( + , 𝐹)))
59 brralrspcev 5208 . . . . . . . 8 ((( ⇝ β€˜seq1( + , 𝐹)) ∈ ℝ ∧ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ ( ⇝ β€˜seq1( + , 𝐹))) β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯)
6028, 58, 59syl2anc 584 . . . . . . 7 (seq1( + , 𝐹) ∈ dom ⇝ β†’ βˆƒπ‘₯ ∈ ℝ βˆ€π‘˜ ∈ β„• (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯)
61 ffn 6717 . . . . . . . . 9 (seq1( + , 𝐹):β„•βŸΆβ„ β†’ seq1( + , 𝐹) Fn β„•)
62 breq1 5151 . . . . . . . . . 10 (𝑧 = (seq1( + , 𝐹)β€˜π‘˜) β†’ (𝑧 ≀ π‘₯ ↔ (seq1( + , 𝐹)β€˜π‘˜) ≀ π‘₯))
6362ralrn 7089 . . . . . . . . 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 12176 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ β†’ sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
68 2rp 12978 . . . . . 6 2 ∈ ℝ+
69 rpreccl 12999 . . . . . 6 (2 ∈ ℝ+ β†’ (1 / 2) ∈ ℝ+)
7068, 69ax-mp 5 . . . . 5 (1 / 2) ∈ ℝ+
71 ltsubrp 13009 . . . . 5 ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ+) β†’ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
7267, 70, 71sylancl 586 . . . 4 (seq1( + , 𝐹) ∈ dom ⇝ β†’ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
73 halfre 12425 . . . . . 6 (1 / 2) ∈ ℝ
74 resubcl 11523 . . . . . 6 ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ) β†’ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) ∈ ℝ)
7567, 73, 74sylancl 586 . . . . 5 (seq1( + , 𝐹) ∈ dom ⇝ β†’ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) ∈ ℝ)
76 suprlub 12177 . . . . 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 1373 . . . 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 5152 . . . . 5 (𝑦 = (seq1( + , 𝐹)β€˜π‘˜) β†’ ((sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < 𝑦 ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜)))
8079rexrn 7088 . . . 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 12285 . . . . . 6 2 ∈ ℝ
84 2nn 12284 . . . . . . . . 9 2 ∈ β„•
85 nnmulcl 12235 . . . . . . . . 9 ((2 ∈ β„• ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„•)
8684, 29, 85sylancr 587 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„•)
8786peano2nnd 12228 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
8887nnnn0d 12531 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
89 reexpcl 14043 . . . . . 6 ((2 ∈ ℝ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ ℝ)
9083, 88, 89sylancr 587 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ ℝ)
9190ltnrd 11347 . . . 4 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Β¬ (2↑((2 Β· π‘˜) + 1)) < (2↑((2 Β· π‘˜) + 1)))
9229adantr 481 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ π‘˜ ∈ β„•)
93 peano2nn 12223 . . . . . . . . . . . 12 (π‘˜ ∈ β„• β†’ (π‘˜ + 1) ∈ β„•)
9493adantl 482 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„•)
9594nnnn0d 12531 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„•0)
96 nnexpcl 14039 . . . . . . . . . 10 ((2 ∈ β„• ∧ (π‘˜ + 1) ∈ β„•0) β†’ (2↑(π‘˜ + 1)) ∈ β„•)
9784, 95, 96sylancr 587 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(π‘˜ + 1)) ∈ β„•)
9897nnsqcld 14206 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2↑(π‘˜ + 1))↑2) ∈ β„•)
9998adantr 481 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ ((2↑(π‘˜ + 1))↑2) ∈ β„•)
100 breq1 5151 . . . . . . . . . . 11 (𝑝 = 𝑀 β†’ (𝑝 βˆ₯ π‘Ÿ ↔ 𝑀 βˆ₯ π‘Ÿ))
101100notbid 317 . . . . . . . . . 10 (𝑝 = 𝑀 β†’ (Β¬ 𝑝 βˆ₯ π‘Ÿ ↔ Β¬ 𝑀 βˆ₯ π‘Ÿ))
102101cbvralvw 3234 . . . . . . . . 9 (βˆ€π‘ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑝 βˆ₯ π‘Ÿ ↔ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ π‘Ÿ)
103 breq2 5152 . . . . . . . . . . 11 (π‘Ÿ = 𝑛 β†’ (𝑀 βˆ₯ π‘Ÿ ↔ 𝑀 βˆ₯ 𝑛))
104103notbid 317 . . . . . . . . . 10 (π‘Ÿ = 𝑛 β†’ (Β¬ 𝑀 βˆ₯ π‘Ÿ ↔ Β¬ 𝑀 βˆ₯ 𝑛))
105104ralbidv 3177 . . . . . . . . 9 (π‘Ÿ = 𝑛 β†’ (βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ π‘Ÿ ↔ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ 𝑛))
106102, 105bitrid 282 . . . . . . . 8 (π‘Ÿ = 𝑛 β†’ (βˆ€π‘ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑝 βˆ₯ π‘Ÿ ↔ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ 𝑛))
107106cbvrabv 3442 . . . . . . 7 {π‘Ÿ ∈ (1...((2↑(π‘˜ + 1))↑2)) ∣ βˆ€π‘ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑝 βˆ₯ π‘Ÿ} = {𝑛 ∈ (1...((2↑(π‘˜ + 1))↑2)) ∣ βˆ€π‘€ ∈ (β„™ βˆ– (1...π‘˜)) Β¬ 𝑀 βˆ₯ 𝑛}
108 simpll 765 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ seq1( + , 𝐹) ∈ dom ⇝ )
109 eleq1w 2816 . . . . . . . . . 10 (π‘š = 𝑗 β†’ (π‘š ∈ β„™ ↔ 𝑗 ∈ β„™))
110 oveq2 7416 . . . . . . . . . 10 (π‘š = 𝑗 β†’ (1 / π‘š) = (1 / 𝑗))
111109, 110ifbieq1d 4552 . . . . . . . . 9 (π‘š = 𝑗 β†’ if(π‘š ∈ β„™, (1 / π‘š), 0) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
112111cbvsumv 15641 . . . . . . . 8 Ξ£π‘š ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(π‘š ∈ β„™, (1 / π‘š), 0) = Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)
113 simpr 485 . . . . . . . 8 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2))
114112, 113eqbrtrid 5183 . . . . . . 7 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ Ξ£π‘š ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(π‘š ∈ β„™, (1 / π‘š), 0) < (1 / 2))
115 eqid 2732 . . . . . . 7 (𝑀 ∈ β„• ↦ {𝑛 ∈ (1...((2↑(π‘˜ + 1))↑2)) ∣ (𝑀 ∈ β„™ ∧ 𝑀 βˆ₯ 𝑛)}) = (𝑀 ∈ β„• ↦ {𝑛 ∈ (1...((2↑(π‘˜ + 1))↑2)) ∣ (𝑀 ∈ β„™ ∧ 𝑀 βˆ₯ 𝑛)})
1168, 92, 99, 107, 108, 114, 115prmreclem5 16852 . . . . . 6 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2)) β†’ (((2↑(π‘˜ + 1))↑2) / 2) < ((2β†‘π‘˜) Β· (βˆšβ€˜((2↑(π‘˜ + 1))↑2))))
117116ex 413 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2) β†’ (((2↑(π‘˜ + 1))↑2) / 2) < ((2β†‘π‘˜) Β· (βˆšβ€˜((2↑(π‘˜ + 1))↑2)))))
118 eqid 2732 . . . . . . . . 9 (β„€β‰₯β€˜(π‘˜ + 1)) = (β„€β‰₯β€˜(π‘˜ + 1))
11994nnzd 12584 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„€)
120 eluznn 12901 . . . . . . . . . . 11 (((π‘˜ + 1) ∈ β„• ∧ 𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))) β†’ 𝑗 ∈ β„•)
12194, 120sylan 580 . . . . . . . . . 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 483 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ seq1( + , 𝐹) ∈ dom ⇝ )
12541adantl 482 . . . . . . . . . . . 12 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
12639recni 11227 . . . . . . . . . . . . 13 if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ β„‚
127126a1i 11 . . . . . . . . . . . 12 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ β„‚)
128125, 127eqeltrd 2833 . . . . . . . . . . 11 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ β„•) β†’ (πΉβ€˜π‘—) ∈ β„‚)
1291, 94, 128iserex 15602 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(π‘˜ + 1)( + , 𝐹) ∈ dom ⇝ ))
130124, 129mpbid 231 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ seq(π‘˜ + 1)( + , 𝐹) ∈ dom ⇝ )
131118, 119, 122, 123, 130isumrecl 15710 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
13273a1i 11 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (1 / 2) ∈ ℝ)
133 elfznn 13529 . . . . . . . . . . . 12 (𝑗 ∈ (1...π‘˜) β†’ 𝑗 ∈ β„•)
134133adantl 482 . . . . . . . . . . 11 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...π‘˜)) β†’ 𝑗 ∈ β„•)
135134, 41syl 17 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...π‘˜)) β†’ (πΉβ€˜π‘—) = if(𝑗 ∈ β„™, (1 / 𝑗), 0))
13629, 1eleqtrdi 2843 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ (β„€β‰₯β€˜1))
137126a1i 11 . . . . . . . . . 10 (((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) ∧ 𝑗 ∈ (1...π‘˜)) β†’ if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ β„‚)
138135, 136, 137fsumser 15675 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) = (seq1( + , 𝐹)β€˜π‘˜))
139138, 27eqeltrd 2833 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
140131, 132, 139ltadd2d 11369 . . . . . . 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 15785 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...((π‘˜ + 1) βˆ’ 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) + Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
142 nncn 12219 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„‚)
143142adantl 482 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„‚)
144 ax-1cn 11167 . . . . . . . . . . . . 13 1 ∈ β„‚
145 pncan 11465 . . . . . . . . . . . . 13 ((π‘˜ ∈ β„‚ ∧ 1 ∈ β„‚) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
146143, 144, 145sylancl 586 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) βˆ’ 1) = π‘˜)
147146oveq2d 7424 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (1...((π‘˜ + 1) βˆ’ 1)) = (1...π‘˜))
148147sumeq1d 15646 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ (1...((π‘˜ + 1) βˆ’ 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) = Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0))
149148oveq1d 7423 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ (1...((π‘˜ + 1) βˆ’ 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) + Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)) = (Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) + Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
150141, 149eqtrd 2772 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) + Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0)))
151150breq1d 5158 . . . . . . 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 281 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2) ↔ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) + (1 / 2))))
153 eqid 2732 . . . . . . . . . 10 seq1( + , 𝐹) = seq1( + , 𝐹)
1541, 153, 23, 42, 43, 54, 60isumsup 15792 . . . . . . . . 9 (seq1( + , 𝐹) ∈ dom ⇝ β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
155154, 67eqeltrd 2833 . . . . . . . 8 (seq1( + , 𝐹) ∈ dom ⇝ β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
156155adantr 481 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) ∈ ℝ)
157156, 132, 139ltsubaddd 11809 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) βˆ’ (1 / 2)) < Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) ↔ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) + (1 / 2))))
158154adantr 481 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
159158oveq1d 7423 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) βˆ’ (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)))
160159, 138breq12d 5161 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((Σ𝑗 ∈ β„• if(𝑗 ∈ β„™, (1 / 𝑗), 0) βˆ’ (1 / 2)) < Σ𝑗 ∈ (1...π‘˜)if(𝑗 ∈ β„™, (1 / 𝑗), 0) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜)))
161152, 157, 1603bitr2d 306 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (Σ𝑗 ∈ (β„€β‰₯β€˜(π‘˜ + 1))if(𝑗 ∈ β„™, (1 / 𝑗), 0) < (1 / 2) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) βˆ’ (1 / 2)) < (seq1( + , 𝐹)β€˜π‘˜)))
162 2cn 12286 . . . . . . . . . . . . 13 2 ∈ β„‚
163162a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ 2 ∈ β„‚)
164144a1i 11 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ 1 ∈ β„‚)
165163, 143, 164adddid 11237 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· (π‘˜ + 1)) = ((2 Β· π‘˜) + (2 Β· 1)))
16694nncnd 12227 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (π‘˜ + 1) ∈ β„‚)
167 mulcom 11195 . . . . . . . . . . . 12 (((π‘˜ + 1) ∈ β„‚ ∧ 2 ∈ β„‚) β†’ ((π‘˜ + 1) Β· 2) = (2 Β· (π‘˜ + 1)))
168166, 162, 167sylancl 586 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) Β· 2) = (2 Β· (π‘˜ + 1)))
16986nncnd 12227 . . . . . . . . . . . . 13 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) ∈ β„‚)
170169, 164, 164addassd 11235 . . . . . . . . . . . 12 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2 Β· π‘˜) + 1) + 1) = ((2 Β· π‘˜) + (1 + 1)))
1711442timesi 12349 . . . . . . . . . . . . 13 (2 Β· 1) = (1 + 1)
172171oveq2i 7419 . . . . . . . . . . . 12 ((2 Β· π‘˜) + (2 Β· 1)) = ((2 Β· π‘˜) + (1 + 1))
173170, 172eqtr4di 2790 . . . . . . . . . . 11 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2 Β· π‘˜) + 1) + 1) = ((2 Β· π‘˜) + (2 Β· 1)))
174165, 168, 1733eqtr4d 2782 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + 1) Β· 2) = (((2 Β· π‘˜) + 1) + 1))
175174oveq2d 7424 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((π‘˜ + 1) Β· 2)) = (2↑(((2 Β· π‘˜) + 1) + 1)))
176 2nn0 12488 . . . . . . . . . . 11 2 ∈ β„•0
177176a1i 11 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ 2 ∈ β„•0)
178163, 177, 95expmuld 14113 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((π‘˜ + 1) Β· 2)) = ((2↑(π‘˜ + 1))↑2))
179 expp1 14033 . . . . . . . . . 10 ((2 ∈ β„‚ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (2↑(((2 Β· π‘˜) + 1) + 1)) = ((2↑((2 Β· π‘˜) + 1)) Β· 2))
180162, 88, 179sylancr 587 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(((2 Β· π‘˜) + 1) + 1)) = ((2↑((2 Β· π‘˜) + 1)) Β· 2))
181175, 178, 1803eqtr3d 2780 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2↑(π‘˜ + 1))↑2) = ((2↑((2 Β· π‘˜) + 1)) Β· 2))
182181oveq1d 7423 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2↑(π‘˜ + 1))↑2) / 2) = (((2↑((2 Β· π‘˜) + 1)) Β· 2) / 2))
183 expcl 14044 . . . . . . . . 9 ((2 ∈ β„‚ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ β„‚)
184162, 88, 183sylancr 587 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((2 Β· π‘˜) + 1)) ∈ β„‚)
185 2ne0 12315 . . . . . . . . 9 2 β‰  0
186 divcan4 11898 . . . . . . . . 9 (((2↑((2 Β· π‘˜) + 1)) ∈ β„‚ ∧ 2 ∈ β„‚ ∧ 2 β‰  0) β†’ (((2↑((2 Β· π‘˜) + 1)) Β· 2) / 2) = (2↑((2 Β· π‘˜) + 1)))
187162, 185, 186mp3an23 1453 . . . . . . . 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 2772 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (((2↑(π‘˜ + 1))↑2) / 2) = (2↑((2 Β· π‘˜) + 1)))
190 nnnn0 12478 . . . . . . . . 9 (π‘˜ ∈ β„• β†’ π‘˜ ∈ β„•0)
191190adantl 482 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ π‘˜ ∈ β„•0)
192163, 95, 191expaddd 14112 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(π‘˜ + (π‘˜ + 1))) = ((2β†‘π‘˜) Β· (2↑(π‘˜ + 1))))
1931432timesd 12454 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2 Β· π‘˜) = (π‘˜ + π‘˜))
194193oveq1d 7423 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) = ((π‘˜ + π‘˜) + 1))
195143, 143, 164addassd 11235 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((π‘˜ + π‘˜) + 1) = (π‘˜ + (π‘˜ + 1)))
196194, 195eqtrd 2772 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2 Β· π‘˜) + 1) = (π‘˜ + (π‘˜ + 1)))
197196oveq2d 7424 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑((2 Β· π‘˜) + 1)) = (2↑(π‘˜ + (π‘˜ + 1))))
19897nnrpd 13013 . . . . . . . . . 10 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (2↑(π‘˜ + 1)) ∈ ℝ+)
199198rprege0d 13022 . . . . . . . . 9 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2↑(π‘˜ + 1)) ∈ ℝ ∧ 0 ≀ (2↑(π‘˜ + 1))))
200 sqrtsq 15215 . . . . . . . . 9 (((2↑(π‘˜ + 1)) ∈ ℝ ∧ 0 ≀ (2↑(π‘˜ + 1))) β†’ (βˆšβ€˜((2↑(π‘˜ + 1))↑2)) = (2↑(π‘˜ + 1)))
201199, 200syl 17 . . . . . . . 8 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ (βˆšβ€˜((2↑(π‘˜ + 1))↑2)) = (2↑(π‘˜ + 1)))
202201oveq2d 7424 . . . . . . 7 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2β†‘π‘˜) Β· (βˆšβ€˜((2↑(π‘˜ + 1))↑2))) = ((2β†‘π‘˜) Β· (2↑(π‘˜ + 1))))
203192, 197, 2023eqtr4rd 2783 . . . . . 6 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((2β†‘π‘˜) Β· (βˆšβ€˜((2↑(π‘˜ + 1))↑2))) = (2↑((2 Β· π‘˜) + 1)))
204189, 203breq12d 5161 . . . . 5 ((seq1( + , 𝐹) ∈ dom ⇝ ∧ π‘˜ ∈ β„•) β†’ ((((2↑(π‘˜ + 1))↑2) / 2) < ((2β†‘π‘˜) Β· (βˆšβ€˜((2↑(π‘˜ + 1))↑2))) ↔ (2↑((2 Β· π‘˜) + 1)) < (2↑((2 Β· π‘˜) + 1))))
205117, 161, 2043imtr3d 292 . . . 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 3149 . 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 396   = wceq 1541  βŠ€wtru 1542   ∈ wcel 2106   β‰  wne 2940  βˆ€wral 3061  βˆƒwrex 3070  {crab 3432   βˆ– cdif 3945   βŠ† wss 3948  βˆ…c0 4322  ifcif 4528   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676  ran crn 5677   Fn wfn 6538  βŸΆwf 6539  β€˜cfv 6543  (class class class)co 7408  supcsup 9434  β„‚cc 11107  β„cr 11108  0cc0 11109  1c1 11110   + caddc 11112   Β· cmul 11114   < clt 11247   ≀ cle 11248   βˆ’ cmin 11443   / cdiv 11870  β„•cn 12211  2c2 12266  β„•0cn0 12471  β„€β‰₯cuz 12821  β„+crp 12973  ...cfz 13483  seqcseq 13965  β†‘cexp 14026  βˆšcsqrt 15179   ⇝ cli 15427  Ξ£csu 15631   βˆ₯ cdvds 16196  β„™cprime 16607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7724  ax-inf2 9635  ax-cnex 11165  ax-resscn 11166  ax-1cn 11167  ax-icn 11168  ax-addcl 11169  ax-addrcl 11170  ax-mulcl 11171  ax-mulrcl 11172  ax-mulcom 11173  ax-addass 11174  ax-mulass 11175  ax-distr 11176  ax-i2m1 11177  ax-1ne0 11178  ax-1rid 11179  ax-rnegex 11180  ax-rrecex 11181  ax-cnre 11182  ax-pre-lttri 11183  ax-pre-lttrn 11184  ax-pre-ltadd 11185  ax-pre-mulgt0 11186  ax-pre-sup 11187
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7364  df-ov 7411  df-oprab 7412  df-mpo 7413  df-om 7855  df-1st 7974  df-2nd 7975  df-frecs 8265  df-wrecs 8296  df-recs 8370  df-rdg 8409  df-1o 8465  df-2o 8466  df-oadd 8469  df-er 8702  df-map 8821  df-pm 8822  df-en 8939  df-dom 8940  df-sdom 8941  df-fin 8942  df-sup 9436  df-inf 9437  df-oi 9504  df-dju 9895  df-card 9933  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11445  df-neg 11446  df-div 11871  df-nn 12212  df-2 12274  df-3 12275  df-n0 12472  df-xnn0 12544  df-z 12558  df-uz 12822  df-q 12932  df-rp 12974  df-fz 13484  df-fzo 13627  df-fl 13756  df-mod 13834  df-seq 13966  df-exp 14027  df-hash 14290  df-cj 15045  df-re 15046  df-im 15047  df-sqrt 15181  df-abs 15182  df-clim 15431  df-rlim 15432  df-sum 15632  df-dvds 16197  df-gcd 16435  df-prm 16608  df-pc 16769
This theorem is referenced by:  prmrec  16854
  Copyright terms: Public domain W3C validator