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 16980

Description: Lemma for prmrec 16981. 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 16979 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 12900	. . . . . . . . 9 ⊢ ℕ = (ℤ_≥‘1)
2		1zzd 12624	. . . . . . . . 9 ⊢ (⊤ → 1 ∈ ℤ)
3		nnrecre 12277	. . . . . . . . . . . . 13 ⊢ (𝑛 ∈ ℕ → (1 / 𝑛) ∈ ℝ)
4	3	adantl 486	. . . . . . . . . . . 12 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → (1 / 𝑛) ∈ ℝ)
5		0re 11209	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
6		ifcl 4538	. . . . . . . . . . . 12 ⊢ (((1 / 𝑛) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) ∈ ℝ)
7	4, 5, 6	sylancl 597	. . . . . . . . . . 11 ⊢ ((⊤ ∧ 𝑛 ∈ ℕ) → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) ∈ ℝ)
8		prmrec.1	. . . . . . . . . . 11 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
9	7, 8	fmptd 7110	. . . . . . . . . 10 ⊢ (⊤ → 𝐹:ℕ⟶ℝ)
10	9	ffvelcdmda 7080	. . . . . . . . 9 ⊢ ((⊤ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
11	1, 2, 10	serfre 14066	. . . . . . . 8 ⊢ (⊤ → seq1( + , 𝐹):ℕ⟶ℝ)
12	11	mptru 1574	. . . . . . 7 ⊢ seq1( + , 𝐹):ℕ⟶ℝ
13		frn 6714	. . . . . . 7 ⊢ (seq1( + , 𝐹):ℕ⟶ℝ → ran seq1( + , 𝐹) ⊆ ℝ)
14	12, 13	mp1i 14	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ran seq1( + , 𝐹) ⊆ ℝ)
15		1nn 12243	. . . . . . . 8 ⊢ 1 ∈ ℕ
16	12	fdmi 6718	. . . . . . . 8 ⊢ dom seq1( + , 𝐹) = ℕ
17	15, 16	eleqtrri 2868	. . . . . . 7 ⊢ 1 ∈ dom seq1( + , 𝐹)
18		ne0i 4302	. . . . . . . 8 ⊢ (1 ∈ dom seq1( + , 𝐹) → dom seq1( + , 𝐹) ≠ ∅)
19		dm0rn0 5915	. . . . . . . . 9 ⊢ (dom seq1( + , 𝐹) = ∅ ↔ ran seq1( + , 𝐹) = ∅)
20	19	necon3bii 3016	. . . . . . . 8 ⊢ (dom seq1( + , 𝐹) ≠ ∅ ↔ ran seq1( + , 𝐹) ≠ ∅)
21	18, 20	sylib 221	. . . . . . 7 ⊢ (1 ∈ dom seq1( + , 𝐹) → ran seq1( + , 𝐹) ≠ ∅)
22	17, 21	mp1i 14	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ran seq1( + , 𝐹) ≠ ∅)
23		1zzd 12624	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → 1 ∈ ℤ)
24		climdm 15604	. . . . . . . . . 10 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
25	24	biimpi 219	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
26	12	a1i 11	. . . . . . . . . 10 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → seq1( + , 𝐹):ℕ⟶ℝ)
27	26	ffvelcdmda 7080	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ∈ ℝ)
28	1, 23, 25, 27	climrecl 15633	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ)
29		simpr 489	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
30	25	adantr 485	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq1( + , 𝐹) ⇝ ( ⇝ ‘seq1( + , 𝐹)))
31		eleq1w 2852	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → (𝑛 ∈ ℙ ↔ 𝑗 ∈ ℙ))
32		oveq2 7419	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑗 → (1 / 𝑛) = (1 / 𝑗))
33	31, 32	ifbieq1d 4517	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑗 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
34		prmnn 16731	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑗 ∈ ℙ → 𝑗 ∈ ℕ)
35	34	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((⊤ ∧ 𝑗 ∈ ℙ) → 𝑗 ∈ ℕ)
36	35	nnrecred 12286	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ 𝑗 ∈ ℙ) → (1 / 𝑗) ∈ ℝ)
37	5	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ ((⊤ ∧ ¬ 𝑗 ∈ ℙ) → 0 ∈ ℝ)
38	36, 37	ifclda 4528	. . . . . . . . . . . . . . . 16 ⊢ (⊤ → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
39	38	mptru 1574	. . . . . . . . . . . . . . 15 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ
40	39	elexi 3485	. . . . . . . . . . . . . 14 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ V
41	33, 8, 40	fvmpt 6990	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ ℕ → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
42	41	adantl 486	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
43	39	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
44	42, 43	eqeltrd 2869	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
45	44	adantlr 727	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℝ)
46		nnrp 13027	. . . . . . . . . . . . . . . 16 ⊢ (𝑗 ∈ ℕ → 𝑗 ∈ ℝ⁺)
47	46	adantl 486	. . . . . . . . . . . . . . 15 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 𝑗 ∈ ℝ⁺)
48	47	rpreccld 13069	. . . . . . . . . . . . . 14 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → (1 / 𝑗) ∈ ℝ⁺)
49	48	rpge0d 13063	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (1 / 𝑗))
50		0le0 12341	. . . . . . . . . . . . 13 ⊢ 0 ≤ 0
51		breq2 5117	. . . . . . . . . . . . . 14 ⊢ ((1 / 𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ (1 / 𝑗) ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
52		breq2 5117	. . . . . . . . . . . . . 14 ⊢ (0 = if(𝑗 ∈ ℙ, (1 / 𝑗), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
53	51, 52	ifboth 4532	. . . . . . . . . . . . 13 ⊢ ((0 ≤ (1 / 𝑗) ∧ 0 ≤ 0) → 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
54	49, 50, 53	sylancl 597	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
55	54, 42	breqtrrd 5143	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹‘𝑗))
56	55	adantlr 727	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → 0 ≤ (𝐹‘𝑗))
57	1, 29, 30, 45, 56	climserle 15713	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
58	57	ralrimiva 3163	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹)))
59		brralrspcev 5175	. . . . . . . 8 ⊢ ((( ⇝ ‘seq1( + , 𝐹)) ∈ ℝ ∧ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ ( ⇝ ‘seq1( + , 𝐹))) → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
60	28, 58, 59	syl2anc 595	. . . . . . 7 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
61		ffn 6706	. . . . . . . . 9 ⊢ (seq1( + , 𝐹):ℕ⟶ℝ → seq1( + , 𝐹) Fn ℕ)
62		breq1 5116	. . . . . . . . . 10 ⊢ (𝑧 = (seq1( + , 𝐹)‘𝑘) → (𝑧 ≤ 𝑥 ↔ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
63	62	ralrn 7084	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) Fn ℕ → (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥))
64	12, 61, 63	mp2b 10	. . . . . . . 8 ⊢ (∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
65	64	rexbii 3118	. . . . . . 7 ⊢ (∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑘 ∈ ℕ (seq1( + , 𝐹)‘𝑘) ≤ 𝑥)
66	60, 65	sylibr 237	. . . . . 6 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑥 ∈ ℝ ∀𝑧 ∈ ran seq1( + , 𝐹)𝑧 ≤ 𝑥)
67	14, 22, 66	suprcld 12177	. . . . 5 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ)
68		2rp 13020	. . . . . 6 ⊢ 2 ∈ ℝ⁺
69		rpreccl 13043	. . . . . 6 ⊢ (2 ∈ ℝ⁺ → (1 / 2) ∈ ℝ⁺)
70	68, 69	ax-mp 5	. . . . 5 ⊢ (1 / 2) ∈ ℝ⁺
71		ltsubrp 13053	. . . . 5 ⊢ ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ⁺) → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
72	67, 70, 71	sylancl 597	. . . 4 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ))
73		halfre 12456	. . . . . 6 ⊢ (1 / 2) ∈ ℝ
74		resubcl 11521	. . . . . 6 ⊢ ((sup(ran seq1( + , 𝐹), ℝ, < ) ∈ ℝ ∧ (1 / 2) ∈ ℝ) → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈ ℝ)
75	67, 73, 74	sylancl 597	. . . . 5 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) ∈ ℝ)
76		suprlub 12178	. . . . 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 1398	. . . 4 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < sup(ran seq1( + , 𝐹), ℝ, < ) ↔ ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦))
78	72, 77	mpbid 235	. . 3 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑦 ∈ ran seq1( + , 𝐹)(sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦)
79		breq2 5117	. . . . 5 ⊢ (𝑦 = (seq1( + , 𝐹)‘𝑘) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < 𝑦 ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
80	79	rexrn 7083	. . . 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 221	. 2 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
83		2re 12314	. . . . . 6 ⊢ 2 ∈ ℝ
84		2nn 12313	. . . . . . . . 9 ⊢ 2 ∈ ℕ
85		nnmulcl 12256	. . . . . . . . 9 ⊢ ((2 ∈ ℕ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
86	84, 29, 85	sylancr 598	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℕ)
87	86	peano2nnd 12249	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ)
88	87	nnnn0d 12564	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) ∈ ℕ₀)
89		reexpcl 14113	. . . . . 6 ⊢ ((2 ∈ ℝ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
90	83, 88, 89	sylancr 598	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℝ)
91	90	ltnrd 11343	. . . 4 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ¬ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1)))
92	29	adantr 485	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → 𝑘 ∈ ℕ)
93		peano2nn 12244	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝑘 + 1) ∈ ℕ)
94	93	adantl 486	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ)
95	94	nnnn0d 12564	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℕ₀)
96		nnexpcl 14109	. . . . . . . . . 10 ⊢ ((2 ∈ ℕ ∧ (𝑘 + 1) ∈ ℕ₀) → (2↑(𝑘 + 1)) ∈ ℕ)
97	84, 95, 96	sylancr 598	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℕ)
98	97	nnsqcld 14279	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
99	98	adantr 485	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → ((2↑(𝑘 + 1))↑2) ∈ ℕ)
100		breq1 5116	. . . . . . . . . . 11 ⊢ (𝑝 = 𝑤 → (𝑝 ∥ 𝑟 ↔ 𝑤 ∥ 𝑟))
101	100	notbid 321	. . . . . . . . . 10 ⊢ (𝑝 = 𝑤 → (¬ 𝑝 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑟))
102	101	cbvralvw 3249	. . . . . . . . 9 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟)
103		breq2 5117	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑛 → (𝑤 ∥ 𝑟 ↔ 𝑤 ∥ 𝑛))
104	103	notbid 321	. . . . . . . . . 10 ⊢ (𝑟 = 𝑛 → (¬ 𝑤 ∥ 𝑟 ↔ ¬ 𝑤 ∥ 𝑛))
105	104	ralbidv 3194	. . . . . . . . 9 ⊢ (𝑟 = 𝑛 → (∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛))
106	102, 105	bitrid 286	. . . . . . . 8 ⊢ (𝑟 = 𝑛 → (∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟 ↔ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛))
107	106	cbvrabv 3433	. . . . . . 7 ⊢ {𝑟 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑝 ∥ 𝑟} = {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ ∀𝑤 ∈ (ℙ ∖ (1...𝑘)) ¬ 𝑤 ∥ 𝑛}
108		simpll 778	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → seq1( + , 𝐹) ∈ dom ⇝ )
109		eleq1w 2852	. . . . . . . . . 10 ⊢ (𝑚 = 𝑗 → (𝑚 ∈ ℙ ↔ 𝑗 ∈ ℙ))
110		oveq2 7419	. . . . . . . . . 10 ⊢ (𝑚 = 𝑗 → (1 / 𝑚) = (1 / 𝑗))
111	109, 110	ifbieq1d 4517	. . . . . . . . 9 ⊢ (𝑚 = 𝑗 → if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
112	111	cbvsumv 15746	. . . . . . . 8 ⊢ Σ𝑚 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) = Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)
113		simpr 489	. . . . . . . 8 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2))
114	112, 113	eqbrtrid 5150	. . . . . . 7 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → Σ𝑚 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑚 ∈ ℙ, (1 / 𝑚), 0) < (1 / 2))
115		eqid 2769	. . . . . . 7 ⊢ (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)}) = (𝑤 ∈ ℕ ↦ {𝑛 ∈ (1...((2↑(𝑘 + 1))↑2)) ∣ (𝑤 ∈ ℙ ∧ 𝑤 ∥ 𝑛)})
116	8, 92, 99, 107, 108, 114, 115	prmreclem5 16979	. . . . . 6 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2)) → (((2↑(𝑘 + 1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))))
117	116	ex 417	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) → (((2↑(𝑘 + 1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2)))))
118		eqid 2769	. . . . . . . . 9 ⊢ (ℤ_≥‘(𝑘 + 1)) = (ℤ_≥‘(𝑘 + 1))
119	94	nnzd 12616	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℤ)
120		eluznn 12941	. . . . . . . . . . 11 ⊢ (((𝑘 + 1) ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
121	94, 120	sylan 591	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → 𝑗 ∈ ℕ)
122	121, 41	syl 18	. . . . . . . . 9 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
123	39	a1i 11	. . . . . . . . 9 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (ℤ_≥‘(𝑘 + 1))) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
124		simpl 487	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq1( + , 𝐹) ∈ dom ⇝ )
125	41	adantl 486	. . . . . . . . . . . 12 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
126	39	recni 11222	. . . . . . . . . . . . 13 ⊢ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ
127	126	a1i 11	. . . . . . . . . . . 12 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
128	125, 127	eqeltrd 2869	. . . . . . . . . . 11 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ ℕ) → (𝐹‘𝑗) ∈ ℂ)
129	1, 94, 128	iserex 15707	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝑘 + 1)( + , 𝐹) ∈ dom ⇝ ))
130	124, 129	mpbid 235	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → seq(𝑘 + 1)( + , 𝐹) ∈ dom ⇝ )
131	118, 119, 122, 123, 130	isumrecl 15815	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
132	73	a1i 11	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1 / 2) ∈ ℝ)
133		elfznn 13580	. . . . . . . . . . . 12 ⊢ (𝑗 ∈ (1...𝑘) → 𝑗 ∈ ℕ)
134	133	adantl 486	. . . . . . . . . . 11 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → 𝑗 ∈ ℕ)
135	134, 41	syl 18	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → (𝐹‘𝑗) = if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
136	29, 1	eleqtrdi 2879	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ (ℤ_≥‘1))
137	126	a1i 11	. . . . . . . . . 10 ⊢ (((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) ∧ 𝑗 ∈ (1...𝑘)) → if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℂ)
138	135, 136, 137	fsumser 15780	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (seq1( + , 𝐹)‘𝑘))
139	138, 27	eqeltrd 2869	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
140	131, 132, 139	ltadd2d 11365	. . . . . . 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 15893	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
142		nncn 12240	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℂ)
143	142	adantl 486	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ)
144		ax-1cn 11157	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℂ
145		pncan 11462	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 + 1) − 1) = 𝑘)
146	143, 144, 145	sylancl 597	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) − 1) = 𝑘)
147	146	oveq2d 7427	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (1...((𝑘 + 1) − 1)) = (1...𝑘))
148	147	sumeq1d 15750	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ (1...((𝑘 + 1) − 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0))
149	148	oveq1d 7426	. . . . . . . . 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 2804	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0)))
151	150	breq1d 5123	. . . . . . 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 285	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2))))
153		eqid 2769	. . . . . . . . . 10 ⊢ seq1( + , 𝐹) = seq1( + , 𝐹)
154	1, 153, 23, 42, 43, 54, 60	isumsup 15900	. . . . . . . . 9 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
155	154, 67	eqeltrd 2869	. . . . . . . 8 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
156	155	adantr 485	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ∈ ℝ)
157	156, 132, 139	ltsubaddd 11809	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) + (1 / 2))))
158	154	adantr 485	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) = sup(ran seq1( + , 𝐹), ℝ, < ))
159	158	oveq1d 7426	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) = (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)))
160	159, 138	breq12d 5126	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((Σ𝑗 ∈ ℕ if(𝑗 ∈ ℙ, (1 / 𝑗), 0) − (1 / 2)) < Σ𝑗 ∈ (1...𝑘)if(𝑗 ∈ ℙ, (1 / 𝑗), 0) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
161	152, 157, 160	3bitr2d 310	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (Σ𝑗 ∈ (ℤ_≥‘(𝑘 + 1))if(𝑗 ∈ ℙ, (1 / 𝑗), 0) < (1 / 2) ↔ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘)))
162		2cn 12315	. . . . . . . . . . . . 13 ⊢ 2 ∈ ℂ
163	162	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℂ)
164	144	a1i 11	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 1 ∈ ℂ)
165	163, 143, 164	adddid 11232	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · (𝑘 + 1)) = ((2 · 𝑘) + (2 · 1)))
166	94	nncnd 12248	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (𝑘 + 1) ∈ ℂ)
167		mulcom 11185	. . . . . . . . . . . 12 ⊢ (((𝑘 + 1) ∈ ℂ ∧ 2 ∈ ℂ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
168	166, 162, 167	sylancl 597	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (2 · (𝑘 + 1)))
169	86	nncnd 12248	. . . . . . . . . . . . 13 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) ∈ ℂ)
170	169, 164, 164	addassd 11230	. . . . . . . . . . . 12 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (1 + 1)))
171	144	2timesi 12377	. . . . . . . . . . . . 13 ⊢ (2 · 1) = (1 + 1)
172	171	oveq2i 7422	. . . . . . . . . . . 12 ⊢ ((2 · 𝑘) + (2 · 1)) = ((2 · 𝑘) + (1 + 1))
173	170, 172	eqtr4di 2822	. . . . . . . . . . 11 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2 · 𝑘) + 1) + 1) = ((2 · 𝑘) + (2 · 1)))
174	165, 168, 173	3eqtr4d 2814	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 1) · 2) = (((2 · 𝑘) + 1) + 1))
175	174	oveq2d 7427	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = (2↑(((2 · 𝑘) + 1) + 1)))
176		2nn0 12520	. . . . . . . . . . 11 ⊢ 2 ∈ ℕ₀
177	176	a1i 11	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 2 ∈ ℕ₀)
178	163, 177, 95	expmuld 14184	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((𝑘 + 1) · 2)) = ((2↑(𝑘 + 1))↑2))
179		expp1 14103	. . . . . . . . . 10 ⊢ ((2 ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑(((2 · 𝑘) + 1) + 1)) = ((2↑((2 · 𝑘) + 1)) · 2))
180	162, 88, 179	sylancr 598	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(((2 · 𝑘) + 1) + 1)) = ((2↑((2 · 𝑘) + 1)) · 2))
181	175, 178, 180	3eqtr3d 2812	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1))↑2) = ((2↑((2 · 𝑘) + 1)) · 2))
182	181	oveq1d 7426	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (((2↑((2 · 𝑘) + 1)) · 2) / 2))
183		expcl 14114	. . . . . . . . 9 ⊢ ((2 ∈ ℂ ∧ ((2 · 𝑘) + 1) ∈ ℕ₀) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
184	162, 88, 183	sylancr 598	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) ∈ ℂ)
185		2ne0 12346	. . . . . . . . 9 ⊢ 2 ≠ 0
186		divcan4 11898	. . . . . . . . 9 ⊢ (((2↑((2 · 𝑘) + 1)) ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
187	162, 185, 186	mp3an23 1479	. . . . . . . 8 ⊢ ((2↑((2 · 𝑘) + 1)) ∈ ℂ → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
188	184, 187	syl 18	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑((2 · 𝑘) + 1)) · 2) / 2) = (2↑((2 · 𝑘) + 1)))
189	182, 188	eqtrd 2804	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (((2↑(𝑘 + 1))↑2) / 2) = (2↑((2 · 𝑘) + 1)))
190		nnnn0 12510	. . . . . . . . 9 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℕ₀)
191	190	adantl 486	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
192	163, 95, 191	expaddd 14183	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + (𝑘 + 1))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
193	143	2timesd 12486	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2 · 𝑘) = (𝑘 + 𝑘))
194	193	oveq1d 7426	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = ((𝑘 + 𝑘) + 1))
195	143, 143, 164	addassd 11230	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((𝑘 + 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
196	194, 195	eqtrd 2804	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2 · 𝑘) + 1) = (𝑘 + (𝑘 + 1)))
197	196	oveq2d 7427	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑((2 · 𝑘) + 1)) = (2↑(𝑘 + (𝑘 + 1))))
198	97	nnrpd 13057	. . . . . . . . . 10 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (2↑(𝑘 + 1)) ∈ ℝ⁺)
199	198	rprege0d 13066	. . . . . . . . 9 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑(𝑘 + 1)) ∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))))
200		sqrtsq 15319	. . . . . . . . 9 ⊢ (((2↑(𝑘 + 1)) ∈ ℝ ∧ 0 ≤ (2↑(𝑘 + 1))) → (√‘((2↑(𝑘 + 1))↑2)) = (2↑(𝑘 + 1)))
201	199, 200	syl 18	. . . . . . . 8 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → (√‘((2↑(𝑘 + 1))↑2)) = (2↑(𝑘 + 1)))
202	201	oveq2d 7427	. . . . . . 7 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = ((2↑𝑘) · (2↑(𝑘 + 1))))
203	192, 197, 202	3eqtr4rd 2815	. . . . . 6 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) = (2↑((2 · 𝑘) + 1)))
204	189, 203	breq12d 5126	. . . . 5 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((((2↑(𝑘 + 1))↑2) / 2) < ((2↑𝑘) · (√‘((2↑(𝑘 + 1))↑2))) ↔ (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))))
205	117, 161, 204	3imtr3d 296	. . . 4 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ((sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘) → (2↑((2 · 𝑘) + 1)) < (2↑((2 · 𝑘) + 1))))
206	91, 205	mtod 201	. . 3 ⊢ ((seq1( + , 𝐹) ∈ dom ⇝ ∧ 𝑘 ∈ ℕ) → ¬ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
207	206	nrexdv 3166	. 2 ⊢ (seq1( + , 𝐹) ∈ dom ⇝ → ¬ ∃𝑘 ∈ ℕ (sup(ran seq1( + , 𝐹), ℝ, < ) − (1 / 2)) < (seq1( + , 𝐹)‘𝑘))
208	82, 207	pm2.65i 196	1 ⊢ ¬ seq1( + , 𝐹) ∈ dom ⇝

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 ↔ wb 209 ∧ wa 400 = wceq 1567 ⊤wtru 1568 ∈ wcel 2149 ≠ wne 2964 ∀wral 3085 ∃wrex 3095 {crab 3423 ∖ cdif 3910 ⊆ wss 3913 ∅c0 4294 ifcif 4492 class class class wbr 5113 ↦ cmpt 5196 dom cdm 5662 ran crn 5663 Fn wfn 6532 ⟶wf 6533 ‘cfv 6537 (class class class)co 7411 supcsup 9399 ℂcc 11097 ℝcr 11098 0cc0 11099 1c1 11100 + caddc 11102 · cmul 11104 < clt 11242 ≤ cle 11243 − cmin 11440 / cdiv 11870 ℕcn 12232 2c2 12294 ℕ₀cn0 12503 ℤ_≥cuz 12861 ℝ⁺crp 13015 ...cfz 13534 seqcseq 14036 ↑cexp 14096 √csqrt 15283 ⇝ cli 15534 Σcsu 15736 ∥ cdvds 16309 ℙcprime 16728

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-inf2 9609 ax-cnex 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-pre-sup 11177

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-se 5616 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-isom 6546 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7862 df-1st 7985 df-2nd 7986 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-oadd 8456 df-er 8693 df-map 8825 df-pm 8826 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-sup 9401 df-inf 9402 df-oi 9471 df-dju 9886 df-card 9924 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-div 11871 df-nn 12233 df-2 12302 df-3 12303 df-n0 12504 df-xnn0 12577 df-z 12591 df-uz 12862 df-q 12972 df-rp 13016 df-fz 13535 df-fzo 13682 df-fl 13824 df-mod 13902 df-seq 14037 df-exp 14097 df-hash 14366 df-cj 15149 df-re 15150 df-im 15151 df-sqrt 15285 df-abs 15286 df-clim 15538 df-rlim 15539 df-sum 15737 df-dvds 16310 df-gcd 16552 df-prm 16729 df-pc 16896

This theorem is referenced by: prmrec 16981

W3C validator