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 16954

Description: Lemma for prmrec 16955. 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 16953 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 12918	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
2		1zzd 12645	. . . . . . . . 9 ⊢ (⊤ → 1 ∈ ℤ)
3		nnrecre 12305	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
4	3	adantl 481	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
5		0re 11260	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
6		ifcl 4575	. . . . . . . . . . . 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 7133	. . . . . . . . . 10 ⊢ (⊤ → 𝐹:ℕ⟶ℝ)
10	9	ffvelcdmda 7103	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
11	1, 2, 10	serfre 14068	. . . . . . . 8 ⊢ (⊤ → seq1( + , 𝐹):ℕ⟶ℝ)
12	11	mptru 1543	. . . . . . 7 ⊢ seq1( + , 𝐹):ℕ⟶ℝ
13		frn 6743	. . . . . . 7 ⊢ (seq1( + , 𝐹):ℕ⟶ℝ → ran seq1( + , 𝐹) ⊆ ℝ)
14	12, 13	mp1i 13	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ran seq1( + , 𝐹) ⊆ ℝ)
15		1nn 12274	. . . . . . . 8 ⊢ 1 ∈ ℕ
16	12	fdmi 6747	. . . . . . . 8 ⊢ dom seq1( + , 𝐹) = ℕ
17	15, 16	eleqtrri 2837	. . . . . . 7 ⊢ 1 ∈ dom seq1( + , 𝐹)
18		ne0i 4346	. . . . . . . 8 ⊢ (1 ∈ dom seq1( + , 𝐹) → dom seq1( + , 𝐹) ≠ ∅)
19		dm0rn0 5937	. . . . . . . . 9 ⊢ (dom seq1( + , 𝐹) = ∅ ↔ ran seq1( + , 𝐹) = ∅)
20	19	necon3bii 2990	. . . . . . . 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 12645	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → 1 ∈ ℤ)
24		climdm 15586	. . . . . . . . . 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 7103	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℝ)
28	1, 23, 25, 27	climrecl 15615	. . . . . . . 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 7438	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗))
33	31, 32	ifbieq1d 4554	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
34		prmnn 16707	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℙ → 𝑗 ∈ ℕ)
35	34	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑗 ∈ ℙ) → 𝑗 ∈ ℕ)
36	35	nnrecred 12314	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑗 ∈ ℙ) → (1 / 𝑗) ∈ ℝ)
37	5	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ ¬ 𝑗 ∈ ℙ) → 0 ∈ ℝ)
38	36, 37	ifclda 4565	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
39	38	mptru 1543	. . . . . . . . . . . . . . 15 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ
40	39	elexi 3500	. . . . . . . . . . . . . 14 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ V
41	33, 8, 40	fvmpt 7015	. . . . . . . . . . . . 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 2838	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
45	44	adantlr 715	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
46		nnrp 13043	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ⁺)
47	46	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℝ⁺)
48	47	rpreccld 13084	. . . . . . . . . . . . . 14 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (1 / 𝑗) ∈ ℝ⁺)
49	48	rpge0d 13078	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (1 / 𝑗))
50		0le0 12364	. . . . . . . . . . . . 13 ⊢ 0 ≤ 0
51		breq2 5151	. . . . . . . . . . . . . 14 ⊢ ((1 / 𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ (1 / 𝑗) ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
52		breq2 5151	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
53	51, 52	ifboth 4569	. . . . . . . . . . . . 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 5175	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹‘𝑗))
56	55	adantlr 715	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹‘𝑗))
57	1, 29, 30, 45, 56	climserle 15695	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
58	57	ralrimiva 3143	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
59		brralrspcev 5207	. . . . . . . 8 ⊢ ((( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
60	28, 58, 59	syl2anc 584	. . . . . . 7 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
61		ffn 6736	. . . . . . . . 9 ⊢ (seq1( + , 𝐹):ℕ⟶ℝ → seq1( + , 𝐹) Fn ℕ)
62		breq1 5150	. . . . . . . . . 10 ⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
63	62	ralrn 7107	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) Fn ℕ → (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
64	12, 61, 63	mp2b 10	. . . . . . . 8 ⊢ (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
65	64	rexbii 3091	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
66	60, 65	sylibr 234	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥)
67	14, 22, 66	suprcld 12228	. . . . 5 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
68		2rp 13036	. . . . . 6 ⊢ 2 ∈ ℝ⁺
69		rpreccl 13058	. . . . . 6 ⊢ (2 ∈ ℝ⁺ → (1 / 2) ∈ ℝ⁺)
70	68, 69	ax-mp 5	. . . . 5 ⊢ (1 / 2) ∈ ℝ⁺
71		ltsubrp 13068	. . . . 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 12477	. . . . . 6 ⊢ (1 / 2) ∈ ℝ
74		resubcl 11570	. . . . . 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 12229	. . . . 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 1372	. . . 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 5151	. . . . 5 ⊢ (𝑦 = (seq1( + , 𝐹)‘𝑘) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦 ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
80	79	rexrn 7106	. . . 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 12337	. . . . . 6 ⊢ 2 ∈ ℝ
84		2nn 12336	. . . . . . . . 9 ⊢ 2 ∈ ℕ
85		nnmulcl 12287	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
86	84, 29, 85	sylancr 587	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
87	86	peano2nnd 12280	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
88	87	nnnn0d 12584	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ₀)
89		reexpcl 14115	. . . . . 6 ⊢ ((2 ∈ ℝ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
90	83, 88, 89	sylancr 587	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
91	90	ltnrd 11392	. . . 4 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ¬ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1)))
92	29	adantr 480	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → 𝑘 ∈ ℕ)
93		peano2nn 12275	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
94	93	adantl 481	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
95	94	nnnn0d 12584	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ₀)
96		nnexpcl 14111	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ₀) → (2↑(𝑘 + 1)) ∈ ℕ)
97	84, 95, 96	sylancr 587	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℕ)
98	97	nnsqcld 14279	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
99	98	adantr 480	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
100		breq1 5150	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑤 → (𝑝 ∥ 𝑟 ↔ 𝑤 ∥ 𝑟))
101	100	notbid 318	. . . . . . . . . 10 ⊢ (𝑝 = 𝑤 → (¬ 𝑝 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑟))
102	101	cbvralvw 3234	. . . . . . . . 9 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟)
103		breq2 5151	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑛 → (𝑤 ∥ 𝑟 ↔ 𝑤 ∥ 𝑛))
104	103	notbid 318	. . . . . . . . . 10 ⊢ (𝑟 = 𝑛 → (¬ 𝑤 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑛))
105	104	ralbidv 3175	. . . . . . . . 9 ⊢ (𝑟 = 𝑛 → (∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛))
106	102, 105	bitrid 283	. . . . . . . 8 ⊢ (𝑟 = 𝑛 → (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛))
107	106	cbvrabv 3443	. . . . . . 7 ⊢ {𝑟 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟} = {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛}
108		simpll 767	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → seq1( + , 𝐹) ∈ dom ⇝ )
109		eleq1w 2821	. . . . . . . . . 10 ⊢ (𝑚 = 𝑗 → (𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ))
110		oveq2 7438	. . . . . . . . . 10 ⊢ (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
111	109, 110	ifbieq1d 4554	. . . . . . . . 9 ⊢ (𝑚 = 𝑗 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
112	111	cbvsumv 15728	. . . . . . . 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 5182	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑚 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) < (1 / 2))
115		eqid 2734	. . . . . . 7 ⊢ (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) = (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)})
116	8, 92, 99, 107, 108, 114, 115	prmreclem5 16953	. . . . . 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 2734	. . . . . . . . 9 ⊢ (ℤ_≥‘(𝑘 + 1)) = (ℤ_≥‘(𝑘 + 1))
119	94	nnzd 12637	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℤ)
120		eluznn 12957	. . . . . . . . . . 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 11272	. . . . . . . . . . . . 13 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ
127	126	a1i 11	. . . . . . . . . . . 12 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
128	125, 127	eqeltrd 2838	. . . . . . . . . . 11 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℂ)
129	1, 94, 128	iserex 15689	. . . . . . . . . 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 15797	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
132	73	a1i 11	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1 / 2) ∈ ℝ)
133		elfznn 13589	. . . . . . . . . . . 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 2848	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
137	126	a1i 11	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
138	135, 136, 137	fsumser 15762	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (seq1( + , 𝐹)‘𝑘))
139	138, 27	eqeltrd 2838	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
140	131, 132, 139	ltadd2d 11414	. . . . . . 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 15872	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
142		nncn 12271	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
143	142	adantl 481	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
144		ax-1cn 11210	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
145		pncan 11511	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
146	143, 144, 145	sylancl 586	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) − 1) = 𝑘)
147	146	oveq2d 7446	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
148	147	sumeq1d 15732	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
149	148	oveq1d 7445	. . . . . . . . 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 2774	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
151	150	breq1d 5157	. . . . . . 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 2734	. . . . . . . . . 10 ⊢ seq1( + , 𝐹) = seq1( + , 𝐹)
154	1, 153, 23, 42, 43, 54, 60	isumsup 15879	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
155	154, 67	eqeltrd 2838	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
156	155	adantr 480	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
157	156, 132, 139	ltsubaddd 11856	. . . . . 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 7445	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)))
160	159, 138	breq12d 5160	. . . . . 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 12338	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
163	162	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
164	144	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
165	163, 143, 164	adddid 11282	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
166	94	nncnd 12279	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
167		mulcom 11238	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
168	166, 162, 167	sylancl 586	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
169	86	nncnd 12279	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
170	169, 164, 164	addassd 11280	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
171	144	2timesi 12401	. . . . . . . . . . . . 13 ⊢ (2 · 1) = (1 + 1)
172	171	oveq2i 7441	. . . . . . . . . . . 12 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
173	170, 172	eqtr4di 2792	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (2 · 1)))
174	165, 168, 173	3eqtr4d 2784	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (((2 · 𝑘) + 1) + 1))
175	174	oveq2d 7446	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = (2↑(((2 · 𝑘) + 1) + 1)))
176		2nn0 12540	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
177	176	a1i 11	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℕ₀)
178	163, 177, 95	expmuld 14185	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = ((2↑(𝑘 + 1))↑2))
179		expp1 14105	. . . . . . . . . 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 2782	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) = ((2↑((2 · 𝑘) + 1)) · 2))
182	181	oveq1d 7445	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (((2↑((2 · 𝑘) + 1)) · 2) / 2))
183		expcl 14116	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
184	162, 88, 183	sylancr 587	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
185		2ne0 12367	. . . . . . . . 9 ⊢ 2 ≠ 0
186		divcan4 11946	. . . . . . . . 9 ⊢ (((2↑((2 · 𝑘) + 1)) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
187	162, 185, 186	mp3an23 1452	. . . . . . . 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 2774	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (2↑((2 · 𝑘) + 1)))
190		nnnn0 12530	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
191	190	adantl 481	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
192	163, 95, 191	expaddd 14184	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + (𝑘 + 1))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
193	143	2timesd 12506	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) = (𝑘 + 𝑘))
194	193	oveq1d 7445	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = ((𝑘 + 𝑘) + 1))
195	143, 143, 164	addassd 11280	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
196	194, 195	eqtrd 2774	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
197	196	oveq2d 7446	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) = (2↑(𝑘 + (𝑘 + 1))))
198	97	nnrpd 13072	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℝ⁺)
199	198	rprege0d 13081	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1)) ∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))))
200		sqrtsq 15304	. . . . . . . . 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 7446	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
203	192, 197, 202	3eqtr4rd 2785	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = (2↑((2 · 𝑘) + 1)))
204	189, 203	breq12d 5160	. . . . 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 3146	. 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 1536 ⊤wtru 1537 ∈ wcel 2105 ≠ wne 2937 ∀wral 3058 ∃wrex 3067 {crab 3432 ∖ cdif 3959 ⊆ wss 3962 ∅c0 4338 ifcif 4530 class class class wbr 5147 ↦ cmpt 5230 dom cdm 5688 ran crn 5689 Fn wfn 6557 ⟶wf 6558 ‘cfv 6562 (class class class)co 7430 supcsup 9477 ℂcc 11150 ℝcr 11151 0cc0 11152 1c1 11153 + caddc 11155 · cmul 11157 < clt 11292 ≤ cle 11293 − cmin 11489 / cdiv 11917 ℕcn 12263 2c2 12318 ℕ₀cn0 12523 ℤ_≥cuz 12875 ℝ⁺crp 13031 ...cfz 13543 seqcseq 14038 ↑cexp 14098 √csqrt 15268 ⇝ cli 15516 Σcsu 15718 ∥ cdvds 16286 ℙcprime 16704

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1791 ax-4 1805 ax-5 1907 ax-6 1964 ax-7 2004 ax-8 2107 ax-9 2115 ax-10 2138 ax-11 2154 ax-12 2174 ax-ext 2705 ax-rep 5284 ax-sep 5301 ax-nul 5311 ax-pow 5370 ax-pr 5437 ax-un 7753 ax-inf2 9678 ax-cnex 11208 ax-resscn 11209 ax-1cn 11210 ax-icn 11211 ax-addcl 11212 ax-addrcl 11213 ax-mulcl 11214 ax-mulrcl 11215 ax-mulcom 11216 ax-addass 11217 ax-mulass 11218 ax-distr 11219 ax-i2m1 11220 ax-1ne0 11221 ax-1rid 11222 ax-rnegex 11223 ax-rrecex 11224 ax-cnre 11225 ax-pre-lttri 11226 ax-pre-lttrn 11227 ax-pre-ltadd 11228 ax-pre-mulgt0 11229 ax-pre-sup 11230

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1539 df-fal 1549 df-ex 1776 df-nf 1780 df-sb 2062 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2889 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-rmo 3377 df-reu 3378 df-rab 3433 df-v 3479 df-sbc 3791 df-csb 3908 df-dif 3965 df-un 3967 df-in 3969 df-ss 3979 df-pss 3982 df-nul 4339 df-if 4531 df-pw 4606 df-sn 4631 df-pr 4633 df-op 4637 df-uni 4912 df-int 4951 df-iun 4997 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5640 df-se 5641 df-we 5642 df-xp 5694 df-rel 5695 df-cnv 5696 df-co 5697 df-dm 5698 df-rn 5699 df-res 5700 df-ima 5701 df-pred 6322 df-ord 6388 df-on 6389 df-lim 6390 df-suc 6391 df-iota 6515 df-fun 6564 df-fn 6565 df-f 6566 df-f1 6567 df-fo 6568 df-f1o 6569 df-fv 6570 df-isom 6571 df-riota 7387 df-ov 7433 df-oprab 7434 df-mpo 7435 df-om 7887 df-1st 8012 df-2nd 8013 df-frecs 8304 df-wrecs 8335 df-recs 8409 df-rdg 8448 df-1o 8504 df-2o 8505 df-oadd 8508 df-er 8743 df-map 8866 df-pm 8867 df-en 8984 df-dom 8985 df-sdom 8986 df-fin 8987 df-sup 9479 df-inf 9480 df-oi 9547 df-dju 9938 df-card 9976 df-pnf 11294 df-mnf 11295 df-xr 11296 df-ltxr 11297 df-le 11298 df-sub 11491 df-neg 11492 df-div 11918 df-nn 12264 df-2 12326 df-3 12327 df-n0 12524 df-xnn0 12597 df-z 12611 df-uz 12876 df-q 12988 df-rp 13032 df-fz 13544 df-fzo 13691 df-fl 13828 df-mod 13906 df-seq 14039 df-exp 14099 df-hash 14366 df-cj 15134 df-re 15135 df-im 15136 df-sqrt 15270 df-abs 15271 df-clim 15520 df-rlim 15521 df-sum 15719 df-dvds 16287 df-gcd 16528 df-prm 16705 df-pc 16870

This theorem is referenced by: prmrec 16955

W3C validator