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 16550

Description: Lemma for prmrec 16551. 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 16549 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 12550	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
2		1zzd 12281	. . . . . . . . 9 ⊢ (⊤ → 1 ∈ ℤ)
3		nnrecre 11945	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
4	3	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
5		0re 10908	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
6		ifcl 4501	. . . . . . . . . . . 12 ⊢ (((1 / 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) ∈ ℝ)
7	4, 5, 6	sylancl 585	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) ∈ ℝ)
8		prmrec.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
9	7, 8	fmptd 6970	. . . . . . . . . 10 ⊢ (⊤ → 𝐹:ℕ⟶ℝ)
10	9	ffvelrnda 6943	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
11	1, 2, 10	serfre 13680	. . . . . . . 8 ⊢ (⊤ → seq1( + , 𝐹):ℕ⟶ℝ)
12	11	mptru 1546	. . . . . . 7 ⊢ seq1( + , 𝐹):ℕ⟶ℝ
13		frn 6591	. . . . . . 7 ⊢ (seq1( + , 𝐹):ℕ⟶ℝ → ran seq1( + , 𝐹) ⊆ ℝ)
14	12, 13	mp1i 13	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ran seq1( + , 𝐹) ⊆ ℝ)
15		1nn 11914	. . . . . . . 8 ⊢ 1 ∈ ℕ
16	12	fdmi 6596	. . . . . . . 8 ⊢ dom seq1( + , 𝐹) = ℕ
17	15, 16	eleqtrri 2838	. . . . . . 7 ⊢ 1 ∈ dom seq1( + , 𝐹)
18		ne0i 4265	. . . . . . . 8 ⊢ (1 ∈ dom seq1( + , 𝐹) → dom seq1( + , 𝐹) ≠ ∅)
19		dm0rn0 5823	. . . . . . . . 9 ⊢ (dom seq1( + , 𝐹) = ∅ ↔ ran seq1( + , 𝐹) = ∅)
20	19	necon3bii 2995	. . . . . . . 8 ⊢ (dom seq1( + , 𝐹) ≠ ∅ ↔ ran seq1( + , 𝐹) ≠ ∅)
21	18, 20	sylib 217	. . . . . . 7 ⊢ (1 ∈ dom seq1( + , 𝐹) → ran seq1( + , 𝐹) ≠ ∅)
22	17, 21	mp1i 13	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ran seq1( + , 𝐹) ≠ ∅)
23		1zzd 12281	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → 1 ∈ ℤ)
24		climdm 15191	. . . . . . . . . 10 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
25	24	biimpi 215	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
26	12	a1i 11	. . . . . . . . . 10 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → seq1( + , 𝐹):ℕ⟶ℝ)
27	26	ffvelrnda 6943	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℝ)
28	1, 23, 25, 27	climrecl 15220	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ)
29		simpr 484	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
30	25	adantr 480	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
31		eleq1w 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ ℙ ↔ 𝑗 ∈ ℙ))
32		oveq2 7263	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗))
33	31, 32	ifbieq1d 4480	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
34		prmnn 16307	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℙ → 𝑗 ∈ ℕ)
35	34	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑗 ∈ ℙ) → 𝑗 ∈ ℕ)
36	35	nnrecred 11954	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑗 ∈ ℙ) → (1 / 𝑗) ∈ ℝ)
37	5	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ ¬ 𝑗 ∈ ℙ) → 0 ∈ ℝ)
38	36, 37	ifclda 4491	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
39	38	mptru 1546	. . . . . . . . . . . . . . 15 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ
40	39	elexi 3441	. . . . . . . . . . . . . 14 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ V
41	33, 8, 40	fvmpt 6857	. . . . . . . . . . . . 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 2839	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
45	44	adantlr 711	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
46		nnrp 12670	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ⁺)
47	46	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℝ⁺)
48	47	rpreccld 12711	. . . . . . . . . . . . . 14 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (1 / 𝑗) ∈ ℝ⁺)
49	48	rpge0d 12705	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (1 / 𝑗))
50		0le0 12004	. . . . . . . . . . . . 13 ⊢ 0 ≤ 0
51		breq2 5074	. . . . . . . . . . . . . 14 ⊢ ((1 / 𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ (1 / 𝑗) ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
52		breq2 5074	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
53	51, 52	ifboth 4495	. . . . . . . . . . . . 13 ⊢ ((0 ≤ (1 / 𝑗) ∧ 0 ≤ 0) → 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
54	49, 50, 53	sylancl 585	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
55	54, 42	breqtrrd 5098	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹‘𝑗))
56	55	adantlr 711	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹‘𝑗))
57	1, 29, 30, 45, 56	climserle 15302	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
58	57	ralrimiva 3107	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
59		brralrspcev 5130	. . . . . . . 8 ⊢ ((( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
60	28, 58, 59	syl2anc 583	. . . . . . 7 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
61		ffn 6584	. . . . . . . . 9 ⊢ (seq1( + , 𝐹):ℕ⟶ℝ → seq1( + , 𝐹) Fn ℕ)
62		breq1 5073	. . . . . . . . . 10 ⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
63	62	ralrn 6946	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) Fn ℕ → (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
64	12, 61, 63	mp2b 10	. . . . . . . 8 ⊢ (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
65	64	rexbii 3177	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
66	60, 65	sylibr 233	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥)
67	14, 22, 66	suprcld 11868	. . . . 5 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
68		2rp 12664	. . . . . 6 ⊢ 2 ∈ ℝ⁺
69		rpreccl 12685	. . . . . 6 ⊢ (2 ∈ ℝ⁺ → (1 / 2) ∈ ℝ⁺)
70	68, 69	ax-mp 5	. . . . 5 ⊢ (1 / 2) ∈ ℝ⁺
71		ltsubrp 12695	. . . . 5 ⊢ ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ⁺) → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
72	67, 70, 71	sylancl 585	. . . 4 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
73		halfre 12117	. . . . . 6 ⊢ (1 / 2) ∈ ℝ
74		resubcl 11215	. . . . . 6 ⊢ ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈ ℝ)
75	67, 73, 74	sylancl 585	. . . . 5 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈ ℝ)
76		suprlub 11869	. . . . 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 1371	. . . 4 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦))
78	72, 77	mpbid 231	. . 3 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦)
79		breq2 5074	. . . . 5 ⊢ (𝑦 = (seq1( + , 𝐹)‘𝑘) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦 ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
80	79	rexrn 6945	. . . 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 217	. 2 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
83		2re 11977	. . . . . 6 ⊢ 2 ∈ ℝ
84		2nn 11976	. . . . . . . . 9 ⊢ 2 ∈ ℕ
85		nnmulcl 11927	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
86	84, 29, 85	sylancr 586	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
87	86	peano2nnd 11920	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
88	87	nnnn0d 12223	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ₀)
89		reexpcl 13727	. . . . . 6 ⊢ ((2 ∈ ℝ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
90	83, 88, 89	sylancr 586	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
91	90	ltnrd 11039	. . . 4 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ¬ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1)))
92	29	adantr 480	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → 𝑘 ∈ ℕ)
93		peano2nn 11915	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
94	93	adantl 481	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
95	94	nnnn0d 12223	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ₀)
96		nnexpcl 13723	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ₀) → (2↑(𝑘 + 1)) ∈ ℕ)
97	84, 95, 96	sylancr 586	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℕ)
98	97	nnsqcld 13887	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
99	98	adantr 480	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
100		breq1 5073	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑤 → (𝑝 ∥ 𝑟 ↔ 𝑤 ∥ 𝑟))
101	100	notbid 317	. . . . . . . . . 10 ⊢ (𝑝 = 𝑤 → (¬ 𝑝 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑟))
102	101	cbvralvw 3372	. . . . . . . . 9 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟)
103		breq2 5074	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑛 → (𝑤 ∥ 𝑟 ↔ 𝑤 ∥ 𝑛))
104	103	notbid 317	. . . . . . . . . 10 ⊢ (𝑟 = 𝑛 → (¬ 𝑤 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑛))
105	104	ralbidv 3120	. . . . . . . . 9 ⊢ (𝑟 = 𝑛 → (∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛))
106	102, 105	syl5bb 282	. . . . . . . 8 ⊢ (𝑟 = 𝑛 → (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛))
107	106	cbvrabv 3416	. . . . . . 7 ⊢ {𝑟 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟} = {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛}
108		simpll 763	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → seq1( + , 𝐹) ∈ dom ⇝ )
109		eleq1w 2821	. . . . . . . . . 10 ⊢ (𝑚 = 𝑗 → (𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ))
110		oveq2 7263	. . . . . . . . . 10 ⊢ (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
111	109, 110	ifbieq1d 4480	. . . . . . . . 9 ⊢ (𝑚 = 𝑗 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
112	111	cbvsumv 15336	. . . . . . . 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 5105	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑚 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) < (1 / 2))
115		eqid 2738	. . . . . . 7 ⊢ (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) = (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)})
116	8, 92, 99, 107, 108, 114, 115	prmreclem5 16549	. . . . . 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 2738	. . . . . . . . 9 ⊢ (ℤ_≥‘(𝑘 + 1)) = (ℤ_≥‘(𝑘 + 1))
119	94	nnzd 12354	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℤ)
120		eluznn 12587	. . . . . . . . . . 11 ⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
121	94, 120	sylan 579	. . . . . . . . . 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 10920	. . . . . . . . . . . . 13 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ
127	126	a1i 11	. . . . . . . . . . . 12 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
128	125, 127	eqeltrd 2839	. . . . . . . . . . 11 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℂ)
129	1, 94, 128	iserex 15296	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝑘 + 1)( + , 𝐹) ∈ dom ⇝ ))
130	124, 129	mpbid 231	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq(𝑘 + 1)( + , 𝐹) ∈ dom ⇝ )
131	118, 119, 122, 123, 130	isumrecl 15405	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
132	73	a1i 11	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1 / 2) ∈ ℝ)
133		elfznn 13214	. . . . . . . . . . . 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 2849	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
137	126	a1i 11	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
138	135, 136, 137	fsumser 15370	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (seq1( + , 𝐹)‘𝑘))
139	138, 27	eqeltrd 2839	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
140	131, 132, 139	ltadd2d 11061	. . . . . . 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 15480	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
142		nncn 11911	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
143	142	adantl 481	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
144		ax-1cn 10860	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
145		pncan 11157	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
146	143, 144, 145	sylancl 585	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) − 1) = 𝑘)
147	146	oveq2d 7271	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
148	147	sumeq1d 15341	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
149	148	oveq1d 7270	. . . . . . . . 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 2778	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
151	150	breq1d 5080	. . . . . . 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 281	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2))))
153		eqid 2738	. . . . . . . . . 10 ⊢ seq1( + , 𝐹) = seq1( + , 𝐹)
154	1, 153, 23, 42, 43, 54, 60	isumsup 15487	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
155	154, 67	eqeltrd 2839	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
156	155	adantr 480	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
157	156, 132, 139	ltsubaddd 11501	. . . . . 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 7270	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)))
160	159, 138	breq12d 5083	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
161	152, 157, 160	3bitr2d 306	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
162		2cn 11978	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
163	162	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
164	144	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
165	163, 143, 164	adddid 10930	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
166	94	nncnd 11919	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
167		mulcom 10888	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
168	166, 162, 167	sylancl 585	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
169	86	nncnd 11919	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
170	169, 164, 164	addassd 10928	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
171	144	2timesi 12041	. . . . . . . . . . . . 13 ⊢ (2 · 1) = (1 + 1)
172	171	oveq2i 7266	. . . . . . . . . . . 12 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
173	170, 172	eqtr4di 2797	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (2 · 1)))
174	165, 168, 173	3eqtr4d 2788	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (((2 · 𝑘) + 1) + 1))
175	174	oveq2d 7271	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = (2↑(((2 · 𝑘) + 1) + 1)))
176		2nn0 12180	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
177	176	a1i 11	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℕ₀)
178	163, 177, 95	expmuld 13795	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = ((2↑(𝑘 + 1))↑2))
179		expp1 13717	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑(((2 · 𝑘) + 1) + 1)) = ((2↑((2 · 𝑘) + 1)) · 2))
180	162, 88, 179	sylancr 586	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(((2 · 𝑘) + 1) + 1)) = ((2↑((2 · 𝑘) + 1)) · 2))
181	175, 178, 180	3eqtr3d 2786	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) = ((2↑((2 · 𝑘) + 1)) · 2))
182	181	oveq1d 7270	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (((2↑((2 · 𝑘) + 1)) · 2) / 2))
183		expcl 13728	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
184	162, 88, 183	sylancr 586	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
185		2ne0 12007	. . . . . . . . 9 ⊢ 2 ≠ 0
186		divcan4 11590	. . . . . . . . 9 ⊢ (((2↑((2 · 𝑘) + 1)) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
187	162, 185, 186	mp3an23 1451	. . . . . . . 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 2778	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (2↑((2 · 𝑘) + 1)))
190		nnnn0 12170	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
191	190	adantl 481	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
192	163, 95, 191	expaddd 13794	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + (𝑘 + 1))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
193	143	2timesd 12146	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) = (𝑘 + 𝑘))
194	193	oveq1d 7270	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = ((𝑘 + 𝑘) + 1))
195	143, 143, 164	addassd 10928	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
196	194, 195	eqtrd 2778	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
197	196	oveq2d 7271	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) = (2↑(𝑘 + (𝑘 + 1))))
198	97	nnrpd 12699	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℝ⁺)
199	198	rprege0d 12708	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1)) ∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))))
200		sqrtsq 14909	. . . . . . . . 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 7271	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
203	192, 197, 202	3eqtr4rd 2789	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = (2↑((2 · 𝑘) + 1)))
204	189, 203	breq12d 5083	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((((2↑(𝑘 + 1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) ↔ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))))
205	117, 161, 204	3imtr3d 292	. . . 4 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘) → (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))))
206	91, 205	mtod 197	. . 3 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ¬ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
207	206	nrexdv 3197	. 2 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ¬ ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
208	82, 207	pm2.65i 193	1 ⊢ ¬ seq1( + , 𝐹) ∈ dom ⇝

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 395 = wceq 1539 ⊤wtru 1540 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 ∃wrex 3064 {crab 3067 ∖ cdif 3880 ⊆ wss 3883 ∅c0 4253 ifcif 4456 class class class wbr 5070 ↦ cmpt 5153 dom cdm 5580 ran crn 5581 Fn wfn 6413 ⟶wf 6414 ‘cfv 6418 (class class class)co 7255 supcsup 9129 ℂcc 10800 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 < clt 10940 ≤ cle 10941 − cmin 11135 / cdiv 11562 ℕcn 11903 2c2 11958 ℕ₀cn0 12163 ℤ_≥cuz 12511 ℝ⁺crp 12659 ...cfz 13168 seqcseq 13649 ↑cexp 13710 √csqrt 14872 ⇝ cli 15121 Σcsu 15325 ∥ cdvds 15891 ℙcprime 16304

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-inf2 9329 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-se 5536 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-isom 6427 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-oadd 8271 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-oi 9199 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-xnn0 12236 df-z 12250 df-uz 12512 df-q 12618 df-rp 12660 df-fz 13169 df-fzo 13312 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-clim 15125 df-rlim 15126 df-sum 15326 df-dvds 15892 df-gcd 16130 df-prm 16305 df-pc 16466

This theorem is referenced by: prmrec 16551

W3C validator