prmreclem5 - Metamath Proof Explorer

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

Theorem prmreclem5 16719

Description: Lemma for prmrec 16721. Here we show the inequality 𝑁 / 2 < ♯𝑀 by decomposing the set (1...𝑁) into the disjoint union of the set 𝑀 of those numbers that are not divisible by any "large" primes (above 𝐾) and the indexed union over 𝐾 < 𝑘 of the numbers 𝑊‘𝑘 that divide the prime 𝑘. By prmreclem4 16718 the second of these has size less than 𝑁 times the prime reciprocal series, which is less than 1 / 2 by assumption, we find that the complementary part 𝑀 must be at least 𝑁 / 2 large. (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
prmreclem5	⊢ (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁)))

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

Proof of Theorem prmreclem5 Dummy variables 𝑟 𝑥 𝑞 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		prmrec.3	. . . 4 ⊢ (𝜑 → 𝑁 ∈ ℕ)
2	1	nnred 12090	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℝ)
3	2	rehalfcld 12322	. 2 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ)
4		fzfi 13794	. . . . . 6 ⊢ (1...𝑁) ∈ Fin
5		prmrec.4	. . . . . . 7 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
6	5	ssrab3 4028	. . . . . 6 ⊢ 𝑀 ⊆ (1...𝑁)
7		ssfi 9039	. . . . . 6 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
8	4, 6, 7	mp2an 689	. . . . 5 ⊢ 𝑀 ∈ Fin
9		hashcl 14172	. . . . 5 ⊢ (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ₀)
10	8, 9	ax-mp 5	. . . 4 ⊢ (♯‘𝑀) ∈ ℕ₀
11	10	nn0rei 12346	. . 3 ⊢ (♯‘𝑀) ∈ ℝ
12	11	a1i 11	. 2 ⊢ (𝜑 → (♯‘𝑀) ∈ ℝ)
13		2nn 12148	. . . . 5 ⊢ 2 ∈ ℕ
14		prmrec.2	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ)
15	14	nnnn0d 12395	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
16		nnexpcl 13897	. . . . 5 ⊢ ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ₀) → (2↑𝐾) ∈ ℕ)
17	13, 15, 16	sylancr 587	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ)
18	17	nnred 12090	. . 3 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ)
19	1	nnrpd 12872	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
20	19	rpsqrtcld 15223	. . . 4 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
21	20	rpred 12874	. . 3 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
22	18, 21	remulcld 11107	. 2 ⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
23	2	recnd 11105	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
24	23	2halvesd 12321	. . . . 5 ⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁)
25	6	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ⊆ (1...𝑁))
26	14	peano2nnd 12092	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ)
27		elfzuz 13354	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
28		eluznn 12760	. . . . . . . . . . . . 13 ⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
29	26, 27, 28	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
30		eleq1w 2819	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
31		breq1 5096	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛))
32	30, 31	anbi12d 631	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)))
33	32	rabbidv 3411	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
34		prmrec.7	. . . . . . . . . . . . . . 15 ⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)})
35		ovex 7371	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑁) ∈ V
36	35	rabex 5277	. . . . . . . . . . . . . . 15 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V
37	33, 34, 36	fvmpt 6932	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
38	37	adantl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
39		ssrab2 4025	. . . . . . . . . . . . 13 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁)
40	38, 39	eqsstrdi 3986	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁))
41	29, 40	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) ⊆ (1...𝑁))
42	41	ralrimiva 3139	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁))
43		iunss 4993	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁))
44	42, 43	sylibr 233	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁))
45	25, 44	unssd 4134	. . . . . . . 8 ⊢ (𝜑 → (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ⊆ (1...𝑁))
46		breq1 5096	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑝 ∥ 𝑛 ↔ 𝑞 ∥ 𝑛))
47	46	notbid 317	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑛))
48	47	cbvralvw 3221	. . . . . . . . . . . . . 14 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑛)
49		breq2 5097	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → (𝑞 ∥ 𝑛 ↔ 𝑞 ∥ 𝑥))
50	49	notbid 317	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → (¬ 𝑞 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑥))
51	50	ralbidv 3170	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑥 → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥))
52	48, 51	bitrid 282	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥))
53	52, 5	elrab2 3637	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥))
54		elun1 4124	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
55	53, 54	sylbir 234	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
56	55	ex 413	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...𝑁) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
57	56	adantl 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
58		dfrex2 3073	. . . . . . . . . 10 ⊢ (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 ↔ ¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)
59	14	nnzd 12527	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℤ)
60	59	peano2zd 12531	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾 + 1) ∈ ℤ)
61	60	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ∈ ℤ)
62	1	nnzd 12527	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
63	62	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℤ)
64		eldifi 4074	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 ∈ (ℙ ∖ (1...𝐾)) → 𝑞 ∈ ℙ)
65	64	ad2antrl 725	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℙ)
66		prmz 16478	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
67	65, 66	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℤ)
68		eldifn 4075	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ (ℙ ∖ (1...𝐾)) → ¬ 𝑞 ∈ (1...𝐾))
69	68	ad2antrl 725	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ∈ (1...𝐾))
70		prmnn 16477	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
71	65, 70	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℕ)
72		nnuz 12723	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ = (ℤ_≥‘1)
73	71, 72	eleqtrdi 2847	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ (ℤ_≥‘1))
74	59	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℤ)
75		elfz5 13350	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ (ℤ_≥‘1) ∧ 𝐾 ∈ ℤ) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾))
76	73, 74, 75	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾))
77	69, 76	mtbid 323	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ≤ 𝐾)
78	14	nnred 12090	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ ℝ)
79	78	ad2antrr 723	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℝ)
80	71	nnred 12090	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℝ)
81	79, 80	ltnled 11224	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ ¬ 𝑞 ≤ 𝐾))
82	77, 81	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 < 𝑞)
83		zltp1le 12472	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
84	74, 67, 83	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
85	82, 84	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ≤ 𝑞)
86		elfznn 13387	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
87	86	ad2antlr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℕ)
88	87	nnred 12090	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℝ)
89	2	ad2antrr 723	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℝ)
90		simprr 770	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∥ 𝑥)
91		dvdsle 16119	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥))
92	67, 87, 91	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥))
93	90, 92	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑥)
94		elfzle2 13362	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁)
95	94	ad2antlr 724	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ≤ 𝑁)
96	80, 88, 89, 93, 95	letrd 11234	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑁)
97	61, 63, 67, 85, 96	elfzd 13349	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ((𝐾 + 1)...𝑁))
98	49	anbi2d 629	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → ((𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥)))
99		simplr 766	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (1...𝑁))
100	65, 90	jca 512	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥))
101	98, 99, 100	elrabd 3636	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
102		eleq1w 2819	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ))
103	102, 46	anbi12d 631	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)))
104	103	rabbidv 3411	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
105	35	rabex 5277	. . . . . . . . . . . . . . . 16 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)} ∈ V
106	104, 34, 105	fvmpt 6932	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ ℕ → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
107	71, 106	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
108	101, 107	eleqtrrd 2840	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑊‘𝑞))
109		fveq2 6826	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑞 → (𝑊‘𝑘) = (𝑊‘𝑞))
110	109	eliuni 4948	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑥 ∈ (𝑊‘𝑞)) → 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
111	97, 108, 110	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
112		elun2 4125	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
113	111, 112	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
114	113	rexlimdvaa 3149	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
115	58, 114	syl5bir 242	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
116	57, 115	pm2.61d 179	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
117	45, 116	eqelssd 3953	. . . . . . 7 ⊢ (𝜑 → (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = (1...𝑁))
118	117	fveq2d 6830	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = (♯‘(1...𝑁)))
119	1	nnnn0d 12395	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
120		hashfz1 14162	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
121	119, 120	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
122	118, 121	eqtr2d 2777	. . . . 5 ⊢ (𝜑 → 𝑁 = (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
123	8	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ Fin)
124		ssfi 9039	. . . . . . 7 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin)
125	4, 44, 124	sylancr 587	. . . . . 6 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin)
126		breq1 5096	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑥 ↔ 𝑘 ∥ 𝑥))
127	126	notbid 317	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑘 → (¬ 𝑝 ∥ 𝑥 ↔ ¬ 𝑘 ∥ 𝑥))
128		breq2 5097	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑥 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑥))
129	128	notbid 317	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑥 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑥))
130	129	ralbidv 3170	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥))
131	130, 5	elrab2 3637	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥))
132	131	simprbi 497	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)
133	132	ad2antlr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)
134		simprr 770	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ℙ)
135		noel 4278	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 𝑘 ∈ ∅
136		simprl 768	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ((𝐾 + 1)...𝑁))
137	136	biantrud 532	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁))))
138		elin 3914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)))
139	137, 138	bitr4di 288	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁))))
140	78	ltp1d 12007	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
141		fzdisj 13385	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐾 < (𝐾 + 1) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
143	142	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
144	143	eleq2d 2822	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ 𝑘 ∈ ∅))
145	139, 144	bitrd 278	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ∅))
146	135, 145	mtbiri 326	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∈ (1...𝐾))
147	134, 146	eldifd 3909	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ (ℙ ∖ (1...𝐾)))
148	127, 133, 147	rspcdva 3571	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∥ 𝑥)
149	148	expr 457	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥))
150		imnan 400	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥) ↔ ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))
151	149, 150	sylib 217	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))
152	29	adantlr 712	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
153	152, 37	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
154	153	eleq2d 2822	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) ↔ 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}))
155		breq2 5097	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑥 → (𝑘 ∥ 𝑛 ↔ 𝑘 ∥ 𝑥))
156	155	anbi2d 629	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → ((𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)))
157	156	elrab 3634	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)))
158	157	simprbi 497	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))
159	154, 158	syl6bi 252	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)))
160	151, 159	mtod 197	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ 𝑥 ∈ (𝑊‘𝑘))
161	160	nrexdv 3142	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘))
162		eliun 4946	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ↔ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘))
163	161, 162	sylnibr 328	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
164	163	ex 413	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
165		imnan 400	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
166	164, 165	sylib 217	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
167		elin 3914	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
168	166, 167	sylnibr 328	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑥 ∈ (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
169	168	eq0rdv 4352	. . . . . 6 ⊢ (𝜑 → (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅)
170		hashun 14198	. . . . . 6 ⊢ ((𝑀 ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin ∧ (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅) → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
171	123, 125, 169, 170	syl3anc 1370	. . . . 5 ⊢ (𝜑 → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
172	24, 122, 171	3eqtrd 2780	. . . 4 ⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
173		hashcl 14172	. . . . . . 7 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℕ₀)
174	125, 173	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℕ₀)
175	174	nn0red 12396	. . . . 5 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℝ)
176		fzfid 13795	. . . . . . . 8 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
177	26, 28	sylan 580	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
178		nnrecre 12117	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
179		0re 11079	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
180		ifcl 4519	. . . . . . . . . . 11 ⊢ (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
181	178, 179, 180	sylancl 586	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
182	177, 181	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
183	27, 182	sylan2 593	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
184	176, 183	fsumrecl 15546	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
185	2, 184	remulcld 11107	. . . . . 6 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ)
186		prmrec.1	. . . . . . . 8 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
187		prmrec.5	. . . . . . . 8 ⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝ )
188		prmrec.6	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ (ℤ_≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
189	186, 14, 1, 5, 187, 188, 34	prmreclem4 16718	. . . . . . 7 ⊢ (𝜑 → (𝑁 ∈ (ℤ_≥‘𝐾) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
190		eluz 12698	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (ℤ_≥‘𝑁) ↔ 𝑁 ≤ 𝐾))
191	62, 59, 190	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ (ℤ_≥‘𝑁) ↔ 𝑁 ≤ 𝐾))
192		nnleltp1 12477	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1)))
193	1, 14, 192	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1)))
194		fzn 13374	. . . . . . . . . 10 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
195	60, 62, 194	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
196	191, 193, 195	3bitrd 304	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∈ (ℤ_≥‘𝑁) ↔ ((𝐾 + 1)...𝑁) = ∅))
197		0le0 12176	. . . . . . . . . 10 ⊢ 0 ≤ 0
198	23	mul01d 11276	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · 0) = 0)
199	197, 198	breqtrrid 5131	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝑁 · 0))
200		iuneq1 4958	. . . . . . . . . . . . 13 ⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘))
201		0iun 5011	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅
202	200, 201	eqtrdi 2792	. . . . . . . . . . . 12 ⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∅)
203	202	fveq2d 6830	. . . . . . . . . . 11 ⊢ (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = (♯‘∅))
204		hash0 14183	. . . . . . . . . . 11 ⊢ (♯‘∅) = 0
205	203, 204	eqtrdi 2792	. . . . . . . . . 10 ⊢ (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = 0)
206		sumeq1 15500	. . . . . . . . . . . 12 ⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
207		sum0 15533	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
208	206, 207	eqtrdi 2792	. . . . . . . . . . 11 ⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
209	208	oveq2d 7354	. . . . . . . . . 10 ⊢ (((𝐾 + 1)...𝑁) = ∅ → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
210	205, 209	breq12d 5106	. . . . . . . . 9 ⊢ (((𝐾 + 1)...𝑁) = ∅ → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ 0 ≤ (𝑁 · 0)))
211	199, 210	syl5ibrcom 246	. . . . . . . 8 ⊢ (𝜑 → (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
212	196, 211	sylbid 239	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∈ (ℤ_≥‘𝑁) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
213		uztric 12708	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ_≥‘𝐾) ∨ 𝐾 ∈ (ℤ_≥‘𝑁)))
214	59, 62, 213	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑁 ∈ (ℤ_≥‘𝐾) ∨ 𝐾 ∈ (ℤ_≥‘𝑁)))
215	189, 212, 214	mpjaod 857	. . . . . 6 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
216		eqid 2736	. . . . . . . . . 10 ⊢ (ℤ_≥‘(𝐾 + 1)) = (ℤ_≥‘(𝐾 + 1))
217		eleq1w 2819	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
218		oveq2 7346	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
219	217, 218	ifbieq1d 4498	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
220		ovex 7371	. . . . . . . . . . . . 13 ⊢ (1 / 𝑘) ∈ V
221		c0ex 11071	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
222	220, 221	ifex 4524	. . . . . . . . . . . 12 ⊢ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ V
223	219, 186, 222	fvmpt 6932	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
224	177, 223	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
225	181	recnd 11105	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
226	223, 225	eqeltrd 2837	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ)
227	226	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
228	72, 26, 227	iserex 15468	. . . . . . . . . . 11 ⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ ))
229	187, 228	mpbid 231	. . . . . . . . . 10 ⊢ (𝜑 → seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ )
230	216, 60, 224, 182, 229	isumrecl 15577	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ (ℤ_≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
231		halfre 12289	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℝ
232	231	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
233		fzssuz 13399	. . . . . . . . . . 11 ⊢ ((𝐾 + 1)...𝑁) ⊆ (ℤ_≥‘(𝐾 + 1))
234	233	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ⊆ (ℤ_≥‘(𝐾 + 1)))
235		nnrp 12843	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ⁺)
236	235	rpreccld 12884	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ⁺)
237	236	rpge0d 12878	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
238		breq2 5097	. . . . . . . . . . . . 13 ⊢ ((1 / 𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ (1 / 𝑘) ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
239		breq2 5097	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
240	238, 239	ifboth 4513	. . . . . . . . . . . 12 ⊢ ((0 ≤ (1 / 𝑘) ∧ 0 ≤ 0) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
241	237, 197, 240	sylancl 586	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
242	177, 241	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
243	216, 60, 176, 234, 224, 182, 242, 229	isumless 15657	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ≤ Σ𝑘 ∈ (ℤ_≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
244	184, 230, 232, 243, 188	lelttrd 11235	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
245	1	nngt0d 12124	. . . . . . . . 9 ⊢ (𝜑 → 0 < 𝑁)
246		ltmul2 11928	. . . . . . . . 9 ⊢ ((Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ ∧ (1 / 2) ∈ ℝ ∧ (𝑁 ∈ ℝ ∧ 0 < 𝑁)) → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
247	184, 232, 2, 245, 246	syl112anc 1373	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
248	244, 247	mpbid 231	. . . . . . 7 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))
249		2cn 12150	. . . . . . . . 9 ⊢ 2 ∈ ℂ
250		2ne0 12179	. . . . . . . . 9 ⊢ 2 ≠ 0
251		divrec 11751	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (𝑁 / 2) = (𝑁 · (1 / 2)))
252	249, 250, 251	mp3an23 1452	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → (𝑁 / 2) = (𝑁 · (1 / 2)))
253	23, 252	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2)))
254	248, 253	breqtrrd 5121	. . . . . 6 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 / 2))
255	175, 185, 3, 215, 254	lelttrd 11235	. . . . 5 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) < (𝑁 / 2))
256	175, 3, 12, 255	ltadd2dd 11236	. . . 4 ⊢ (𝜑 → ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) < ((♯‘𝑀) + (𝑁 / 2)))
257	172, 256	eqbrtrd 5115	. . 3 ⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2)))
258	3, 12, 3	ltadd1d 11670	. . 3 ⊢ (𝜑 → ((𝑁 / 2) < (♯‘𝑀) ↔ ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2))))
259	257, 258	mpbird 256	. 2 ⊢ (𝜑 → (𝑁 / 2) < (♯‘𝑀))
260		oveq1 7345	. . . . . . . 8 ⊢ (𝑘 = 𝑟 → (𝑘↑2) = (𝑟↑2))
261	260	breq1d 5103	. . . . . . 7 ⊢ (𝑘 = 𝑟 → ((𝑘↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑥))
262	261	cbvrabv 3413	. . . . . 6 ⊢ {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥}
263		breq2 5097	. . . . . . 7 ⊢ (𝑥 = 𝑛 → ((𝑟↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑛))
264	263	rabbidv 3411	. . . . . 6 ⊢ (𝑥 = 𝑛 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
265	262, 264	eqtrid 2788	. . . . 5 ⊢ (𝑥 = 𝑛 → {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
266	265	supeq1d 9304	. . . 4 ⊢ (𝑥 = 𝑛 → sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
267	266	cbvmptv 5206	. . 3 ⊢ (𝑥 ∈ ℕ ↦ sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < )) = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
268	186, 14, 1, 5, 267	prmreclem3 16717	. 2 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
269	3, 12, 22, 259, 268	ltletrd 11237	1 ⊢ (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 396 ∨ wo 844 = wceq 1540 ∈ wcel 2105 ≠ wne 2940 ∀wral 3061 ∃wrex 3070 {crab 3403 ∖ cdif 3895 ∪ cun 3896 ∩ cin 3897 ⊆ wss 3898 ∅c0 4270 ifcif 4474 ∪ ciun 4942 class class class wbr 5093 ↦ cmpt 5176 dom cdm 5621 ‘cfv 6480 (class class class)co 7338 Fincfn 8805 supcsup 9298 ℂcc 10971 ℝcr 10972 0cc0 10973 1c1 10974 + caddc 10976 · cmul 10978 < clt 11111 ≤ cle 11112 / cdiv 11734 ℕcn 12075 2c2 12130 ℕ₀cn0 12335 ℤcz 12421 ℤ_≥cuz 12684 ...cfz 13341 seqcseq 13823 ↑cexp 13884 ♯chash 14146 √csqrt 15044 ⇝ cli 15293 Σcsu 15497 ∥ cdvds 16063 ℙcprime 16474

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2707 ax-rep 5230 ax-sep 5244 ax-nul 5251 ax-pow 5309 ax-pr 5373 ax-un 7651 ax-inf2 9499 ax-cnex 11029 ax-resscn 11030 ax-1cn 11031 ax-icn 11032 ax-addcl 11033 ax-addrcl 11034 ax-mulcl 11035 ax-mulrcl 11036 ax-mulcom 11037 ax-addass 11038 ax-mulass 11039 ax-distr 11040 ax-i2m1 11041 ax-1ne0 11042 ax-1rid 11043 ax-rnegex 11044 ax-rrecex 11045 ax-cnre 11046 ax-pre-lttri 11047 ax-pre-lttrn 11048 ax-pre-ltadd 11049 ax-pre-mulgt0 11050 ax-pre-sup 11051

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3349 df-reu 3350 df-rab 3404 df-v 3443 df-sbc 3728 df-csb 3844 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3917 df-nul 4271 df-if 4475 df-pw 4550 df-sn 4575 df-pr 4577 df-op 4581 df-uni 4854 df-int 4896 df-iun 4944 df-br 5094 df-opab 5156 df-mpt 5177 df-tr 5211 df-id 5519 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5576 df-se 5577 df-we 5578 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6239 df-ord 6306 df-on 6307 df-lim 6308 df-suc 6309 df-iota 6432 df-fun 6482 df-fn 6483 df-f 6484 df-f1 6485 df-fo 6486 df-f1o 6487 df-fv 6488 df-isom 6489 df-riota 7294 df-ov 7341 df-oprab 7342 df-mpo 7343 df-om 7782 df-1st 7900 df-2nd 7901 df-frecs 8168 df-wrecs 8199 df-recs 8273 df-rdg 8312 df-1o 8368 df-2o 8369 df-oadd 8372 df-er 8570 df-map 8689 df-pm 8690 df-en 8806 df-dom 8807 df-sdom 8808 df-fin 8809 df-sup 9300 df-inf 9301 df-oi 9368 df-dju 9759 df-card 9797 df-pnf 11113 df-mnf 11114 df-xr 11115 df-ltxr 11116 df-le 11117 df-sub 11309 df-neg 11310 df-div 11735 df-nn 12076 df-2 12138 df-3 12139 df-n0 12336 df-xnn0 12408 df-z 12422 df-uz 12685 df-q 12791 df-rp 12833 df-fz 13342 df-fzo 13485 df-fl 13614 df-mod 13692 df-seq 13824 df-exp 13885 df-hash 14147 df-cj 14910 df-re 14911 df-im 14912 df-sqrt 15046 df-abs 15047 df-clim 15297 df-rlim 15298 df-sum 15498 df-dvds 16064 df-gcd 16302 df-prm 16475 df-pc 16636

This theorem is referenced by: prmreclem6 16720

W3C validator