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 16852

Description: Lemma for prmrec 16855. Show by induction that the indexed (nondisjoint) union 𝑊‘𝑘 is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 16708, 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 7417	. . . . . . 7 ⊢ (𝑥 = 𝐾 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝐾))
2	1	iuneq1d 5025	. . . . . 6 ⊢ (𝑥 = 𝐾 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘))
3	2	fveq2d 6896	. . . . 5 ⊢ (𝑥 = 𝐾 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)))
4	1	sumeq1d 15647	. . . . . 6 ⊢ (𝑥 = 𝐾 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
5	4	oveq2d 7425	. . . . 5 ⊢ (𝑥 = 𝐾 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
6	3, 5	breq12d 5162	. . . 4 ⊢ (𝑥 = 𝐾 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
7	6	imbi2d 341	. . 3 ⊢ (𝑥 = 𝐾 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
8		oveq2 7417	. . . . . . 7 ⊢ (𝑥 = 𝑗 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑗))
9	8	iuneq1d 5025	. . . . . 6 ⊢ (𝑥 = 𝑗 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘))
10	9	fveq2d 6896	. . . . 5 ⊢ (𝑥 = 𝑗 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)))
11	8	sumeq1d 15647	. . . . . 6 ⊢ (𝑥 = 𝑗 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
12	11	oveq2d 7425	. . . . 5 ⊢ (𝑥 = 𝑗 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
13	10, 12	breq12d 5162	. . . 4 ⊢ (𝑥 = 𝑗 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
14	13	imbi2d 341	. . 3 ⊢ (𝑥 = 𝑗 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
15		oveq2 7417	. . . . . . 7 ⊢ (𝑥 = (𝑗 + 1) → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...(𝑗 + 1)))
16	15	iuneq1d 5025	. . . . . 6 ⊢ (𝑥 = (𝑗 + 1) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘))
17	16	fveq2d 6896	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)))
18	15	sumeq1d 15647	. . . . . 6 ⊢ (𝑥 = (𝑗 + 1) → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
19	18	oveq2d 7425	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
20	17, 19	breq12d 5162	. . . 4 ⊢ (𝑥 = (𝑗 + 1) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
21	20	imbi2d 341	. . 3 ⊢ (𝑥 = (𝑗 + 1) → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
22		oveq2 7417	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑁))
23	22	iuneq1d 5025	. . . . . 6 ⊢ (𝑥 = 𝑁 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
24	23	fveq2d 6896	. . . . 5 ⊢ (𝑥 = 𝑁 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
25	22	sumeq1d 15647	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
26	25	oveq2d 7425	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
27	24, 26	breq12d 5162	. . . 4 ⊢ (𝑥 = 𝑁 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
28	27	imbi2d 341	. . 3 ⊢ (𝑥 = 𝑁 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
29		0le0 12313	. . . . 5 ⊢ 0 ≤ 0
30		prmrec.3	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ)
31	30	nncnd 12228	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
32	31	mul01d 11413	. . . . 5 ⊢ (𝜑 → (𝑁 · 0) = 0)
33	29, 32	breqtrrid 5187	. . . 4 ⊢ (𝜑 → 0 ≤ (𝑁 · 0))
34		prmrec.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ)
35	34	nnred 12227	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℝ)
36	35	ltp1d 12144	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
37	34	nnzd 12585	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℤ)
38	37	peano2zd 12669	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾 + 1) ∈ ℤ)
39		fzn 13517	. . . . . . . . . 10 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
40	38, 37, 39	syl2anc 585	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
41	36, 40	mpbid 231	. . . . . . . 8 ⊢ (𝜑 → ((𝐾 + 1)...𝐾) = ∅)
42	41	iuneq1d 5025	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘))
43		0iun 5067	. . . . . . 7 ⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅
44	42, 43	eqtrdi 2789	. . . . . 6 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∅)
45	44	fveq2d 6896	. . . . 5 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = (♯‘∅))
46		hash0 14327	. . . . 5 ⊢ (♯‘∅) = 0
47	45, 46	eqtrdi 2789	. . . 4 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = 0)
48	41	sumeq1d 15647	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
49		sum0 15667	. . . . . 6 ⊢ Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
50	48, 49	eqtrdi 2789	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
51	50	oveq2d 7425	. . . 4 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
52	33, 47, 51	3brtr4d 5181	. . 3 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
53		fzfi 13937	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ Fin
54		elfzuz 13497	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑗) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
55	34	peano2nnd 12229	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ)
56		eluznn 12902	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
57	55, 56	sylan 581	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
58		eleq1 2822	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
59		breq1 5152	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛))
60	58, 59	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)))
61	60	rabbidv 3441	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
62		prmrec.7	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)})
63		ovex 7442	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ∈ V
64	63	rabex 5333	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V
65	61, 62, 64	fvmpt 6999	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
66	65	adantl 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
67		ssrab2 4078	. . . . . . . . . . . . . . . . 17 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁)
68	66, 67	eqsstrdi 4037	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁))
69	57, 68	syldan 592	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁))
70	54, 69	sylan2 594	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → (𝑊‘𝑘) ⊆ (1...𝑁))
71	70	ralrimiva 3147	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
72	71	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
73		iunss 5049	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
74	72, 73	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
75		ssfi 9173	. . . . . . . . . . 11 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin)
76	53, 74, 75	sylancr 588	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin)
77		hashcl 14316	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℕ₀)
78	76, 77	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℕ₀)
79	78	nn0red 12533	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℝ)
80	30	nnred 12227	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ)
81	80	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ ℝ)
82		fzfid 13938	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...𝑗) ∈ Fin)
83	55	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝐾 + 1) ∈ ℕ)
84	83, 54, 56	syl2an 597	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → 𝑘 ∈ ℕ)
85		nnrecre 12254	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
86		0re 11216	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
87		ifcl 4574	. . . . . . . . . . . 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 15680	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
91	81, 90	remulcld 11244	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
92		prmnn 16611	. . . . . . . . . . . 12 ⊢ ((𝑗 + 1) ∈ ℙ → (𝑗 + 1) ∈ ℕ)
93	92	nnrecred 12263	. . . . . . . . . . 11 ⊢ ((𝑗 + 1) ∈ ℙ → (1 / (𝑗 + 1)) ∈ ℝ)
94	93	adantl 483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (1 / (𝑗 + 1)) ∈ ℝ)
95		0red 11217	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ∈ ℝ)
96	94, 95	ifclda 4564	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℝ)
97	81, 96	remulcld 11244	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) ∈ ℝ)
98	79, 91, 97	leadd1d 11808	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))))
99		eluzp1p1 12850	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → (𝑗 + 1) ∈ (ℤ_≥‘(𝐾 + 1)))
100	99	adantl 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ (ℤ_≥‘(𝐾 + 1)))
101		simpl 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝜑)
102		elfzuz 13497	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1)) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
103	88	recnd 11242	. . . . . . . . . . . . . 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 2822	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
107		oveq2 7417	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (1 / 𝑘) = (1 / (𝑗 + 1)))
108	106, 107	ifbieq1d 4553	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))
109	100, 105, 108	fsumm1 15697	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
110		eluzelz 12832	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → 𝑗 ∈ ℤ)
111	110	adantl 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℤ)
112	111	zcnd 12667	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℂ)
113		ax-1cn 11168	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
114		pncan 11466	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
115	112, 113, 114	sylancl 587	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝑗 + 1) − 1) = 𝑗)
116	115	oveq2d 7425	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...((𝑗 + 1) − 1)) = ((𝐾 + 1)...𝑗))
117	116	sumeq1d 15647	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
118	117	oveq1d 7424	. . . . . . . . . . 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 2773	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
120	119	oveq2d 7425	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
121	31	adantr 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ ℂ)
122	90	recnd 11242	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
123	96	recnd 11242	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℂ)
124	121, 122, 123	adddid 11238	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
125	120, 124	eqtrd 2773	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
126	125	breq2d 5161	. . . . . . 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 3147	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
130	129	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
131		iunss 5049	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
132	130, 131	sylibr 233	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
133		ssfi 9173	. . . . . . . . . . 11 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin)
134	53, 132, 133	sylancr 588	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin)
135		hashcl 14316	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℕ₀)
136	134, 135	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℕ₀)
137	136	nn0red 12533	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℝ)
138		fveq2 6892	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑗 + 1) → (𝑊‘𝑘) = (𝑊‘(𝑗 + 1)))
139	138	sseq1d 4014	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → ((𝑊‘𝑘) ⊆ (1...𝑁) ↔ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)))
140	68	ralrimiva 3147	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁))
141	140	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁))
142		eluznn 12902	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℕ)
143	34, 142	sylan 581	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℕ)
144	143	peano2nnd 12229	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ ℕ)
145	139, 141, 144	rspcdva 3614	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁))
146		ssfi 9173	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
147	53, 145, 146	sylancr 588	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
148		hashcl 14316	. . . . . . . . . . 11 ⊢ ((𝑊‘(𝑗 + 1)) ∈ Fin → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ₀)
149	147, 148	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ₀)
150	149	nn0red 12533	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℝ)
151	79, 150	readdcld 11243	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ∈ ℝ)
152	79, 97	readdcld 11243	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈ ℝ)
153	38	adantr 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝐾 + 1) ∈ ℤ)
154		simpr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ (ℤ_≥‘𝐾))
155	34	nncnd 12228	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℂ)
156	155	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ ℂ)
157		pncan 11466	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 + 1) − 1) = 𝐾)
158	156, 113, 157	sylancl 587	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1) − 1) = 𝐾)
159	158	fveq2d 6896	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (ℤ_≥‘((𝐾 + 1) − 1)) = (ℤ_≥‘𝐾))
160	154, 159	eleqtrrd 2837	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ (ℤ_≥‘((𝐾 + 1) − 1)))
161		fzsuc2 13559	. . . . . . . . . . . . 13 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑗 ∈ (ℤ_≥‘((𝐾 + 1) − 1))) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
162	153, 160, 161	syl2anc 585	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
163	162	iuneq1d 5025	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘))
164		iunxun 5098	. . . . . . . . . . . 12 ⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘))
165		ovex 7442	. . . . . . . . . . . . . 14 ⊢ (𝑗 + 1) ∈ V
166	165, 138	iunxsn 5095	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘) = (𝑊‘(𝑗 + 1))
167	166	uneq2i 4161	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘)) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))
168	164, 167	eqtri 2761	. . . . . . . . . . 11 ⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))
169	163, 168	eqtrdi 2789	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1))))
170	169	fveq2d 6896	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) = (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))))
171		hashun2 14343	. . . . . . . . . 10 ⊢ ((∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ∈ Fin) → (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
172	76, 147, 171	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
173	170, 172	eqbrtrd 5171	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
174	81, 144	nndivred 12266	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 / (𝑗 + 1)) ∈ ℝ)
175		flle 13764	. . . . . . . . . . . . . 14 ⊢ ((𝑁 / (𝑗 + 1)) ∈ ℝ → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
176	174, 175	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
177		elfznn 13530	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
178	177	nncnd 12228	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
179	178	subid1d 11560	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...𝑁) → (𝑛 − 0) = 𝑛)
180	179	breq2d 5161	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑗 + 1) ∥ (𝑛 − 0) ↔ (𝑗 + 1) ∥ 𝑛))
181	180	rabbiia 3437	. . . . . . . . . . . . . . 15 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)} = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}
182	181	fveq2i 6895	. . . . . . . . . . . . . 14 ⊢ (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
183		1zzd 12593	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 1 ∈ ℤ)
184	30	nnnn0d 12532	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
185		nn0uz 12864	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ₀ = (ℤ_≥‘0)
186		1m1e0 12284	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
187	186	fveq2i 6895	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℤ_≥‘(1 − 1)) = (ℤ_≥‘0)
188	185, 187	eqtr4i 2764	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ = (ℤ_≥‘(1 − 1))
189	184, 188	eleqtrdi 2844	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(1 − 1)))
190	189	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ (ℤ_≥‘(1 − 1)))
191		0zd 12570	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 0 ∈ ℤ)
192	144, 183, 190, 191	hashdvds 16708	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))))
193	121	subid1d 11560	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 − 0) = 𝑁)
194	193	fvoveq1d 7431	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘((𝑁 − 0) / (𝑗 + 1))) = (⌊‘(𝑁 / (𝑗 + 1))))
195	186	oveq1i 7419	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 − 1) − 0) = (0 − 0)
196		0m0e0 12332	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 − 0) = 0
197	195, 196	eqtri 2761	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − 1) − 0) = 0
198	197	oveq1i 7419	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 1) − 0) / (𝑗 + 1)) = (0 / (𝑗 + 1))
199	144	nncnd 12228	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ ℂ)
200	144	nnne0d 12262	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ≠ 0)
201	199, 200	div0d 11989	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (0 / (𝑗 + 1)) = 0)
202	198, 201	eqtrid 2785	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (((1 − 1) − 0) / (𝑗 + 1)) = 0)
203	202	fveq2d 6896	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = (⌊‘0))
204		0z 12569	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
205		flid 13773	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ∈ ℤ → (⌊‘0) = 0)
206	204, 205	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⌊‘0) = 0
207	203, 206	eqtrdi 2789	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = 0)
208	194, 207	oveq12d 7427	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))) = ((⌊‘(𝑁 / (𝑗 + 1))) − 0))
209	174	flcld 13763	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℤ)
210	209	zcnd 12667	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℂ)
211	210	subid1d 11560	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((⌊‘(𝑁 / (𝑗 + 1))) − 0) = (⌊‘(𝑁 / (𝑗 + 1))))
212	192, 208, 211	3eqtrd 2777	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (⌊‘(𝑁 / (𝑗 + 1))))
213	182, 212	eqtr3id 2787	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) = (⌊‘(𝑁 / (𝑗 + 1))))
214	121, 199, 200	divrecd 11993	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 / (𝑗 + 1)) = (𝑁 · (1 / (𝑗 + 1))))
215	214	eqcomd 2739	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · (1 / (𝑗 + 1))) = (𝑁 / (𝑗 + 1)))
216	176, 213, 215	3brtr4d 5181	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
217	216	adantr 482	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
218		eleq1 2822	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
219		breq1 5152	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∥ 𝑛 ↔ (𝑗 + 1) ∥ 𝑛))
220	218, 219	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = (𝑗 + 1) → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)))
221	220	rabbidv 3441	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑗 + 1) → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
222	63	rabex 5333	. . . . . . . . . . . . . . . 16 ⊢ {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} ∈ V
223	221, 62, 222	fvmpt 6999	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 + 1) ∈ ℕ → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
224	144, 223	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
225	224	adantr 482	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
226		simpr 486	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑗 + 1) ∈ ℙ)
227	226	biantrurd 534	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → ((𝑗 + 1) ∥ 𝑛 ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)))
228	227	rabbidv 3441	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
229	225, 228	eqtr4d 2776	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
230	229	fveq2d 6896	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}))
231		iftrue 4535	. . . . . . . . . . . . 13 ⊢ ((𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = (1 / (𝑗 + 1)))
232	231	adantl 483	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = (1 / (𝑗 + 1)))
233	232	oveq2d 7425	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · (1 / (𝑗 + 1))))
234	217, 230, 233	3brtr4d 5181	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
235	29	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ≤ 0)
236		simpl 484	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛) → (𝑗 + 1) ∈ ℙ)
237	236	con3i 154	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑗 + 1) ∈ ℙ → ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
238	237	ralrimivw 3151	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑗 + 1) ∈ ℙ → ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
239		rabeq0 4385	. . . . . . . . . . . . . . 15 ⊢ ({𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅ ↔ ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
240	238, 239	sylibr 233	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑗 + 1) ∈ ℙ → {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅)
241	224, 240	sylan9eq 2793	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = ∅)
242	241	fveq2d 6896	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘∅))
243	242, 46	eqtrdi 2789	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = 0)
244		iffalse 4538	. . . . . . . . . . . . 13 ⊢ (¬ (𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = 0)
245	244	oveq2d 7425	. . . . . . . . . . . 12 ⊢ (¬ (𝑗 + 1) ∈ ℙ → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · 0))
246	32	adantr 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · 0) = 0)
247	245, 246	sylan9eqr 2795	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = 0)
248	235, 243, 247	3brtr4d 5181	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
249	234, 248	pm2.61dan 812	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
250	150, 97, 79, 249	leadd2dd 11829	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
251	137, 151, 152, 173, 250	letrd 11371	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
252		fzfid 13938	. . . . . . . . . 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 15680	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
256	81, 255	remulcld 11244	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
257		letr 11308	. . . . . . . 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 1372	. . . . . . 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 694	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
260	127, 259	sylbid 239	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
261	260	expcom 415	. . . 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 12894	. 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 205 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∀wral 3062 {crab 3433 ∖ cdif 3946 ∪ cun 3947 ⊆ wss 3949 ∅c0 4323 ifcif 4529 {csn 4629 ∪ ciun 4998 class class class wbr 5149 ↦ cmpt 5232 dom cdm 5677 ‘cfv 6544 (class class class)co 7409 Fincfn 8939 ℂcc 11108 ℝcr 11109 0cc0 11110 1c1 11111 + caddc 11113 · cmul 11115 < clt 11248 ≤ cle 11249 − cmin 11444 / cdiv 11871 ℕcn 12212 2c2 12267 ℕ₀cn0 12472 ℤcz 12558 ℤ_≥cuz 12822 ...cfz 13484 ⌊cfl 13755 seqcseq 13966 ♯chash 14290 ⇝ cli 15428 Σcsu 15632 ∥ cdvds 16197 ℙcprime 16608

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5286 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-inf2 9636 ax-cnex 11166 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 ax-pre-sup 11188

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-int 4952 df-iun 5000 df-br 5150 df-opab 5212 df-mpt 5233 df-tr 5267 df-id 5575 df-eprel 5581 df-po 5589 df-so 5590 df-fr 5632 df-se 5633 df-we 5634 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-pred 6301 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-isom 6553 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-om 7856 df-1st 7975 df-2nd 7976 df-frecs 8266 df-wrecs 8297 df-recs 8371 df-rdg 8410 df-1o 8466 df-oadd 8470 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9437 df-inf 9438 df-oi 9505 df-dju 9896 df-card 9934 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 df-nn 12213 df-2 12275 df-3 12276 df-n0 12473 df-xnn0 12545 df-z 12559 df-uz 12823 df-rp 12975 df-fz 13485 df-fzo 13628 df-fl 13757 df-seq 13967 df-exp 14028 df-hash 14291 df-cj 15046 df-re 15047 df-im 15048 df-sqrt 15182 df-abs 15183 df-clim 15432 df-sum 15633 df-dvds 16198 df-prm 16609

This theorem is referenced by: prmreclem5 16853

W3C validator