prmreclem6 - Metamath Proof Explorer

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

Theorem prmreclem6 16833

Description: Lemma for prmrec 16834. 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 16832 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.

Step	Hyp	Ref	Expression
1		nnuz 12778	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
2		1zzd 12506	. . . . . . . . 9 ⊢ (⊤ → 1 ∈ ℤ)
3		nnrecre 12170	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
4	3	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
5		0re 11117	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
6		ifcl 4522	. . . . . . . . . . . 12 ⊢ (((1 / 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) ∈ ℝ)
7	4, 5, 6	sylancl 586	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) ∈ ℝ)
8		prmrec.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
9	7, 8	fmptd 7048	. . . . . . . . . 10 ⊢ (⊤ → 𝐹:ℕ⟶ℝ)
10	9	ffvelcdmda 7018	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
11	1, 2, 10	serfre 13938	. . . . . . . 8 ⊢ (⊤ → seq1( + , 𝐹):ℕ⟶ℝ)
12	11	mptru 1547	. . . . . . 7 ⊢ seq1( + , 𝐹):ℕ⟶ℝ
13		frn 6659	. . . . . . 7 ⊢ (seq1( + , 𝐹):ℕ⟶ℝ → ran seq1( + , 𝐹) ⊆ ℝ)
14	12, 13	mp1i 13	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ran seq1( + , 𝐹) ⊆ ℝ)
15		1nn 12139	. . . . . . . 8 ⊢ 1 ∈ ℕ
16	12	fdmi 6663	. . . . . . . 8 ⊢ dom seq1( + , 𝐹) = ℕ
17	15, 16	eleqtrri 2827	. . . . . . 7 ⊢ 1 ∈ dom seq1( + , 𝐹)
18		ne0i 4292	. . . . . . . 8 ⊢ (1 ∈ dom seq1( + , 𝐹) → dom seq1( + , 𝐹) ≠ ∅)
19		dm0rn0 5867	. . . . . . . . 9 ⊢ (dom seq1( + , 𝐹) = ∅ ↔ ran seq1( + , 𝐹) = ∅)
20	19	necon3bii 2977	. . . . . . . 8 ⊢ (dom seq1( + , 𝐹) ≠ ∅ ↔ ran seq1( + , 𝐹) ≠ ∅)
21	18, 20	sylib 218	. . . . . . 7 ⊢ (1 ∈ dom seq1( + , 𝐹) → ran seq1( + , 𝐹) ≠ ∅)
22	17, 21	mp1i 13	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ran seq1( + , 𝐹) ≠ ∅)
23		1zzd 12506	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → 1 ∈ ℤ)
24		climdm 15461	. . . . . . . . . 10 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
25	24	biimpi 216	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
26	12	a1i 11	. . . . . . . . . 10 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → seq1( + , 𝐹):ℕ⟶ℝ)
27	26	ffvelcdmda 7018	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℝ)
28	1, 23, 25, 27	climrecl 15490	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ)
29		simpr 484	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
30	25	adantr 480	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
31		eleq1w 2811	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ ℙ ↔ 𝑗 ∈ ℙ))
32		oveq2 7357	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗))
33	31, 32	ifbieq1d 4501	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
34		prmnn 16585	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℙ → 𝑗 ∈ ℕ)
35	34	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑗 ∈ ℙ) → 𝑗 ∈ ℕ)
36	35	nnrecred 12179	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑗 ∈ ℙ) → (1 / 𝑗) ∈ ℝ)
37	5	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ ¬ 𝑗 ∈ ℙ) → 0 ∈ ℝ)
38	36, 37	ifclda 4512	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
39	38	mptru 1547	. . . . . . . . . . . . . . 15 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ
40	39	elexi 3459	. . . . . . . . . . . . . 14 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ V
41	33, 8, 40	fvmpt 6930	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
42	41	adantl 481	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
43	39	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
44	42, 43	eqeltrd 2828	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
45	44	adantlr 715	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
46		nnrp 12905	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ⁺)
47	46	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℝ⁺)
48	47	rpreccld 12947	. . . . . . . . . . . . . 14 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (1 / 𝑗) ∈ ℝ⁺)
49	48	rpge0d 12941	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (1 / 𝑗))
50		0le0 12229	. . . . . . . . . . . . 13 ⊢ 0 ≤ 0
51		breq2 5096	. . . . . . . . . . . . . 14 ⊢ ((1 / 𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ (1 / 𝑗) ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
52		breq2 5096	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
53	51, 52	ifboth 4516	. . . . . . . . . . . . 13 ⊢ ((0 ≤ (1 / 𝑗) ∧ 0 ≤ 0) → 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
54	49, 50, 53	sylancl 586	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
55	54, 42	breqtrrd 5120	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹‘𝑗))
56	55	adantlr 715	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹‘𝑗))
57	1, 29, 30, 45, 56	climserle 15570	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
58	57	ralrimiva 3121	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
59		brralrspcev 5152	. . . . . . . 8 ⊢ ((( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
60	28, 58, 59	syl2anc 584	. . . . . . 7 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
61		ffn 6652	. . . . . . . . 9 ⊢ (seq1( + , 𝐹):ℕ⟶ℝ → seq1( + , 𝐹) Fn ℕ)
62		breq1 5095	. . . . . . . . . 10 ⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
63	62	ralrn 7022	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) Fn ℕ → (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
64	12, 61, 63	mp2b 10	. . . . . . . 8 ⊢ (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
65	64	rexbii 3076	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
66	60, 65	sylibr 234	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥)
67	14, 22, 66	suprcld 12088	. . . . 5 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
68		2rp 12898	. . . . . 6 ⊢ 2 ∈ ℝ⁺
69		rpreccl 12921	. . . . . 6 ⊢ (2 ∈ ℝ⁺ → (1 / 2) ∈ ℝ⁺)
70	68, 69	ax-mp 5	. . . . 5 ⊢ (1 / 2) ∈ ℝ⁺
71		ltsubrp 12931	. . . . 5 ⊢ ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ⁺) → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
72	67, 70, 71	sylancl 586	. . . 4 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
73		halfre 12337	. . . . . 6 ⊢ (1 / 2) ∈ ℝ
74		resubcl 11428	. . . . . 6 ⊢ ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈ ℝ)
75	67, 73, 74	sylancl 586	. . . . 5 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈ ℝ)
76		suprlub 12089	. . . . 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)) < 𝑦))
77	14, 22, 66, 75, 76	syl31anc 1375	. . . 4 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦))
78	72, 77	mpbid 232	. . 3 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦)
79		breq2 5096	. . . . 5 ⊢ (𝑦 = (seq1( + , 𝐹)‘𝑘) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦 ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
80	79	rexrn 7021	. . . 4 ⊢ (seq1( + , 𝐹) Fn ℕ → (∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦 ↔ ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
81	12, 61, 80	mp2b 10	. . 3 ⊢ (∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦 ↔ ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
82	78, 81	sylib 218	. 2 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
83		2re 12202	. . . . . 6 ⊢ 2 ∈ ℝ
84		2nn 12201	. . . . . . . . 9 ⊢ 2 ∈ ℕ
85		nnmulcl 12152	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
86	84, 29, 85	sylancr 587	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
87	86	peano2nnd 12145	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
88	87	nnnn0d 12445	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ₀)
89		reexpcl 13985	. . . . . 6 ⊢ ((2 ∈ ℝ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
90	83, 88, 89	sylancr 587	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
91	90	ltnrd 11250	. . . 4 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ¬ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1)))
92	29	adantr 480	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → 𝑘 ∈ ℕ)
93		peano2nn 12140	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
94	93	adantl 481	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
95	94	nnnn0d 12445	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ₀)
96		nnexpcl 13981	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ₀) → (2↑(𝑘 + 1)) ∈ ℕ)
97	84, 95, 96	sylancr 587	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℕ)
98	97	nnsqcld 14151	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
99	98	adantr 480	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
100		breq1 5095	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑤 → (𝑝 ∥ 𝑟 ↔ 𝑤 ∥ 𝑟))
101	100	notbid 318	. . . . . . . . . 10 ⊢ (𝑝 = 𝑤 → (¬ 𝑝 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑟))
102	101	cbvralvw 3207	. . . . . . . . 9 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟)
103		breq2 5096	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑛 → (𝑤 ∥ 𝑟 ↔ 𝑤 ∥ 𝑛))
104	103	notbid 318	. . . . . . . . . 10 ⊢ (𝑟 = 𝑛 → (¬ 𝑤 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑛))
105	104	ralbidv 3152	. . . . . . . . 9 ⊢ (𝑟 = 𝑛 → (∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛))
106	102, 105	bitrid 283	. . . . . . . 8 ⊢ (𝑟 = 𝑛 → (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛))
107	106	cbvrabv 3405	. . . . . . 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 2811	. . . . . . . . . 10 ⊢ (𝑚 = 𝑗 → (𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ))
110		oveq2 7357	. . . . . . . . . 10 ⊢ (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
111	109, 110	ifbieq1d 4501	. . . . . . . . 9 ⊢ (𝑚 = 𝑗 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
112	111	cbvsumv 15603	. . . . . . . 8 ⊢ Σ𝑚 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)
113		simpr 484	. . . . . . . 8 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2))
114	112, 113	eqbrtrid 5127	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑚 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) < (1 / 2))
115		eqid 2729	. . . . . . 7 ⊢ (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) = (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)})
116	8, 92, 99, 107, 108, 114, 115	prmreclem5 16832	. . . . . 6 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → (((2↑(𝑘 + 1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))))
117	116	ex 412	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) → (((2↑(𝑘 + 1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2)))))
118		eqid 2729	. . . . . . . . 9 ⊢ (ℤ_≥‘(𝑘 + 1)) = (ℤ_≥‘(𝑘 + 1))
119	94	nnzd 12498	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℤ)
120		eluznn 12819	. . . . . . . . . . 11 ⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
121	94, 120	sylan 580	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
122	121, 41	syl 17	. . . . . . . . 9 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
123	39	a1i 11	. . . . . . . . 9 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
124		simpl 482	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq1( + , 𝐹) ∈ dom ⇝ )
125	41	adantl 481	. . . . . . . . . . . 12 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
126	39	recni 11129	. . . . . . . . . . . . 13 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ
127	126	a1i 11	. . . . . . . . . . . 12 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
128	125, 127	eqeltrd 2828	. . . . . . . . . . 11 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℂ)
129	1, 94, 128	iserex 15564	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝑘 + 1)( + , 𝐹) ∈ dom ⇝ ))
130	124, 129	mpbid 232	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq(𝑘 + 1)( + , 𝐹) ∈ dom ⇝ )
131	118, 119, 122, 123, 130	isumrecl 15672	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
132	73	a1i 11	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1 / 2) ∈ ℝ)
133		elfznn 13456	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ)
134	133	adantl 481	. . . . . . . . . . 11 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ)
135	134, 41	syl 17	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
136	29, 1	eleqtrdi 2838	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
137	126	a1i 11	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
138	135, 136, 137	fsumser 15637	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (seq1( + , 𝐹)‘𝑘))
139	138, 27	eqeltrd 2828	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
140	131, 132, 139	ltadd2d 11272	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2))))
141	1, 118, 94, 125, 127, 124	isumsplit 15747	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
142		nncn 12136	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
143	142	adantl 481	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
144		ax-1cn 11067	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
145		pncan 11369	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
146	143, 144, 145	sylancl 586	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) − 1) = 𝑘)
147	146	oveq2d 7365	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
148	147	sumeq1d 15607	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
149	148	oveq1d 7364	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)) = (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
150	141, 149	eqtrd 2764	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
151	150	breq1d 5102	. . . . . . 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))))
152	140, 151	bitr4d 282	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2))))
153		eqid 2729	. . . . . . . . . 10 ⊢ seq1( + , 𝐹) = seq1( + , 𝐹)
154	1, 153, 23, 42, 43, 54, 60	isumsup 15754	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
155	154, 67	eqeltrd 2828	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
156	155	adantr 480	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
157	156, 132, 139	ltsubaddd 11716	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2))))
158	154	adantr 480	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
159	158	oveq1d 7364	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)))
160	159, 138	breq12d 5105	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
161	152, 157, 160	3bitr2d 307	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
162		2cn 12203	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
163	162	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
164	144	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
165	163, 143, 164	adddid 11139	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
166	94	nncnd 12144	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
167		mulcom 11095	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
168	166, 162, 167	sylancl 586	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
169	86	nncnd 12144	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
170	169, 164, 164	addassd 11137	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
171	144	2timesi 12261	. . . . . . . . . . . . 13 ⊢ (2 · 1) = (1 + 1)
172	171	oveq2i 7360	. . . . . . . . . . . 12 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
173	170, 172	eqtr4di 2782	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (2 · 1)))
174	165, 168, 173	3eqtr4d 2774	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (((2 · 𝑘) + 1) + 1))
175	174	oveq2d 7365	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = (2↑(((2 · 𝑘) + 1) + 1)))
176		2nn0 12401	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
177	176	a1i 11	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℕ₀)
178	163, 177, 95	expmuld 14056	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = ((2↑(𝑘 + 1))↑2))
179		expp1 13975	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑(((2 · 𝑘) + 1) + 1)) = ((2↑((2 · 𝑘) + 1)) · 2))
180	162, 88, 179	sylancr 587	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(((2 · 𝑘) + 1) + 1)) = ((2↑((2 · 𝑘) + 1)) · 2))
181	175, 178, 180	3eqtr3d 2772	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) = ((2↑((2 · 𝑘) + 1)) · 2))
182	181	oveq1d 7364	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (((2↑((2 · 𝑘) + 1)) · 2) / 2))
183		expcl 13986	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
184	162, 88, 183	sylancr 587	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
185		2ne0 12232	. . . . . . . . 9 ⊢ 2 ≠ 0
186		divcan4 11806	. . . . . . . . 9 ⊢ (((2↑((2 · 𝑘) + 1)) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
187	162, 185, 186	mp3an23 1455	. . . . . . . 8 ⊢ ((2↑((2 · 𝑘) + 1)) ∈ ℂ → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
188	184, 187	syl 17	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
189	182, 188	eqtrd 2764	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (2↑((2 · 𝑘) + 1)))
190		nnnn0 12391	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
191	190	adantl 481	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
192	163, 95, 191	expaddd 14055	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + (𝑘 + 1))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
193	143	2timesd 12367	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) = (𝑘 + 𝑘))
194	193	oveq1d 7364	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = ((𝑘 + 𝑘) + 1))
195	143, 143, 164	addassd 11137	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
196	194, 195	eqtrd 2764	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
197	196	oveq2d 7365	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) = (2↑(𝑘 + (𝑘 + 1))))
198	97	nnrpd 12935	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℝ⁺)
199	198	rprege0d 12944	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1)) ∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))))
200		sqrtsq 15176	. . . . . . . . 9 ⊢ (((2↑(𝑘 + 1)) ∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))) → (√‘((2↑(𝑘 + 1))↑2)) = (2↑(𝑘 + 1)))
201	199, 200	syl 17	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (√‘((2↑(𝑘 + 1))↑2)) = (2↑(𝑘 + 1)))
202	201	oveq2d 7365	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
203	192, 197, 202	3eqtr4rd 2775	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = (2↑((2 · 𝑘) + 1)))
204	189, 203	breq12d 5105	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((((2↑(𝑘 + 1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) ↔ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))))
205	117, 161, 204	3imtr3d 293	. . . 4 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘) → (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))))
206	91, 205	mtod 198	. . 3 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ¬ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
207	206	nrexdv 3124	. 2 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ¬ ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
208	82, 207	pm2.65i 194	1 ⊢ ¬ seq1( + , 𝐹) ∈ dom ⇝

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 = wceq 1540 ⊤wtru 1541 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3394 ∖ cdif 3900 ⊆ wss 3903 ∅c0 4284 ifcif 4476 class class class wbr 5092 ↦ cmpt 5173 dom cdm 5619 ran crn 5620 Fn wfn 6477 ⟶wf 6478 ‘cfv 6482 (class class class)co 7349 supcsup 9330 ℂcc 11007 ℝcr 11008 0cc0 11009 1c1 11010 + caddc 11012 · cmul 11014 < clt 11149 ≤ cle 11150 − cmin 11347 / cdiv 11777 ℕcn 12128 2c2 12183 ℕ₀cn0 12384 ℤ_≥cuz 12735 ℝ⁺crp 12893 ...cfz 13410 seqcseq 13908 ↑cexp 13968 √csqrt 15140 ⇝ cli 15391 Σcsu 15593 ∥ cdvds 16163 ℙcprime 16582

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5218 ax-sep 5235 ax-nul 5245 ax-pow 5304 ax-pr 5371 ax-un 7671 ax-inf2 9537 ax-cnex 11065 ax-resscn 11066 ax-1cn 11067 ax-icn 11068 ax-addcl 11069 ax-addrcl 11070 ax-mulcl 11071 ax-mulrcl 11072 ax-mulcom 11073 ax-addass 11074 ax-mulass 11075 ax-distr 11076 ax-i2m1 11077 ax-1ne0 11078 ax-1rid 11079 ax-rnegex 11080 ax-rrecex 11081 ax-cnre 11082 ax-pre-lttri 11083 ax-pre-lttrn 11084 ax-pre-ltadd 11085 ax-pre-mulgt0 11086 ax-pre-sup 11087

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3343 df-reu 3344 df-rab 3395 df-v 3438 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4285 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4859 df-int 4897 df-iun 4943 df-br 5093 df-opab 5155 df-mpt 5174 df-tr 5200 df-id 5514 df-eprel 5519 df-po 5527 df-so 5528 df-fr 5572 df-se 5573 df-we 5574 df-xp 5625 df-rel 5626 df-cnv 5627 df-co 5628 df-dm 5629 df-rn 5630 df-res 5631 df-ima 5632 df-pred 6249 df-ord 6310 df-on 6311 df-lim 6312 df-suc 6313 df-iota 6438 df-fun 6484 df-fn 6485 df-f 6486 df-f1 6487 df-fo 6488 df-f1o 6489 df-fv 6490 df-isom 6491 df-riota 7306 df-ov 7352 df-oprab 7353 df-mpo 7354 df-om 7800 df-1st 7924 df-2nd 7925 df-frecs 8214 df-wrecs 8245 df-recs 8294 df-rdg 8332 df-1o 8388 df-2o 8389 df-oadd 8392 df-er 8625 df-map 8755 df-pm 8756 df-en 8873 df-dom 8874 df-sdom 8875 df-fin 8876 df-sup 9332 df-inf 9333 df-oi 9402 df-dju 9797 df-card 9835 df-pnf 11151 df-mnf 11152 df-xr 11153 df-ltxr 11154 df-le 11155 df-sub 11349 df-neg 11350 df-div 11778 df-nn 12129 df-2 12191 df-3 12192 df-n0 12385 df-xnn0 12458 df-z 12472 df-uz 12736 df-q 12850 df-rp 12894 df-fz 13411 df-fzo 13558 df-fl 13696 df-mod 13774 df-seq 13909 df-exp 13969 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-rlim 15396 df-sum 15594 df-dvds 16164 df-gcd 16406 df-prm 16583 df-pc 16749

This theorem is referenced by: prmrec 16834

W3C validator