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 16954

Description: Lemma for prmrec 16958. 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 13985	. . . . . 6 ⊢ (1...𝑁) ∈ Fin
2		prmrec.4	. . . . . . 7 ⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛}
3	2	ssrab3 4035	. . . . . 6 ⊢ 𝑀 ⊆ (1...𝑁)
4		ssfi 9141	. . . . . 6 ⊢ (((1...𝑁) ∈ Fin ∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin)
5	1, 3, 4	mp2an 702	. . . . 5 ⊢ 𝑀 ∈ Fin
6		hashcl 14369	. . . . 5 ⊢ (𝑀 ∈ Fin → (♯‘𝑀) ∈ ℕ₀)
7	5, 6	ax-mp 5	. . . 4 ⊢ (♯‘𝑀) ∈ ℕ₀
8	7	nn0rei 12492	. . 3 ⊢ (♯‘𝑀) ∈ ℝ
9	8	a1i 11	. 2 ⊢ (𝜑 → (♯‘𝑀) ∈ ℝ)
10		2nn 12291	. . . . . 6 ⊢ 2 ∈ ℕ
11		prmrec.2	. . . . . . 7 ⊢ (𝜑 → 𝐾 ∈ ℕ)
12	11	nnnn0d 12542	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ ℕ₀)
13		nnexpcl 14087	. . . . . 6 ⊢ ((2 ∈ ℕ ∧ 𝐾 ∈ ℕ₀) → (2↑𝐾) ∈ ℕ)
14	10, 12, 13	sylancr 596	. . . . 5 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ)
15	14	nnnn0d 12542	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℕ₀)
16		prmrec.3	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℕ)
17	16	nnrpd 13035	. . . . . . 7 ⊢ (𝜑 → 𝑁 ∈ ℝ⁺)
18	17	rpsqrtcld 15439	. . . . . 6 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ⁺)
19	18	rprege0d 13044	. . . . 5 ⊢ (𝜑 → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
20		flge0nn0 13830	. . . . 5 ⊢ (((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)) → (⌊‘(√‘𝑁)) ∈ ℕ₀)
21	19, 20	syl 17	. . . 4 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℕ₀)
22	15, 21	nn0mulcld 12547	. . 3 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℕ₀)
23	22	nn0red 12543	. 2 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ∈ ℝ)
24	14	nnred 12225	. . 3 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ)
25	18	rpred 13037	. . 3 ⊢ (𝜑 → (√‘𝑁) ∈ ℝ)
26	24, 25	remulcld 11212	. 2 ⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ)
27		ssrab2 4033	. . . . . . 7 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀
28		ssfi 9141	. . . . . . 7 ⊢ ((𝑀 ∈ Fin ∧ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ⊆ 𝑀) → {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin)
29	5, 27, 28	mp2an 702	. . . . . 6 ⊢ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin
30		hashcl 14369	. . . . . 6 ⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℕ₀)
31	29, 30	ax-mp 5	. . . . 5 ⊢ (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℕ₀
32	31	nn0rei 12492	. . . 4 ⊢ (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ
33	21	nn0red 12543	. . . 4 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℝ)
34		remulcl 11158	. . . 4 ⊢ (((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ ∧ (⌊‘(√‘𝑁)) ∈ ℝ) → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
35	32, 33, 34	sylancr 596	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ∈ ℝ)
36		fzfi 13985	. . . . . . 7 ⊢ (1...(⌊‘(√‘𝑁))) ∈ Fin
37		xpfi 9264	. . . . . . 7 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin)
38	29, 36, 37	mp2an 702	. . . . . 6 ⊢ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin
39		fveqeq2 6876	. . . . . . . . . 10 ⊢ (𝑥 = (𝑦 / ((𝑄‘𝑦)↑2)) → ((𝑄‘𝑥) = 1 ↔ (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) = 1))
40		simpr 488	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ 𝑀)
41	3, 40	sselid 3934	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ (1...𝑁))
42		elfznn 13558	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ∈ ℕ)
43	41, 42	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℕ)
44		prmreclem2.5	. . . . . . . . . . . . . . . . . . 19 ⊢ 𝑄 = (𝑛 ∈ ℕ ↦ sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < ))
45	44	prmreclem1 16952	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ (𝑛 ∈ (ℤ_≥‘2) → ¬ (𝑛↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
46	45	simp2d 1156	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦)↑2) ∥ 𝑦)
47	43, 46	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∥ 𝑦)
48	45	simp1d 1155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ ℕ → (𝑄‘𝑦) ∈ ℕ)
49	43, 48	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℕ)
50	49	nnsqcld 14257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℕ)
51	50	nnzd 12594	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℤ)
52	50	nnne0d 12263	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≠ 0)
53	43	nnzd 12594	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℤ)
54		dvdsval2 16289	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑄‘𝑦)↑2) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ≠ 0 ∧ 𝑦 ∈ ℤ) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ))
55	51, 52, 53, 54	syl3anc 1390	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (((𝑄‘𝑦)↑2) ∥ 𝑦 ↔ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ))
56	47, 55	mpbid 234	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ)
57		nnre 12217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 𝑦 ∈ ℝ)
58		nngt0 12244	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ → 0 < 𝑦)
59	57, 58	jca 519	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ ℕ → (𝑦 ∈ ℝ ∧ 0 < 𝑦))
60		nnre 12217	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → ((𝑄‘𝑦)↑2) ∈ ℝ)
61		nngt0 12244	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → 0 < ((𝑄‘𝑦)↑2))
62	60, 61	jca 519	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑄‘𝑦)↑2) ∈ ℕ → (((𝑄‘𝑦)↑2) ∈ ℝ ∧ 0 < ((𝑄‘𝑦)↑2)))
63		divgt0 12060	. . . . . . . . . . . . . . . . 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 12578	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 0 < (𝑦 / ((𝑄‘𝑦)↑2))))
67	56, 65, 66	sylanbrc 592	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ)
68	67	nnred 12225	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℝ)
69	43	nnred 12225	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℝ)
70	16	nnred 12225	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℝ)
71	70	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℝ)
72		dvdsmul1 16311	. . . . . . . . . . . . . . . 16 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ ((𝑄‘𝑦)↑2) ∈ ℤ) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)))
73	56, 51, 72	syl2anc 593	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)))
74	43	nncnd 12226	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ∈ ℂ)
75	50	nncnd 12226	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℂ)
76	74, 75, 52	divcan1d 11968	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = 𝑦)
77	73, 76	breqtrd 5126	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦)
78		dvdsle 16344	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℕ) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦))
79	56, 43, 78	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦 → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦))
80	77, 79	mpd 15	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑦)
81		elfzle2 13533	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ (1...𝑁) → 𝑦 ≤ 𝑁)
82	41, 81	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑦 ≤ 𝑁)
83	68, 69, 71, 80, 82	letrd 11340	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ≤ 𝑁)
84		nnuz 12878	. . . . . . . . . . . . . 14 ⊢ ℕ = (ℤ_≥‘1)
85	67, 84	eleqtrdi 2872	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ (ℤ_≥‘1))
86	16	nnzd 12594	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑁 ∈ ℤ)
87	86	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℤ)
88		elfz5 13521	. . . . . . . . . . . . 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 5104	. . . . . . . . . . . . . . . . 17 ⊢ (𝑛 = 𝑦 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦))
92	91	notbid 320	. . . . . . . . . . . . . . . 16 ⊢ (𝑛 = 𝑦 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦))
93	92	ralbidv 3185	. . . . . . . . . . . . . . 15 ⊢ (𝑛 = 𝑦 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦))
94	93, 2	elrab2 3654	. . . . . . . . . . . . . 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 4084	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ (ℙ ∖ (1...𝐾)) → 𝑝 ∈ ℙ)
99		prmz 16709	. . . . . . . . . . . . . . . . . 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 16328	. . . . . . . . . . . . . . . 16 ⊢ ((𝑝 ∈ ℤ ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℤ ∧ 𝑦 ∈ ℤ) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦))
105	101, 102, 103, 104	syl3anc 1390	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → ((𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝑦 / ((𝑄‘𝑦)↑2)) ∥ 𝑦) → 𝑝 ∥ 𝑦))
106	97, 105	mpan2d 704	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)) → 𝑝 ∥ 𝑦))
107	106	con3d 152	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑀) ∧ 𝑝 ∈ (ℙ ∖ (1...𝐾))) → (¬ 𝑝 ∥ 𝑦 → ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
108	107	ralimdva 3174	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑦 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
109	96, 108	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
110		breq2 5104	. . . . . . . . . . . . . 14 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
111	110	notbid 320	. . . . . . . . . . . . 13 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
112	111	ralbidv 3185	. . . . . . . . . . . 12 ⊢ (𝑛 = (𝑦 / ((𝑄‘𝑦)↑2)) → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
113	112, 2	elrab2 3654	. . . . . . . . . . 11 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀 ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ (𝑦 / ((𝑄‘𝑦)↑2))))
114	90, 109, 113	sylanbrc 592	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ 𝑀)
115	44	prmreclem1 16952	. . . . . . . . . . . . 13 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)) ∧ (𝐴 ∈ (ℤ_≥‘2) → ¬ (𝐴↑2) ∥ ((𝑦 / ((𝑄‘𝑦)↑2)) / ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2)))))
116	115	simp2d 1156	. . . . . . . . . . . 12 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
117	67, 116	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))
118	115	simp1d 1155	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 / ((𝑄‘𝑦)↑2)) ∈ ℕ → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ)
119	67, 118	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ ℕ)
120		elnn1uz2 12926	. . . . . . . . . . . . . 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 16952	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℕ → ((𝑄‘𝑦) ∈ ℕ ∧ ((𝑄‘𝑦)↑2) ∥ 𝑦 ∧ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2))) ∈ (ℤ_≥‘2) → ¬ ((𝑄‘(𝑦 / ((𝑄‘𝑦)↑2)))↑2) ∥ (𝑦 / ((𝑄‘𝑦)↑2)))))
124	123	simp3d 1157	. . . . . . . . . . . 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 3652	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑦 / ((𝑄‘𝑦)↑2)) ∈ {𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1})
128	50	nnred 12225	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ∈ ℝ)
129		dvdsle 16344	. . . . . . . . . . . . . . . 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 11340	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ 𝑁)
133	71	recnd 11210	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → 𝑁 ∈ ℂ)
134	133	sqsqrtd 15469	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((√‘𝑁)↑2) = 𝑁)
135	132, 134	breqtrrd 5128	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦)↑2) ≤ ((√‘𝑁)↑2))
136	49	nnrpd 13035	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℝ⁺)
137	18	adantr 484	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (√‘𝑁) ∈ ℝ⁺)
138		rprege0 13009	. . . . . . . . . . . . . 14 ⊢ ((𝑄‘𝑦) ∈ ℝ⁺ → ((𝑄‘𝑦) ∈ ℝ ∧ 0 ≤ (𝑄‘𝑦)))
139		rprege0 13009	. . . . . . . . . . . . . 14 ⊢ ((√‘𝑁) ∈ ℝ⁺ → ((√‘𝑁) ∈ ℝ ∧ 0 ≤ (√‘𝑁)))
140		le2sq 14147	. . . . . . . . . . . . . 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 12594	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ ℤ)
146		flge 13815	. . . . . . . . . . . 12 ⊢ (((√‘𝑁) ∈ ℝ ∧ (𝑄‘𝑦) ∈ ℤ) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
147	144, 145, 146	syl2anc 593	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ≤ (√‘𝑁) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
148	143, 147	mpbid 234	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁)))
149	49, 84	eleqtrdi 2872	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ (ℤ_≥‘1))
150	21	nn0zd 12593	. . . . . . . . . . . 12 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ∈ ℤ)
151	150	adantr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (⌊‘(√‘𝑁)) ∈ ℤ)
152		elfz5 13521	. . . . . . . . . . 11 ⊢ (((𝑄‘𝑦) ∈ (ℤ_≥‘1) ∧ (⌊‘(√‘𝑁)) ∈ ℤ) → ((𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
153	149, 151, 152	syl2anc 593	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ((𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))) ↔ (𝑄‘𝑦) ≤ (⌊‘(√‘𝑁))))
154	148, 153	mpbird 259	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → (𝑄‘𝑦) ∈ (1...(⌊‘(√‘𝑁))))
155	127, 154	opelxpd 5686	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑀) → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
156	155	ex 416	. . . . . . 7 ⊢ (𝜑 → (𝑦 ∈ 𝑀 → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ ∈ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
157		ovex 7429	. . . . . . . . . . . 12 ⊢ (𝑦 / ((𝑄‘𝑦)↑2)) ∈ V
158		fvex 6880	. . . . . . . . . . . 12 ⊢ (𝑄‘𝑦) ∈ V
159	157, 158	opth 5444	. . . . . . . . . . 11 ⊢ (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ ((𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)) ∧ (𝑄‘𝑦) = (𝑄‘𝑧)))
160		oveq1 7403	. . . . . . . . . . . 12 ⊢ ((𝑄‘𝑦) = (𝑄‘𝑧) → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2))
161		oveq12 7405	. . . . . . . . . . . 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 13560	. . . . . . . . . . . . . . 15 ⊢ (1...𝑁) ⊆ ℕ
166	3, 165	sstri 3945	. . . . . . . . . . . . . 14 ⊢ 𝑀 ⊆ ℕ
167		simprr 782	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ 𝑀)
168	166, 167	sselid 3934	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℕ)
169	168	nncnd 12226	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → 𝑧 ∈ ℂ)
170	44	prmreclem1 16952	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ ℕ → ((𝑄‘𝑧) ∈ ℕ ∧ ((𝑄‘𝑧)↑2) ∥ 𝑧 ∧ (2 ∈ (ℤ_≥‘2) → ¬ (2↑2) ∥ (𝑧 / ((𝑄‘𝑧)↑2)))))
171	170	simp1d 1155	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ ℕ → (𝑄‘𝑧) ∈ ℕ)
172	168, 171	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (𝑄‘𝑧) ∈ ℕ)
173	172	nnsqcld 14257	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℕ)
174	173	nncnd 12226	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ∈ ℂ)
175	173	nnne0d 12263	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑄‘𝑧)↑2) ≠ 0)
176	169, 174, 175	divcan1d 11968	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) = 𝑧)
177	164, 176	eqeq12d 2778	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (((𝑦 / ((𝑄‘𝑦)↑2)) · ((𝑄‘𝑦)↑2)) = ((𝑧 / ((𝑄‘𝑧)↑2)) · ((𝑄‘𝑧)↑2)) ↔ 𝑦 = 𝑧))
178	163, 177	imbitrid 246	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ → 𝑦 = 𝑧))
179		id 22	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → 𝑦 = 𝑧)
180		fveq2 6867	. . . . . . . . . . . 12 ⊢ (𝑦 = 𝑧 → (𝑄‘𝑦) = (𝑄‘𝑧))
181	180	oveq1d 7411	. . . . . . . . . . 11 ⊢ (𝑦 = 𝑧 → ((𝑄‘𝑦)↑2) = ((𝑄‘𝑧)↑2))
182	179, 181	oveq12d 7414	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑦 / ((𝑄‘𝑦)↑2)) = (𝑧 / ((𝑄‘𝑧)↑2)))
183	182, 180	opeq12d 4839	. . . . . . . . 9 ⊢ (𝑦 = 𝑧 → ⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩)
184	178, 183	impbid1 227	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀)) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ 𝑦 = 𝑧))
185	184	ex 416	. . . . . . 7 ⊢ (𝜑 → ((𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀) → (⟨(𝑦 / ((𝑄‘𝑦)↑2)), (𝑄‘𝑦)⟩ = ⟨(𝑧 / ((𝑄‘𝑧)↑2)), (𝑄‘𝑧)⟩ ↔ 𝑦 = 𝑧)))
186	156, 185	dom2d 8974	. . . . . 6 ⊢ (𝜑 → (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))) ∈ Fin → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))))
187	38, 186	mpi 20	. . . . 5 ⊢ (𝜑 → 𝑀 ≼ ({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁)))))
188		hashdom 14392	. . . . . 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 14447	. . . . . 6 ⊢ (({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} ∈ Fin ∧ (1...(⌊‘(√‘𝑁))) ∈ Fin) → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))))
192	29, 36, 191	mp2an 702	. . . . 5 ⊢ (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁)))))
193		hashfz1 14359	. . . . . . 7 ⊢ ((⌊‘(√‘𝑁)) ∈ ℕ₀ → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
194	21, 193	syl 17	. . . . . 6 ⊢ (𝜑 → (♯‘(1...(⌊‘(√‘𝑁)))) = (⌊‘(√‘𝑁)))
195	194	oveq2d 7412	. . . . 5 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (♯‘(1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
196	192, 195	eqtrid 2809	. . . 4 ⊢ (𝜑 → (♯‘({𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1} × (1...(⌊‘(√‘𝑁))))) = ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
197	190, 196	breqtrd 5126	. . 3 ⊢ (𝜑 → (♯‘𝑀) ≤ ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))))
198	32	a1i 11	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ∈ ℝ)
199	21	nn0ge0d 12545	. . . 4 ⊢ (𝜑 → 0 ≤ (⌊‘(√‘𝑁)))
200		prmrec.1	. . . . 5 ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0))
201	200, 11, 16, 2, 44	prmreclem2 16953	. . . 4 ⊢ (𝜑 → (♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) ≤ (2↑𝐾))
202	198, 24, 33, 199, 201	lemul1ad 12131	. . 3 ⊢ (𝜑 → ((♯‘{𝑥 ∈ 𝑀 ∣ (𝑄‘𝑥) = 1}) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
203	9, 35, 23, 197, 202	letrd 11340	. 2 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (⌊‘(√‘𝑁))))
204	14	nnrpd 13035	. . . 4 ⊢ (𝜑 → (2↑𝐾) ∈ ℝ⁺)
205	204	rprege0d 13044	. . 3 ⊢ (𝜑 → ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾)))
206		fllelt 13807	. . . . 5 ⊢ ((√‘𝑁) ∈ ℝ → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
207	25, 206	syl 17	. . . 4 ⊢ (𝜑 → ((⌊‘(√‘𝑁)) ≤ (√‘𝑁) ∧ (√‘𝑁) < ((⌊‘(√‘𝑁)) + 1)))
208	207	simpld 498	. . 3 ⊢ (𝜑 → (⌊‘(√‘𝑁)) ≤ (√‘𝑁))
209		lemul2a 12046	. . 3 ⊢ ((((⌊‘(√‘𝑁)) ∈ ℝ ∧ (√‘𝑁) ∈ ℝ ∧ ((2↑𝐾) ∈ ℝ ∧ 0 ≤ (2↑𝐾))) ∧ (⌊‘(√‘𝑁)) ≤ (√‘𝑁)) → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
210	33, 25, 205, 208, 209	syl31anc 1392	. 2 ⊢ (𝜑 → ((2↑𝐾) · (⌊‘(√‘𝑁))) ≤ ((2↑𝐾) · (√‘𝑁)))
211	9, 23, 26, 203, 210	letrd 11340	1 ⊢ (𝜑 → (♯‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 ∨ wo 858 = wceq 1560 ∈ wcel 2142 ≠ wne 2957 ∀wral 3076 {crab 3414 ∖ cdif 3901 ⊆ wss 3904 ifcif 4480 ⟨cop 4588 class class class wbr 5100 ↦ cmpt 5181 × cxp 5645 ‘cfv 6521 (class class class)co 7396 ≼ cdom 8925 Fincfn 8927 supcsup 9386 ℝcr 11072 0cc0 11073 1c1 11074 + caddc 11076 · cmul 11078 < clt 11216 ≤ cle 11217 / cdiv 11844 ℕcn 12210 2c2 12272 ℕ₀cn0 12481 ℤcz 12568 ℤ_≥cuz 12839 ℝ⁺crp 12993 ...cfz 13512 ⌊cfl 13800 ↑cexp 14074 ♯chash 14343 √csqrt 15260 ∥ cdvds 16286 ℙcprime 16705

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5227 ax-sep 5246 ax-nul 5256 ax-pow 5322 ax-pr 5390 ax-un 7718 ax-cnex 11129 ax-resscn 11130 ax-1cn 11131 ax-icn 11132 ax-addcl 11133 ax-addrcl 11134 ax-mulcl 11135 ax-mulrcl 11136 ax-mulcom 11137 ax-addass 11138 ax-mulass 11139 ax-distr 11140 ax-i2m1 11141 ax-1ne0 11142 ax-1rid 11143 ax-rnegex 11144 ax-rrecex 11145 ax-cnre 11146 ax-pre-lttri 11147 ax-pre-lttrn 11148 ax-pre-ltadd 11149 ax-pre-mulgt0 11150 ax-pre-sup 11151

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1099 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-nf 1804 df-sb 2091 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3367 df-reu 3368 df-rab 3415 df-v 3456 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4481 df-pw 4557 df-sn 4583 df-pr 4585 df-op 4589 df-uni 4866 df-int 4906 df-iun 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5542 df-eprel 5547 df-po 5555 df-so 5556 df-fr 5600 df-we 5602 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-res 5659 df-ima 5660 df-pred 6288 df-ord 6349 df-on 6350 df-lim 6351 df-suc 6352 df-iota 6477 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 df-fv 6529 df-riota 7353 df-ov 7399 df-oprab 7400 df-mpo 7401 df-om 7847 df-1st 7970 df-2nd 7971 df-frecs 8262 df-wrecs 8293 df-recs 8342 df-rdg 8381 df-1o 8437 df-2o 8438 df-oadd 8441 df-er 8678 df-map 8810 df-pm 8811 df-en 8928 df-dom 8929 df-sdom 8930 df-fin 8931 df-sup 9388 df-inf 9389 df-dju 9859 df-card 9897 df-pnf 11218 df-mnf 11219 df-xr 11220 df-ltxr 11221 df-le 11222 df-sub 11416 df-neg 11417 df-div 11845 df-nn 12211 df-2 12280 df-3 12281 df-n0 12482 df-xnn0 12555 df-z 12569 df-uz 12840 df-q 12950 df-rp 12994 df-fz 13513 df-fl 13802 df-mod 13880 df-seq 14015 df-exp 14075 df-hash 14344 df-cj 15126 df-re 15127 df-im 15128 df-sqrt 15262 df-abs 15263 df-dvds 16287 df-gcd 16529 df-prm 16706 df-pc 16873

This theorem is referenced by: prmreclem5 16956

W3C validator