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 17001

Description: Lemma for prmrec 17004. Show by induction that the indexed (nondisjoint) union 𝑊‘𝑘 is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 16856, 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 7427	. . . . . . 7 ⊢ (𝑥 = 𝐾 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝐾))
2	1	iuneq1d 4986	. . . . . 6 ⊢ (𝑥 = 𝐾 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘))
3	2	fveq2d 6889	. . . . 5 ⊢ (𝑥 = 𝐾 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)))
4	1	sumeq1d 15775	. . . . . 6 ⊢ (𝑥 = 𝐾 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
5	4	oveq2d 7435	. . . . 5 ⊢ (𝑥 = 𝐾 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
6	3, 5	breq12d 5124	. . . 4 ⊢ (𝑥 = 𝐾 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
7	6	imbi2d 343	. . 3 ⊢ (𝑥 = 𝐾 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
8		oveq2 7427	. . . . . . 7 ⊢ (𝑥 = 𝑗 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑗))
9	8	iuneq1d 4986	. . . . . 6 ⊢ (𝑥 = 𝑗 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘))
10	9	fveq2d 6889	. . . . 5 ⊢ (𝑥 = 𝑗 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)))
11	8	sumeq1d 15775	. . . . . 6 ⊢ (𝑥 = 𝑗 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
12	11	oveq2d 7435	. . . . 5 ⊢ (𝑥 = 𝑗 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
13	10, 12	breq12d 5124	. . . 4 ⊢ (𝑥 = 𝑗 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
14	13	imbi2d 343	. . 3 ⊢ (𝑥 = 𝑗 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
15		oveq2 7427	. . . . . . 7 ⊢ (𝑥 = (𝑗 + 1) → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...(𝑗 + 1)))
16	15	iuneq1d 4986	. . . . . 6 ⊢ (𝑥 = (𝑗 + 1) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘))
17	16	fveq2d 6889	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)))
18	15	sumeq1d 15775	. . . . . 6 ⊢ (𝑥 = (𝑗 + 1) → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
19	18	oveq2d 7435	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
20	17, 19	breq12d 5124	. . . 4 ⊢ (𝑥 = (𝑗 + 1) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
21	20	imbi2d 343	. . 3 ⊢ (𝑥 = (𝑗 + 1) → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
22		oveq2 7427	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑁))
23	22	iuneq1d 4986	. . . . . 6 ⊢ (𝑥 = 𝑁 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
24	23	fveq2d 6889	. . . . 5 ⊢ (𝑥 = 𝑁 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
25	22	sumeq1d 15775	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
26	25	oveq2d 7435	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
27	24, 26	breq12d 5124	. . . 4 ⊢ (𝑥 = 𝑁 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
28	27	imbi2d 343	. . 3 ⊢ (𝑥 = 𝑁 → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) ↔ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
29		0le0 12357	. . . . 5 ⊢ 0 ≤ 0
30		prmrec.3	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ)
31	30	nncnd 12264	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
32	31	mul01d 11424	. . . . 5 ⊢ (𝜑 → (𝑁 · 0) = 0)
33	29, 32	breqtrrid 5151	. . . 4 ⊢ (𝜑 → 0 ≤ (𝑁 · 0))
34		prmrec.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ)
35	34	nnred 12263	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℝ)
36	35	ltp1d 12160	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
37	34	nnzd 12632	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℤ)
38	37	peano2zd 12719	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾 + 1) ∈ ℤ)
39		fzn 13584	. . . . . . . . . 10 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
40	38, 37, 39	syl2anc 596	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
41	36, 40	mpbid 235	. . . . . . . 8 ⊢ (𝜑 → ((𝐾 + 1)...𝐾) = ∅)
42	41	iuneq1d 4986	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘))
43		0iun 5029	. . . . . . 7 ⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅
44	42, 43	eqtrdi 2816	. . . . . 6 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∅)
45	44	fveq2d 6889	. . . . 5 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = (♯‘∅))
46		hash0 14421	. . . . 5 ⊢ (♯‘∅) = 0
47	45, 46	eqtrdi 2816	. . . 4 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = 0)
48	41	sumeq1d 15775	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
49		sum0 15795	. . . . . 6 ⊢ Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
50	48, 49	eqtrdi 2816	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
51	50	oveq2d 7435	. . . 4 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
52	33, 47, 51	3brtr4d 5145	. . 3 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
53		fzfi 14026	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ Fin
54		elfzuz 13564	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑗) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
55	34	peano2nnd 12265	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ)
56		eluznn 12958	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
57	55, 56	sylan 592	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
58		eleq1 2853	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
59		breq1 5114	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛))
60	58, 59	anbi12d 644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)))
61	60	rabbidv 3425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
62		prmrec.7	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)})
63		ovex 7452	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ∈ V
64	63	rabex 5311	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V
65	61, 62, 64	fvmpt 6993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
66	65	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
67		ssrab2 4035	. . . . . . . . . . . . . . . . 17 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁)
68	66, 67	eqsstrdi 3982	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁))
69	57, 68	syldan 603	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁))
70	54, 69	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → (𝑊‘𝑘) ⊆ (1...𝑁))
71	70	ralrimiva 3159	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
72	71	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
73		iunss 5011	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
74	72, 73	sylibr 237	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
75		ssfi 9164	. . . . . . . . . . 11 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin)
76	53, 74, 75	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin)
77		hashcl 14410	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℕ₀)
78	76, 77	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℕ₀)
79	78	nn0red 12581	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℝ)
80	30	nnred 12263	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ)
81	80	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ ℝ)
82		fzfid 14027	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...𝑗) ∈ Fin)
83	55	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝐾 + 1) ∈ ℕ)
84	83, 54, 56	syl2an 608	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → 𝑘 ∈ ℕ)
85		nnrecre 12293	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
86		0re 11225	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
87		ifcl 4535	. . . . . . . . . . . 12 ⊢ (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
88	85, 86, 87	sylancl 598	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
89	84, 88	syl 18	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
90	82, 89	fsumrecl 15808	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
91	81, 90	remulcld 11254	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
92		prmnn 16754	. . . . . . . . . . . 12 ⊢ ((𝑗 + 1) ∈ ℙ → (𝑗 + 1) ∈ ℕ)
93	92	nnrecred 12302	. . . . . . . . . . 11 ⊢ ((𝑗 + 1) ∈ ℙ → (1 / (𝑗 + 1)) ∈ ℝ)
94	93	adantl 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (1 / (𝑗 + 1)) ∈ ℝ)
95		0red 11226	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ∈ ℝ)
96	94, 95	ifclda 4525	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℝ)
97	81, 96	remulcld 11254	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) ∈ ℝ)
98	79, 91, 97	leadd1d 11823	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))))
99		eluzp1p1 12906	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → (𝑗 + 1) ∈ (ℤ_≥‘(𝐾 + 1)))
100	99	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ (ℤ_≥‘(𝐾 + 1)))
101		simpl 488	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝜑)
102		elfzuz 13564	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1)) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
103	88	recnd 11252	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
104	57, 103	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
105	101, 102, 104	syl2an 608	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
106		eleq1 2853	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
107		oveq2 7427	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (1 / 𝑘) = (1 / (𝑗 + 1)))
108	106, 107	ifbieq1d 4514	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))
109	100, 105, 108	fsumm1 15825	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
110		eluzelz 12888	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → 𝑗 ∈ ℤ)
111	110	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℤ)
112	111	zcnd 12717	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℂ)
113		ax-1cn 11173	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
114		pncan 11478	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
115	112, 113, 114	sylancl 598	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝑗 + 1) − 1) = 𝑗)
116	115	oveq2d 7435	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...((𝑗 + 1) − 1)) = ((𝐾 + 1)...𝑗))
117	116	sumeq1d 15775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
118	117	oveq1d 7434	. . . . . . . . . . 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 2800	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
120	119	oveq2d 7435	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
121	31	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ ℂ)
122	90	recnd 11252	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
123	96	recnd 11252	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℂ)
124	121, 122, 123	adddid 11248	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
125	120, 124	eqtrd 2800	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
126	125	breq2d 5123	. . . . . . 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 285	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
128	102, 69	sylan2 605	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁))
129	128	ralrimiva 3159	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
130	129	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
131		iunss 5011	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
132	130, 131	sylibr 237	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
133		ssfi 9164	. . . . . . . . . . 11 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin)
134	53, 132, 133	sylancr 599	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin)
135		hashcl 14410	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℕ₀)
136	134, 135	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℕ₀)
137	136	nn0red 12581	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℝ)
138		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑗 + 1) → (𝑊‘𝑘) = (𝑊‘(𝑗 + 1)))
139	138	sseq1d 3969	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → ((𝑊‘𝑘) ⊆ (1...𝑁) ↔ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)))
140	68	ralrimiva 3159	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁))
141	140	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁))
142		eluznn 12958	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℕ)
143	34, 142	sylan 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℕ)
144	143	peano2nnd 12265	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ ℕ)
145	139, 141, 144	rspcdva 3584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁))
146		ssfi 9164	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
147	53, 145, 146	sylancr 599	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
148		hashcl 14410	. . . . . . . . . . 11 ⊢ ((𝑊‘(𝑗 + 1)) ∈ Fin → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ₀)
149	147, 148	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ₀)
150	149	nn0red 12581	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℝ)
151	79, 150	readdcld 11253	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ∈ ℝ)
152	79, 97	readdcld 11253	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈ ℝ)
153	38	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝐾 + 1) ∈ ℤ)
154		simpr 490	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ (ℤ_≥‘𝐾))
155	34	nncnd 12264	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℂ)
156	155	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ ℂ)
157		pncan 11478	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 + 1) − 1) = 𝐾)
158	156, 113, 157	sylancl 598	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1) − 1) = 𝐾)
159	158	fveq2d 6889	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (ℤ_≥‘((𝐾 + 1) − 1)) = (ℤ_≥‘𝐾))
160	154, 159	eleqtrrd 2868	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ (ℤ_≥‘((𝐾 + 1) − 1)))
161		fzsuc2 13627	. . . . . . . . . . . . 13 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑗 ∈ (ℤ_≥‘((𝐾 + 1) − 1))) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
162	153, 160, 161	syl2anc 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
163	162	iuneq1d 4986	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘))
164		iunxun 5062	. . . . . . . . . . . 12 ⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘))
165		ovex 7452	. . . . . . . . . . . . . 14 ⊢ (𝑗 + 1) ∈ V
166	165, 138	iunxsn 5059	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘) = (𝑊‘(𝑗 + 1))
167	166	uneq2i 4119	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘)) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))
168	164, 167	eqtri 2788	. . . . . . . . . . 11 ⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))
169	163, 168	eqtrdi 2816	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1))))
170	169	fveq2d 6889	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) = (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))))
171		hashun2 14437	. . . . . . . . . 10 ⊢ ((∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ∈ Fin) → (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
172	76, 147, 171	syl2anc 596	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
173	170, 172	eqbrtrd 5135	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
174	81, 144	nndivred 12305	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 / (𝑗 + 1)) ∈ ℝ)
175		flle 13850	. . . . . . . . . . . . . 14 ⊢ ((𝑁 / (𝑗 + 1)) ∈ ℝ → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
176	174, 175	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
177		elfznn 13598	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
178	177	nncnd 12264	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
179	178	subid1d 11573	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...𝑁) → (𝑛 − 0) = 𝑛)
180	179	breq2d 5123	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑗 + 1) ∥ (𝑛 − 0) ↔ (𝑗 + 1) ∥ 𝑛))
181	180	rabbiia 3422	. . . . . . . . . . . . . . 15 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)} = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}
182	181	fveq2i 6888	. . . . . . . . . . . . . 14 ⊢ (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
183		1zzd 12640	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 1 ∈ ℤ)
184	30	nnnn0d 12580	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
185		nn0uz 12916	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ₀ = (ℤ_≥‘0)
186		1m1e0 12328	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
187	186	fveq2i 6888	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℤ_≥‘(1 − 1)) = (ℤ_≥‘0)
188	185, 187	eqtr4i 2791	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ = (ℤ_≥‘(1 − 1))
189	184, 188	eleqtrdi 2875	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(1 − 1)))
190	189	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ (ℤ_≥‘(1 − 1)))
191		0zd 12618	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 0 ∈ ℤ)
192	144, 183, 190, 191	hashdvds 16856	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))))
193	121	subid1d 11573	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 − 0) = 𝑁)
194	193	fvoveq1d 7441	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘((𝑁 − 0) / (𝑗 + 1))) = (⌊‘(𝑁 / (𝑗 + 1))))
195	186	oveq1i 7429	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 − 1) − 0) = (0 − 0)
196		0m0e0 12374	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 − 0) = 0
197	195, 196	eqtri 2788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − 1) − 0) = 0
198	197	oveq1i 7429	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 1) − 0) / (𝑗 + 1)) = (0 / (𝑗 + 1))
199	144	nncnd 12264	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ ℂ)
200	144	nnne0d 12301	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ≠ 0)
201	199, 200	div0d 12005	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (0 / (𝑗 + 1)) = 0)
202	198, 201	eqtrid 2812	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (((1 − 1) − 0) / (𝑗 + 1)) = 0)
203	202	fveq2d 6889	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = (⌊‘0))
204		0z 12617	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
205		flid 13859	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ∈ ℤ → (⌊‘0) = 0)
206	204, 205	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⌊‘0) = 0
207	203, 206	eqtrdi 2816	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = 0)
208	194, 207	oveq12d 7437	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))) = ((⌊‘(𝑁 / (𝑗 + 1))) − 0))
209	174	flcld 13849	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℤ)
210	209	zcnd 12717	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℂ)
211	210	subid1d 11573	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((⌊‘(𝑁 / (𝑗 + 1))) − 0) = (⌊‘(𝑁 / (𝑗 + 1))))
212	192, 208, 211	3eqtrd 2804	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (⌊‘(𝑁 / (𝑗 + 1))))
213	182, 212	eqtr3id 2814	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) = (⌊‘(𝑁 / (𝑗 + 1))))
214	121, 199, 200	divrecd 12009	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 / (𝑗 + 1)) = (𝑁 · (1 / (𝑗 + 1))))
215	214	eqcomd 2771	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · (1 / (𝑗 + 1))) = (𝑁 / (𝑗 + 1)))
216	176, 213, 215	3brtr4d 5145	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
217	216	adantr 486	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
218		eleq1 2853	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
219		breq1 5114	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∥ 𝑛 ↔ (𝑗 + 1) ∥ 𝑛))
220	218, 219	anbi12d 644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = (𝑗 + 1) → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)))
221	220	rabbidv 3425	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = (𝑗 + 1) → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
222	63	rabex 5311	. . . . . . . . . . . . . . . 16 ⊢ {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} ∈ V
223	221, 62, 222	fvmpt 6993	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 + 1) ∈ ℕ → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
224	144, 223	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
225	224	adantr 486	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
226		simpr 490	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑗 + 1) ∈ ℙ)
227	226	biantrurd 542	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → ((𝑗 + 1) ∥ 𝑛 ↔ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)))
228	227	rabbidv 3425	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
229	225, 228	eqtr4d 2803	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
230	229	fveq2d 6889	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}))
231		iftrue 4495	. . . . . . . . . . . . 13 ⊢ ((𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = (1 / (𝑗 + 1)))
232	231	adantl 487	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = (1 / (𝑗 + 1)))
233	232	oveq2d 7435	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · (1 / (𝑗 + 1))))
234	217, 230, 233	3brtr4d 5145	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
235	29	a1i 11	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ≤ 0)
236		simpl 488	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛) → (𝑗 + 1) ∈ ℙ)
237	236	con3i 155	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑗 + 1) ∈ ℙ → ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
238	237	ralrimivw 3163	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑗 + 1) ∈ ℙ → ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
239		rabeq0 4345	. . . . . . . . . . . . . . 15 ⊢ ({𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅ ↔ ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
240	238, 239	sylibr 237	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑗 + 1) ∈ ℙ → {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅)
241	224, 240	sylan9eq 2820	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = ∅)
242	241	fveq2d 6889	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘∅))
243	242, 46	eqtrdi 2816	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = 0)
244		iffalse 4498	. . . . . . . . . . . . 13 ⊢ (¬ (𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = 0)
245	244	oveq2d 7435	. . . . . . . . . . . 12 ⊢ (¬ (𝑗 + 1) ∈ ℙ → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · 0))
246	32	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · 0) = 0)
247	245, 246	sylan9eqr 2822	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = 0)
248	235, 243, 247	3brtr4d 5145	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
249	234, 248	pm2.61dan 825	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ≤ (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
250	150, 97, 79, 249	leadd2dd 11844	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
251	137, 151, 152, 173, 250	letrd 11382	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
252		fzfid 14027	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) ∈ Fin)
253	57, 88	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
254	101, 102, 253	syl2an 608	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
255	252, 254	fsumrecl 15808	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
256	81, 255	remulcld 11254	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
257		letr 11319	. . . . . . . 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 1398	. . . . . . 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 708	. . . . . 6 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
260	127, 259	sylbid 243	. . . . 5 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
261	260	expcom 419	. . . 4 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → (𝜑 → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
262	261	a2d 30	. . 3 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → ((𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) → (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))))
263	7, 14, 21, 28, 52, 262	uzind4i 12950	. 2 ⊢ (𝑁 ∈ (ℤ_≥‘𝐾) → (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
264	263	com12 33	1 ⊢ (𝜑 → (𝑁 ∈ (ℤ_≥‘𝐾) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ∀wral 3081 {crab 3418 ∖ cdif 3903 ∪ cun 3904 ⊆ wss 3906 ∅c0 4286 ifcif 4489 {csn 4591 ∪ ciun 4958 class class class wbr 5111 ↦ cmpt 5194 dom cdm 5663 ‘cfv 6540 (class class class)co 7419 Fincfn 8949 ℂcc 11113 ℝcr 11114 0cc0 11115 1c1 11116 + caddc 11118 · cmul 11120 < clt 11258 ≤ cle 11259 − cmin 11456 / cdiv 11886 ℕcn 12248 2c2 12310 ℕ₀cn0 12519 ℤcz 12606 ℤ_≥cuz 12878 ...cfz 13551 ⌊cfl 13841 seqcseq 14055 ♯chash 14384 ⇝ cli 15559 Σcsu 15761 ∥ cdvds 16332 ℙcprime 16751

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11171 ax-resscn 11172 ax-1cn 11173 ax-icn 11174 ax-addcl 11175 ax-addrcl 11176 ax-mulcl 11177 ax-mulrcl 11178 ax-mulcom 11179 ax-addass 11180 ax-mulass 11181 ax-distr 11182 ax-i2m1 11183 ax-1ne0 11184 ax-1rid 11185 ax-rnegex 11186 ax-rrecex 11187 ax-cnre 11188 ax-pre-lttri 11189 ax-pre-lttrn 11190 ax-pre-ltadd 11191 ax-pre-mulgt0 11192 ax-pre-sup 11193

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-om 7869 df-1st 7992 df-2nd 7993 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-oadd 8463 df-er 8700 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-sup 9409 df-inf 9410 df-oi 9479 df-dju 9903 df-card 9941 df-pnf 11260 df-mnf 11261 df-xr 11262 df-ltxr 11263 df-le 11264 df-sub 11458 df-neg 11459 df-div 11887 df-nn 12249 df-2 12318 df-3 12319 df-n0 12520 df-xnn0 12593 df-z 12607 df-uz 12879 df-rp 13033 df-fz 13552 df-fzo 13700 df-fl 13843 df-seq 14056 df-exp 14116 df-hash 14385 df-cj 15174 df-re 15175 df-im 15176 df-sqrt 15310 df-abs 15311 df-clim 15563 df-sum 15762 df-dvds 16333 df-prm 16752

This theorem is used by: prmreclem5 17002

W3C validator