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 16975

Description: Lemma for prmrec 16977. 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 16974 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 12243	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℝ)
3	2	rehalfcld 12486	. 2 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ)
4		fzfi 14004	. . . . . 6 ⊢ (1...𝑁) ∈ Fin
5		prmrec.4	. . . . . . 7 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
6	5	ssrab3 4036	. . . . . 6 ⊢ 𝑀 ⊆ (1...𝑁)
7		ssfi 9153	. . . . . 6 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
8	4, 6, 7	mp2an 704	. . . . 5 ⊢ 𝑀 ∈ Fin
9		hashcl 14388	. . . . 5 ⊢ (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ₀)
10	8, 9	ax-mp 5	. . . 4 ⊢ (♯‘𝑀) ∈ ℕ₀
11	10	nn0rei 12510	. . 3 ⊢ (♯‘𝑀) ∈ ℝ
12	11	a1i 11	. 2 ⊢ (𝜑 → (♯‘𝑀) ∈ ℝ)
13		2nn 12309	. . . . 5 ⊢ 2 ∈ ℕ
14		prmrec.2	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ)
15	14	nnnn0d 12560	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
16		nnexpcl 14106	. . . . 5 ⊢ ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ₀) → (2↑𝐾) ∈ ℕ)
17	13, 15, 16	sylancr 598	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ)
18	17	nnred 12243	. . 3 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ)
19	1	nnrpd 13053	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
20	19	rpsqrtcld 15459	. . . 4 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
21	20	rpred 13055	. . 3 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
22	18, 21	remulcld 11234	. 2 ⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
23	2	recnd 11232	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
24	23	2halvesd 12485	. . . . 5 ⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁)
25	6	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ⊆ (1...𝑁))
26	14	peano2nnd 12245	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ)
27		elfzuz 13543	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
28		eluznn 12937	. . . . . . . . . . . . 13 ⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
29	26, 27, 28	syl2an 607	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
30		eleq1w 2846	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
31		breq1 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛))
32	30, 31	anbi12d 643	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)))
33	32	rabbidv 3423	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
34		prmrec.7	. . . . . . . . . . . . . . 15 ⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)})
35		ovex 7443	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑁) ∈ V
36	35	rabex 5309	. . . . . . . . . . . . . . 15 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V
37	33, 34, 36	fvmpt 6989	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
38	37	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
39		ssrab2 4034	. . . . . . . . . . . . 13 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁)
40	38, 39	eqsstrdi 3981	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁))
41	29, 40	syldan 602	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) ⊆ (1...𝑁))
42	41	ralrimiva 3157	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁))
43		iunss 5009	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁))
44	42, 43	sylibr 237	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁))
45	25, 44	unssd 4145	. . . . . . . 8 ⊢ (𝜑 → (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ⊆ (1...𝑁))
46		breq1 5112	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑝 ∥ 𝑛 ↔ 𝑞 ∥ 𝑛))
47	46	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑛))
48	47	cbvralvw 3243	. . . . . . . . . . . . . 14 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑛)
49		breq2 5113	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → (𝑞 ∥ 𝑛 ↔ 𝑞 ∥ 𝑥))
50	49	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → (¬ 𝑞 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑥))
51	50	ralbidv 3188	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑥 → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥))
52	48, 51	bitrid 286	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥))
53	52, 5	elrab2 3654	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥))
54		elun1 4135	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
55	53, 54	sylbir 238	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
56	55	ex 417	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...𝑁) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
57	56	adantl 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
58		dfrex2 3092	. . . . . . . . . 10 ⊢ (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 ↔ ¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)
59	14	nnzd 12612	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℤ)
60	59	peano2zd 12698	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾 + 1) ∈ ℤ)
61	60	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ∈ ℤ)
62	1	nnzd 12612	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
63	62	ad2antrr 738	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℤ)
64		eldifi 4085	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 ∈ (ℙ ∖ (1...𝐾)) → 𝑞 ∈ ℙ)
65	64	ad2antrl 740	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℙ)
66		prmz 16728	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
67	65, 66	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℤ)
68		eldifn 4086	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ (ℙ ∖ (1...𝐾)) → ¬ 𝑞 ∈ (1...𝐾))
69	68	ad2antrl 740	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ∈ (1...𝐾))
70		prmnn 16727	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
71	65, 70	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℕ)
72		nnuz 12896	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ = (ℤ_≥‘1)
73	71, 72	eleqtrdi 2873	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ (ℤ_≥‘1))
74	59	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℤ)
75		elfz5 13539	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ (ℤ_≥‘1) ∧ 𝐾 ∈ ℤ) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾))
76	73, 74, 75	syl2anc 595	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾))
77	69, 76	mtbid 327	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ≤ 𝐾)
78	14	nnred 12243	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ ℝ)
79	78	ad2antrr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℝ)
80	71	nnred 12243	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℝ)
81	79, 80	ltnled 11352	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ ¬ 𝑞 ≤ 𝐾))
82	77, 81	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 < 𝑞)
83		zltp1le 12639	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
84	74, 67, 83	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
85	82, 84	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ≤ 𝑞)
86		elfznn 13577	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
87	86	ad2antlr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℕ)
88	87	nnred 12243	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℝ)
89	2	ad2antrr 738	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℝ)
90		simprr 784	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∥ 𝑥)
91		dvdsle 16363	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥))
92	67, 87, 91	syl2anc 595	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥))
93	90, 92	mpd 16	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑥)
94		elfzle2 13551	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁)
95	94	ad2antlr 739	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ≤ 𝑁)
96	80, 88, 89, 93, 95	letrd 11362	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑁)
97	61, 63, 67, 85, 96	elfzd 13538	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ((𝐾 + 1)...𝑁))
98	49	anbi2d 641	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → ((𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥)))
99		simplr 780	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (1...𝑁))
100	65, 90	jca 520	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥))
101	98, 99, 100	elrabd 3652	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
102		eleq1w 2846	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ))
103	102, 46	anbi12d 643	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)))
104	103	rabbidv 3423	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
105	35	rabex 5309	. . . . . . . . . . . . . . . 16 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)} ∈ V
106	104, 34, 105	fvmpt 6989	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ ℕ → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
107	71, 106	syl 18	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
108	101, 107	eleqtrrd 2866	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑊‘𝑞))
109		fveq2 6881	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑞 → (𝑊‘𝑘) = (𝑊‘𝑞))
110	109	eliuni 4962	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑥 ∈ (𝑊‘𝑞)) → 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
111	97, 108, 110	syl2anc 595	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
112		elun2 4136	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
113	111, 112	syl 18	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
114	113	rexlimdvaa 3167	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
115	58, 114	biimtrrid 246	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
116	57, 115	pm2.61d 181	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
117	45, 116	eqelssd 3958	. . . . . . 7 ⊢ (𝜑 → (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = (1...𝑁))
118	117	fveq2d 6885	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = (♯‘(1...𝑁)))
119	1	nnnn0d 12560	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
120		hashfz1 14378	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
121	119, 120	syl 18	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
122	118, 121	eqtr2d 2799	. . . . 5 ⊢ (𝜑 → 𝑁 = (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
123	8	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ Fin)
124		ssfi 9153	. . . . . . 7 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin)
125	4, 44, 124	sylancr 598	. . . . . 6 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin)
126		breq1 5112	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑥 ↔ 𝑘 ∥ 𝑥))
127	126	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑘 → (¬ 𝑝 ∥ 𝑥 ↔ ¬ 𝑘 ∥ 𝑥))
128		breq2 5113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑥 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑥))
129	128	notbid 321	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑥 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑥))
130	129	ralbidv 3188	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥))
131	130, 5	elrab2 3654	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥))
132	131	simprbi 502	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)
133	132	ad2antlr 739	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)
134		simprr 784	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ℙ)
135		noel 4291	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 𝑘 ∈ ∅
136		simprl 782	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ((𝐾 + 1)...𝑁))
137	136	biantrud 540	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁))))
138		elin 3921	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)))
139	137, 138	bitr4di 292	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁))))
140	78	ltp1d 12140	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
141		fzdisj 13575	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐾 < (𝐾 + 1) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
142	140, 141	syl 18	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
143	142	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
144	143	eleq2d 2849	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ 𝑘 ∈ ∅))
145	139, 144	bitrd 282	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ∅))
146	135, 145	mtbiri 330	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∈ (1...𝐾))
147	134, 146	eldifd 3916	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ (ℙ ∖ (1...𝐾)))
148	127, 133, 147	rspcdva 3582	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∥ 𝑥)
149	148	expr 461	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥))
150		imnan 404	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥) ↔ ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))
151	149, 150	sylib 221	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))
152	29	adantlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
153	152, 37	syl 18	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
154	153	eleq2d 2849	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) ↔ 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}))
155		breq2 5113	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑥 → (𝑘 ∥ 𝑛 ↔ 𝑘 ∥ 𝑥))
156	155	anbi2d 641	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → ((𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)))
157	156	elrab 3650	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)))
158	157	simprbi 502	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))
159	154, 158	biimtrdi 256	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)))
160	151, 159	mtod 201	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ 𝑥 ∈ (𝑊‘𝑘))
161	160	nrexdv 3160	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘))
162		eliun 4960	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ↔ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘))
163	161, 162	sylnibr 332	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
164	163	ex 417	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
165		imnan 404	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
166	164, 165	sylib 221	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
167		elin 3921	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
168	166, 167	sylnibr 332	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑥 ∈ (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
169	168	eq0rdv 4372	. . . . . 6 ⊢ (𝜑 → (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅)
170		hashun 14414	. . . . . 6 ⊢ ((𝑀 ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin ∧ (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅) → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
171	123, 125, 169, 170	syl3anc 1398	. . . . 5 ⊢ (𝜑 → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
172	24, 122, 171	3eqtrd 2802	. . . 4 ⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
173		hashcl 14388	. . . . . . 7 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℕ₀)
174	125, 173	syl 18	. . . . . 6 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℕ₀)
175	174	nn0red 12561	. . . . 5 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℝ)
176		fzfid 14005	. . . . . . . 8 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
177	26, 28	sylan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
178		nnrecre 12273	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
179		0re 11205	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
180		ifcl 4533	. . . . . . . . . . 11 ⊢ (((1 / 𝑘) ∈ ℝ ∧ 0 ∈ ℝ) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
181	178, 179, 180	sylancl 597	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
182	177, 181	syl 18	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
183	27, 182	sylan2 604	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
184	176, 183	fsumrecl 15781	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
185	2, 184	remulcld 11234	. . . . . 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 16974	. . . . . . 7 ⊢ (𝜑 → (𝑁 ∈ (ℤ_≥‘𝐾) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
190		eluz 12871	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (ℤ_≥‘𝑁) ↔ 𝑁 ≤ 𝐾))
191	62, 59, 190	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ (ℤ_≥‘𝑁) ↔ 𝑁 ≤ 𝐾))
192		nnleltp1 12646	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1)))
193	1, 14, 192	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1)))
194		fzn 13563	. . . . . . . . . 10 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
195	60, 62, 194	syl2anc 595	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
196	191, 193, 195	3bitrd 308	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∈ (ℤ_≥‘𝑁) ↔ ((𝐾 + 1)...𝑁) = ∅))
197		0le0 12337	. . . . . . . . . 10 ⊢ 0 ≤ 0
198	23	mul01d 11404	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · 0) = 0)
199	197, 198	breqtrrid 5149	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝑁 · 0))
200		iuneq1 4973	. . . . . . . . . . . . 13 ⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘))
201		0iun 5027	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅
202	200, 201	eqtrdi 2814	. . . . . . . . . . . 12 ⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∅)
203	202	fveq2d 6885	. . . . . . . . . . 11 ⊢ (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = (♯‘∅))
204		hash0 14399	. . . . . . . . . . 11 ⊢ (♯‘∅) = 0
205	203, 204	eqtrdi 2814	. . . . . . . . . 10 ⊢ (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = 0)
206		sumeq1 15736	. . . . . . . . . . . 12 ⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
207		sum0 15768	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
208	206, 207	eqtrdi 2814	. . . . . . . . . . 11 ⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
209	208	oveq2d 7426	. . . . . . . . . 10 ⊢ (((𝐾 + 1)...𝑁) = ∅ → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
210	205, 209	breq12d 5122	. . . . . . . . 9 ⊢ (((𝐾 + 1)...𝑁) = ∅ → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ 0 ≤ (𝑁 · 0)))
211	199, 210	syl5ibrcom 250	. . . . . . . 8 ⊢ (𝜑 → (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
212	196, 211	sylbid 243	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∈ (ℤ_≥‘𝑁) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
213		uztric 12881	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ_≥‘𝐾) ∨ 𝐾 ∈ (ℤ_≥‘𝑁)))
214	59, 62, 213	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → (𝑁 ∈ (ℤ_≥‘𝐾) ∨ 𝐾 ∈ (ℤ_≥‘𝑁)))
215	189, 212, 214	mpjaod 873	. . . . . 6 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
216		eqid 2763	. . . . . . . . . 10 ⊢ (ℤ_≥‘(𝐾 + 1)) = (ℤ_≥‘(𝐾 + 1))
217		eleq1w 2846	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
218		oveq2 7418	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
219	217, 218	ifbieq1d 4512	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
220		ovex 7443	. . . . . . . . . . . . 13 ⊢ (1 / 𝑘) ∈ V
221		c0ex 11195	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
222	220, 221	ifex 4538	. . . . . . . . . . . 12 ⊢ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ V
223	219, 186, 222	fvmpt 6989	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
224	177, 223	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
225	181	recnd 11232	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
226	223, 225	eqeltrd 2863	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ)
227	226	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
228	72, 26, 227	iserex 15704	. . . . . . . . . . 11 ⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ ))
229	187, 228	mpbid 235	. . . . . . . . . 10 ⊢ (𝜑 → seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ )
230	216, 60, 224, 182, 229	isumrecl 15812	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ (ℤ_≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
231		halfre 12452	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℝ
232	231	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
233		fzssuz 13589	. . . . . . . . . . 11 ⊢ ((𝐾 + 1)...𝑁) ⊆ (ℤ_≥‘(𝐾 + 1))
234	233	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ⊆ (ℤ_≥‘(𝐾 + 1)))
235		nnrp 13023	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ⁺)
236	235	rpreccld 13065	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ⁺)
237	236	rpge0d 13059	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
238		breq2 5113	. . . . . . . . . . . . 13 ⊢ ((1 / 𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ (1 / 𝑘) ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
239		breq2 5113	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
240	238, 239	ifboth 4527	. . . . . . . . . . . 12 ⊢ ((0 ≤ (1 / 𝑘) ∧ 0 ≤ 0) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
241	237, 197, 240	sylancl 597	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
242	177, 241	syl 18	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
243	216, 60, 176, 234, 224, 182, 242, 229	isumless 15895	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ≤ Σ𝑘 ∈ (ℤ_≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
244	184, 230, 232, 243, 188	lelttrd 11363	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
245	1	nngt0d 12280	. . . . . . . . 9 ⊢ (𝜑 → 0 < 𝑁)
246		ltmul2 12061	. . . . . . . . 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 1401	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
248	244, 247	mpbid 235	. . . . . . 7 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))
249		2cn 12311	. . . . . . . . 9 ⊢ 2 ∈ ℂ
250		2ne0 12342	. . . . . . . . 9 ⊢ 2 ≠ 0
251		divrec 11883	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (𝑁 / 2) = (𝑁 · (1 / 2)))
252	249, 250, 251	mp3an23 1482	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → (𝑁 / 2) = (𝑁 · (1 / 2)))
253	23, 252	syl 18	. . . . . . 7 ⊢ (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2)))
254	248, 253	breqtrrd 5139	. . . . . 6 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 / 2))
255	175, 185, 3, 215, 254	lelttrd 11363	. . . . 5 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) < (𝑁 / 2))
256	175, 3, 12, 255	ltadd2dd 11364	. . . 4 ⊢ (𝜑 → ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) < ((♯‘𝑀) + (𝑁 / 2)))
257	172, 256	eqbrtrd 5133	. . 3 ⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2)))
258	3, 12, 3	ltadd1d 11802	. . 3 ⊢ (𝜑 → ((𝑁 / 2) < (♯‘𝑀) ↔ ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2))))
259	257, 258	mpbird 260	. 2 ⊢ (𝜑 → (𝑁 / 2) < (♯‘𝑀))
260		oveq1 7417	. . . . . . . 8 ⊢ (𝑘 = 𝑟 → (𝑘↑2) = (𝑟↑2))
261	260	breq1d 5119	. . . . . . 7 ⊢ (𝑘 = 𝑟 → ((𝑘↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑥))
262	261	cbvrabv 3426	. . . . . 6 ⊢ {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥}
263		breq2 5113	. . . . . . 7 ⊢ (𝑥 = 𝑛 → ((𝑟↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑛))
264	263	rabbidv 3423	. . . . . 6 ⊢ (𝑥 = 𝑛 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
265	262, 264	eqtrid 2810	. . . . 5 ⊢ (𝑥 = 𝑛 → {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
266	265	supeq1d 9402	. . . 4 ⊢ (𝑥 = 𝑛 → sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
267	266	cbvmptv 5215	. . 3 ⊢ (𝑥 ∈ ℕ ↦ sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < )) = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
268	186, 14, 1, 5, 267	prmreclem3 16973	. 2 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
269	3, 12, 22, 259, 268	ltletrd 11365	1 ⊢ (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 ∃wrex 3089 {crab 3416 ∖ cdif 3902 ∪ cun 3903 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 ifcif 4487 ∪ ciun 4956 class class class wbr 5109 ↦ cmpt 5192 dom cdm 5661 ‘cfv 6536 (class class class)co 7410 Fincfn 8939 supcsup 9396 ℂcc 11093 ℝcr 11094 0cc0 11095 1c1 11096 + caddc 11098 · cmul 11100 < clt 11238 ≤ cle 11239 / cdiv 11866 ℕcn 12228 2c2 12290 ℕ₀cn0 12499 ℤcz 12586 ℤ_≥cuz 12857 ...cfz 13530 seqcseq 14033 ↑cexp 14093 ♯chash 14362 √csqrt 15280 ⇝ cli 15531 Σcsu 15733 ∥ cdvds 16305 ℙcprime 16724

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-inf2 9606 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172 ax-pre-sup 11173

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-2o 8450 df-oadd 8453 df-er 8690 df-map 8822 df-pm 8823 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9398 df-inf 9399 df-oi 9468 df-dju 9883 df-card 9921 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-div 11867 df-nn 12229 df-2 12298 df-3 12299 df-n0 12500 df-xnn0 12573 df-z 12587 df-uz 12858 df-q 12968 df-rp 13012 df-fz 13531 df-fzo 13679 df-fl 13821 df-mod 13899 df-seq 14034 df-exp 14094 df-hash 14363 df-cj 15146 df-re 15147 df-im 15148 df-sqrt 15282 df-abs 15283 df-clim 15535 df-rlim 15536 df-sum 15734 df-dvds 16306 df-gcd 16548 df-prm 16725 df-pc 16892

This theorem is referenced by: prmreclem6 16976

W3C validator