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 16891

Description: Lemma for prmrec 16893. 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 16890 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 12201	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℝ)
3	2	rehalfcld 12429	. 2 ⊢ (𝜑 → (𝑁 / 2) ∈ ℝ)
4		fzfi 13937	. . . . . 6 ⊢ (1...𝑁) ∈ Fin
5		prmrec.4	. . . . . . 7 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
6	5	ssrab3 4045	. . . . . 6 ⊢ 𝑀 ⊆ (1...𝑁)
7		ssfi 9137	. . . . . 6 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
8	4, 6, 7	mp2an 692	. . . . 5 ⊢ 𝑀 ∈ Fin
9		hashcl 14321	. . . . 5 ⊢ (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ₀)
10	8, 9	ax-mp 5	. . . 4 ⊢ (♯‘𝑀) ∈ ℕ₀
11	10	nn0rei 12453	. . 3 ⊢ (♯‘𝑀) ∈ ℝ
12	11	a1i 11	. 2 ⊢ (𝜑 → (♯‘𝑀) ∈ ℝ)
13		2nn 12259	. . . . 5 ⊢ 2 ∈ ℕ
14		prmrec.2	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ)
15	14	nnnn0d 12503	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
16		nnexpcl 14039	. . . . 5 ⊢ ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ₀) → (2↑𝐾) ∈ ℕ)
17	13, 15, 16	sylancr 587	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ)
18	17	nnred 12201	. . 3 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ)
19	1	nnrpd 12993	. . . . 5 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
20	19	rpsqrtcld 15378	. . . 4 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
21	20	rpred 12995	. . 3 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
22	18, 21	remulcld 11204	. 2 ⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
23	2	recnd 11202	. . . . . 6 ⊢ (𝜑 → 𝑁 ∈ ℂ)
24	23	2halvesd 12428	. . . . 5 ⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁)
25	6	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → 𝑀 ⊆ (1...𝑁))
26	14	peano2nnd 12203	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐾 + 1) ∈ ℕ)
27		elfzuz 13481	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ_≥‘(𝐾 + 1)))
28		eluznn 12877	. . . . . . . . . . . . 13 ⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
29	26, 27, 28	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
30		eleq1w 2811	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ))
31		breq1 5110	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛))
32	30, 31	anbi12d 632	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)))
33	32	rabbidv 3413	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
34		prmrec.7	. . . . . . . . . . . . . . 15 ⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)})
35		ovex 7420	. . . . . . . . . . . . . . . 16 ⊢ (1...𝑁) ∈ V
36	35	rabex 5294	. . . . . . . . . . . . . . 15 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V
37	33, 34, 36	fvmpt 6968	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
38	37	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
39		ssrab2 4043	. . . . . . . . . . . . 13 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁)
40	38, 39	eqsstrdi 3991	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁))
41	29, 40	syldan 591	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) ⊆ (1...𝑁))
42	41	ralrimiva 3125	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁))
43		iunss 5009	. . . . . . . . . 10 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁))
44	42, 43	sylibr 234	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁))
45	25, 44	unssd 4155	. . . . . . . 8 ⊢ (𝜑 → (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ⊆ (1...𝑁))
46		breq1 5110	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → (𝑝 ∥ 𝑛 ↔ 𝑞 ∥ 𝑛))
47	46	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑝 = 𝑞 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑛))
48	47	cbvralvw 3215	. . . . . . . . . . . . . 14 ⊢ (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑛)
49		breq2 5111	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → (𝑞 ∥ 𝑛 ↔ 𝑞 ∥ 𝑥))
50	49	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → (¬ 𝑞 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑥))
51	50	ralbidv 3156	. . . . . . . . . . . . . 14 ⊢ (𝑛 = 𝑥 → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥))
52	48, 51	bitrid 283	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥))
53	52, 5	elrab2 3662	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥))
54		elun1 4145	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ 𝑀 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
55	53, 54	sylbir 235	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
56	55	ex 412	. . . . . . . . . 10 ⊢ (𝑥 ∈ (1...𝑁) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
57	56	adantl 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
58		dfrex2 3056	. . . . . . . . . 10 ⊢ (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 ↔ ¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)
59	14	nnzd 12556	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐾 ∈ ℤ)
60	59	peano2zd 12641	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐾 + 1) ∈ ℤ)
61	60	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ∈ ℤ)
62	1	nnzd 12556	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℤ)
63	62	ad2antrr 726	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℤ)
64		eldifi 4094	. . . . . . . . . . . . . . . 16 ⊢ (𝑞 ∈ (ℙ ∖ (1...𝐾)) → 𝑞 ∈ ℙ)
65	64	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℙ)
66		prmz 16645	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℤ)
67	65, 66	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℤ)
68		eldifn 4095	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑞 ∈ (ℙ ∖ (1...𝐾)) → ¬ 𝑞 ∈ (1...𝐾))
69	68	ad2antrl 728	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ∈ (1...𝐾))
70		prmnn 16644	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ ℙ → 𝑞 ∈ ℕ)
71	65, 70	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℕ)
72		nnuz 12836	. . . . . . . . . . . . . . . . . . 19 ⊢ ℕ = (ℤ_≥‘1)
73	71, 72	eleqtrdi 2838	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ (ℤ_≥‘1))
74	59	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℤ)
75		elfz5 13477	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ (ℤ_≥‘1) ∧ 𝐾 ∈ ℤ) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾))
76	73, 74, 75	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾))
77	69, 76	mtbid 324	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ≤ 𝐾)
78	14	nnred 12201	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ ℝ)
79	78	ad2antrr 726	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℝ)
80	71	nnred 12201	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℝ)
81	79, 80	ltnled 11321	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ ¬ 𝑞 ≤ 𝐾))
82	77, 81	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 < 𝑞)
83		zltp1le 12583	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
84	74, 67, 83	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞))
85	82, 84	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ≤ 𝑞)
86		elfznn 13514	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
87	86	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℕ)
88	87	nnred 12201	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℝ)
89	2	ad2antrr 726	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℝ)
90		simprr 772	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∥ 𝑥)
91		dvdsle 16280	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥))
92	67, 87, 91	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥))
93	90, 92	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑥)
94		elfzle2 13489	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁)
95	94	ad2antlr 727	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ≤ 𝑁)
96	80, 88, 89, 93, 95	letrd 11331	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑁)
97	61, 63, 67, 85, 96	elfzd 13476	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ((𝐾 + 1)...𝑁))
98	49	anbi2d 630	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑥 → ((𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥)))
99		simplr 768	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (1...𝑁))
100	65, 90	jca 511	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥))
101	98, 99, 100	elrabd 3661	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
102		eleq1w 2811	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 = 𝑞 → (𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ))
103	102, 46	anbi12d 632	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑞 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)))
104	103	rabbidv 3413	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑞 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
105	35	rabex 5294	. . . . . . . . . . . . . . . 16 ⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)} ∈ V
106	104, 34, 105	fvmpt 6968	. . . . . . . . . . . . . . 15 ⊢ (𝑞 ∈ ℕ → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
107	71, 106	syl 17	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)})
108	101, 107	eleqtrrd 2831	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑊‘𝑞))
109		fveq2 6858	. . . . . . . . . . . . . 14 ⊢ (𝑘 = 𝑞 → (𝑊‘𝑘) = (𝑊‘𝑞))
110	109	eliuni 4961	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑥 ∈ (𝑊‘𝑞)) → 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
111	97, 108, 110	syl2anc 584	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
112		elun2 4146	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
113	111, 112	syl 17	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
114	113	rexlimdvaa 3135	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
115	58, 114	biimtrrid 243	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
116	57, 115	pm2.61d 179	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → 𝑥 ∈ (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
117	45, 116	eqelssd 3968	. . . . . . 7 ⊢ (𝜑 → (𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = (1...𝑁))
118	117	fveq2d 6862	. . . . . 6 ⊢ (𝜑 → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = (♯‘(1...𝑁)))
119	1	nnnn0d 12503	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
120		hashfz1 14311	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → (♯‘(1...𝑁)) = 𝑁)
121	119, 120	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘(1...𝑁)) = 𝑁)
122	118, 121	eqtr2d 2765	. . . . 5 ⊢ (𝜑 → 𝑁 = (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
123	8	a1i 11	. . . . . 6 ⊢ (𝜑 → 𝑀 ∈ Fin)
124		ssfi 9137	. . . . . . 7 ⊢ (((1...𝑁) ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin)
125	4, 44, 124	sylancr 587	. . . . . 6 ⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin)
126		breq1 5110	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑥 ↔ 𝑘 ∥ 𝑥))
127	126	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑝 = 𝑘 → (¬ 𝑝 ∥ 𝑥 ↔ ¬ 𝑘 ∥ 𝑥))
128		breq2 5111	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑛 = 𝑥 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑥))
129	128	notbid 318	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑥 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑥))
130	129	ralbidv 3156	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥))
131	130, 5	elrab2 3662	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥))
132	131	simprbi 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)
133	132	ad2antlr 727	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)
134		simprr 772	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ℙ)
135		noel 4301	. . . . . . . . . . . . . . . . . 18 ⊢ ¬ 𝑘 ∈ ∅
136		simprl 770	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ((𝐾 + 1)...𝑁))
137	136	biantrud 531	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁))))
138		elin 3930	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)))
139	137, 138	bitr4di 289	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁))))
140	78	ltp1d 12113	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝜑 → 𝐾 < (𝐾 + 1))
141		fzdisj 13512	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝐾 < (𝐾 + 1) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
142	140, 141	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝜑 → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
143	142	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅)
144	143	eleq2d 2814	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ 𝑘 ∈ ∅))
145	139, 144	bitrd 279	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ∅))
146	135, 145	mtbiri 327	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∈ (1...𝐾))
147	134, 146	eldifd 3925	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ (ℙ ∖ (1...𝐾)))
148	127, 133, 147	rspcdva 3589	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∥ 𝑥)
149	148	expr 456	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥))
150		imnan 399	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥) ↔ ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))
151	149, 150	sylib 218	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))
152	29	adantlr 715	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ)
153	152, 37	syl 17	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})
154	153	eleq2d 2814	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) ↔ 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}))
155		breq2 5111	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑥 → (𝑘 ∥ 𝑛 ↔ 𝑘 ∥ 𝑥))
156	155	anbi2d 630	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑥 → ((𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)))
157	156	elrab 3659	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)))
158	157	simprbi 496	. . . . . . . . . . . . . 14 ⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))
159	154, 158	biimtrdi 253	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)))
160	151, 159	mtod 198	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ 𝑥 ∈ (𝑊‘𝑘))
161	160	nrexdv 3128	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘))
162		eliun 4959	. . . . . . . . . . 11 ⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ↔ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘))
163	161, 162	sylnibr 329	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))
164	163	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
165		imnan 399	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
166	164, 165	sylib 218	. . . . . . . 8 ⊢ (𝜑 → ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
167		elin 3930	. . . . . . . 8 ⊢ (𝑥 ∈ (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
168	166, 167	sylnibr 329	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑥 ∈ (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))
169	168	eq0rdv 4370	. . . . . 6 ⊢ (𝜑 → (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅)
170		hashun 14347	. . . . . 6 ⊢ ((𝑀 ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin ∧ (𝑀 ∩ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅) → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
171	123, 125, 169, 170	syl3anc 1373	. . . . 5 ⊢ (𝜑 → (♯‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
172	24, 122, 171	3eqtrd 2768	. . . 4 ⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))))
173		hashcl 14321	. . . . . . 7 ⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℕ₀)
174	125, 173	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℕ₀)
175	174	nn0red 12504	. . . . 5 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℝ)
176		fzfid 13938	. . . . . . . 8 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin)
177	26, 28	sylan 580	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ)
178		nnrecre 12228	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ)
179		0re 11176	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
180		ifcl 4534	. . . . . . . . . . 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 15700	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
185	2, 184	remulcld 11204	. . . . . 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 16890	. . . . . . 7 ⊢ (𝜑 → (𝑁 ∈ (ℤ_≥‘𝐾) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
190		eluz 12807	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (ℤ_≥‘𝑁) ↔ 𝑁 ≤ 𝐾))
191	62, 59, 190	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ (ℤ_≥‘𝑁) ↔ 𝑁 ≤ 𝐾))
192		nnleltp1 12589	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1)))
193	1, 14, 192	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1)))
194		fzn 13501	. . . . . . . . . 10 ⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
195	60, 62, 194	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅))
196	191, 193, 195	3bitrd 305	. . . . . . . 8 ⊢ (𝜑 → (𝐾 ∈ (ℤ_≥‘𝑁) ↔ ((𝐾 + 1)...𝑁) = ∅))
197		0le0 12287	. . . . . . . . . 10 ⊢ 0 ≤ 0
198	23	mul01d 11373	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁 · 0) = 0)
199	197, 198	breqtrrid 5145	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝑁 · 0))
200		iuneq1 4972	. . . . . . . . . . . . 13 ⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘))
201		0iun 5027	. . . . . . . . . . . . 13 ⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅
202	200, 201	eqtrdi 2780	. . . . . . . . . . . 12 ⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∅)
203	202	fveq2d 6862	. . . . . . . . . . 11 ⊢ (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = (♯‘∅))
204		hash0 14332	. . . . . . . . . . 11 ⊢ (♯‘∅) = 0
205	203, 204	eqtrdi 2780	. . . . . . . . . 10 ⊢ (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = 0)
206		sumeq1 15655	. . . . . . . . . . . 12 ⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
207		sum0 15687	. . . . . . . . . . . 12 ⊢ Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0
208	206, 207	eqtrdi 2780	. . . . . . . . . . 11 ⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0)
209	208	oveq2d 7403	. . . . . . . . . 10 ⊢ (((𝐾 + 1)...𝑁) = ∅ → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0))
210	205, 209	breq12d 5120	. . . . . . . . 9 ⊢ (((𝐾 + 1)...𝑁) = ∅ → ((♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ 0 ≤ (𝑁 · 0)))
211	199, 210	syl5ibrcom 247	. . . . . . . 8 ⊢ (𝜑 → (((𝐾 + 1)...𝑁) = ∅ → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
212	196, 211	sylbid 240	. . . . . . 7 ⊢ (𝜑 → (𝐾 ∈ (ℤ_≥‘𝑁) → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))))
213		uztric 12817	. . . . . . . 8 ⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ_≥‘𝐾) ∨ 𝐾 ∈ (ℤ_≥‘𝑁)))
214	59, 62, 213	syl2anc 584	. . . . . . 7 ⊢ (𝜑 → (𝑁 ∈ (ℤ_≥‘𝐾) ∨ 𝐾 ∈ (ℤ_≥‘𝑁)))
215	189, 212, 214	mpjaod 860	. . . . . 6 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
216		eqid 2729	. . . . . . . . . 10 ⊢ (ℤ_≥‘(𝐾 + 1)) = (ℤ_≥‘(𝐾 + 1))
217		eleq1w 2811	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ))
218		oveq2 7395	. . . . . . . . . . . . 13 ⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘))
219	217, 218	ifbieq1d 4513	. . . . . . . . . . . 12 ⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
220		ovex 7420	. . . . . . . . . . . . 13 ⊢ (1 / 𝑘) ∈ V
221		c0ex 11168	. . . . . . . . . . . . 13 ⊢ 0 ∈ V
222	220, 221	ifex 4539	. . . . . . . . . . . 12 ⊢ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ V
223	219, 186, 222	fvmpt 6968	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
224	177, 223	syl 17	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ_≥‘(𝐾 + 1))) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
225	181	recnd 11202	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℂ)
226	223, 225	eqeltrd 2828	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ)
227	226	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ)
228	72, 26, 227	iserex 15623	. . . . . . . . . . 11 ⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔ seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ ))
229	187, 228	mpbid 232	. . . . . . . . . 10 ⊢ (𝜑 → seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ )
230	216, 60, 224, 182, 229	isumrecl 15731	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ (ℤ_≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ)
231		halfre 12395	. . . . . . . . . 10 ⊢ (1 / 2) ∈ ℝ
232	231	a1i 11	. . . . . . . . 9 ⊢ (𝜑 → (1 / 2) ∈ ℝ)
233		fzssuz 13526	. . . . . . . . . . 11 ⊢ ((𝐾 + 1)...𝑁) ⊆ (ℤ_≥‘(𝐾 + 1))
234	233	a1i 11	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐾 + 1)...𝑁) ⊆ (ℤ_≥‘(𝐾 + 1)))
235		nnrp 12963	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℕ → 𝑘 ∈ ℝ⁺)
236	235	rpreccld 13005	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (1 / 𝑘) ∈ ℝ⁺)
237	236	rpge0d 12999	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → 0 ≤ (1 / 𝑘))
238		breq2 5111	. . . . . . . . . . . . 13 ⊢ ((1 / 𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ (1 / 𝑘) ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
239		breq2 5111	. . . . . . . . . . . . 13 ⊢ (0 = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ 0 ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))
240	238, 239	ifboth 4528	. . . . . . . . . . . 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 15811	. . . . . . . . 9 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ≤ Σ𝑘 ∈ (ℤ_≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0))
244	184, 230, 232, 243, 188	lelttrd 11332	. . . . . . . 8 ⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2))
245	1	nngt0d 12235	. . . . . . . . 9 ⊢ (𝜑 → 0 < 𝑁)
246		ltmul2 12033	. . . . . . . . 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 1376	. . . . . . . 8 ⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))))
248	244, 247	mpbid 232	. . . . . . 7 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))
249		2cn 12261	. . . . . . . . 9 ⊢ 2 ∈ ℂ
250		2ne0 12290	. . . . . . . . 9 ⊢ 2 ≠ 0
251		divrec 11853	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℂ ∧ 2 ∈ ℂ ∧ 2 ≠ 0) → (𝑁 / 2) = (𝑁 · (1 / 2)))
252	249, 250, 251	mp3an23 1455	. . . . . . . 8 ⊢ (𝑁 ∈ ℂ → (𝑁 / 2) = (𝑁 · (1 / 2)))
253	23, 252	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2)))
254	248, 253	breqtrrd 5135	. . . . . 6 ⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 / 2))
255	175, 185, 3, 215, 254	lelttrd 11332	. . . . 5 ⊢ (𝜑 → (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) < (𝑁 / 2))
256	175, 3, 12, 255	ltadd2dd 11333	. . . 4 ⊢ (𝜑 → ((♯‘𝑀) + (♯‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) < ((♯‘𝑀) + (𝑁 / 2)))
257	172, 256	eqbrtrd 5129	. . 3 ⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2)))
258	3, 12, 3	ltadd1d 11771	. . 3 ⊢ (𝜑 → ((𝑁 / 2) < (♯‘𝑀) ↔ ((𝑁 / 2) + (𝑁 / 2)) < ((♯‘𝑀) + (𝑁 / 2))))
259	257, 258	mpbird 257	. 2 ⊢ (𝜑 → (𝑁 / 2) < (♯‘𝑀))
260		oveq1 7394	. . . . . . . 8 ⊢ (𝑘 = 𝑟 → (𝑘↑2) = (𝑟↑2))
261	260	breq1d 5117	. . . . . . 7 ⊢ (𝑘 = 𝑟 → ((𝑘↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑥))
262	261	cbvrabv 3416	. . . . . 6 ⊢ {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥}
263		breq2 5111	. . . . . . 7 ⊢ (𝑥 = 𝑛 → ((𝑟↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑛))
264	263	rabbidv 3413	. . . . . 6 ⊢ (𝑥 = 𝑛 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
265	262, 264	eqtrid 2776	. . . . 5 ⊢ (𝑥 = 𝑛 → {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛})
266	265	supeq1d 9397	. . . 4 ⊢ (𝑥 = 𝑛 → sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
267	266	cbvmptv 5211	. . 3 ⊢ (𝑥 ∈ ℕ ↦ sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < )) = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
268	186, 14, 1, 5, 267	prmreclem3 16889	. 2 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))
269	3, 12, 22, 259, 268	ltletrd 11334	1 ⊢ (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∃wrex 3053 {crab 3405 ∖ cdif 3911 ∪ cun 3912 ∩ cin 3913 ⊆ wss 3914 ∅c0 4296 ifcif 4488 ∪ ciun 4955 class class class wbr 5107 ↦ cmpt 5188 dom cdm 5638 ‘cfv 6511 (class class class)co 7387 Fincfn 8918 supcsup 9391 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 < clt 11208 ≤ cle 11209 / cdiv 11835 ℕcn 12186 2c2 12241 ℕ₀cn0 12442 ℤcz 12529 ℤ_≥cuz 12793 ...cfz 13468 seqcseq 13966 ↑cexp 14026 ♯chash 14295 √csqrt 15199 ⇝ cli 15450 Σcsu 15652 ∥ cdvds 16222 ℙcprime 16641

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5234 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-inf2 9594 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145 ax-pre-sup 11146

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-int 4911 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-se 5592 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-isom 6520 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-1o 8434 df-2o 8435 df-oadd 8438 df-er 8671 df-map 8801 df-pm 8802 df-en 8919 df-dom 8920 df-sdom 8921 df-fin 8922 df-sup 9393 df-inf 9394 df-oi 9463 df-dju 9854 df-card 9892 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-2 12249 df-3 12250 df-n0 12443 df-xnn0 12516 df-z 12530 df-uz 12794 df-q 12908 df-rp 12952 df-fz 13469 df-fzo 13616 df-fl 13754 df-mod 13832 df-seq 13967 df-exp 14027 df-hash 14296 df-cj 15065 df-re 15066 df-im 15067 df-sqrt 15201 df-abs 15202 df-clim 15454 df-rlim 15455 df-sum 15653 df-dvds 16223 df-gcd 16465 df-prm 16642 df-pc 16808

This theorem is referenced by: prmreclem6 16892

W3C validator