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 16945

Description: Lemma for prmrec 16949. 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 13979	. . . . . 6 ⊢ (1...𝑁) ∈ Fin
2		prmrec.4	. . . . . . 7 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
3	2	ssrab3 4033	. . . . . 6 ⊢ 𝑀 ⊆ (1...𝑁)
4		ssfi 9135	. . . . . 6 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
5	1, 3, 4	mp2an 702	. . . . 5 ⊢ 𝑀 ∈ Fin
6		hashcl 14363	. . . . 5 ⊢ (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ₀)
7	5, 6	ax-mp 5	. . . 4 ⊢ (♯‘𝑀) ∈ ℕ₀
8	7	nn0rei 12486	. . 3 ⊢ (♯‘𝑀) ∈ ℝ
9	8	a1i 11	. 2 ⊢ (𝜑 → (♯‘𝑀) ∈ ℝ)
10		2nn 12285	. . . . . 6 ⊢ 2 ∈ ℕ
11		prmrec.2	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ)
12	11	nnnn0d 12536	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
13		nnexpcl 14081	. . . . . 6 ⊢ ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ₀) → (2↑𝐾) ∈ ℕ)
14	10, 12, 13	sylancr 596	. . . . 5 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ)
15	14	nnnn0d 12536	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ₀)
16		prmrec.3	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
17	16	nnrpd 13029	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
18	17	rpsqrtcld 15430	. . . . . 6 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
19	18	rprege0d 13038	. . . . 5 ⊢ (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
20		flge0nn0 13824	. . . . 5 ⊢ (((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)) → (⌊‘(√‘𝑁)) ∈ ℕ₀)
21	19, 20	syl 17	. . . 4 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℕ₀)
22	15, 21	nn0mulcld 12541	. . 3 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℕ₀)
23	22	nn0red 12537	. 2 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℝ)
24	14	nnred 12219	. . 3 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ)
25	18	rpred 13031	. . 3 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
26	24, 25	remulcld 11206	. 2 ⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
27		ssrab2 4031	. . . . . . 7 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀
28		ssfi 9135	. . . . . . 7 ⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin)
29	5, 27, 28	mp2an 702	. . . . . 6 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin
30		hashcl 14363	. . . . . 6 ⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℕ₀)
31	29, 30	ax-mp 5	. . . . 5 ⊢ (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℕ₀
32	31	nn0rei 12486	. . . 4 ⊢ (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ
33	21	nn0red 12537	. . . 4 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℝ)
34		remulcl 11152	. . . 4 ⊢ (((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ ∧ (⌊‘(√‘𝑁)) ∈ ℝ) → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
35	32, 33, 34	sylancr 596	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
36		fzfi 13979	. . . . . . 7 ⊢ (1...(⌊‘(√‘𝑁))) ∈ Fin
37		xpfi 9258	. . . . . . 7 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin)
38	29, 36, 37	mp2an 702	. . . . . 6 ⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin
39		fveqeq2 6871	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 / ((𝑄‘𝑦)↑2)) → ((𝑄‘𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1))
40		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ 𝑀)
41	3, 40	sselid 3932	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ (1...𝑁))
42		elfznn 13552	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
43	41, 42	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℕ)
44		prmreclem2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
45	44	prmreclem1 16943	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
46	45	simp2d 1155	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦)↑2) ∥ 𝑦)
47	43, 46	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∥ 𝑦)
48	45	simp1d 1154	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ → (𝑄‘𝑦) ∈ ℕ)
49	43, 48	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℕ)
50	49	nnsqcld 14251	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℕ)
51	50	nnzd 12588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℤ)
52	50	nnne0d 12257	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≠ 0)
53	43	nnzd 12588	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℤ)
54		dvdsval2 16280	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ))
55	51, 52, 53, 54	syl3anc 1389	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ))
56	47, 55	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ)
57		nnre 12211	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
58		nngt0 12238	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
59	57, 58	jca 519	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
60		nnre 12211	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → ((𝑄‘𝑦)↑2) ∈ ℝ)
61		nngt0 12238	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → 0 < ((𝑄‘𝑦)↑2))
62	60, 61	jca 519	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2)))
63		divgt0 12054	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑦 ∈ ℝ ∧ 0 < 𝑦) ∧ (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2))) → 0 < (𝑦 / ((𝑄‘𝑦)↑2)))
64	59, 62, 63	syl2an 605	. . . . . . . . . . . . . . . 16 ⊢ ((𝑦 ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∈ ℕ) → 0 < (𝑦 / ((𝑄‘𝑦)↑2)))
65	43, 50, 64	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 0 < (𝑦 / ((𝑄‘𝑦)↑2)))
66		elnnz 12572	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄‘𝑦)↑2))))
67	56, 65, 66	sylanbrc 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ)
68	67	nnred 12219	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℝ)
69	43	nnred 12219	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℝ)
70	16	nnred 12219	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ)
71	70	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℝ)
72		dvdsmul1 16302	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)))
73	56, 51, 72	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)))
74	43	nncnd 12220	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℂ)
75	50	nncnd 12220	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℂ)
76	74, 75, 52	divcan1d 11962	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦)
77	73, 76	breqtrd 5123	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦)
78		dvdsle 16335	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦))
79	56, 43, 78	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦))
80	77, 79	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦)
81		elfzle2 13527	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ≤ 𝑁)
82	41, 81	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ≤ 𝑁)
83	68, 69, 71, 80, 82	letrd 11334	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁)
84		nnuz 12872	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
85	67, 84	eleqtrdi 2871	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ (ℤ_≥‘1))
86	16	nnzd 12588	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
87	86	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℤ)
88		elfz5 13515	. . . . . . . . . . . . 13 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (ℤ_≥‘1) ∧ 𝑁 ∈ ℤ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁))
89	85, 87, 88	syl2anc 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁))
90	83, 89	mpbird 259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁))
91		breq2 5101	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦))
92	91	notbid 320	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦))
93	92	ralbidv 3184	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
94	93, 2	elrab2 3652	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ 𝑀 ↔ (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
95	40, 94	sylib 220	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
96	95	simprd 499	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦)
97	77	adantr 484	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦)
98		eldifi 4082	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
99		prmz 16700	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℙ → 𝑝 ∈ ℤ)
100	98, 99	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℤ)
101	100	adantl 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑝 ∈ ℤ)
102	56	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ)
103	53	adantr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → 𝑦 ∈ ℤ)
104		dvdstr 16319	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦))
105	101, 102, 103, 104	syl3anc 1389	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦))
106	97, 105	mpan2d 704	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) → 𝑝 ∥ 𝑦))
107	106	con3d 152	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝 ∥ 𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
108	107	ralimdva 3173	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
109	96, 108	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
110		breq2 5101	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
111	110	notbid 320	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
112	111	ralbidv 3184	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
113	112, 2	elrab2 3652	. . . . . . . . . . 11 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
114	90, 109, 113	sylanbrc 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀)
115	44	prmreclem1 16943	. . . . . . . . . . . . 13 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝐴 ∈ (ℤ_≥‘2) → ¬ (𝐴↑2) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2)))))
116	115	simp2d 1155	. . . . . . . . . . . 12 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
117	67, 116	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
118	115	simp1d 1154	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ)
119	67, 118	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ)
120		elnn1uz2 12920	. . . . . . . . . . . . . 14 ⊢ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ↔ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
121	119, 120	sylib 220	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 ∨ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
122	121	ord 875	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (¬ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1 → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2)))
123	44	prmreclem1 16943	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
124	123	simp3d 1156	. . . . . . . . . . . 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 3651	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1})
128	50	nnred 12219	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℝ)
129		dvdsle 16335	. . . . . . . . . . . . . . . 16 ⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ 𝑦 ∈ ℕ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 → ((𝑄‘𝑦)↑2) ≤ 𝑦))
130	51, 43, 129	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 → ((𝑄‘𝑦)↑2) ≤ 𝑦))
131	47, 130	mpd 15	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑦)
132	128, 69, 71, 131, 82	letrd 11334	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑁)
133	71	recnd 11204	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℂ)
134	133	sqsqrtd 15460	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((√‘𝑁)↑2) = 𝑁)
135	132, 134	breqtrrd 5125	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))
136	49	nnrpd 13029	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℝ⁺)
137	18	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈ ℝ⁺)
138		rprege0 13003	. . . . . . . . . . . . . 14 ⊢ ((𝑄‘𝑦) ∈ ℝ⁺ → ((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦)))
139		rprege0 13003	. . . . . . . . . . . . . 14 ⊢ ((√‘𝑁) ∈ ℝ⁺ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
140		le2sq 14141	. . . . . . . . . . . . . 14 ⊢ ((((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦)) ∧ ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁))) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)))
141	138, 139, 140	syl2an 605	. . . . . . . . . . . . 13 ⊢ (((𝑄‘𝑦) ∈ ℝ⁺ ∧ (√‘𝑁) ∈ ℝ⁺) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)))
142	136, 137, 141	syl2anc 593	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2)))
143	135, 142	mpbird 259	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (√‘𝑁))
144	25	adantr 484	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈ ℝ)
145	49	nnzd 12588	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℤ)
146		flge 13809	. . . . . . . . . . . 12 ⊢ (((√‘𝑁) ∈ ℝ ∧ (𝑄‘𝑦) ∈ ℤ) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
147	144, 145, 146	syl2anc 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
148	143, 147	mpbid 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))
149	49, 84	eleqtrdi 2871	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ (ℤ_≥‘1))
150	21	nn0zd 12587	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℤ)
151	150	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (⌊‘(√‘𝑁)) ∈ ℤ)
152		elfz5 13515	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑦) ∈ (ℤ_≥‘1) ∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
153	149, 151, 152	syl2anc 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
154	148, 153	mpbird 259	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))))
155	127, 154	opelxpd 5682	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
156	155	ex 416	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝑀 → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
157		ovex 7424	. . . . . . . . . . . 12 ⊢ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ V
158		fvex 6875	. . . . . . . . . . . 12 ⊢ (𝑄‘𝑦) ∈ V
159	157, 158	opth 5441	. . . . . . . . . . 11 ⊢ (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧)))
160		oveq1 7398	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑦) = (𝑄‘𝑧) → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2))
161		oveq12 7400	. . . . . . . . . . . 12 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)))
162	160, 161	sylan2 602	. . . . . . . . . . 11 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)))
163	159, 162	sylbi 219	. . . . . . . . . 10 ⊢ (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)))
164	76	adantrr 727	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦)
165		fz1ssnn 13554	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ⊆ ℕ
166	3, 165	sstri 3943	. . . . . . . . . . . . . 14 ⊢ 𝑀 ⊆ ℕ
167		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ 𝑀)
168	166, 167	sselid 3932	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℕ)
169	168	nncnd 12220	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℂ)
170	44	prmreclem1 16943	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ → ((𝑄‘𝑧) ∈ ℕ ∧ ((𝑄‘𝑧)↑2) ∥ 𝑧 ∧ (2 ∈ (ℤ_≥‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄‘𝑧)↑2)))))
171	170	simp1d 1154	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ → (𝑄‘𝑧) ∈ ℕ)
172	168, 171	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (𝑄‘𝑧) ∈ ℕ)
173	172	nnsqcld 14251	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℕ)
174	173	nncnd 12220	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℂ)
175	173	nnne0d 12257	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ≠ 0)
176	169, 174, 175	divcan1d 11962	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) = 𝑧)
177	164, 176	eqeq12d 2777	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) ↔ 𝑦 = 𝑧))
178	163, 177	imbitrid 246	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ → 𝑦 = 𝑧))
179		id 22	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
180		fveq2 6862	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑄‘𝑦) = (𝑄‘𝑧))
181	180	oveq1d 7406	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2))
182	179, 181	oveq12d 7409	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)))
183	182, 180	opeq12d 4836	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩)
184	178, 183	impbid1 227	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ 𝑦 = 𝑧))
185	184	ex 416	. . . . . . 7 ⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ 𝑦 = 𝑧)))
186	156, 185	dom2d 8968	. . . . . 6 ⊢ (𝜑 → (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
187	38, 186	mpi 20	. . . . 5 ⊢ (𝜑 → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
188		hashdom 14386	. . . . . 6 ⊢ ((𝑀 ∈ Fin ∧ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin) → ((♯‘𝑀) ≤ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
189	5, 38, 188	mp2an 702	. . . . 5 ⊢ ((♯‘𝑀) ≤ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) ↔ 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
190	187, 189	sylibr 236	. . . 4 ⊢ (𝜑 → (♯‘𝑀) ≤ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
191		hashxp 14441	. . . . . 6 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))))
192	29, 36, 191	mp2an 702	. . . . 5 ⊢ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁)))))
193		hashfz1 14353	. . . . . . 7 ⊢ ((⌊‘(√‘𝑁)) ∈ ℕ₀ → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
194	21, 193	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
195	194	oveq2d 7407	. . . . 5 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
196	192, 195	eqtrid 2808	. . . 4 ⊢ (𝜑 → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
197	190, 196	breqtrd 5123	. . 3 ⊢ (𝜑 → (♯‘𝑀) ≤ ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
198	32	a1i 11	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ)
199	21	nn0ge0d 12539	. . . 4 ⊢ (𝜑 → 0 ≤ (⌊‘(√‘𝑁)))
200		prmrec.1	. . . . 5 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
201	200, 11, 16, 2, 44	prmreclem2 16944	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))
202	198, 24, 33, 199, 201	lemul1ad 12125	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
203	9, 35, 23, 197, 202	letrd 11334	. 2 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
204	14	nnrpd 13029	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ⁺)
205	204	rprege0d 13038	. . 3 ⊢ (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾)))
206		fllelt 13801	. . . . 5 ⊢ ((√‘𝑁) ∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
207	25, 206	syl 17	. . . 4 ⊢ (𝜑 → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
208	207	simpld 498	. . 3 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ≤ (√‘𝑁))
209		lemul2a 12040	. . 3 ⊢ ((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧ ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) ∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
210	33, 25, 205, 208, 209	syl31anc 1391	. 2 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
211	9, 23, 26, 203, 210	letrd 11334	1 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∀wral 3075 {crab 3413 ∖ cdif 3899 ⊆ wss 3902 ifcif 4477 ⟨cop 4585 class class class wbr 5097 ↦ cmpt 5178 × cxp 5641 ‘cfv 6516 (class class class)co 7391 ≼ cdom 8919 Fincfn 8921 supcsup 9380 ℝcr 11066 0cc0 11067 1c1 11068 + caddc 11070 · cmul 11072 < clt 11210 ≤ cle 11211 / cdiv 11838 ℕcn 12204 2c2 12266 ℕ₀cn0 12475 ℤcz 12562 ℤ_≥cuz 12833 ℝ⁺crp 12987 ...cfz 13506 ⌊cfl 13794 ↑cexp 14068 ♯chash 14337 √csqrt 15251 ∥ cdvds 16277 ℙcprime 16696

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-pre-sup 11145

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-om 7842 df-1st 7965 df-2nd 7966 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-2o 8432 df-oadd 8435 df-er 8672 df-map 8804 df-pm 8805 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-sup 9382 df-inf 9383 df-dju 9853 df-card 9891 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-div 11839 df-nn 12205 df-2 12274 df-3 12275 df-n0 12476 df-xnn0 12549 df-z 12563 df-uz 12834 df-q 12944 df-rp 12988 df-fz 13507 df-fl 13796 df-mod 13874 df-seq 14009 df-exp 14069 df-hash 14338 df-cj 15117 df-re 15118 df-im 15119 df-sqrt 15253 df-abs 15254 df-dvds 16278 df-gcd 16520 df-prm 16697 df-pc 16864

This theorem is referenced by: prmreclem5 16947

W3C validator