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	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
Assertion	prmreclem6	⊢ ¬ seq 1 ( + , 𝐹 ) ∈ dom ⇝

Proof

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