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 16956

Description: Lemma for prmrec 16960. 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 14013	. . . . . 6 ⊢ (1...𝑁) ∈ Fin
2		prmrec.4	. . . . . . 7 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
3	2	ssrab3 4082	. . . . . 6 ⊢ 𝑀 ⊆ (1...𝑁)
4		ssfi 9213	. . . . . 6 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
5	1, 3, 4	mp2an 692	. . . . 5 ⊢ 𝑀 ∈ Fin
6		hashcl 14395	. . . . 5 ⊢ (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ₀)
7	5, 6	ax-mp 5	. . . 4 ⊢ (♯‘𝑀) ∈ ℕ₀
8	7	nn0rei 12537	. . 3 ⊢ (♯‘𝑀) ∈ ℝ
9	8	a1i 11	. 2 ⊢ (𝜑 → (♯‘𝑀) ∈ ℝ)
10		2nn 12339	. . . . . 6 ⊢ 2 ∈ ℕ
11		prmrec.2	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ)
12	11	nnnn0d 12587	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
13		nnexpcl 14115	. . . . . 6 ⊢ ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ₀) → (2↑𝐾) ∈ ℕ)
14	10, 12, 13	sylancr 587	. . . . 5 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ)
15	14	nnnn0d 12587	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ₀)
16		prmrec.3	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
17	16	nnrpd 13075	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
18	17	rpsqrtcld 15450	. . . . . 6 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
19	18	rprege0d 13084	. . . . 5 ⊢ (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
20		flge0nn0 13860	. . . . 5 ⊢ (((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)) → (⌊‘(√‘𝑁)) ∈ ℕ₀)
21	19, 20	syl 17	. . . 4 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℕ₀)
22	15, 21	nn0mulcld 12592	. . 3 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℕ₀)
23	22	nn0red 12588	. 2 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℝ)
24	14	nnred 12281	. . 3 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ)
25	18	rpred 13077	. . 3 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
26	24, 25	remulcld 11291	. 2 ⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
27		ssrab2 4080	. . . . . . 7 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀
28		ssfi 9213	. . . . . . 7 ⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin)
29	5, 27, 28	mp2an 692	. . . . . 6 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin
30		hashcl 14395	. . . . . 6 ⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℕ₀)
31	29, 30	ax-mp 5	. . . . 5 ⊢ (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℕ₀
32	31	nn0rei 12537	. . . 4 ⊢ (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ
33	21	nn0red 12588	. . . 4 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℝ)
34		remulcl 11240	. . . 4 ⊢ (((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ ∧ (⌊‘(√‘𝑁)) ∈ ℝ) → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
35	32, 33, 34	sylancr 587	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
36		fzfi 14013	. . . . . . 7 ⊢ (1...(⌊‘(√‘𝑁))) ∈ Fin
37		xpfi 9358	. . . . . . 7 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin)
38	29, 36, 37	mp2an 692	. . . . . 6 ⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin
39		fveqeq2 6915	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 / ((𝑄‘𝑦)↑2)) → ((𝑄‘𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1))
40		simpr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ 𝑀)
41	3, 40	sselid 3981	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ (1...𝑁))
42		elfznn 13593	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
43	41, 42	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℕ)
44		prmreclem2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
45	44	prmreclem1 16954	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
46	45	simp2d 1144	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦)↑2) ∥ 𝑦)
47	43, 46	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∥ 𝑦)
48	45	simp1d 1143	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ → (𝑄‘𝑦) ∈ ℕ)
49	43, 48	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℕ)
50	49	nnsqcld 14283	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℕ)
51	50	nnzd 12640	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℤ)
52	50	nnne0d 12316	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≠ 0)
53	43	nnzd 12640	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℤ)
54		dvdsval2 16293	. . . . . . . . . . . . . . . . 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 12273	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
58		nngt0 12297	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
59	57, 58	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
60		nnre 12273	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → ((𝑄‘𝑦)↑2) ∈ ℝ)
61		nngt0 12297	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → 0 < ((𝑄‘𝑦)↑2))
62	60, 61	jca 511	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2)))
63		divgt0 12136	. . . . . . . . . . . . . . . . 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 12623	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄‘𝑦)↑2))))
67	56, 65, 66	sylanbrc 583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ)
68	67	nnred 12281	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℝ)
69	43	nnred 12281	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℝ)
70	16	nnred 12281	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ)
71	70	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℝ)
72		dvdsmul1 16315	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)))
73	56, 51, 72	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)))
74	43	nncnd 12282	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℂ)
75	50	nncnd 12282	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℂ)
76	74, 75, 52	divcan1d 12044	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦)
77	73, 76	breqtrd 5169	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦)
78		dvdsle 16347	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦))
79	56, 43, 78	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦))
80	77, 79	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦)
81		elfzle2 13568	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ≤ 𝑁)
82	41, 81	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ≤ 𝑁)
83	68, 69, 71, 80, 82	letrd 11418	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁)
84		nnuz 12921	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
85	67, 84	eleqtrdi 2851	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ (ℤ_≥‘1))
86	16	nnzd 12640	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
87	86	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℤ)
88		elfz5 13556	. . . . . . . . . . . . 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 5147	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦))
92	91	notbid 318	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦))
93	92	ralbidv 3178	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
94	93, 2	elrab2 3695	. . . . . . . . . . . . . 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 4131	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
99		prmz 16712	. . . . . . . . . . . . . . . . . 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 16331	. . . . . . . . . . . . . . . 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 3167	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
109	96, 108	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
110		breq2 5147	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
111	110	notbid 318	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
112	111	ralbidv 3178	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
113	112, 2	elrab2 3695	. . . . . . . . . . 11 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
114	90, 109, 113	sylanbrc 583	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀)
115	44	prmreclem1 16954	. . . . . . . . . . . . 13 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝐴 ∈ (ℤ_≥‘2) → ¬ (𝐴↑2) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2)))))
116	115	simp2d 1144	. . . . . . . . . . . 12 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
117	67, 116	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
118	115	simp1d 1143	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ)
119	67, 118	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ)
120		elnn1uz2 12967	. . . . . . . . . . . . . 14 ⊢ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
121	119, 120	sylib 218	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
122	121	ord 865	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
123	44	prmreclem1 16954	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
124	123	simp3d 1145	. . . . . . . . . . . 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 3694	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1})
128	50	nnred 12281	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℝ)
129		dvdsle 16347	. . . . . . . . . . . . . . . 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 11418	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑁)
133	71	recnd 11289	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℂ)
134	133	sqsqrtd 15478	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((√‘𝑁)↑2) = 𝑁)
135	132, 134	breqtrrd 5171	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))
136	49	nnrpd 13075	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℝ⁺)
137	18	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈ ℝ⁺)
138		rprege0 13050	. . . . . . . . . . . . . 14 ⊢ ((𝑄‘𝑦) ∈ ℝ⁺ → ((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦)))
139		rprege0 13050	. . . . . . . . . . . . . 14 ⊢ ((√‘𝑁) ∈ ℝ⁺ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
140		le2sq 14174	. . . . . . . . . . . . . 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 12640	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℤ)
146		flge 13845	. . . . . . . . . . . 12 ⊢ (((√‘𝑁) ∈ ℝ ∧ (𝑄‘𝑦) ∈ ℤ) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
147	144, 145, 146	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
148	143, 147	mpbid 232	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))
149	49, 84	eleqtrdi 2851	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ (ℤ_≥‘1))
150	21	nn0zd 12639	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℤ)
151	150	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (⌊‘(√‘𝑁)) ∈ ℤ)
152		elfz5 13556	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑦) ∈ (ℤ_≥‘1) ∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
153	149, 151, 152	syl2anc 584	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
154	148, 153	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))))
155	127, 154	opelxpd 5724	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
156	155	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝑀 → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
157		ovex 7464	. . . . . . . . . . . 12 ⊢ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ V
158		fvex 6919	. . . . . . . . . . . 12 ⊢ (𝑄‘𝑦) ∈ V
159	157, 158	opth 5481	. . . . . . . . . . 11 ⊢ (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧)))
160		oveq1 7438	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑦) = (𝑄‘𝑧) → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2))
161		oveq12 7440	. . . . . . . . . . . 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 13595	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ⊆ ℕ
166	3, 165	sstri 3993	. . . . . . . . . . . . . 14 ⊢ 𝑀 ⊆ ℕ
167		simprr 773	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ 𝑀)
168	166, 167	sselid 3981	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℕ)
169	168	nncnd 12282	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℂ)
170	44	prmreclem1 16954	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ → ((𝑄‘𝑧) ∈ ℕ ∧ ((𝑄‘𝑧)↑2) ∥ 𝑧 ∧ (2 ∈ (ℤ_≥‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄‘𝑧)↑2)))))
171	170	simp1d 1143	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ → (𝑄‘𝑧) ∈ ℕ)
172	168, 171	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (𝑄‘𝑧) ∈ ℕ)
173	172	nnsqcld 14283	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℕ)
174	173	nncnd 12282	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℂ)
175	173	nnne0d 12316	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ≠ 0)
176	169, 174, 175	divcan1d 12044	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) = 𝑧)
177	164, 176	eqeq12d 2753	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) ↔ 𝑦 = 𝑧))
178	163, 177	imbitrid 244	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ → 𝑦 = 𝑧))
179		id 22	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
180		fveq2 6906	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑄‘𝑦) = (𝑄‘𝑧))
181	180	oveq1d 7446	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2))
182	179, 181	oveq12d 7449	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)))
183	182, 180	opeq12d 4881	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩)
184	178, 183	impbid1 225	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ 𝑦 = 𝑧))
185	184	ex 412	. . . . . . 7 ⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ 𝑦 = 𝑧)))
186	156, 185	dom2d 9033	. . . . . 6 ⊢ (𝜑 → (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
187	38, 186	mpi 20	. . . . 5 ⊢ (𝜑 → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
188		hashdom 14418	. . . . . 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 14473	. . . . . 6 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))))
192	29, 36, 191	mp2an 692	. . . . 5 ⊢ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁)))))
193		hashfz1 14385	. . . . . . 7 ⊢ ((⌊‘(√‘𝑁)) ∈ ℕ₀ → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
194	21, 193	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
195	194	oveq2d 7447	. . . . 5 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
196	192, 195	eqtrid 2789	. . . 4 ⊢ (𝜑 → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
197	190, 196	breqtrd 5169	. . 3 ⊢ (𝜑 → (♯‘𝑀) ≤ ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
198	32	a1i 11	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ)
199	21	nn0ge0d 12590	. . . 4 ⊢ (𝜑 → 0 ≤ (⌊‘(√‘𝑁)))
200		prmrec.1	. . . . 5 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
201	200, 11, 16, 2, 44	prmreclem2 16955	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))
202	198, 24, 33, 199, 201	lemul1ad 12207	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
203	9, 35, 23, 197, 202	letrd 11418	. 2 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
204	14	nnrpd 13075	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ⁺)
205	204	rprege0d 13084	. . 3 ⊢ (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾)))
206		fllelt 13837	. . . . 5 ⊢ ((√‘𝑁) ∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
207	25, 206	syl 17	. . . 4 ⊢ (𝜑 → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
208	207	simpld 494	. . 3 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ≤ (√‘𝑁))
209		lemul2a 12122	. . 3 ⊢ ((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧ ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) ∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
210	33, 25, 205, 208, 209	syl31anc 1375	. 2 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
211	9, 23, 26, 203, 210	letrd 11418	1 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 {crab 3436 ∖ cdif 3948 ⊆ wss 3951 ifcif 4525 ⟨cop 4632 class class class wbr 5143 ↦ cmpt 5225 × cxp 5683 ‘cfv 6561 (class class class)co 7431 ≼ cdom 8983 Fincfn 8985 supcsup 9480 ℝcr 11154 0cc0 11155 1c1 11156 + caddc 11158 · cmul 11160 < clt 11295 ≤ cle 11296 / cdiv 11920 ℕcn 12266 2c2 12321 ℕ₀cn0 12526 ℤcz 12613 ℤ_≥cuz 12878 ℝ⁺crp 13034 ...cfz 13547 ⌊cfl 13830 ↑cexp 14102 ♯chash 14369 √csqrt 15272 ∥ cdvds 16290 ℙcprime 16708

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232 ax-pre-sup 11233

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-oadd 8510 df-er 8745 df-map 8868 df-pm 8869 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-sup 9482 df-inf 9483 df-dju 9941 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-div 11921 df-nn 12267 df-2 12329 df-3 12330 df-n0 12527 df-xnn0 12600 df-z 12614 df-uz 12879 df-q 12991 df-rp 13035 df-fz 13548 df-fl 13832 df-mod 13910 df-seq 14043 df-exp 14103 df-hash 14370 df-cj 15138 df-re 15139 df-im 15140 df-sqrt 15274 df-abs 15275 df-dvds 16291 df-gcd 16532 df-prm 16709 df-pc 16875

This theorem is referenced by: prmreclem5 16958

W3C validator