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	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, \frac{1}{n}, 0))$
	prmrec.2	$⊢ φ \to K \in ℕ$
	prmrec.3	$⊢ φ \to N \in ℕ$
	prmrec.4	$⊢ M = \{n \in (1 \dots N) \| \forall p \in (ℙ ∖ (1 \dots K)) \neg p ∥ n\}$
	prmreclem2.5	$⊢ Q = (n \in ℕ ⟼ sup (\{r \in ℕ \| r^{2} ∥ n\} ℝ <))$
Assertion	prmreclem3	$⊢ φ \to \|M\| \leq 2^{K} \sqrt{N}$

Proof

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

Metamath Proof Explorer

Theorem prmreclem3

Proof