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 16953

Description: Lemma for prmrec 16956. Show by induction that the indexed (nondisjoint) union 𝑊‘𝑘 is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 16809, 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 7439	. . . . . . 7 ⊢ (𝑥 = 𝐾 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝐾))
2	1	iuneq1d 5024	. . . . . 6 ⊢ (𝑥 = 𝐾 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘))
3	2	fveq2d 6911	. . . . 5 ⊢ (𝑥 = 𝐾 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)))
4	1	sumeq1d 15733	. . . . . 6 ⊢ (𝑥 = 𝐾 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
5	4	oveq2d 7447	. . . . 5 ⊢ (𝑥 = 𝐾 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
6	3, 5	breq12d 5161	. . . 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 7439	. . . . . . 7 ⊢ (𝑥 = 𝑗 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑗))
9	8	iuneq1d 5024	. . . . . 6 ⊢ (𝑥 = 𝑗 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘))
10	9	fveq2d 6911	. . . . 5 ⊢ (𝑥 = 𝑗 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)))
11	8	sumeq1d 15733	. . . . . 6 ⊢ (𝑥 = 𝑗 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
12	11	oveq2d 7447	. . . . 5 ⊢ (𝑥 = 𝑗 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
13	10, 12	breq12d 5161	. . . 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 7439	. . . . . . 7 ⊢ (𝑥 = (𝑗 + 1) → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...(𝑗 + 1)))
16	15	iuneq1d 5024	. . . . . 6 ⊢ (𝑥 = (𝑗 + 1) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘))
17	16	fveq2d 6911	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)))
18	15	sumeq1d 15733	. . . . . 6 ⊢ (𝑥 = (𝑗 + 1) → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
19	18	oveq2d 7447	. . . . 5 ⊢ (𝑥 = (𝑗 + 1) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
20	17, 19	breq12d 5161	. . . 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 7439	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝐾 + 1)...𝑥) = ((𝐾 + 1)...𝑁))
23	22	iuneq1d 5024	. . . . . 6 ⊢ (𝑥 = 𝑁 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘) = ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
24	23	fveq2d 6911	. . . . 5 ⊢ (𝑥 = 𝑁 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑥)(𝑊‘𝑘)) = (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
25	22	sumeq1d 15733	. . . . . 6 ⊢ (𝑥 = 𝑁 → Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
26	25	oveq2d 7447	. . . . 5 ⊢ (𝑥 = 𝑁 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑥)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
27	24, 26	breq12d 5161	. . . 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 12365	. . . . 5 ⊢ 0 ≤ 0
30		prmrec.3	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ)
31	30	nncnd 12280	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
32	31	mul01d 11458	. . . . 5 ⊢ (𝜑 → (𝑁 · 0) = 0)
33	29, 32	breqtrrid 5186	. . . 4 ⊢ (𝜑 → 0 ≤ (𝑁 · 0))
34		prmrec.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℕ)
35	34	nnred 12279	. . . . . . . . . 10 ⊢ (𝜑 → 𝐾 ∈ ℝ)
36	35	ltp1d 12196	. . . . . . . . 9 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
37	34	nnzd 12638	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐾 ∈ ℤ)
38	37	peano2zd 12723	. . . . . . . . . 10 ⊢ (𝜑 → (𝐾 + 1) ∈ ℤ)
39		fzn 13577	. . . . . . . . . 10 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
40	38, 37, 39	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝐾) = ∅))
41	36, 40	mpbid 232	. . . . . . . 8 ⊢ (𝜑 → ((𝐾 + 1)...𝐾) = ∅)
42	41	iuneq1d 5024	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘))
43		0iun 5068	. . . . . . 7 ⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅
44	42, 43	eqtrdi 2791	. . . . . 6 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘) = ∅)
45	44	fveq2d 6911	. . . . 5 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = (♯‘∅))
46		hash0 14403	. . . . 5 ⊢ (♯‘∅) = 0
47	45, 46	eqtrdi 2791	. . . 4 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) = 0)
48	41	sumeq1d 15733	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
49		sum0 15754	. . . . . 6 ⊢ Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
50	48, 49	eqtrdi 2791	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
51	50	oveq2d 7447	. . . 4 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
52	33, 47, 51	3brtr4d 5180	. . 3 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝐾)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝐾)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
53		fzfi 14010	. . . . . . . . . . 11 ⊢ (1...𝑁) ∈ Fin
54		elfzuz 13557	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑗) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
55	34	peano2nnd 12281	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ)
56		eluznn 12958	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
57	55, 56	sylan 580	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
58		eleq1 2827	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
59		breq1 5151	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛))
60	58, 59	anbi12d 632	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)))
61	60	rabbidv 3441	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
62		prmrec.7	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)})
63		ovex 7464	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1...𝑁) ∈ V
64	63	rabex 5345	. . . . . . . . . . . . . . . . . . 19 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V
65	61, 62, 64	fvmpt 7016	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
66	65	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
67		ssrab2 4090	. . . . . . . . . . . . . . . . 17 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁)
68	66, 67	eqsstrdi 4050	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁))
69	57, 68	syldan 591	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁))
70	54, 69	sylan2 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → (𝑊‘𝑘) ⊆ (1...𝑁))
71	70	ralrimiva 3144	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
72	71	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
73		iunss 5050	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
74	72, 73	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁))
75		ssfi 9212	. . . . . . . . . . 11 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin)
76	53, 74, 75	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin)
77		hashcl 14392	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℕ₀)
78	76, 77	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℕ₀)
79	78	nn0red 12586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ∈ ℝ)
80	30	nnred 12279	. . . . . . . . . 10 ⊢ (𝜑 → 𝑁 ∈ ℝ)
81	80	adantr 480	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ ℝ)
82		fzfid 14011	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...𝑗) ∈ Fin)
83	55	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝐾 + 1) ∈ ℕ)
84	83, 54, 56	syl2an 596	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → 𝑘 ∈ ℕ)
85		nnrecre 12306	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
86		0re 11261	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
87		ifcl 4576	. . . . . . . . . . . 12 ⊢ (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
88	85, 86, 87	sylancl 586	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
89	84, 88	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑗)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
90	82, 89	fsumrecl 15767	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
91	81, 90	remulcld 11289	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
92		prmnn 16708	. . . . . . . . . . . 12 ⊢ ((𝑗 + 1) ∈ ℙ → (𝑗 + 1) ∈ ℕ)
93	92	nnrecred 12315	. . . . . . . . . . 11 ⊢ ((𝑗 + 1) ∈ ℙ → (1 / (𝑗 + 1)) ∈ ℝ)
94	93	adantl 481	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (1 / (𝑗 + 1)) ∈ ℝ)
95		0red 11262	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → 0 ∈ ℝ)
96	94, 95	ifclda 4566	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℝ)
97	81, 96	remulcld 11289	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) ∈ ℝ)
98	79, 91, 97	leadd1d 11855	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ≤ ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))))
99		eluzp1p1 12904	. . . . . . . . . . . . 13 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → (𝑗 + 1) ∈ (ℤ_≥‘(𝐾 + 1)))
100	99	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ (ℤ_≥‘(𝐾 + 1)))
101		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝜑)
102		elfzuz 13557	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1)) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
103	88	recnd 11287	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
104	57, 103	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
105	101, 102, 104	syl2an 596	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
106		eleq1 2827	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (𝑘 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
107		oveq2 7439	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → (1 / 𝑘) = (1 / (𝑗 + 1)))
108	106, 107	ifbieq1d 4555	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 + 1) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))
109	100, 105, 108	fsumm1 15784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
110		eluzelz 12886	. . . . . . . . . . . . . . . . 17 ⊢ (𝑗 ∈ (ℤ_≥‘𝐾) → 𝑗 ∈ ℤ)
111	110	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℤ)
112	111	zcnd 12721	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℂ)
113		ax-1cn 11211	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
114		pncan 11512	. . . . . . . . . . . . . . 15 ⊢ ((𝑗 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑗 + 1) − 1) = 𝑗)
115	112, 113, 114	sylancl 586	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝑗 + 1) − 1) = 𝑗)
116	115	oveq2d 7447	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...((𝑗 + 1) − 1)) = ((𝐾 + 1)...𝑗))
117	116	sumeq1d 15733	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...((𝑗 + 1) − 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
118	117	oveq1d 7446	. . . . . . . . . . 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 2775	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)))
120	119	oveq2d 7447	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
121	31	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ ℂ)
122	90	recnd 11287	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
123	96	recnd 11287	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) ∈ ℂ)
124	121, 122, 123	adddid 11283	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · (Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) + if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
125	120, 124	eqtrd 2775	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = ((𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑗)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
126	125	breq2d 5160	. . . . . . 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 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → (𝑊‘𝑘) ⊆ (1...𝑁))
129	128	ralrimiva 3144	. . . . . . . . . . . . 13 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
130	129	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
131		iunss 5050	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
132	130, 131	sylibr 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁))
133		ssfi 9212	. . . . . . . . . . 11 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin)
134	53, 132, 133	sylancr 587	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin)
135		hashcl 14392	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℕ₀)
136	134, 135	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℕ₀)
137	136	nn0red 12586	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ∈ ℝ)
138		fveq2 6907	. . . . . . . . . . . . . 14 ⊢ (𝑘 = (𝑗 + 1) → (𝑊‘𝑘) = (𝑊‘(𝑗 + 1)))
139	138	sseq1d 4027	. . . . . . . . . . . . 13 ⊢ (𝑘 = (𝑗 + 1) → ((𝑊‘𝑘) ⊆ (1...𝑁) ↔ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)))
140	68	ralrimiva 3144	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁))
141	140	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∀𝑘 ∈ ℕ (𝑊‘𝑘) ⊆ (1...𝑁))
142		eluznn 12958	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ ℕ ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℕ)
143	34, 142	sylan 580	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ ℕ)
144	143	peano2nnd 12281	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ ℕ)
145	139, 141, 144	rspcdva 3623	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁))
146		ssfi 9212	. . . . . . . . . . . 12 ⊢ (((1...𝑁) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ⊆ (1...𝑁)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
147	53, 145, 146	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑊‘(𝑗 + 1)) ∈ Fin)
148		hashcl 14392	. . . . . . . . . . 11 ⊢ ((𝑊‘(𝑗 + 1)) ∈ Fin → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ₀)
149	147, 148	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℕ₀)
150	149	nn0red 12586	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(𝑊‘(𝑗 + 1))) ∈ ℝ)
151	79, 150	readdcld 11288	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ∈ ℝ)
152	79, 97	readdcld 11288	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))) ∈ ℝ)
153	38	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝐾 + 1) ∈ ℤ)
154		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ (ℤ_≥‘𝐾))
155	34	nncnd 12280	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ ℂ)
156	155	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝐾 ∈ ℂ)
157		pncan 11512	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 + 1) − 1) = 𝐾)
158	156, 113, 157	sylancl 586	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1) − 1) = 𝐾)
159	158	fveq2d 6911	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (ℤ_≥‘((𝐾 + 1) − 1)) = (ℤ_≥‘𝐾))
160	154, 159	eleqtrrd 2842	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑗 ∈ (ℤ_≥‘((𝐾 + 1) − 1)))
161		fzsuc2 13619	. . . . . . . . . . . . 13 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑗 ∈ (ℤ_≥‘((𝐾 + 1) − 1))) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
162	153, 160, 161	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) = (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)}))
163	162	iuneq1d 5024	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘))
164		iunxun 5099	. . . . . . . . . . . 12 ⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘))
165		ovex 7464	. . . . . . . . . . . . . 14 ⊢ (𝑗 + 1) ∈ V
166	165, 138	iunxsn 5096	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘) = (𝑊‘(𝑗 + 1))
167	166	uneq2i 4175	. . . . . . . . . . . 12 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ ∪ 𝑘 ∈ {(𝑗 + 1)} (𝑊‘𝑘)) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))
168	164, 167	eqtri 2763	. . . . . . . . . . 11 ⊢ ∪ 𝑘 ∈ (((𝐾 + 1)...𝑗) ∪ {(𝑗 + 1)})(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))
169	163, 168	eqtrdi 2791	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘) = (∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1))))
170	169	fveq2d 6911	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) = (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))))
171		hashun2 14419	. . . . . . . . . 10 ⊢ ((∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∈ Fin ∧ (𝑊‘(𝑗 + 1)) ∈ Fin) → (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
172	76, 147, 171	syl2anc 584	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘(∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘) ∪ (𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
173	170, 172	eqbrtrd 5170	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))))
174	81, 144	nndivred 12318	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 / (𝑗 + 1)) ∈ ℝ)
175		flle 13836	. . . . . . . . . . . . . 14 ⊢ ((𝑁 / (𝑗 + 1)) ∈ ℝ → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
176	174, 175	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ≤ (𝑁 / (𝑗 + 1)))
177		elfznn 13590	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℕ)
178	177	nncnd 12280	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑛 ∈ (1...𝑁) → 𝑛 ∈ ℂ)
179	178	subid1d 11607	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 ∈ (1...𝑁) → (𝑛 − 0) = 𝑛)
180	179	breq2d 5160	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 ∈ (1...𝑁) → ((𝑗 + 1) ∥ (𝑛 − 0) ↔ (𝑗 + 1) ∥ 𝑛))
181	180	rabbiia 3437	. . . . . . . . . . . . . . 15 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)} = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}
182	181	fveq2i 6910	. . . . . . . . . . . . . 14 ⊢ (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
183		1zzd 12646	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 1 ∈ ℤ)
184	30	nnnn0d 12585	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
185		nn0uz 12918	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ₀ = (ℤ_≥‘0)
186		1m1e0 12336	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1 − 1) = 0
187	186	fveq2i 6910	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℤ_≥‘(1 − 1)) = (ℤ_≥‘0)
188	185, 187	eqtr4i 2766	. . . . . . . . . . . . . . . . . 18 ⊢ ℕ₀ = (ℤ_≥‘(1 − 1))
189	184, 188	eleqtrdi 2849	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑁 ∈ (ℤ_≥‘(1 − 1)))
190	189	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 𝑁 ∈ (ℤ_≥‘(1 − 1)))
191		0zd 12623	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → 0 ∈ ℤ)
192	144, 183, 190, 191	hashdvds 16809	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))))
193	121	subid1d 11607	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 − 0) = 𝑁)
194	193	fvoveq1d 7453	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘((𝑁 − 0) / (𝑗 + 1))) = (⌊‘(𝑁 / (𝑗 + 1))))
195	186	oveq1i 7441	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((1 − 1) − 0) = (0 − 0)
196		0m0e0 12384	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (0 − 0) = 0
197	195, 196	eqtri 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((1 − 1) − 0) = 0
198	197	oveq1i 7441	. . . . . . . . . . . . . . . . . . 19 ⊢ (((1 − 1) − 0) / (𝑗 + 1)) = (0 / (𝑗 + 1))
199	144	nncnd 12280	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ∈ ℂ)
200	144	nnne0d 12314	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑗 + 1) ≠ 0)
201	199, 200	div0d 12040	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (0 / (𝑗 + 1)) = 0)
202	198, 201	eqtrid 2787	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (((1 − 1) − 0) / (𝑗 + 1)) = 0)
203	202	fveq2d 6911	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = (⌊‘0))
204		0z 12622	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ ℤ
205		flid 13845	. . . . . . . . . . . . . . . . . 18 ⊢ (0 ∈ ℤ → (⌊‘0) = 0)
206	204, 205	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ (⌊‘0) = 0
207	203, 206	eqtrdi 2791	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(((1 − 1) − 0) / (𝑗 + 1))) = 0)
208	194, 207	oveq12d 7449	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((⌊‘((𝑁 − 0) / (𝑗 + 1))) − (⌊‘(((1 − 1) − 0) / (𝑗 + 1)))) = ((⌊‘(𝑁 / (𝑗 + 1))) − 0))
209	174	flcld 13835	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℤ)
210	209	zcnd 12721	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (⌊‘(𝑁 / (𝑗 + 1))) ∈ ℂ)
211	210	subid1d 11607	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((⌊‘(𝑁 / (𝑗 + 1))) − 0) = (⌊‘(𝑁 / (𝑗 + 1))))
212	192, 208, 211	3eqtrd 2779	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ (𝑛 − 0)}) = (⌊‘(𝑁 / (𝑗 + 1))))
213	182, 212	eqtr3id 2789	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) = (⌊‘(𝑁 / (𝑗 + 1))))
214	121, 199, 200	divrecd 12044	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 / (𝑗 + 1)) = (𝑁 · (1 / (𝑗 + 1))))
215	214	eqcomd 2741	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · (1 / (𝑗 + 1))) = (𝑁 / (𝑗 + 1)))
216	176, 213, 215	3brtr4d 5180	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
217	216	adantr 480	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}) ≤ (𝑁 · (1 / (𝑗 + 1))))
218		eleq1 2827	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = (𝑗 + 1) → (𝑝 ∈ ℙ ↔ (𝑗 + 1) ∈ ℙ))
219		breq1 5151	. . . . . . . . . . . . . . . . . 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 5345	. . . . . . . . . . . . . . . 16 ⊢ {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} ∈ V
223	221, 62, 222	fvmpt 7016	. . . . . . . . . . . . . . 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 3441	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛} = {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)})
229	225, 228	eqtr4d 2778	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = {𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛})
230	229	fveq2d 6911	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘{𝑛 ∈ (1...𝑁) ∣ (𝑗 + 1) ∥ 𝑛}))
231		iftrue 4537	. . . . . . . . . . . . 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 7447	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · (1 / (𝑗 + 1))))
234	217, 230, 233	3brtr4d 5180	. . . . . . . . . 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 3148	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑗 + 1) ∈ ℙ → ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
239		rabeq0 4394	. . . . . . . . . . . . . . 15 ⊢ ({𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅ ↔ ∀𝑛 ∈ (1...𝑁) ¬ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛))
240	238, 239	sylibr 234	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑗 + 1) ∈ ℙ → {𝑛 ∈ (1...𝑁) ∣ ((𝑗 + 1) ∈ ℙ ∧ (𝑗 + 1) ∥ 𝑛)} = ∅)
241	224, 240	sylan9eq 2795	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑊‘(𝑗 + 1)) = ∅)
242	241	fveq2d 6911	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = (♯‘∅))
243	242, 46	eqtrdi 2791	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (♯‘(𝑊‘(𝑗 + 1))) = 0)
244		iffalse 4540	. . . . . . . . . . . . 13 ⊢ (¬ (𝑗 + 1) ∈ ℙ → if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0) = 0)
245	244	oveq2d 7447	. . . . . . . . . . . 12 ⊢ (¬ (𝑗 + 1) ∈ ℙ → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = (𝑁 · 0))
246	32	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · 0) = 0)
247	245, 246	sylan9eqr 2797	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ ¬ (𝑗 + 1) ∈ ℙ) → (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0)) = 0)
248	235, 243, 247	3brtr4d 5180	. . . . . . . . . 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 11876	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (♯‘(𝑊‘(𝑗 + 1)))) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
251	137, 151, 152, 173, 250	letrd 11416	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))(𝑊‘𝑘)) ≤ ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑗)(𝑊‘𝑘)) + (𝑁 · if((𝑗 + 1) ∈ ℙ, (1 / (𝑗 + 1)), 0))))
252		fzfid 14011	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → ((𝐾 + 1)...(𝑗 + 1)) ∈ Fin)
253	57, 88	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
254	101, 102, 253	syl2an 596	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) ∧ 𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
255	252, 254	fsumrecl 15767	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
256	81, 255	remulcld 11289	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ (ℤ_≥‘𝐾)) → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...(𝑗 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
257		letr 11353	. . . . . . . 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 1370	. . . . . . 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 695	. . . . . 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 12950	. 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 1537 ∈ wcel 2106 ∀wral 3059 {crab 3433 ∖ cdif 3960 ∪ cun 3961 ⊆ wss 3963 ∅c0 4339 ifcif 4531 {csn 4631 ∪ ciun 4996 class class class wbr 5148 ↦ cmpt 5231 dom cdm 5689 ‘cfv 6563 (class class class)co 7431 Fincfn 8984 ℂcc 11151 ℝcr 11152 0cc0 11153 1c1 11154 + caddc 11156 · cmul 11158 < clt 11293 ≤ cle 11294 − cmin 11490 / cdiv 11918 ℕcn 12264 2c2 12319 ℕ₀cn0 12524 ℤcz 12611 ℤ_≥cuz 12876 ...cfz 13544 ⌊cfl 13827 seqcseq 14039 ♯chash 14366 ⇝ cli 15517 Σcsu 15719 ∥ cdvds 16287 ℙcprime 16705

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-10 2139 ax-11 2155 ax-12 2175 ax-ext 2706 ax-rep 5285 ax-sep 5302 ax-nul 5312 ax-pow 5371 ax-pr 5438 ax-un 7754 ax-inf2 9679 ax-cnex 11209 ax-resscn 11210 ax-1cn 11211 ax-icn 11212 ax-addcl 11213 ax-addrcl 11214 ax-mulcl 11215 ax-mulrcl 11216 ax-mulcom 11217 ax-addass 11218 ax-mulass 11219 ax-distr 11220 ax-i2m1 11221 ax-1ne0 11222 ax-1rid 11223 ax-rnegex 11224 ax-rrecex 11225 ax-cnre 11226 ax-pre-lttri 11227 ax-pre-lttrn 11228 ax-pre-ltadd 11229 ax-pre-mulgt0 11230 ax-pre-sup 11231

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-nf 1781 df-sb 2063 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2727 df-clel 2814 df-nfc 2890 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3378 df-reu 3379 df-rab 3434 df-v 3480 df-sbc 3792 df-csb 3909 df-dif 3966 df-un 3968 df-in 3970 df-ss 3980 df-pss 3983 df-nul 4340 df-if 4532 df-pw 4607 df-sn 4632 df-pr 4634 df-op 4638 df-uni 4913 df-int 4952 df-iun 4998 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5583 df-eprel 5589 df-po 5597 df-so 5598 df-fr 5641 df-se 5642 df-we 5643 df-xp 5695 df-rel 5696 df-cnv 5697 df-co 5698 df-dm 5699 df-rn 5700 df-res 5701 df-ima 5702 df-pred 6323 df-ord 6389 df-on 6390 df-lim 6391 df-suc 6392 df-iota 6516 df-fun 6565 df-fn 6566 df-f 6567 df-f1 6568 df-fo 6569 df-f1o 6570 df-fv 6571 df-isom 6572 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8013 df-2nd 8014 df-frecs 8305 df-wrecs 8336 df-recs 8410 df-rdg 8449 df-1o 8505 df-oadd 8509 df-er 8744 df-en 8985 df-dom 8986 df-sdom 8987 df-fin 8988 df-sup 9480 df-inf 9481 df-oi 9548 df-dju 9939 df-card 9977 df-pnf 11295 df-mnf 11296 df-xr 11297 df-ltxr 11298 df-le 11299 df-sub 11492 df-neg 11493 df-div 11919 df-nn 12265 df-2 12327 df-3 12328 df-n0 12525 df-xnn0 12598 df-z 12612 df-uz 12877 df-rp 13033 df-fz 13545 df-fzo 13692 df-fl 13829 df-seq 14040 df-exp 14100 df-hash 14367 df-cj 15135 df-re 15136 df-im 15137 df-sqrt 15271 df-abs 15272 df-clim 15521 df-sum 15720 df-dvds 16288 df-prm 16706

This theorem is referenced by: prmreclem5 16954

W3C validator