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 16547

Description: Lemma for prmrec 16551. 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 13620	. . . . . 6 ⊢ (1...𝑁) ∈ Fin
2		prmrec.4	. . . . . . 7 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
3	2	ssrab3 4011	. . . . . 6 ⊢ 𝑀 ⊆ (1...𝑁)
4		ssfi 8918	. . . . . 6 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
5	1, 3, 4	mp2an 688	. . . . 5 ⊢ 𝑀 ∈ Fin
6		hashcl 13999	. . . . 5 ⊢ (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ₀)
7	5, 6	ax-mp 5	. . . 4 ⊢ (♯‘𝑀) ∈ ℕ₀
8	7	nn0rei 12174	. . 3 ⊢ (♯‘𝑀) ∈ ℝ
9	8	a1i 11	. 2 ⊢ (𝜑 → (♯‘𝑀) ∈ ℝ)
10		2nn 11976	. . . . . 6 ⊢ 2 ∈ ℕ
11		prmrec.2	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ)
12	11	nnnn0d 12223	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
13		nnexpcl 13723	. . . . . 6 ⊢ ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ₀) → (2↑𝐾) ∈ ℕ)
14	10, 12, 13	sylancr 586	. . . . 5 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ)
15	14	nnnn0d 12223	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ₀)
16		prmrec.3	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
17	16	nnrpd 12699	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
18	17	rpsqrtcld 15051	. . . . . 6 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
19	18	rprege0d 12708	. . . . 5 ⊢ (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
20		flge0nn0 13468	. . . . 5 ⊢ (((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)) → (⌊‘(√‘𝑁)) ∈ ℕ₀)
21	19, 20	syl 17	. . . 4 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℕ₀)
22	15, 21	nn0mulcld 12228	. . 3 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℕ₀)
23	22	nn0red 12224	. 2 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℝ)
24	14	nnred 11918	. . 3 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ)
25	18	rpred 12701	. . 3 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
26	24, 25	remulcld 10936	. 2 ⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
27		ssrab2 4009	. . . . . . 7 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀
28		ssfi 8918	. . . . . . 7 ⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin)
29	5, 27, 28	mp2an 688	. . . . . 6 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin
30		hashcl 13999	. . . . . 6 ⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℕ₀)
31	29, 30	ax-mp 5	. . . . 5 ⊢ (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℕ₀
32	31	nn0rei 12174	. . . 4 ⊢ (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ
33	21	nn0red 12224	. . . 4 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℝ)
34		remulcl 10887	. . . 4 ⊢ (((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ ∧ (⌊‘(√‘𝑁)) ∈ ℝ) → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
35	32, 33, 34	sylancr 586	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
36		fzfi 13620	. . . . . . 7 ⊢ (1...(⌊‘(√‘𝑁))) ∈ Fin
37		xpfi 9015	. . . . . . 7 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin)
38	29, 36, 37	mp2an 688	. . . . . 6 ⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin
39		fveqeq2 6765	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 / ((𝑄‘𝑦)↑2)) → ((𝑄‘𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1))
40		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ 𝑀)
41	3, 40	sselid 3915	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ (1...𝑁))
42		elfznn 13214	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
43	41, 42	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℕ)
44		prmreclem2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
45	44	prmreclem1 16545	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
46	45	simp2d 1141	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦)↑2) ∥ 𝑦)
47	43, 46	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∥ 𝑦)
48	45	simp1d 1140	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ → (𝑄‘𝑦) ∈ ℕ)
49	43, 48	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℕ)
50	49	nnsqcld 13887	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℕ)
51	50	nnzd 12354	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℤ)
52	50	nnne0d 11953	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≠ 0)
53	43	nnzd 12354	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℤ)
54		dvdsval2 15894	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ))
55	51, 52, 53, 54	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ))
56	47, 55	mpbid 231	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ)
57		nnre 11910	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
58		nngt0 11934	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
59	57, 58	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
60		nnre 11910	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → ((𝑄‘𝑦)↑2) ∈ ℝ)
61		nngt0 11934	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → 0 < ((𝑄‘𝑦)↑2))
62	60, 61	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2)))
63		divgt0 11773	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℝ ∧ 0 < 𝑦) ∧ (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2))) → 0 < (𝑦 / ((𝑄‘𝑦)↑2)))
64	59, 62, 63	syl2an 595	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∈ ℕ) → 0 < (𝑦 / ((𝑄‘𝑦)↑2)))
65	43, 50, 64	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 0 < (𝑦 / ((𝑄‘𝑦)↑2)))
66		elnnz 12259	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄‘𝑦)↑2))))
67	56, 65, 66	sylanbrc 582	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ)
68	67	nnred 11918	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℝ)
69	43	nnred 11918	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℝ)
70	16	nnred 11918	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ)
71	70	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℝ)
72		dvdsmul1 15915	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)))
73	56, 51, 72	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)))
74	43	nncnd 11919	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℂ)
75	50	nncnd 11919	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℂ)
76	74, 75, 52	divcan1d 11682	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦)
77	73, 76	breqtrd 5096	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦)
78		dvdsle 15947	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦))
79	56, 43, 78	syl2anc 583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦))
80	77, 79	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦)
81		elfzle2 13189	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ≤ 𝑁)
82	41, 81	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ≤ 𝑁)
83	68, 69, 71, 80, 82	letrd 11062	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁)
84		nnuz 12550	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
85	67, 84	eleqtrdi 2849	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ (ℤ_≥‘1))
86	16	nnzd 12354	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
87	86	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℤ)
88		elfz5 13177	. . . . . . . . . . . . 13 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁))
89	85, 87, 88	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁))
90	83, 89	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁))
91		breq2 5074	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦))
92	91	notbid 317	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦))
93	92	ralbidv 3120	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
94	93, 2	elrab2 3620	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
95	40, 94	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
96	95	simprd 495	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
97	77	adantr 480	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦)
98		eldifi 4057	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
99		prmz 16308	. . . . . . . . . . . . . . . . . 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 15931	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦))
105	101, 102, 103, 104	syl3anc 1369	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦))
106	97, 105	mpan2d 690	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) → 𝑝 ∥ 𝑦))
107	106	con3d 152	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝 ∥ 𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
108	107	ralimdva 3102	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
109	96, 108	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
110		breq2 5074	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
111	110	notbid 317	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
112	111	ralbidv 3120	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
113	112, 2	elrab2 3620	. . . . . . . . . . 11 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
114	90, 109, 113	sylanbrc 582	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀)
115	44	prmreclem1 16545	. . . . . . . . . . . . 13 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝐴 ∈ (ℤ_≥‘2) → ¬ (𝐴↑2) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2)))))
116	115	simp2d 1141	. . . . . . . . . . . 12 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
117	67, 116	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
118	115	simp1d 1140	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ)
119	67, 118	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ)
120		elnn1uz2 12594	. . . . . . . . . . . . . 14 ⊢ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
121	119, 120	sylib 217	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
122	121	ord 860	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
123	44	prmreclem1 16545	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
124	123	simp3d 1142	. . . . . . . . . . . 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 3619	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1})
128	50	nnred 11918	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℝ)
129		dvdsle 15947	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ 𝑦 ∈ ℕ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 → ((𝑄‘𝑦)↑2) ≤ 𝑦))
130	51, 43, 129	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 → ((𝑄‘𝑦)↑2) ≤ 𝑦))
131	47, 130	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑦)
132	128, 69, 71, 131, 82	letrd 11062	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑁)
133	71	recnd 10934	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℂ)
134	133	sqsqrtd 15079	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((√‘𝑁)↑2) = 𝑁)
135	132, 134	breqtrrd 5098	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))
136	49	nnrpd 12699	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℝ⁺)
137	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈ ℝ⁺)
138		rprege0 12674	. . . . . . . . . . . . . 14 ⊢ ((𝑄‘𝑦) ∈ ℝ⁺ → ((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦)))
139		rprege0 12674	. . . . . . . . . . . . . 14 ⊢ ((√‘𝑁) ∈ ℝ⁺ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
140		le2sq 13781	. . . . . . . . . . . . . 14 ⊢ ((((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦)) ∧ ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁))) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)))
141	138, 139, 140	syl2an 595	. . . . . . . . . . . . 13 ⊢ (((𝑄‘𝑦) ∈ ℝ⁺ ∧ (√‘𝑁) ∈ ℝ⁺) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)))
142	136, 137, 141	syl2anc 583	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)))
143	135, 142	mpbird 256	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (√‘𝑁))
144	25	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈ ℝ)
145	49	nnzd 12354	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℤ)
146		flge 13453	. . . . . . . . . . . 12 ⊢ (((√‘𝑁) ∈ ℝ ∧ (𝑄‘𝑦) ∈ ℤ) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
147	144, 145, 146	syl2anc 583	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
148	143, 147	mpbid 231	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))
149	49, 84	eleqtrdi 2849	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ (ℤ_≥‘1))
150	21	nn0zd 12353	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℤ)
151	150	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (⌊‘(√‘𝑁)) ∈ ℤ)
152		elfz5 13177	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑦) ∈ (ℤ_≥‘1) ∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
153	149, 151, 152	syl2anc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
154	148, 153	mpbird 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))))
155	127, 154	opelxpd 5618	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
156	155	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝑀 → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
157		ovex 7288	. . . . . . . . . . . 12 ⊢ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ V
158		fvex 6769	. . . . . . . . . . . 12 ⊢ (𝑄‘𝑦) ∈ V
159	157, 158	opth 5385	. . . . . . . . . . 11 ⊢ (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧)))
160		oveq1 7262	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑦) = (𝑄‘𝑧) → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2))
161		oveq12 7264	. . . . . . . . . . . 12 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)))
162	160, 161	sylan2 592	. . . . . . . . . . 11 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)))
163	159, 162	sylbi 216	. . . . . . . . . 10 ⊢ (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)))
164	76	adantrr 713	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦)
165		fz1ssnn 13216	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ⊆ ℕ
166	3, 165	sstri 3926	. . . . . . . . . . . . . 14 ⊢ 𝑀 ⊆ ℕ
167		simprr 769	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ 𝑀)
168	166, 167	sselid 3915	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℕ)
169	168	nncnd 11919	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℂ)
170	44	prmreclem1 16545	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ → ((𝑄‘𝑧) ∈ ℕ ∧ ((𝑄‘𝑧)↑2) ∥ 𝑧 ∧ (2 ∈ (ℤ_≥‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄‘𝑧)↑2)))))
171	170	simp1d 1140	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ → (𝑄‘𝑧) ∈ ℕ)
172	168, 171	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (𝑄‘𝑧) ∈ ℕ)
173	172	nnsqcld 13887	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℕ)
174	173	nncnd 11919	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℂ)
175	173	nnne0d 11953	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ≠ 0)
176	169, 174, 175	divcan1d 11682	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) = 𝑧)
177	164, 176	eqeq12d 2754	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) ↔ 𝑦 = 𝑧))
178	163, 177	syl5ib 243	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ → 𝑦 = 𝑧))
179		id 22	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
180		fveq2 6756	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑄‘𝑦) = (𝑄‘𝑧))
181	180	oveq1d 7270	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2))
182	179, 181	oveq12d 7273	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)))
183	182, 180	opeq12d 4809	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩)
184	178, 183	impbid1 224	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ 𝑦 = 𝑧))
185	184	ex 412	. . . . . . 7 ⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ 𝑦 = 𝑧)))
186	156, 185	dom2d 8736	. . . . . 6 ⊢ (𝜑 → (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
187	38, 186	mpi 20	. . . . 5 ⊢ (𝜑 → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
188		hashdom 14022	. . . . . 6 ⊢ ((𝑀 ∈ Fin ∧ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin) → ((♯‘𝑀) ≤ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
189	5, 38, 188	mp2an 688	. . . . 5 ⊢ ((♯‘𝑀) ≤ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
190	187, 189	sylibr 233	. . . 4 ⊢ (𝜑 → (♯‘𝑀) ≤ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
191		hashxp 14077	. . . . . 6 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))))
192	29, 36, 191	mp2an 688	. . . . 5 ⊢ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁)))))
193		hashfz1 13988	. . . . . . 7 ⊢ ((⌊‘(√‘𝑁)) ∈ ℕ₀ → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
194	21, 193	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
195	194	oveq2d 7271	. . . . 5 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
196	192, 195	eqtrid 2790	. . . 4 ⊢ (𝜑 → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
197	190, 196	breqtrd 5096	. . 3 ⊢ (𝜑 → (♯‘𝑀) ≤ ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
198	32	a1i 11	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ)
199	21	nn0ge0d 12226	. . . 4 ⊢ (𝜑 → 0 ≤ (⌊‘(√‘𝑁)))
200		prmrec.1	. . . . 5 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
201	200, 11, 16, 2, 44	prmreclem2 16546	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))
202	198, 24, 33, 199, 201	lemul1ad 11844	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
203	9, 35, 23, 197, 202	letrd 11062	. 2 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
204	14	nnrpd 12699	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ⁺)
205	204	rprege0d 12708	. . 3 ⊢ (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾)))
206		fllelt 13445	. . . . 5 ⊢ ((√‘𝑁) ∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
207	25, 206	syl 17	. . . 4 ⊢ (𝜑 → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
208	207	simpld 494	. . 3 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ≤ (√‘𝑁))
209		lemul2a 11760	. . 3 ⊢ ((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧ ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) ∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
210	33, 25, 205, 208, 209	syl31anc 1371	. 2 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
211	9, 23, 26, 203, 210	letrd 11062	1 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∨ wo 843 = wceq 1539 ∈ wcel 2108 ≠ wne 2942 ∀wral 3063 {crab 3067 ∖ cdif 3880 ⊆ wss 3883 ifcif 4456 ⟨cop 4564 class class class wbr 5070 ↦ cmpt 5153 × cxp 5578 ‘cfv 6418 (class class class)co 7255 ≼ cdom 8689 Fincfn 8691 supcsup 9129 ℝcr 10801 0cc0 10802 1c1 10803 + caddc 10805 · cmul 10807 < clt 10940 ≤ cle 10941 / cdiv 11562 ℕcn 11903 2c2 11958 ℕ₀cn0 12163 ℤcz 12249 ℤ_≥cuz 12511 ℝ⁺crp 12659 ...cfz 13168 ⌊cfl 13438 ↑cexp 13710 ♯chash 13972 √csqrt 14872 ∥ cdvds 15891 ℙcprime 16304

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1799 ax-4 1813 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2156 ax-12 2173 ax-ext 2709 ax-rep 5205 ax-sep 5218 ax-nul 5225 ax-pow 5283 ax-pr 5347 ax-un 7566 ax-cnex 10858 ax-resscn 10859 ax-1cn 10860 ax-icn 10861 ax-addcl 10862 ax-addrcl 10863 ax-mulcl 10864 ax-mulrcl 10865 ax-mulcom 10866 ax-addass 10867 ax-mulass 10868 ax-distr 10869 ax-i2m1 10870 ax-1ne0 10871 ax-1rid 10872 ax-rnegex 10873 ax-rrecex 10874 ax-cnre 10875 ax-pre-lttri 10876 ax-pre-lttrn 10877 ax-pre-ltadd 10878 ax-pre-mulgt0 10879 ax-pre-sup 10880

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1784 df-nf 1788 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2817 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3068 df-rex 3069 df-reu 3070 df-rmo 3071 df-rab 3072 df-v 3424 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4254 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-br 5071 df-opab 5133 df-mpt 5154 df-tr 5188 df-id 5480 df-eprel 5486 df-po 5494 df-so 5495 df-fr 5535 df-we 5537 df-xp 5586 df-rel 5587 df-cnv 5588 df-co 5589 df-dm 5590 df-rn 5591 df-res 5592 df-ima 5593 df-pred 6191 df-ord 6254 df-on 6255 df-lim 6256 df-suc 6257 df-iota 6376 df-fun 6420 df-fn 6421 df-f 6422 df-f1 6423 df-fo 6424 df-f1o 6425 df-fv 6426 df-riota 7212 df-ov 7258 df-oprab 7259 df-mpo 7260 df-om 7688 df-1st 7804 df-2nd 7805 df-frecs 8068 df-wrecs 8099 df-recs 8173 df-rdg 8212 df-1o 8267 df-2o 8268 df-oadd 8271 df-er 8456 df-map 8575 df-pm 8576 df-en 8692 df-dom 8693 df-sdom 8694 df-fin 8695 df-sup 9131 df-inf 9132 df-dju 9590 df-card 9628 df-pnf 10942 df-mnf 10943 df-xr 10944 df-ltxr 10945 df-le 10946 df-sub 11137 df-neg 11138 df-div 11563 df-nn 11904 df-2 11966 df-3 11967 df-n0 12164 df-xnn0 12236 df-z 12250 df-uz 12512 df-q 12618 df-rp 12660 df-fz 13169 df-fl 13440 df-mod 13518 df-seq 13650 df-exp 13711 df-hash 13973 df-cj 14738 df-re 14739 df-im 14740 df-sqrt 14874 df-abs 14875 df-dvds 15892 df-gcd 16130 df-prm 16305 df-pc 16466

This theorem is referenced by: prmreclem5 16549

W3C validator