prmreclem1

Description: Lemma for prmrec . Properties of the "square part" function, which extracts the m of the decomposition N = r m ^ 2 , with m maximal and r squarefree. (Contributed by Mario Carneiro, 5-Aug-2014)

		Ref	Expression
	Hypothesis	prmreclem1.1	$⊢ Q = (n \in ℕ ⟼ sup (\{r \in ℕ \| r^{2} ∥ n\} ℝ <))$
	Assertion	prmreclem1	$⊢ N \in ℕ \to (Q (N) \in ℕ \land {Q (N)}^{2} ∥ N \land (K \in ℤ_{\geq 2} \to \neg K^{2} ∥ (\frac{N}{{Q (N)}^{2}})))$

Proof

Step	Hyp	Ref	Expression
1		prmreclem1.1	$⊢ Q = (n \in ℕ ⟼ sup (\{r \in ℕ \| r^{2} ∥ n\} ℝ <))$
2		ssrab2	$⊢ \{r \in ℕ \| r^{2} ∥ N\} \subseteq ℕ$
3		breq2	$⊢ n = N \to (r^{2} ∥ n \leftrightarrow r^{2} ∥ N)$
4	3	rabbidv	$⊢ n = N \to \{r \in ℕ \| r^{2} ∥ n\} = \{r \in ℕ \| r^{2} ∥ N\}$
5	4	supeq1d	$⊢ n = N \to sup (\{r \in ℕ \| r^{2} ∥ n\} ℝ <) = sup (\{r \in ℕ \| r^{2} ∥ N\} ℝ <)$
6		ltso	$⊢ < Or ℝ$
7	6	supex	$⊢ sup (\{r \in ℕ \| r^{2} ∥ N\} ℝ <) \in V$
8	5 1 7	fvmpt	$⊢ N \in ℕ \to Q (N) = sup (\{r \in ℕ \| r^{2} ∥ N\} ℝ <)$
9		nnssz	$⊢ ℕ \subseteq ℤ$
10	2 9	sstri	$⊢ \{r \in ℕ \| r^{2} ∥ N\} \subseteq ℤ$
11		oveq1	$⊢ r = 1 \to r^{2} = 1^{2}$
12		sq1	$⊢ 1^{2} = 1$
13	11 12	eqtrdi	$⊢ r = 1 \to r^{2} = 1$
14	13	breq1d	$⊢ r = 1 \to (r^{2} ∥ N \leftrightarrow 1 ∥ N)$
15		1nn	$⊢ 1 \in ℕ$
16	15	a1i	$⊢ N \in ℕ \to 1 \in ℕ$
17		nnz	$⊢ N \in ℕ \to N \in ℤ$
18		1dvds	$⊢ N \in ℤ \to 1 ∥ N$
19	17 18	syl	$⊢ N \in ℕ \to 1 ∥ N$
20	14 16 19	elrabd	$⊢ N \in ℕ \to 1 \in \{r \in ℕ \| r^{2} ∥ N\}$
21	20	ne0d	$⊢ N \in ℕ \to \{r \in ℕ \| r^{2} ∥ N\} \neq \emptyset$
22		nnz	$⊢ z \in ℕ \to z \in ℤ$
23		zsqcl	$⊢ z \in ℤ \to z^{2} \in ℤ$
24	22 23	syl	$⊢ z \in ℕ \to z^{2} \in ℤ$
25		id	$⊢ N \in ℕ \to N \in ℕ$
26		dvdsle	$⊢ (z^{2} \in ℤ \land N \in ℕ) \to (z^{2} ∥ N \to z^{2} \leq N)$
27	24 25 26	syl2anr	$⊢ (N \in ℕ \land z \in ℕ) \to (z^{2} ∥ N \to z^{2} \leq N)$
28		nnlesq	$⊢ z \in ℕ \to z \leq z^{2}$
29	28	adantl	$⊢ (N \in ℕ \land z \in ℕ) \to z \leq z^{2}$
30		nnre	$⊢ z \in ℕ \to z \in ℝ$
31	30	adantl	$⊢ (N \in ℕ \land z \in ℕ) \to z \in ℝ$
32	31	resqcld	$⊢ (N \in ℕ \land z \in ℕ) \to z^{2} \in ℝ$
33		nnre	$⊢ N \in ℕ \to N \in ℝ$
34	33	adantr	$⊢ (N \in ℕ \land z \in ℕ) \to N \in ℝ$
35		letr	$⊢ (z \in ℝ \land z^{2} \in ℝ \land N \in ℝ) \to ((z \leq z^{2} \land z^{2} \leq N) \to z \leq N)$
36	31 32 34 35	syl3anc	$⊢ (N \in ℕ \land z \in ℕ) \to ((z \leq z^{2} \land z^{2} \leq N) \to z \leq N)$
37	29 36	mpand	$⊢ (N \in ℕ \land z \in ℕ) \to (z^{2} \leq N \to z \leq N)$
38	27 37	syld	$⊢ (N \in ℕ \land z \in ℕ) \to (z^{2} ∥ N \to z \leq N)$
39	38	ralrimiva	$⊢ N \in ℕ \to \forall z \in ℕ (z^{2} ∥ N \to z \leq N)$
40		oveq1	$⊢ r = z \to r^{2} = z^{2}$
41	40	breq1d	$⊢ r = z \to (r^{2} ∥ N \leftrightarrow z^{2} ∥ N)$
42	41	ralrab	$⊢ \forall z \in \{r \in ℕ \| r^{2} ∥ N\} z \leq N \leftrightarrow \forall z \in ℕ (z^{2} ∥ N \to z \leq N)$
43	39 42	sylibr	$⊢ N \in ℕ \to \forall z \in \{r \in ℕ \| r^{2} ∥ N\} z \leq N$
44		brralrspcev	$⊢ (N \in ℤ \land \forall z \in \{r \in ℕ \| r^{2} ∥ N\} z \leq N) \to \exists x \in ℤ \forall z \in \{r \in ℕ \| r^{2} ∥ N\} z \leq x$
45	17 43 44	syl2anc	$⊢ N \in ℕ \to \exists x \in ℤ \forall z \in \{r \in ℕ \| r^{2} ∥ N\} z \leq x$
46		suprzcl2	$⊢ (\{r \in ℕ \| r^{2} ∥ N\} \subseteq ℤ \land \{r \in ℕ \| r^{2} ∥ N\} \neq \emptyset \land \exists x \in ℤ \forall z \in \{r \in ℕ \| r^{2} ∥ N\} z \leq x) \to sup (\{r \in ℕ \| r^{2} ∥ N\} ℝ <) \in \{r \in ℕ \| r^{2} ∥ N\}$
47	10 21 45 46	mp3an2i	$⊢ N \in ℕ \to sup (\{r \in ℕ \| r^{2} ∥ N\} ℝ <) \in \{r \in ℕ \| r^{2} ∥ N\}$
48	8 47	eqeltrd	$⊢ N \in ℕ \to Q (N) \in \{r \in ℕ \| r^{2} ∥ N\}$
49	2 48	sselid	$⊢ N \in ℕ \to Q (N) \in ℕ$
50		oveq1	$⊢ z = Q (N) \to z^{2} = {Q (N)}^{2}$
51	50	breq1d	$⊢ z = Q (N) \to (z^{2} ∥ N \leftrightarrow {Q (N)}^{2} ∥ N)$
52	41	cbvrabv	$⊢ \{r \in ℕ \| r^{2} ∥ N\} = \{z \in ℕ \| z^{2} ∥ N\}$
53	51 52	elrab2	$⊢ Q (N) \in \{r \in ℕ \| r^{2} ∥ N\} \leftrightarrow (Q (N) \in ℕ \land {Q (N)}^{2} ∥ N)$
54	48 53	sylib	$⊢ N \in ℕ \to (Q (N) \in ℕ \land {Q (N)}^{2} ∥ N)$
55	54	simprd	$⊢ N \in ℕ \to {Q (N)}^{2} ∥ N$
56	49	adantr	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to Q (N) \in ℕ$
57	56	nncnd	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to Q (N) \in ℂ$
58	57	mulridd	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to Q (N) \cdot 1 = Q (N)$
59		eluz2gt1	$⊢ K \in ℤ_{\geq 2} \to 1 < K$
60	59	adantl	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to 1 < K$
61		1red	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to 1 \in ℝ$
62		eluz2nn	$⊢ K \in ℤ_{\geq 2} \to K \in ℕ$
63	62	adantl	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to K \in ℕ$
64	63	nnred	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to K \in ℝ$
65	56	nnred	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to Q (N) \in ℝ$
66	56	nngt0d	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to 0 < Q (N)$
67		ltmul2	$⊢ (1 \in ℝ \land K \in ℝ \land (Q (N) \in ℝ \land 0 < Q (N))) \to (1 < K \leftrightarrow Q (N) \cdot 1 < Q (N) K)$
68	61 64 65 66 67	syl112anc	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to (1 < K \leftrightarrow Q (N) \cdot 1 < Q (N) K)$
69	60 68	mpbid	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to Q (N) \cdot 1 < Q (N) K$
70	58 69	eqbrtrrd	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to Q (N) < Q (N) K$
71		nnmulcl	$⊢ (Q (N) \in ℕ \land K \in ℕ) \to Q (N) K \in ℕ$
72	49 62 71	syl2an	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to Q (N) K \in ℕ$
73	72	nnred	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to Q (N) K \in ℝ$
74	65 73	ltnled	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to (Q (N) < Q (N) K \leftrightarrow \neg Q (N) K \leq Q (N))$
75	70 74	mpbid	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to \neg Q (N) K \leq Q (N)$
76	45	ad2antrr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to \exists x \in ℤ \forall z \in \{r \in ℕ \| r^{2} ∥ N\} z \leq x$
77		oveq1	$⊢ r = Q (N) K \to r^{2} = {Q (N) K}^{2}$
78	77	breq1d	$⊢ r = Q (N) K \to (r^{2} ∥ N \leftrightarrow {Q (N) K}^{2} ∥ N)$
79	72	adantr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to Q (N) K \in ℕ$
80		simpr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to K^{2} ∥ (\frac{N}{{Q (N)}^{2}})$
81	63	adantr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to K \in ℕ$
82	81	nnsqcld	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to K^{2} \in ℕ$
83		nnz	$⊢ K^{2} \in ℕ \to K^{2} \in ℤ$
84	82 83	syl	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to K^{2} \in ℤ$
85	49	nnsqcld	$⊢ N \in ℕ \to {Q (N)}^{2} \in ℕ$
86	9 85	sselid	$⊢ N \in ℕ \to {Q (N)}^{2} \in ℤ$
87	85	nnne0d	$⊢ N \in ℕ \to {Q (N)}^{2} \neq 0$
88		dvdsval2	$⊢ ({Q (N)}^{2} \in ℤ \land {Q (N)}^{2} \neq 0 \land N \in ℤ) \to ({Q (N)}^{2} ∥ N \leftrightarrow \frac{N}{{Q (N)}^{2}} \in ℤ)$
89	86 87 17 88	syl3anc	$⊢ N \in ℕ \to ({Q (N)}^{2} ∥ N \leftrightarrow \frac{N}{{Q (N)}^{2}} \in ℤ)$
90	55 89	mpbid	$⊢ N \in ℕ \to \frac{N}{{Q (N)}^{2}} \in ℤ$
91	90	ad2antrr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to \frac{N}{{Q (N)}^{2}} \in ℤ$
92	86	ad2antrr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to {Q (N)}^{2} \in ℤ$
93		dvdscmul	$⊢ (K^{2} \in ℤ \land \frac{N}{{Q (N)}^{2}} \in ℤ \land {Q (N)}^{2} \in ℤ) \to (K^{2} ∥ (\frac{N}{{Q (N)}^{2}}) \to {Q (N)}^{2} K^{2} ∥ {Q (N)}^{2} (\frac{N}{{Q (N)}^{2}}))$
94	84 91 92 93	syl3anc	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to (K^{2} ∥ (\frac{N}{{Q (N)}^{2}}) \to {Q (N)}^{2} K^{2} ∥ {Q (N)}^{2} (\frac{N}{{Q (N)}^{2}}))$
95	80 94	mpd	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to {Q (N)}^{2} K^{2} ∥ {Q (N)}^{2} (\frac{N}{{Q (N)}^{2}})$
96	57	adantr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to Q (N) \in ℂ$
97	81	nncnd	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to K \in ℂ$
98	96 97	sqmuld	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to {Q (N) K}^{2} = {Q (N)}^{2} K^{2}$
99	98	eqcomd	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to {Q (N)}^{2} K^{2} = {Q (N) K}^{2}$
100		nncn	$⊢ N \in ℕ \to N \in ℂ$
101	100	ad2antrr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to N \in ℂ$
102	85	ad2antrr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to {Q (N)}^{2} \in ℕ$
103	102	nncnd	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to {Q (N)}^{2} \in ℂ$
104	87	ad2antrr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to {Q (N)}^{2} \neq 0$
105	101 103 104	divcan2d	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to {Q (N)}^{2} (\frac{N}{{Q (N)}^{2}}) = N$
106	95 99 105	3brtr3d	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to {Q (N) K}^{2} ∥ N$
107	78 79 106	elrabd	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to Q (N) K \in \{r \in ℕ \| r^{2} ∥ N\}$
108		suprzub	$⊢ (\{r \in ℕ \| r^{2} ∥ N\} \subseteq ℤ \land \exists x \in ℤ \forall z \in \{r \in ℕ \| r^{2} ∥ N\} z \leq x \land Q (N) K \in \{r \in ℕ \| r^{2} ∥ N\}) \to Q (N) K \leq sup (\{r \in ℕ \| r^{2} ∥ N\} ℝ <)$
109	10 76 107 108	mp3an2i	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to Q (N) K \leq sup (\{r \in ℕ \| r^{2} ∥ N\} ℝ <)$
110	8	ad2antrr	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to Q (N) = sup (\{r \in ℕ \| r^{2} ∥ N\} ℝ <)$
111	109 110	breqtrrd	$⊢ ((N \in ℕ \land K \in ℤ_{\geq 2}) \land K^{2} ∥ (\frac{N}{{Q (N)}^{2}})) \to Q (N) K \leq Q (N)$
112	75 111	mtand	$⊢ (N \in ℕ \land K \in ℤ_{\geq 2}) \to \neg K^{2} ∥ (\frac{N}{{Q (N)}^{2}})$
113	112	ex	$⊢ N \in ℕ \to (K \in ℤ_{\geq 2} \to \neg K^{2} ∥ (\frac{N}{{Q (N)}^{2}}))$
114	49 55 113	3jca	$⊢ N \in ℕ \to (Q (N) \in ℕ \land {Q (N)}^{2} ∥ N \land (K \in ℤ_{\geq 2} \to \neg K^{2} ∥ (\frac{N}{{Q (N)}^{2}})))$

Metamath Proof Explorer

Theorem prmreclem1

Proof