# Metamath Proof Explorer

## Theorem prmreclem6

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

Ref Expression
Hypothesis prmrec.1 ${⊢}{F}=\left({n}\in ℕ⟼if\left({n}\in ℙ,\frac{1}{{n}},0\right)\right)$
Assertion prmreclem6 ${⊢}¬seq1\left(+,{F}\right)\in \mathrm{dom}⇝$

### Proof

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