Theorem prmreclem3

Description: Lemma for prmrec . The main inequality established here is # M <_ # { x e. M | ( Qx ) = 1 } x. sqrt N , where { x e. M | ( Qx ) = 1 } is the set of squarefree numbers in M . This is demonstrated by the map y |-> <. y / ( Qy ) ^ 2 , ( Qy ) >. where Qy is the largest number whose square divides y . (Contributed by Mario Carneiro, 5-Aug-2014)

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

Proof

Step	Hyp	Ref	Expression
1		prmrec.1	⊢ 𝐹 = ( 𝑛 ∈ ℕ ↦ if ( 𝑛 ∈ ℙ , ( 1 / 𝑛 ) , 0 ) )
2		prmrec.2	⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3		prmrec.3	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4		prmrec.4	⊢ 𝑀 = { 𝑛 ∈ ( 1 ... 𝑁 ) ∣ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 }
5		prmreclem2.5	⊢ 𝑄 = ( 𝑛 ∈ ℕ ↦ sup ( { 𝑟 ∈ ℕ ∣ ( 𝑟 ↑ 2 ) ∥ 𝑛 } , ℝ , < ) )
6		fzfi	⊢ ( 1 ... 𝑁 ) ∈ Fin
7	4	ssrab3	⊢ 𝑀 ⊆ ( 1 ... 𝑁 )
8		ssfi	⊢ ( ( ( 1 ... 𝑁 ) ∈ Fin ∧ 𝑀 ⊆ ( 1 ... 𝑁 ) ) → 𝑀 ∈ Fin )
9	6 7 8	mp2an	⊢ 𝑀 ∈ Fin
10		hashcl	⊢ ( 𝑀 ∈ Fin → ( ♯ ‘ 𝑀 ) ∈ ℕ0 )
11	9 10	ax-mp	⊢ ( ♯ ‘ 𝑀 ) ∈ ℕ0
12	11	nn0rei	⊢ ( ♯ ‘ 𝑀 ) ∈ ℝ
13	12	a1i	⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ∈ ℝ )
14		2nn	⊢ 2 ∈ ℕ
15	2	nnnn0d	⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
16		nnexpcl	⊢ ( ( 2 ∈ ℕ ∧ 𝐾 ∈ ℕ0 ) → ( 2 ↑ 𝐾 ) ∈ ℕ )
17	14 15 16	sylancr	⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℕ )
18	17	nnnn0d	⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℕ0 )
19	3	nnrpd	⊢ ( 𝜑 → 𝑁 ∈ ℝ+ )
20	19	rpsqrtcld	⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ+ )
21	20	rprege0d	⊢ ( 𝜑 → ( ( √ ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑁 ) ) )
22		flge0nn0	⊢ ( ( ( √ ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑁 ) ) → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℕ0 )
23	21 22	syl	⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℕ0 )
24	18 23	nn0mulcld	⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℕ0 )
25	24	nn0red	⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
26	17	nnred	⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℝ )
27	20	rpred	⊢ ( 𝜑 → ( √ ‘ 𝑁 ) ∈ ℝ )
28	26 27	remulcld	⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) ∈ ℝ )
29		ssrab2	⊢ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ⊆ 𝑀
30		ssfi	⊢ ( ( 𝑀 ∈ Fin ∧ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ⊆ 𝑀 ) → { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin )
31	9 29 30	mp2an	⊢ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin
32		hashcl	⊢ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ∈ ℕ0 )
33	31 32	ax-mp	⊢ ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ∈ ℕ0
34	33	nn0rei	⊢ ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ∈ ℝ
35	23	nn0red	⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℝ )
36		remulcl	⊢ ( ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ∈ ℝ ∧ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℝ ) → ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
37	34 35 36	sylancr	⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ ℝ )
38		fzfi	⊢ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ Fin
39		xpfi	⊢ ( ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin ∧ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ Fin ) → ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ∈ Fin )
40	31 38 39	mp2an	⊢ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ∈ Fin
41		fveqeq2	⊢ ( 𝑥 = ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) → ( ( 𝑄 ‘ 𝑥 ) = 1 ↔ ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 ) )
42		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ 𝑀 )
43	7 42	sselid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ( 1 ... 𝑁 ) )
44		elfznn	⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → 𝑦 ∈ ℕ )
45	43 44	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ℕ )
46	5	prmreclem1	⊢ ( 𝑦 ∈ ℕ → ( ( 𝑄 ‘ 𝑦 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 ∧ ( 𝑛 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝑛 ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
47	46	simp2d	⊢ ( 𝑦 ∈ ℕ → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 )
48	45 47	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 )
49	46	simp1d	⊢ ( 𝑦 ∈ ℕ → ( 𝑄 ‘ 𝑦 ) ∈ ℕ )
50	45 49	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ∈ ℕ )
51	50	nnsqcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℕ )
52	51	nnzd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℤ )
53	51	nnne0d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≠ 0 )
54	45	nnzd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ℤ )
55		dvdsval2	⊢ ( ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℤ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≠ 0 ∧ 𝑦 ∈ ℤ ) → ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 ↔ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ) )
56	52 53 54 55	syl3anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 ↔ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ) )
57	48 56	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ )
58		nnre	⊢ ( 𝑦 ∈ ℕ → 𝑦 ∈ ℝ )
59		nngt0	⊢ ( 𝑦 ∈ ℕ → 0 < 𝑦 )
60	58 59	jca	⊢ ( 𝑦 ∈ ℕ → ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) )
61		nnre	⊢ ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℕ → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℝ )
62		nngt0	⊢ ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℕ → 0 < ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) )
63	61 62	jca	⊢ ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℕ → ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℝ ∧ 0 < ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
64		divgt0	⊢ ( ( ( 𝑦 ∈ ℝ ∧ 0 < 𝑦 ) ∧ ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℝ ∧ 0 < ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) → 0 < ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
65	60 63 64	syl2an	⊢ ( ( 𝑦 ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℕ ) → 0 < ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
66	45 51 65	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 0 < ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
67		elnnz	⊢ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℕ ↔ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ∧ 0 < ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
68	57 66 67	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℕ )
69	68	nnred	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℝ )
70	45	nnred	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ℝ )
71	3	nnred	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
72	71	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑁 ∈ ℝ )
73		dvdsmul1	⊢ ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℤ ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
74	57 52 73	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
75	45	nncnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ∈ ℂ )
76	51	nncnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℂ )
77	75 76 53	divcan1d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = 𝑦 )
78	74 77	breqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 )
79		dvdsle	⊢ ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑦 ) )
80	57 45 79	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑦 ) )
81	78 80	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑦 )
82		elfzle2	⊢ ( 𝑦 ∈ ( 1 ... 𝑁 ) → 𝑦 ≤ 𝑁 )
83	43 82	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑦 ≤ 𝑁 )
84	69 70 72 81 83	letrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑁 )
85		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
86	68 85	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( ℤ≥ ‘ 1 ) )
87	3	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
88	87	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑁 ∈ ℤ )
89		elfz5	⊢ ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( ℤ≥ ‘ 1 ) ∧ 𝑁 ∈ ℤ ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( 1 ... 𝑁 ) ↔ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑁 ) )
90	86 88 89	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( 1 ... 𝑁 ) ↔ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ≤ 𝑁 ) )
91	84 90	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( 1 ... 𝑁 ) )
92		breq2	⊢ ( 𝑛 = 𝑦 → ( 𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑦 ) )
93	92	notbid	⊢ ( 𝑛 = 𝑦 → ( ¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑦 ) )
94	93	ralbidv	⊢ ( 𝑛 = 𝑦 → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ) )
95	94 4	elrab2	⊢ ( 𝑦 ∈ 𝑀 ↔ ( 𝑦 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ) )
96	42 95	sylib	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 ) )
97	96	simprd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 )
98	78	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 )
99		eldifi	⊢ ( 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) → 𝑝 ∈ ℙ )
100		prmz	⊢ ( 𝑝 ∈ ℙ → 𝑝 ∈ ℤ )
101	99 100	syl	⊢ ( 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) → 𝑝 ∈ ℤ )
102	101	adantl	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → 𝑝 ∈ ℤ )
103	57	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ )
104	54	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → 𝑦 ∈ ℤ )
105		dvdstr	⊢ ( ( 𝑝 ∈ ℤ ∧ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℤ ∧ 𝑦 ∈ ℤ ) → ( ( 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∧ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 ) → 𝑝 ∥ 𝑦 ) )
106	102 103 104 105	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ( 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∧ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∥ 𝑦 ) → 𝑝 ∥ 𝑦 ) )
107	98 106	mpan2d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) → 𝑝 ∥ 𝑦 ) )
108	107	con3d	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) ∧ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ) → ( ¬ 𝑝 ∥ 𝑦 → ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
109	108	ralimdva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑦 → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
110	97 109	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
111		breq2	⊢ ( 𝑛 = ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) → ( 𝑝 ∥ 𝑛 ↔ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
112	111	notbid	⊢ ( 𝑛 = ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) → ( ¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
113	112	ralbidv	⊢ ( 𝑛 = ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) → ( ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ 𝑛 ↔ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
114	113 4	elrab2	⊢ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ 𝑀 ↔ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ( 1 ... 𝑁 ) ∧ ∀ 𝑝 ∈ ( ℙ ∖ ( 1 ... 𝐾 ) ) ¬ 𝑝 ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
115	91 110 114	sylanbrc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ 𝑀 )
116	5	prmreclem1	⊢ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℕ → ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ℕ ∧ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∧ ( 𝐴 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 𝐴 ↑ 2 ) ∥ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) / ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ) ) ) )
117	116	simp2d	⊢ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℕ → ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
118	68 117	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) )
119	116	simp1d	⊢ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ ℕ → ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ℕ )
120	68 119	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ℕ )
121		elnn1uz2	⊢ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ℕ ↔ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 ∨ ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ( ℤ≥ ‘ 2 ) ) )
122	120 121	sylib	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 ∨ ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ( ℤ≥ ‘ 2 ) ) )
123	122	ord	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ¬ ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 → ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ( ℤ≥ ‘ 2 ) ) )
124	5	prmreclem1	⊢ ( 𝑦 ∈ ℕ → ( ( 𝑄 ‘ 𝑦 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 ∧ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ( ℤ≥ ‘ 2 ) → ¬ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ) )
125	124	simp3d	⊢ ( 𝑦 ∈ ℕ → ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ∈ ( ℤ≥ ‘ 2 ) → ¬ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
126	45 123 125	sylsyld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ¬ ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 → ¬ ( ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) ↑ 2 ) ∥ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) )
127	118 126	mt4d	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ) = 1 )
128	41 115 127	elrabd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } )
129	51	nnred	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℝ )
130		dvdsle	⊢ ( ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∈ ℤ ∧ 𝑦 ∈ ℕ ) → ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ 𝑦 ) )
131	52 45 130	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ∥ 𝑦 → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ 𝑦 ) )
132	48 131	mpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ 𝑦 )
133	129 70 72 132 83	letrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ 𝑁 )
134	72	recnd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → 𝑁 ∈ ℂ )
135	134	sqsqrtd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( √ ‘ 𝑁 ) ↑ 2 ) = 𝑁 )
136	133 135	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑁 ) ↑ 2 ) )
137	50	nnrpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ∈ ℝ+ )
138	20	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( √ ‘ 𝑁 ) ∈ ℝ+ )
139		rprege0	⊢ ( ( 𝑄 ‘ 𝑦 ) ∈ ℝ+ → ( ( 𝑄 ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝑄 ‘ 𝑦 ) ) )
140		rprege0	⊢ ( ( √ ‘ 𝑁 ) ∈ ℝ+ → ( ( √ ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑁 ) ) )
141		le2sq	⊢ ( ( ( ( 𝑄 ‘ 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝑄 ‘ 𝑦 ) ) ∧ ( ( √ ‘ 𝑁 ) ∈ ℝ ∧ 0 ≤ ( √ ‘ 𝑁 ) ) ) → ( ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) ↔ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑁 ) ↑ 2 ) ) )
142	139 140 141	syl2an	⊢ ( ( ( 𝑄 ‘ 𝑦 ) ∈ ℝ+ ∧ ( √ ‘ 𝑁 ) ∈ ℝ+ ) → ( ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) ↔ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑁 ) ↑ 2 ) ) )
143	137 138 142	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) ↔ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ≤ ( ( √ ‘ 𝑁 ) ↑ 2 ) ) )
144	136 143	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) )
145	27	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( √ ‘ 𝑁 ) ∈ ℝ )
146	50	nnzd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ∈ ℤ )
147		flge	⊢ ( ( ( √ ‘ 𝑁 ) ∈ ℝ ∧ ( 𝑄 ‘ 𝑦 ) ∈ ℤ ) → ( ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) ↔ ( 𝑄 ‘ 𝑦 ) ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
148	145 146 147	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ≤ ( √ ‘ 𝑁 ) ↔ ( 𝑄 ‘ 𝑦 ) ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
149	144 148	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) )
150	50 85	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 1 ) )
151	23	nn0zd	⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℤ )
152	151	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℤ )
153		elfz5	⊢ ( ( ( 𝑄 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 1 ) ∧ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℤ ) → ( ( 𝑄 ‘ 𝑦 ) ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ↔ ( 𝑄 ‘ 𝑦 ) ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
154	150 152 153	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( ( 𝑄 ‘ 𝑦 ) ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ↔ ( 𝑄 ‘ 𝑦 ) ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
155	149 154	mpbird	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ( 𝑄 ‘ 𝑦 ) ∈ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
156	128 155	opelxpd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑀 ) → ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ ∈ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) )
157	156	ex	⊢ ( 𝜑 → ( 𝑦 ∈ 𝑀 → ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ ∈ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
158		ovex	⊢ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) ∈ V
159		fvex	⊢ ( 𝑄 ‘ 𝑦 ) ∈ V
160	158 159	opth	⊢ ( ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ ↔ ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) ∧ ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ 𝑧 ) ) )
161		oveq1	⊢ ( ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ 𝑧 ) → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) = ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) )
162		oveq12	⊢ ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) ∧ ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) = ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) )
163	161 162	sylan2	⊢ ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) ∧ ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ 𝑧 ) ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) )
164	160 163	sylbi	⊢ ( ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) )
165	77	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = 𝑦 )
166		fz1ssnn	⊢ ( 1 ... 𝑁 ) ⊆ ℕ
167	7 166	sstri	⊢ 𝑀 ⊆ ℕ
168		simprr	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → 𝑧 ∈ 𝑀 )
169	167 168	sselid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → 𝑧 ∈ ℕ )
170	169	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → 𝑧 ∈ ℂ )
171	5	prmreclem1	⊢ ( 𝑧 ∈ ℕ → ( ( 𝑄 ‘ 𝑧 ) ∈ ℕ ∧ ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ∥ 𝑧 ∧ ( 2 ∈ ( ℤ≥ ‘ 2 ) → ¬ ( 2 ↑ 2 ) ∥ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) ) ) )
172	171	simp1d	⊢ ( 𝑧 ∈ ℕ → ( 𝑄 ‘ 𝑧 ) ∈ ℕ )
173	169 172	syl	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( 𝑄 ‘ 𝑧 ) ∈ ℕ )
174	173	nnsqcld	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ∈ ℕ )
175	174	nncnd	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ∈ ℂ )
176	174	nnne0d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ≠ 0 )
177	170 175 176	divcan1d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) = 𝑧 )
178	165 177	eqeq12d	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ( ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) · ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) ↔ 𝑦 = 𝑧 ) )
179	164 178	imbitrid	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ → 𝑦 = 𝑧 ) )
180		id	⊢ ( 𝑦 = 𝑧 → 𝑦 = 𝑧 )
181		fveq2	⊢ ( 𝑦 = 𝑧 → ( 𝑄 ‘ 𝑦 ) = ( 𝑄 ‘ 𝑧 ) )
182	181	oveq1d	⊢ ( 𝑦 = 𝑧 → ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) = ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) )
183	180 182	oveq12d	⊢ ( 𝑦 = 𝑧 → ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) = ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) )
184	183 181	opeq12d	⊢ ( 𝑦 = 𝑧 → ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ )
185	179 184	impbid1	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) ) → ( ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ ↔ 𝑦 = 𝑧 ) )
186	185	ex	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝑀 ∧ 𝑧 ∈ 𝑀 ) → ( ⟨ ( 𝑦 / ( ( 𝑄 ‘ 𝑦 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑦 ) ⟩ = ⟨ ( 𝑧 / ( ( 𝑄 ‘ 𝑧 ) ↑ 2 ) ) , ( 𝑄 ‘ 𝑧 ) ⟩ ↔ 𝑦 = 𝑧 ) ) )
187	157 186	dom2d	⊢ ( 𝜑 → ( ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ∈ Fin → 𝑀 ≼ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
188	40 187	mpi	⊢ ( 𝜑 → 𝑀 ≼ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) )
189		hashdom	⊢ ( ( 𝑀 ∈ Fin ∧ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ∈ Fin ) → ( ( ♯ ‘ 𝑀 ) ≤ ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) ↔ 𝑀 ≼ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
190	9 40 189	mp2an	⊢ ( ( ♯ ‘ 𝑀 ) ≤ ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) ↔ 𝑀 ≼ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) )
191	188 190	sylibr	⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ≤ ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
192		hashxp	⊢ ( ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ∈ Fin ∧ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ∈ Fin ) → ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) )
193	31 38 192	mp2an	⊢ ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) )
194		hashfz1	⊢ ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) = ( ⌊ ‘ ( √ ‘ 𝑁 ) ) )
195	23 194	syl	⊢ ( 𝜑 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) = ( ⌊ ‘ ( √ ‘ 𝑁 ) ) )
196	195	oveq2d	⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
197	193 196	eqtrid	⊢ ( 𝜑 → ( ♯ ‘ ( { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } × ( 1 ... ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ) ) = ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
198	191 197	breqtrd	⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ≤ ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
199	34	a1i	⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ∈ ℝ )
200	23	nn0ge0d	⊢ ( 𝜑 → 0 ≤ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) )
201	1 2 3 4 5	prmreclem2	⊢ ( 𝜑 → ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) ≤ ( 2 ↑ 𝐾 ) )
202	199 26 35 200 201	lemul1ad	⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑥 ∈ 𝑀 ∣ ( 𝑄 ‘ 𝑥 ) = 1 } ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ≤ ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
203	13 37 25 198 202	letrd	⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ≤ ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) )
204	17	nnrpd	⊢ ( 𝜑 → ( 2 ↑ 𝐾 ) ∈ ℝ+ )
205	204	rprege0d	⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ 𝐾 ) ) )
206		fllelt	⊢ ( ( √ ‘ 𝑁 ) ∈ ℝ → ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ≤ ( √ ‘ 𝑁 ) ∧ ( √ ‘ 𝑁 ) < ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) + 1 ) ) )
207	27 206	syl	⊢ ( 𝜑 → ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ≤ ( √ ‘ 𝑁 ) ∧ ( √ ‘ 𝑁 ) < ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) + 1 ) ) )
208	207	simpld	⊢ ( 𝜑 → ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ≤ ( √ ‘ 𝑁 ) )
209		lemul2a	⊢ ( ( ( ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ∈ ℝ ∧ ( √ ‘ 𝑁 ) ∈ ℝ ∧ ( ( 2 ↑ 𝐾 ) ∈ ℝ ∧ 0 ≤ ( 2 ↑ 𝐾 ) ) ) ∧ ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ≤ ( √ ‘ 𝑁 ) ) → ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ≤ ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) )
210	35 27 205 208 209	syl31anc	⊢ ( 𝜑 → ( ( 2 ↑ 𝐾 ) · ( ⌊ ‘ ( √ ‘ 𝑁 ) ) ) ≤ ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) )
211	13 25 28 203 210	letrd	⊢ ( 𝜑 → ( ♯ ‘ 𝑀 ) ≤ ( ( 2 ↑ 𝐾 ) · ( √ ‘ 𝑁 ) ) )