prmreclem3 - Metamath Proof Explorer

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

Theorem prmreclem3 16837

Description: Lemma for prmrec 16841. The main inequality established here is ♯𝑀 ≤ ♯{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} · √𝑁, where {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} is the set of squarefree numbers in 𝑀. This is demonstrated by the map 𝑦 ↦ ⟨𝑦 / (𝑄‘𝑦)↑2, (𝑄‘𝑦)⟩ where 𝑄‘𝑦 is the largest number whose square divides 𝑦. (Contributed by Mario Carneiro, 5-Aug-2014.)

**Hypotheses**
Ref	Expression
prmrec.1	⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
prmrec.2	⊢ (𝜑 → 𝐾 ∈ ℕ)
prmrec.3	⊢ (𝜑 → 𝑁 ∈ ℕ)
prmrec.4	⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
prmreclem2.5	⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))

**Assertion**
Ref	Expression
prmreclem3	⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))

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

Proof of Theorem prmreclem3 Dummy variables 𝑥 𝑦 𝑧 𝐴 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fzfi 13886	. . . . . 6 ⊢ (1...𝑁) ∈ Fin
2		prmrec.4	. . . . . . 7 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
3	2	ssrab3 4031	. . . . . 6 ⊢ 𝑀 ⊆ (1...𝑁)
4		ssfi 9093	. . . . . 6 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
5	1, 3, 4	mp2an 692	. . . . 5 ⊢ 𝑀 ∈ Fin
6		hashcl 14270	. . . . 5 ⊢ (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ₀)
7	5, 6	ax-mp 5	. . . 4 ⊢ (♯‘𝑀) ∈ ℕ₀
8	7	nn0rei 12403	. . 3 ⊢ (♯‘𝑀) ∈ ℝ
9	8	a1i 11	. 2 ⊢ (𝜑 → (♯‘𝑀) ∈ ℝ)
10		2nn 12209	. . . . . 6 ⊢ 2 ∈ ℕ
11		prmrec.2	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ)
12	11	nnnn0d 12453	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
13		nnexpcl 13988	. . . . . 6 ⊢ ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ₀) → (2↑𝐾) ∈ ℕ)
14	10, 12, 13	sylancr 587	. . . . 5 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ)
15	14	nnnn0d 12453	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ₀)
16		prmrec.3	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
17	16	nnrpd 12938	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
18	17	rpsqrtcld 15326	. . . . . 6 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
19	18	rprege0d 12947	. . . . 5 ⊢ (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
20		flge0nn0 13731	. . . . 5 ⊢ (((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)) → (⌊‘(√‘𝑁)) ∈ ℕ₀)
21	19, 20	syl 17	. . . 4 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℕ₀)
22	15, 21	nn0mulcld 12458	. . 3 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℕ₀)
23	22	nn0red 12454	. 2 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℝ)
24	14	nnred 12151	. . 3 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ)
25	18	rpred 12940	. . 3 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
26	24, 25	remulcld 11153	. 2 ⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
27		ssrab2 4029	. . . . . . 7 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀
28		ssfi 9093	. . . . . . 7 ⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin)
29	5, 27, 28	mp2an 692	. . . . . 6 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin
30		hashcl 14270	. . . . . 6 ⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℕ₀)
31	29, 30	ax-mp 5	. . . . 5 ⊢ (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℕ₀
32	31	nn0rei 12403	. . . 4 ⊢ (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ
33	21	nn0red 12454	. . . 4 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℝ)
34		remulcl 11102	. . . 4 ⊢ (((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ ∧ (⌊‘(√‘𝑁)) ∈ ℝ) → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
35	32, 33, 34	sylancr 587	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
36		fzfi 13886	. . . . . . 7 ⊢ (1...(⌊‘(√‘𝑁))) ∈ Fin
37		xpfi 9215	. . . . . . 7 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin)
38	29, 36, 37	mp2an 692	. . . . . 6 ⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin
39		fveqeq2 6840	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 / ((𝑄‘𝑦)↑2)) → ((𝑄‘𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1))
40		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ 𝑀)
41	3, 40	sselid 3928	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ (1...𝑁))
42		elfznn 13460	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
43	41, 42	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℕ)
44		prmreclem2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
45	44	prmreclem1 16835	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
46	45	simp2d 1143	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦)↑2) ∥ 𝑦)
47	43, 46	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∥ 𝑦)
48	45	simp1d 1142	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ → (𝑄‘𝑦) ∈ ℕ)
49	43, 48	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℕ)
50	49	nnsqcld 14158	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℕ)
51	50	nnzd 12505	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℤ)
52	50	nnne0d 12186	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≠ 0)
53	43	nnzd 12505	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℤ)
54		dvdsval2 16173	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ))
55	51, 52, 53, 54	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ))
56	47, 55	mpbid 232	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ)
57		nnre 12143	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
58		nngt0 12167	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
59	57, 58	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
60		nnre 12143	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → ((𝑄‘𝑦)↑2) ∈ ℝ)
61		nngt0 12167	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → 0 < ((𝑄‘𝑦)↑2))
62	60, 61	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2)))
63		divgt0 12001	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℝ ∧ 0 < 𝑦) ∧ (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2))) → 0 < (𝑦 / ((𝑄‘𝑦)↑2)))
64	59, 62, 63	syl2an 596	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∈ ℕ) → 0 < (𝑦 / ((𝑄‘𝑦)↑2)))
65	43, 50, 64	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 0 < (𝑦 / ((𝑄‘𝑦)↑2)))
66		elnnz 12489	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄‘𝑦)↑2))))
67	56, 65, 66	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ)
68	67	nnred 12151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℝ)
69	43	nnred 12151	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℝ)
70	16	nnred 12151	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ)
71	70	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℝ)
72		dvdsmul1 16195	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)))
73	56, 51, 72	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)))
74	43	nncnd 12152	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℂ)
75	50	nncnd 12152	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℂ)
76	74, 75, 52	divcan1d 11909	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦)
77	73, 76	breqtrd 5121	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦)
78		dvdsle 16228	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦))
79	56, 43, 78	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦))
80	77, 79	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦)
81		elfzle2 13435	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ≤ 𝑁)
82	41, 81	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ≤ 𝑁)
83	68, 69, 71, 80, 82	letrd 11281	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁)
84		nnuz 12781	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
85	67, 84	eleqtrdi 2843	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ (ℤ_≥‘1))
86	16	nnzd 12505	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
87	86	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℤ)
88		elfz5 13423	. . . . . . . . . . . . 13 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁))
89	85, 87, 88	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁))
90	83, 89	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁))
91		breq2 5099	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦))
92	91	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦))
93	92	ralbidv 3156	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
94	93, 2	elrab2 3646	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
95	40, 94	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
96	95	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
97	77	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦)
98		eldifi 4080	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
99		prmz 16593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
100	98, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℤ)
101	100	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑝 ∈ ℤ)
102	56	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ)
103	53	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑦 ∈ ℤ)
104		dvdstr 16212	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦))
105	101, 102, 103, 104	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦))
106	97, 105	mpan2d 694	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) → 𝑝 ∥ 𝑦))
107	106	con3d 152	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝 ∥ 𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
108	107	ralimdva 3145	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
109	96, 108	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
110		breq2 5099	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
111	110	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
112	111	ralbidv 3156	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
113	112, 2	elrab2 3646	. . . . . . . . . . 11 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
114	90, 109, 113	sylanbrc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀)
115	44	prmreclem1 16835	. . . . . . . . . . . . 13 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝐴 ∈ (ℤ_≥‘2) → ¬ (𝐴↑2) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2)))))
116	115	simp2d 1143	. . . . . . . . . . . 12 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
117	67, 116	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
118	115	simp1d 1142	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ)
119	67, 118	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ)
120		elnn1uz2 12829	. . . . . . . . . . . . . 14 ⊢ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
121	119, 120	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
122	121	ord 864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
123	44	prmreclem1 16835	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
124	123	simp3d 1144	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
125	43, 122, 124	sylsyld 61	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
126	117, 125	mt4d 117	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1)
127	39, 114, 126	elrabd 3645	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1})
128	50	nnred 12151	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℝ)
129		dvdsle 16228	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ 𝑦 ∈ ℕ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 → ((𝑄‘𝑦)↑2) ≤ 𝑦))
130	51, 43, 129	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 → ((𝑄‘𝑦)↑2) ≤ 𝑦))
131	47, 130	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑦)
132	128, 69, 71, 131, 82	letrd 11281	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑁)
133	71	recnd 11151	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℂ)
134	133	sqsqrtd 15356	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((√‘𝑁)↑2) = 𝑁)
135	132, 134	breqtrrd 5123	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))
136	49	nnrpd 12938	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℝ⁺)
137	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈ ℝ⁺)
138		rprege0 12912	. . . . . . . . . . . . . 14 ⊢ ((𝑄‘𝑦) ∈ ℝ⁺ → ((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦)))
139		rprege0 12912	. . . . . . . . . . . . . 14 ⊢ ((√‘𝑁) ∈ ℝ⁺ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
140		le2sq 14048	. . . . . . . . . . . . . 14 ⊢ ((((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦)) ∧ ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁))) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)))
141	138, 139, 140	syl2an 596	. . . . . . . . . . . . 13 ⊢ (((𝑄‘𝑦) ∈ ℝ⁺ ∧ (√‘𝑁) ∈ ℝ⁺) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)))
142	136, 137, 141	syl2anc 584	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)))
143	135, 142	mpbird 257	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (√‘𝑁))
144	25	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈ ℝ)
145	49	nnzd 12505	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℤ)
146		flge 13716	. . . . . . . . . . . 12 ⊢ (((√‘𝑁) ∈ ℝ ∧ (𝑄‘𝑦) ∈ ℤ) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
147	144, 145, 146	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
148	143, 147	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))
149	49, 84	eleqtrdi 2843	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ (ℤ_≥‘1))
150	21	nn0zd 12504	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℤ)
151	150	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (⌊‘(√‘𝑁)) ∈ ℤ)
152		elfz5 13423	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑦) ∈ (ℤ_≥‘1) ∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
153	149, 151, 152	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
154	148, 153	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))))
155	127, 154	opelxpd 5660	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
156	155	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝑀 → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
157		ovex 7388	. . . . . . . . . . . 12 ⊢ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ V
158		fvex 6844	. . . . . . . . . . . 12 ⊢ (𝑄‘𝑦) ∈ V
159	157, 158	opth 5421	. . . . . . . . . . 11 ⊢ (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧)))
160		oveq1 7362	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑦) = (𝑄‘𝑧) → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2))
161		oveq12 7364	. . . . . . . . . . . 12 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)))
162	160, 161	sylan2 593	. . . . . . . . . . 11 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)))
163	159, 162	sylbi 217	. . . . . . . . . 10 ⊢ (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)))
164	76	adantrr 717	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦)
165		fz1ssnn 13462	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ⊆ ℕ
166	3, 165	sstri 3940	. . . . . . . . . . . . . 14 ⊢ 𝑀 ⊆ ℕ
167		simprr 772	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ 𝑀)
168	166, 167	sselid 3928	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℕ)
169	168	nncnd 12152	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℂ)
170	44	prmreclem1 16835	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ → ((𝑄‘𝑧) ∈ ℕ ∧ ((𝑄‘𝑧)↑2) ∥ 𝑧 ∧ (2 ∈ (ℤ_≥‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄‘𝑧)↑2)))))
171	170	simp1d 1142	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ → (𝑄‘𝑧) ∈ ℕ)
172	168, 171	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (𝑄‘𝑧) ∈ ℕ)
173	172	nnsqcld 14158	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℕ)
174	173	nncnd 12152	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℂ)
175	173	nnne0d 12186	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ≠ 0)
176	169, 174, 175	divcan1d 11909	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) = 𝑧)
177	164, 176	eqeq12d 2749	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) ↔ 𝑦 = 𝑧))
178	163, 177	imbitrid 244	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ → 𝑦 = 𝑧))
179		id 22	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
180		fveq2 6831	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑄‘𝑦) = (𝑄‘𝑧))
181	180	oveq1d 7370	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2))
182	179, 181	oveq12d 7373	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)))
183	182, 180	opeq12d 4834	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩)
184	178, 183	impbid1 225	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ 𝑦 = 𝑧))
185	184	ex 412	. . . . . . 7 ⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ 𝑦 = 𝑧)))
186	156, 185	dom2d 8926	. . . . . 6 ⊢ (𝜑 → (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
187	38, 186	mpi 20	. . . . 5 ⊢ (𝜑 → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
188		hashdom 14293	. . . . . 6 ⊢ ((𝑀 ∈ Fin ∧ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin) → ((♯‘𝑀) ≤ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
189	5, 38, 188	mp2an 692	. . . . 5 ⊢ ((♯‘𝑀) ≤ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
190	187, 189	sylibr 234	. . . 4 ⊢ (𝜑 → (♯‘𝑀) ≤ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
191		hashxp 14348	. . . . . 6 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))))
192	29, 36, 191	mp2an 692	. . . . 5 ⊢ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁)))))
193		hashfz1 14260	. . . . . . 7 ⊢ ((⌊‘(√‘𝑁)) ∈ ℕ₀ → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
194	21, 193	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
195	194	oveq2d 7371	. . . . 5 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
196	192, 195	eqtrid 2780	. . . 4 ⊢ (𝜑 → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
197	190, 196	breqtrd 5121	. . 3 ⊢ (𝜑 → (♯‘𝑀) ≤ ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
198	32	a1i 11	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ)
199	21	nn0ge0d 12456	. . . 4 ⊢ (𝜑 → 0 ≤ (⌊‘(√‘𝑁)))
200		prmrec.1	. . . . 5 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
201	200, 11, 16, 2, 44	prmreclem2 16836	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))
202	198, 24, 33, 199, 201	lemul1ad 12072	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
203	9, 35, 23, 197, 202	letrd 11281	. 2 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
204	14	nnrpd 12938	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ⁺)
205	204	rprege0d 12947	. . 3 ⊢ (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾)))
206		fllelt 13708	. . . . 5 ⊢ ((√‘𝑁) ∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
207	25, 206	syl 17	. . . 4 ⊢ (𝜑 → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
208	207	simpld 494	. . 3 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ≤ (√‘𝑁))
209		lemul2a 11987	. . 3 ⊢ ((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧ ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) ∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
210	33, 25, 205, 208, 209	syl31anc 1375	. 2 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
211	9, 23, 26, 203, 210	letrd 11281	1 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1541 ∈ wcel 2113 ≠ wne 2929 ∀wral 3048 {crab 3396 ∖ cdif 3895 ⊆ wss 3898 ifcif 4476 ⟨cop 4583 class class class wbr 5095 ↦ cmpt 5176 × cxp 5619 ‘cfv 6489 (class class class)co 7355 ≼ cdom 8877 Fincfn 8879 supcsup 9335 ℝcr 11016 0cc0 11017 1c1 11018 + caddc 11020 · cmul 11022 < clt 11157 ≤ cle 11158 / cdiv 11785 ℕcn 12136 2c2 12191 ℕ₀cn0 12392 ℤcz 12479 ℤ_≥cuz 12742 ℝ⁺crp 12896 ...cfz 13414 ⌊cfl 13701 ↑cexp 13975 ♯chash 14244 √csqrt 15147 ∥ cdvds 16170 ℙcprime 16589

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 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2705 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7677 ax-cnex 11073 ax-resscn 11074 ax-1cn 11075 ax-icn 11076 ax-addcl 11077 ax-addrcl 11078 ax-mulcl 11079 ax-mulrcl 11080 ax-mulcom 11081 ax-addass 11082 ax-mulass 11083 ax-distr 11084 ax-i2m1 11085 ax-1ne0 11086 ax-1rid 11087 ax-rnegex 11088 ax-rrecex 11089 ax-cnre 11090 ax-pre-lttri 11091 ax-pre-lttrn 11092 ax-pre-ltadd 11093 ax-pre-mulgt0 11094 ax-pre-sup 11095

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2725 df-clel 2808 df-nfc 2882 df-ne 2930 df-nel 3034 df-ral 3049 df-rex 3058 df-rmo 3347 df-reu 3348 df-rab 3397 df-v 3439 df-sbc 3738 df-csb 3847 df-dif 3901 df-un 3903 df-in 3905 df-ss 3915 df-pss 3918 df-nul 4283 df-if 4477 df-pw 4553 df-sn 4578 df-pr 4580 df-op 4584 df-uni 4861 df-int 4900 df-iun 4945 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-we 5576 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 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-riota 7312 df-ov 7358 df-oprab 7359 df-mpo 7360 df-om 7806 df-1st 7930 df-2nd 7931 df-frecs 8220 df-wrecs 8251 df-recs 8300 df-rdg 8338 df-1o 8394 df-2o 8395 df-oadd 8398 df-er 8631 df-map 8761 df-pm 8762 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-sup 9337 df-inf 9338 df-dju 9805 df-card 9843 df-pnf 11159 df-mnf 11160 df-xr 11161 df-ltxr 11162 df-le 11163 df-sub 11357 df-neg 11358 df-div 11786 df-nn 12137 df-2 12199 df-3 12200 df-n0 12393 df-xnn0 12466 df-z 12480 df-uz 12743 df-q 12853 df-rp 12897 df-fz 13415 df-fl 13703 df-mod 13781 df-seq 13916 df-exp 13976 df-hash 14245 df-cj 15013 df-re 15014 df-im 15015 df-sqrt 15149 df-abs 15150 df-dvds 16171 df-gcd 16413 df-prm 16590 df-pc 16756

This theorem is referenced by: prmreclem5 16839

W3C validator