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 16849

Description: Lemma for prmrec 16850. 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 16848 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 12790	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
2		1zzd 12522	. . . . . . . . 9 ⊢ (⊤ → 1 ∈ ℤ)
3		nnrecre 12187	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
4	3	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
5		0re 11134	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
6		ifcl 4525	. . . . . . . . . . . 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 7059	. . . . . . . . . 10 ⊢ (⊤ → 𝐹:ℕ⟶ℝ)
10	9	ffvelcdmda 7029	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
11	1, 2, 10	serfre 13954	. . . . . . . 8 ⊢ (⊤ → seq1( + , 𝐹):ℕ⟶ℝ)
12	11	mptru 1548	. . . . . . 7 ⊢ seq1( + , 𝐹):ℕ⟶ℝ
13		frn 6669	. . . . . . 7 ⊢ (seq1( + , 𝐹):ℕ⟶ℝ → ran seq1( + , 𝐹) ⊆ ℝ)
14	12, 13	mp1i 13	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ran seq1( + , 𝐹) ⊆ ℝ)
15		1nn 12156	. . . . . . . 8 ⊢ 1 ∈ ℕ
16	12	fdmi 6673	. . . . . . . 8 ⊢ dom seq1( + , 𝐹) = ℕ
17	15, 16	eleqtrri 2835	. . . . . . 7 ⊢ 1 ∈ dom seq1( + , 𝐹)
18		ne0i 4293	. . . . . . . 8 ⊢ (1 ∈ dom seq1( + , 𝐹) → dom seq1( + , 𝐹) ≠ ∅)
19		dm0rn0 5873	. . . . . . . . 9 ⊢ (dom seq1( + , 𝐹) = ∅ ↔ ran seq1( + , 𝐹) = ∅)
20	19	necon3bii 2984	. . . . . . . 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 12522	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → 1 ∈ ℤ)
24		climdm 15477	. . . . . . . . . 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 7029	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℝ)
28	1, 23, 25, 27	climrecl 15506	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ)
29		simpr 484	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
30	25	adantr 480	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
31		eleq1w 2819	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ ℙ ↔ 𝑗 ∈ ℙ))
32		oveq2 7366	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗))
33	31, 32	ifbieq1d 4504	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
34		prmnn 16601	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℙ → 𝑗 ∈ ℕ)
35	34	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑗 ∈ ℙ) → 𝑗 ∈ ℕ)
36	35	nnrecred 12196	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑗 ∈ ℙ) → (1 / 𝑗) ∈ ℝ)
37	5	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ ¬ 𝑗 ∈ ℙ) → 0 ∈ ℝ)
38	36, 37	ifclda 4515	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
39	38	mptru 1548	. . . . . . . . . . . . . . 15 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ
40	39	elexi 3463	. . . . . . . . . . . . . 14 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ V
41	33, 8, 40	fvmpt 6941	. . . . . . . . . . . . 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 2836	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
45	44	adantlr 715	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
46		nnrp 12917	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ⁺)
47	46	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℝ⁺)
48	47	rpreccld 12959	. . . . . . . . . . . . . 14 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (1 / 𝑗) ∈ ℝ⁺)
49	48	rpge0d 12953	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (1 / 𝑗))
50		0le0 12246	. . . . . . . . . . . . 13 ⊢ 0 ≤ 0
51		breq2 5102	. . . . . . . . . . . . . 14 ⊢ ((1 / 𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ (1 / 𝑗) ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
52		breq2 5102	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
53	51, 52	ifboth 4519	. . . . . . . . . . . . 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 5126	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹‘𝑗))
56	55	adantlr 715	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹‘𝑗))
57	1, 29, 30, 45, 56	climserle 15586	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
58	57	ralrimiva 3128	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
59		brralrspcev 5158	. . . . . . . 8 ⊢ ((( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
60	28, 58, 59	syl2anc 584	. . . . . . 7 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
61		ffn 6662	. . . . . . . . 9 ⊢ (seq1( + , 𝐹):ℕ⟶ℝ → seq1( + , 𝐹) Fn ℕ)
62		breq1 5101	. . . . . . . . . 10 ⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
63	62	ralrn 7033	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) Fn ℕ → (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
64	12, 61, 63	mp2b 10	. . . . . . . 8 ⊢ (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
65	64	rexbii 3083	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
66	60, 65	sylibr 234	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥)
67	14, 22, 66	suprcld 12105	. . . . 5 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
68		2rp 12910	. . . . . 6 ⊢ 2 ∈ ℝ⁺
69		rpreccl 12933	. . . . . 6 ⊢ (2 ∈ ℝ⁺ → (1 / 2) ∈ ℝ⁺)
70	68, 69	ax-mp 5	. . . . 5 ⊢ (1 / 2) ∈ ℝ⁺
71		ltsubrp 12943	. . . . 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 12354	. . . . . 6 ⊢ (1 / 2) ∈ ℝ
74		resubcl 11445	. . . . . 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 12106	. . . . 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 5102	. . . . 5 ⊢ (𝑦 = (seq1( + , 𝐹)‘𝑘) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦 ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
80	79	rexrn 7032	. . . 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 12219	. . . . . 6 ⊢ 2 ∈ ℝ
84		2nn 12218	. . . . . . . . 9 ⊢ 2 ∈ ℕ
85		nnmulcl 12169	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
86	84, 29, 85	sylancr 587	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
87	86	peano2nnd 12162	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
88	87	nnnn0d 12462	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ₀)
89		reexpcl 14001	. . . . . 6 ⊢ ((2 ∈ ℝ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
90	83, 88, 89	sylancr 587	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
91	90	ltnrd 11267	. . . 4 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ¬ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1)))
92	29	adantr 480	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → 𝑘 ∈ ℕ)
93		peano2nn 12157	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
94	93	adantl 481	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
95	94	nnnn0d 12462	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ₀)
96		nnexpcl 13997	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ₀) → (2↑(𝑘 + 1)) ∈ ℕ)
97	84, 95, 96	sylancr 587	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℕ)
98	97	nnsqcld 14167	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
99	98	adantr 480	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
100		breq1 5101	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑤 → (𝑝 ∥ 𝑟 ↔ 𝑤 ∥ 𝑟))
101	100	notbid 318	. . . . . . . . . 10 ⊢ (𝑝 = 𝑤 → (¬ 𝑝 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑟))
102	101	cbvralvw 3214	. . . . . . . . 9 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟)
103		breq2 5102	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑛 → (𝑤 ∥ 𝑟 ↔ 𝑤 ∥ 𝑛))
104	103	notbid 318	. . . . . . . . . 10 ⊢ (𝑟 = 𝑛 → (¬ 𝑤 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑛))
105	104	ralbidv 3159	. . . . . . . . 9 ⊢ (𝑟 = 𝑛 → (∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛))
106	102, 105	bitrid 283	. . . . . . . 8 ⊢ (𝑟 = 𝑛 → (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛))
107	106	cbvrabv 3409	. . . . . . 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 2819	. . . . . . . . . 10 ⊢ (𝑚 = 𝑗 → (𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ))
110		oveq2 7366	. . . . . . . . . 10 ⊢ (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
111	109, 110	ifbieq1d 4504	. . . . . . . . 9 ⊢ (𝑚 = 𝑗 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
112	111	cbvsumv 15619	. . . . . . . 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 5133	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑚 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) < (1 / 2))
115		eqid 2736	. . . . . . 7 ⊢ (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) = (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)})
116	8, 92, 99, 107, 108, 114, 115	prmreclem5 16848	. . . . . 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 2736	. . . . . . . . 9 ⊢ (ℤ_≥‘(𝑘 + 1)) = (ℤ_≥‘(𝑘 + 1))
119	94	nnzd 12514	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℤ)
120		eluznn 12831	. . . . . . . . . . 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 11146	. . . . . . . . . . . . 13 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ
127	126	a1i 11	. . . . . . . . . . . 12 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
128	125, 127	eqeltrd 2836	. . . . . . . . . . 11 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℂ)
129	1, 94, 128	iserex 15580	. . . . . . . . . 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 15688	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
132	73	a1i 11	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1 / 2) ∈ ℝ)
133		elfznn 13469	. . . . . . . . . . . 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 2846	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
137	126	a1i 11	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
138	135, 136, 137	fsumser 15653	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (seq1( + , 𝐹)‘𝑘))
139	138, 27	eqeltrd 2836	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
140	131, 132, 139	ltadd2d 11289	. . . . . . 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 15763	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
142		nncn 12153	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
143	142	adantl 481	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
144		ax-1cn 11084	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
145		pncan 11386	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
146	143, 144, 145	sylancl 586	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) − 1) = 𝑘)
147	146	oveq2d 7374	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
148	147	sumeq1d 15623	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
149	148	oveq1d 7373	. . . . . . . . 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 2771	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
151	150	breq1d 5108	. . . . . . 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 2736	. . . . . . . . . 10 ⊢ seq1( + , 𝐹) = seq1( + , 𝐹)
154	1, 153, 23, 42, 43, 54, 60	isumsup 15770	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
155	154, 67	eqeltrd 2836	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
156	155	adantr 480	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
157	156, 132, 139	ltsubaddd 11733	. . . . . 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 7373	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)))
160	159, 138	breq12d 5111	. . . . . 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 12220	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
163	162	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
164	144	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
165	163, 143, 164	adddid 11156	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
166	94	nncnd 12161	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
167		mulcom 11112	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
168	166, 162, 167	sylancl 586	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
169	86	nncnd 12161	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
170	169, 164, 164	addassd 11154	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
171	144	2timesi 12278	. . . . . . . . . . . . 13 ⊢ (2 · 1) = (1 + 1)
172	171	oveq2i 7369	. . . . . . . . . . . 12 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
173	170, 172	eqtr4di 2789	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (2 · 1)))
174	165, 168, 173	3eqtr4d 2781	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (((2 · 𝑘) + 1) + 1))
175	174	oveq2d 7374	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = (2↑(((2 · 𝑘) + 1) + 1)))
176		2nn0 12418	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
177	176	a1i 11	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℕ₀)
178	163, 177, 95	expmuld 14072	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = ((2↑(𝑘 + 1))↑2))
179		expp1 13991	. . . . . . . . . 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 2779	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) = ((2↑((2 · 𝑘) + 1)) · 2))
182	181	oveq1d 7373	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (((2↑((2 · 𝑘) + 1)) · 2) / 2))
183		expcl 14002	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
184	162, 88, 183	sylancr 587	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
185		2ne0 12249	. . . . . . . . 9 ⊢ 2 ≠ 0
186		divcan4 11823	. . . . . . . . 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 2771	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (2↑((2 · 𝑘) + 1)))
190		nnnn0 12408	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
191	190	adantl 481	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
192	163, 95, 191	expaddd 14071	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + (𝑘 + 1))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
193	143	2timesd 12384	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) = (𝑘 + 𝑘))
194	193	oveq1d 7373	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = ((𝑘 + 𝑘) + 1))
195	143, 143, 164	addassd 11154	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
196	194, 195	eqtrd 2771	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
197	196	oveq2d 7374	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) = (2↑(𝑘 + (𝑘 + 1))))
198	97	nnrpd 12947	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℝ⁺)
199	198	rprege0d 12956	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1)) ∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))))
200		sqrtsq 15192	. . . . . . . . 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 7374	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
203	192, 197, 202	3eqtr4rd 2782	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = (2↑((2 · 𝑘) + 1)))
204	189, 203	breq12d 5111	. . . . 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 3131	. 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 1541 ⊤wtru 1542 ∈ wcel 2113 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 {crab 3399 ∖ cdif 3898 ⊆ wss 3901 ∅c0 4285 ifcif 4479 class class class wbr 5098 ↦ cmpt 5179 dom cdm 5624 ran crn 5625 Fn wfn 6487 ⟶wf 6488 ‘cfv 6492 (class class class)co 7358 supcsup 9343 ℂcc 11024 ℝcr 11025 0cc0 11026 1c1 11027 + caddc 11029 · cmul 11031 < clt 11166 ≤ cle 11167 − cmin 11364 / cdiv 11794 ℕcn 12145 2c2 12200 ℕ₀cn0 12401 ℤ_≥cuz 12751 ℝ⁺crp 12905 ...cfz 13423 seqcseq 13924 ↑cexp 13984 √csqrt 15156 ⇝ cli 15407 Σcsu 15609 ∥ cdvds 16179 ℙcprime 16598

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-inf2 9550 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-op 4587 df-uni 4864 df-int 4903 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-se 5578 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-isom 6501 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-2o 8398 df-oadd 8401 df-er 8635 df-map 8765 df-pm 8766 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-inf 9346 df-oi 9415 df-dju 9813 df-card 9851 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-n0 12402 df-xnn0 12475 df-z 12489 df-uz 12752 df-q 12862 df-rp 12906 df-fz 13424 df-fzo 13571 df-fl 13712 df-mod 13790 df-seq 13925 df-exp 13985 df-hash 14254 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-clim 15411 df-rlim 15412 df-sum 15610 df-dvds 16180 df-gcd 16422 df-prm 16599 df-pc 16765

This theorem is referenced by: prmrec 16850

W3C validator