prmreclem4 - Metamath Proof Explorer

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

Theorem prmreclem4 16881

Description: Lemma for prmrec 16884. Show by induction that the indexed (nondisjoint) union 𝑊‘𝑘 is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 16736, to show that the number of numbers in 1...𝑁 that divide 𝑘 is at most 𝑁 / 𝑘. (Contributed by Mario Carneiro, 6-Aug-2014.)

**Hypotheses**
Ref	Expression
prmrec.1	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
prmrec.2	⊢ (𝜑 → 𝐾 ∈ ℕ)
prmrec.3	⊢ (𝜑 → 𝑁 ∈ ℕ)
prmrec.4	⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
prmrec.5	⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
prmrec.6	⊢ (𝜑 → Σ𝑘 ∈ (ℤ_≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
prmrec.7	⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)})

**Assertion**
Ref	Expression
prmreclem4	⊢ (𝜑 → (𝑁 ∈ (ℤ_≥‘𝐾) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))

Distinct variable groups: 𝑘,𝑛,𝑝,𝐹 𝑘,𝐾,𝑛,𝑝 𝑘,𝑀,𝑛,𝑝 𝜑,𝑘,𝑛,𝑝 𝑘,𝑊 𝑘,𝑁,𝑛,𝑝 Allowed substitution hints: 𝑊(𝑛,𝑝)

Proof of Theorem prmreclem4 Dummy variables 𝑗 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7368	. . . . . . 7 ⊢ (𝑥 = 𝐾 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝐾))
2	1	iuneq1d 4962	. . . . . 6 ⊢ (𝑥 = 𝐾 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘))
3	2	fveq2d 6838	. . . . 5 ⊢ (𝑥 = 𝐾 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)))
4	1	sumeq1d 15653	. . . . . 6 ⊢ (𝑥 = 𝐾 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
5	4	oveq2d 7376	. . . . 5 ⊢ (𝑥 = 𝐾 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
6	3, 5	breq12d 5099	. . . 4 ⊢ (𝑥 = 𝐾 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
7	6	imbi2d 340	. . 3 ⊢ (𝑥 = 𝐾 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
8		oveq2 7368	. . . . . . 7 ⊢ (𝑥 = 𝑗 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑗))
9	8	iuneq1d 4962	. . . . . 6 ⊢ (𝑥 = 𝑗 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘))
10	9	fveq2d 6838	. . . . 5 ⊢ (𝑥 = 𝑗 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)))
11	8	sumeq1d 15653	. . . . . 6 ⊢ (𝑥 = 𝑗 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
12	11	oveq2d 7376	. . . . 5 ⊢ (𝑥 = 𝑗 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
13	10, 12	breq12d 5099	. . . 4 ⊢ (𝑥 = 𝑗 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
14	13	imbi2d 340	. . 3 ⊢ (𝑥 = 𝑗 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
15		oveq2 7368	. . . . . . 7 ⊢ (𝑥 = (𝑗 + 1) → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...(𝑗 + 1)))
16	15	iuneq1d 4962	. . . . . 6 ⊢ (𝑥 = (𝑗 + 1) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘))
17	16	fveq2d 6838	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)))
18	15	sumeq1d 15653	. . . . . 6 ⊢ (𝑥 = (𝑗 + 1) → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
19	18	oveq2d 7376	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
20	17, 19	breq12d 5099	. . . 4 ⊢ (𝑥 = (𝑗 + 1) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
21	20	imbi2d 340	. . 3 ⊢ (𝑥 = (𝑗 + 1) → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
22		oveq2 7368	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑁))
23	22	iuneq1d 4962	. . . . . 6 ⊢ (𝑥 = 𝑁 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
24	23	fveq2d 6838	. . . . 5 ⊢ (𝑥 = 𝑁 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
25	22	sumeq1d 15653	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
26	25	oveq2d 7376	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
27	24, 26	breq12d 5099	. . . 4 ⊢ (𝑥 = 𝑁 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
28	27	imbi2d 340	. . 3 ⊢ (𝑥 = 𝑁 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
29		0le0 12273	. . . . 5 ⊢ 0 ≤ 0
30		prmrec.3	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ)
31	30	nncnd 12181	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
32	31	mul01d 11336	. . . . 5 ⊢ (𝜑 → (𝑁 · 0) = 0)
33	29, 32	breqtrrid 5124	. . . 4 ⊢ (𝜑 → 0 ≤ (𝑁 · 0))
34		prmrec.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ)
35	34	nnred 12180	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℝ)
36	35	ltp1d 12077	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
37	34	nnzd 12541	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℤ)
38	37	peano2zd 12627	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾 + 1) ∈ ℤ)
39		fzn 13485	. . . . . . . . . 10 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
40	38, 37, 39	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
41	36, 40	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((𝐾 + 1)...𝐾) = ∅)
42	41	iuneq1d 4962	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘))
43		0iun 5006	. . . . . . 7 ⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅
44	42, 43	eqtrdi 2788	. . . . . 6 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∅)
45	44	fveq2d 6838	. . . . 5 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = (♯‘∅))
46		hash0 14320	. . . . 5 ⊢ (♯‘∅) = 0
47	45, 46	eqtrdi 2788	. . . 4 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = 0)
48	41	sumeq1d 15653	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
49		sum0 15674	. . . . . 6 ⊢ Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
50	48, 49	eqtrdi 2788	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
51	50	oveq2d 7376	. . . 4 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
52	33, 47, 51	3brtr4d 5118	. . 3 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
53		fzfi 13925	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ Fin
54		elfzuz 13465	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑗) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
55	34	peano2nnd 12182	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ)
56		eluznn 12859	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
57	55, 56	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
58		eleq1 2825	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
59		breq1 5089	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛))
60	58, 59	anbi12d 633	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)))
61	60	rabbidv 3397	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
62		prmrec.7	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)})
63		ovex 7393	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ∈ V
64	63	rabex 5276	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V
65	61, 62, 64	fvmpt 6941	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
66	65	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
67		ssrab2 4021	. . . . . . . . . . . . . . . . 17 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁)
68	66, 67	eqsstrdi 3967	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁))
69	57, 68	syldan 592	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁))
70	54, 69	sylan2 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → (𝑊‘𝑘) ⊆ (1...𝑁))
71	70	ralrimiva 3130	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
72	71	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
73		iunss 4988	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
74	72, 73	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
75		ssfi 9100	. . . . . . . . . . 11 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin)
76	53, 74, 75	sylancr 588	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin)
77		hashcl 14309	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℕ₀)
78	76, 77	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℕ₀)
79	78	nn0red 12490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℝ)
80	30	nnred 12180	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ)
81	80	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ ℝ)
82		fzfid 13926	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...𝑗) ∈ Fin)
83	55	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝐾 + 1) ∈ ℕ)
84	83, 54, 56	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → 𝑘 ∈ ℕ)
85		nnrecre 12210	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
86		0re 11137	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
87		ifcl 4513	. . . . . . . . . . . 12 ⊢ (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
88	85, 86, 87	sylancl 587	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
89	84, 88	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
90	82, 89	fsumrecl 15687	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
91	81, 90	remulcld 11166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
92		prmnn 16634	. . . . . . . . . . . 12 ⊢ ((𝑗 + 1) ∈ ℙ → (𝑗 + 1) ∈ ℕ)
93	92	nnrecred 12219	. . . . . . . . . . 11 ⊢ ((𝑗 + 1) ∈ ℙ → (1 / (𝑗 + 1)) ∈ ℝ)
94	93	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (1 / (𝑗 + 1)) ∈ ℝ)
95		0red 11138	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ∈ ℝ)
96	94, 95	ifclda 4503	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℝ)
97	81, 96	remulcld 11166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) ∈ ℝ)
98	79, 91, 97	leadd1d 11735	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))))
99		eluzp1p1 12807	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → (𝑗 + 1) ∈ (ℤ_≥‘(𝐾 + 1)))
100	99	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ (ℤ_≥‘(𝐾 + 1)))
101		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝜑)
102		elfzuz 13465	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1)) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
103	88	recnd 11164	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
104	57, 103	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
105	101, 102, 104	syl2an 597	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
106		eleq1 2825	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
107		oveq2 7368	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (1 / 𝑘) = (1 / (𝑗 + 1)))
108	106, 107	ifbieq1d 4492	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))
109	100, 105, 108	fsumm1 15704	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
110		eluzelz 12789	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → 𝑗 ∈ ℤ)
111	110	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℤ)
112	111	zcnd 12625	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℂ)
113		ax-1cn 11087	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
114		pncan 11390	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
115	112, 113, 114	sylancl 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝑗 + 1) − 1) = 𝑗)
116	115	oveq2d 7376	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...((𝑗 + 1) − 1)) = ((𝐾 + 1)...𝑗))
117	116	sumeq1d 15653	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
118	117	oveq1d 7375	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
119	109, 118	eqtrd 2772	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
120	119	oveq2d 7376	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
121	31	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ ℂ)
122	90	recnd 11164	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
123	96	recnd 11164	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℂ)
124	121, 122, 123	adddid 11160	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
125	120, 124	eqtrd 2772	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
126	125	breq2d 5098	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))))
127	98, 126	bitr4d 282	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
128	102, 69	sylan2 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁))
129	128	ralrimiva 3130	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
130	129	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
131		iunss 4988	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
132	130, 131	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
133		ssfi 9100	. . . . . . . . . . 11 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin)
134	53, 132, 133	sylancr 588	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin)
135		hashcl 14309	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℕ₀)
136	134, 135	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℕ₀)
137	136	nn0red 12490	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℝ)
138		fveq2 6834	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑗 + 1) → (𝑊‘𝑘) = (𝑊‘(𝑗 + 1)))
139	138	sseq1d 3954	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → ((𝑊‘𝑘) ⊆ (1...𝑁) ↔ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)))
140	68	ralrimiva 3130	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁))
141	140	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁))
142		eluznn 12859	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℕ)
143	34, 142	sylan 581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℕ)
144	143	peano2nnd 12182	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ ℕ)
145	139, 141, 144	rspcdva 3566	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁))
146		ssfi 9100	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
147	53, 145, 146	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
148		hashcl 14309	. . . . . . . . . . 11 ⊢ ((𝑊‘(𝑗 + 1)) ∈ Fin → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ₀)
149	147, 148	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ₀)
150	149	nn0red 12490	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℝ)
151	79, 150	readdcld 11165	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ∈ ℝ)
152	79, 97	readdcld 11165	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈ ℝ)
153	38	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝐾 + 1) ∈ ℤ)
154		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ (ℤ_≥‘𝐾))
155	34	nncnd 12181	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℂ)
156	155	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ ℂ)
157		pncan 11390	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 + 1) − 1) = 𝐾)
158	156, 113, 157	sylancl 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1) − 1) = 𝐾)
159	158	fveq2d 6838	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (ℤ_≥‘((𝐾 + 1) − 1)) = (ℤ_≥‘𝐾))
160	154, 159	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ (ℤ_≥‘((𝐾 + 1) − 1)))
161		fzsuc2 13527	. . . . . . . . . . . . 13 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑗 ∈ (ℤ_≥‘((𝐾 + 1) − 1))) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
162	153, 160, 161	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
163	162	iuneq1d 4962	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘))
164		iunxun 5037	. . . . . . . . . . . 12 ⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘))
165		ovex 7393	. . . . . . . . . . . . . 14 ⊢ (𝑗 + 1) ∈ V
166	165, 138	iunxsn 5034	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘) = (𝑊‘(𝑗 + 1))
167	166	uneq2i 4106	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘)) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))
168	164, 167	eqtri 2760	. . . . . . . . . . 11 ⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))
169	163, 168	eqtrdi 2788	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1))))
170	169	fveq2d 6838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) = (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))))
171		hashun2 14336	. . . . . . . . . 10 ⊢ ((∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ∈ Fin) → (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
172	76, 147, 171	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
173	170, 172	eqbrtrd 5108	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
174	81, 144	nndivred 12222	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 / (𝑗 + 1)) ∈ ℝ)
175		flle 13749	. . . . . . . . . . . . . 14 ⊢ ((𝑁 / (𝑗 + 1)) ∈ ℝ → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
176	174, 175	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
177		elfznn 13498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
178	177	nncnd 12181	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
179	178	subid1d 11485	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...𝑁) → (𝑛 − 0) = 𝑛)
180	179	breq2d 5098	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑗 + 1) ∥ (𝑛 − 0) ↔ (𝑗 + 1) ∥ 𝑛))
181	180	rabbiia 3394	. . . . . . . . . . . . . . 15 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)} = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}
182	181	fveq2i 6837	. . . . . . . . . . . . . 14 ⊢ (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
183		1zzd 12549	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 1 ∈ ℤ)
184	30	nnnn0d 12489	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
185		nn0uz 12817	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ₀ = (ℤ_≥‘0)
186		1m1e0 12244	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
187	186	fveq2i 6837	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℤ_≥‘(1 − 1)) = (ℤ_≥‘0)
188	185, 187	eqtr4i 2763	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ = (ℤ_≥‘(1 − 1))
189	184, 188	eleqtrdi 2847	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(1 − 1)))
190	189	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ (ℤ_≥‘(1 − 1)))
191		0zd 12527	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 0 ∈ ℤ)
192	144, 183, 190, 191	hashdvds 16736	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))))
193	121	subid1d 11485	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 − 0) = 𝑁)
194	193	fvoveq1d 7382	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘((𝑁 − 0) / (𝑗 + 1))) = (⌊‘(𝑁 / (𝑗 + 1))))
195	186	oveq1i 7370	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 − 1) − 0) = (0 − 0)
196		0m0e0 12287	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 − 0) = 0
197	195, 196	eqtri 2760	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − 1) − 0) = 0
198	197	oveq1i 7370	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 1) − 0) / (𝑗 + 1)) = (0 / (𝑗 + 1))
199	144	nncnd 12181	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ ℂ)
200	144	nnne0d 12218	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ≠ 0)
201	199, 200	div0d 11921	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (0 / (𝑗 + 1)) = 0)
202	198, 201	eqtrid 2784	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (((1 − 1) − 0) / (𝑗 + 1)) = 0)
203	202	fveq2d 6838	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = (⌊‘0))
204		0z 12526	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
205		flid 13758	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ∈ ℤ → (⌊‘0) = 0)
206	204, 205	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⌊‘0) = 0
207	203, 206	eqtrdi 2788	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = 0)
208	194, 207	oveq12d 7378	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))) = ((⌊‘(𝑁 / (𝑗 + 1))) − 0))
209	174	flcld 13748	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℤ)
210	209	zcnd 12625	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℂ)
211	210	subid1d 11485	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((⌊‘(𝑁 / (𝑗 + 1))) − 0) = (⌊‘(𝑁 / (𝑗 + 1))))
212	192, 208, 211	3eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (⌊‘(𝑁 / (𝑗 + 1))))
213	182, 212	eqtr3id 2786	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) = (⌊‘(𝑁 / (𝑗 + 1))))
214	121, 199, 200	divrecd 11925	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 / (𝑗 + 1)) = (𝑁 · (1 / (𝑗 + 1))))
215	214	eqcomd 2743	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · (1 / (𝑗 + 1))) = (𝑁 / (𝑗 + 1)))
216	176, 213, 215	3brtr4d 5118	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
217	216	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
218		eleq1 2825	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
219		breq1 5089	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∥ 𝑛 ↔ (𝑗 + 1) ∥ 𝑛))
220	218, 219	anbi12d 633	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = (𝑗 + 1) → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)))
221	220	rabbidv 3397	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑗 + 1) → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
222	63	rabex 5276	. . . . . . . . . . . . . . . 16 ⊢ {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} ∈ V
223	221, 62, 222	fvmpt 6941	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 + 1) ∈ ℕ → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
224	144, 223	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
225	224	adantr 480	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
226		simpr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑗 + 1) ∈ ℙ)
227	226	biantrurd 532	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → ((𝑗 + 1) ∥ 𝑛 ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)))
228	227	rabbidv 3397	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
229	225, 228	eqtr4d 2775	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
230	229	fveq2d 6838	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}))
231		iftrue 4473	. . . . . . . . . . . . 13 ⊢ ((𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = (1 / (𝑗 + 1)))
232	231	adantl 481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = (1 / (𝑗 + 1)))
233	232	oveq2d 7376	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · (1 / (𝑗 + 1))))
234	217, 230, 233	3brtr4d 5118	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
235	29	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ≤ 0)
236		simpl 482	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛) → (𝑗 + 1) ∈ ℙ)
237	236	con3i 154	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑗 + 1) ∈ ℙ → ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
238	237	ralrimivw 3134	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑗 + 1) ∈ ℙ → ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
239		rabeq0 4329	. . . . . . . . . . . . . . 15 ⊢ ({𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅ ↔ ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
240	238, 239	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑗 + 1) ∈ ℙ → {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅)
241	224, 240	sylan9eq 2792	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = ∅)
242	241	fveq2d 6838	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘∅))
243	242, 46	eqtrdi 2788	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = 0)
244		iffalse 4476	. . . . . . . . . . . . 13 ⊢ (¬ (𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = 0)
245	244	oveq2d 7376	. . . . . . . . . . . 12 ⊢ (¬ (𝑗 + 1) ∈ ℙ → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · 0))
246	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · 0) = 0)
247	245, 246	sylan9eqr 2794	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = 0)
248	235, 243, 247	3brtr4d 5118	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
249	234, 248	pm2.61dan 813	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
250	150, 97, 79, 249	leadd2dd 11756	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
251	137, 151, 152, 173, 250	letrd 11294	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
252		fzfid 13926	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) ∈ Fin)
253	57, 88	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
254	101, 102, 253	syl2an 597	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
255	252, 254	fsumrecl 15687	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
256	81, 255	remulcld 11166	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
257		letr 11231	. . . . . . . 8 ⊢ (((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℝ ∧ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈ ℝ ∧ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ) → (((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∧ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
258	137, 152, 256, 257	syl3anc 1374	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∧ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
259	251, 258	mpand 696	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
260	127, 259	sylbid 240	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
261	260	expcom 413	. . . 4 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → (𝜑 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
262	261	a2d 29	. . 3 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
263	7, 14, 21, 28, 52, 262	uzind4i 12851	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘𝐾) → (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
264	263	com12 32	1 ⊢ (𝜑 → (𝑁 ∈ (ℤ_≥‘𝐾) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ∀wral 3052 {crab 3390 ∖ cdif 3887 ∪ cun 3888 ⊆ wss 3890 ∅c0 4274 ifcif 4467 {csn 4568 ∪ ciun 4934 class class class wbr 5086 ↦ cmpt 5167 dom cdm 5624 ‘cfv 6492 (class class class)co 7360 Fincfn 8886 ℂcc 11027 ℝcr 11028 0cc0 11029 1c1 11030 + caddc 11032 · cmul 11034 < clt 11170 ≤ cle 11171 − cmin 11368 / cdiv 11798 ℕcn 12165 2c2 12227 ℕ₀cn0 12428 ℤcz 12515 ℤ_≥cuz 12779 ...cfz 13452 ⌊cfl 13740 seqcseq 13954 ♯chash 14283 ⇝ cli 15437 Σcsu 15639 ∥ cdvds 16212 ℙcprime 16631

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682 ax-inf2 9553 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3343 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-int 4891 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 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 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-1o 8398 df-oadd 8402 df-er 8636 df-en 8887 df-dom 8888 df-sdom 8889 df-fin 8890 df-sup 9348 df-inf 9349 df-oi 9418 df-dju 9816 df-card 9854 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-n0 12429 df-xnn0 12502 df-z 12516 df-uz 12780 df-rp 12934 df-fz 13453 df-fzo 13600 df-fl 13742 df-seq 13955 df-exp 14015 df-hash 14284 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-clim 15441 df-sum 15640 df-dvds 16213 df-prm 16632

This theorem is referenced by: prmreclem5 16882

W3C validator