sqgcd

Description: Square distributes over gcd. (Contributed by Scott Fenton, 18-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	sqgcd	$⊢ (M \in ℕ \land N \in ℕ) \to {(M \gcd N)}^{2} = M^{2} \gcd N^{2}$

Proof

Step	Hyp	Ref	Expression
1		gcdnncl	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℕ$
2	1	nnsqcld	$⊢ (M \in ℕ \land N \in ℕ) \to {(M \gcd N)}^{2} \in ℕ$
3	2	nncnd	$⊢ (M \in ℕ \land N \in ℕ) \to {(M \gcd N)}^{2} \in ℂ$
4	3	mulid1d	$⊢ (M \in ℕ \land N \in ℕ) \to {(M \gcd N)}^{2} \cdot 1 = {(M \gcd N)}^{2}$
5		nnsqcl	$⊢ M \in ℕ \to M^{2} \in ℕ$
6	5	nnzd	$⊢ M \in ℕ \to M^{2} \in ℤ$
7	6	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to M^{2} \in ℤ$
8		nnsqcl	$⊢ N \in ℕ \to N^{2} \in ℕ$
9	8	nnzd	$⊢ N \in ℕ \to N^{2} \in ℤ$
10	9	adantl	$⊢ (M \in ℕ \land N \in ℕ) \to N^{2} \in ℤ$
11		nnz	$⊢ M \in ℕ \to M \in ℤ$
12		nnz	$⊢ N \in ℕ \to N \in ℤ$
13		gcddvds	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
14	11 12 13	syl2an	$⊢ (M \in ℕ \land N \in ℕ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
15	14	simpld	$⊢ (M \in ℕ \land N \in ℕ) \to (M \gcd N) ∥ M$
16	1	nnzd	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℤ$
17	11	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to M \in ℤ$
18		dvdssqim	$⊢ (M \gcd N \in ℤ \land M \in ℤ) \to ((M \gcd N) ∥ M \to {(M \gcd N)}^{2} ∥ M^{2})$
19	16 17 18	syl2anc	$⊢ (M \in ℕ \land N \in ℕ) \to ((M \gcd N) ∥ M \to {(M \gcd N)}^{2} ∥ M^{2})$
20	15 19	mpd	$⊢ (M \in ℕ \land N \in ℕ) \to {(M \gcd N)}^{2} ∥ M^{2}$
21	14	simprd	$⊢ (M \in ℕ \land N \in ℕ) \to (M \gcd N) ∥ N$
22	12	adantl	$⊢ (M \in ℕ \land N \in ℕ) \to N \in ℤ$
23		dvdssqim	$⊢ (M \gcd N \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ N \to {(M \gcd N)}^{2} ∥ N^{2})$
24	16 22 23	syl2anc	$⊢ (M \in ℕ \land N \in ℕ) \to ((M \gcd N) ∥ N \to {(M \gcd N)}^{2} ∥ N^{2})$
25	21 24	mpd	$⊢ (M \in ℕ \land N \in ℕ) \to {(M \gcd N)}^{2} ∥ N^{2}$
26		gcddiv	$⊢ ((M^{2} \in ℤ \land N^{2} \in ℤ \land {(M \gcd N)}^{2} \in ℕ) \land ({(M \gcd N)}^{2} ∥ M^{2} \land {(M \gcd N)}^{2} ∥ N^{2})) \to \frac{M^{2} \gcd N^{2}}{{(M \gcd N)}^{2}} = (\frac{M^{2}}{{(M \gcd N)}^{2}}) \gcd (\frac{N^{2}}{{(M \gcd N)}^{2}})$
27	7 10 2 20 25 26	syl32anc	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M^{2} \gcd N^{2}}{{(M \gcd N)}^{2}} = (\frac{M^{2}}{{(M \gcd N)}^{2}}) \gcd (\frac{N^{2}}{{(M \gcd N)}^{2}})$
28		nncn	$⊢ M \in ℕ \to M \in ℂ$
29	28	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to M \in ℂ$
30	1	nncnd	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℂ$
31	1	nnne0d	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \neq 0$
32	29 30 31	sqdivd	$⊢ (M \in ℕ \land N \in ℕ) \to {(\frac{M}{M \gcd N})}^{2} = \frac{M^{2}}{{(M \gcd N)}^{2}}$
33		nncn	$⊢ N \in ℕ \to N \in ℂ$
34	33	adantl	$⊢ (M \in ℕ \land N \in ℕ) \to N \in ℂ$
35	34 30 31	sqdivd	$⊢ (M \in ℕ \land N \in ℕ) \to {(\frac{N}{M \gcd N})}^{2} = \frac{N^{2}}{{(M \gcd N)}^{2}}$
36	32 35	oveq12d	$⊢ (M \in ℕ \land N \in ℕ) \to {(\frac{M}{M \gcd N})}^{2} \gcd {(\frac{N}{M \gcd N})}^{2} = (\frac{M^{2}}{{(M \gcd N)}^{2}}) \gcd (\frac{N^{2}}{{(M \gcd N)}^{2}})$
37		gcddiv	$⊢ ((M \in ℤ \land N \in ℤ \land M \gcd N \in ℕ) \land ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)) \to \frac{M \gcd N}{M \gcd N} = (\frac{M}{M \gcd N}) \gcd (\frac{N}{M \gcd N})$
38	17 22 1 14 37	syl31anc	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \gcd N}{M \gcd N} = (\frac{M}{M \gcd N}) \gcd (\frac{N}{M \gcd N})$
39	30 31	dividd	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M \gcd N}{M \gcd N} = 1$
40	38 39	eqtr3d	$⊢ (M \in ℕ \land N \in ℕ) \to (\frac{M}{M \gcd N}) \gcd (\frac{N}{M \gcd N}) = 1$
41		dvdsval2	$⊢ (M \gcd N \in ℤ \land M \gcd N \neq 0 \land M \in ℤ) \to ((M \gcd N) ∥ M \leftrightarrow \frac{M}{M \gcd N} \in ℤ)$
42	16 31 17 41	syl3anc	$⊢ (M \in ℕ \land N \in ℕ) \to ((M \gcd N) ∥ M \leftrightarrow \frac{M}{M \gcd N} \in ℤ)$
43	15 42	mpbid	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M}{M \gcd N} \in ℤ$
44		nnre	$⊢ M \in ℕ \to M \in ℝ$
45	44	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to M \in ℝ$
46	1	nnred	$⊢ (M \in ℕ \land N \in ℕ) \to M \gcd N \in ℝ$
47		nngt0	$⊢ M \in ℕ \to 0 < M$
48	47	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to 0 < M$
49	1	nngt0d	$⊢ (M \in ℕ \land N \in ℕ) \to 0 < M \gcd N$
50	45 46 48 49	divgt0d	$⊢ (M \in ℕ \land N \in ℕ) \to 0 < \frac{M}{M \gcd N}$
51		elnnz	$⊢ \frac{M}{M \gcd N} \in ℕ \leftrightarrow (\frac{M}{M \gcd N} \in ℤ \land 0 < \frac{M}{M \gcd N})$
52	43 50 51	sylanbrc	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M}{M \gcd N} \in ℕ$
53		dvdsval2	$⊢ (M \gcd N \in ℤ \land M \gcd N \neq 0 \land N \in ℤ) \to ((M \gcd N) ∥ N \leftrightarrow \frac{N}{M \gcd N} \in ℤ)$
54	16 31 22 53	syl3anc	$⊢ (M \in ℕ \land N \in ℕ) \to ((M \gcd N) ∥ N \leftrightarrow \frac{N}{M \gcd N} \in ℤ)$
55	21 54	mpbid	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{N}{M \gcd N} \in ℤ$
56		nnre	$⊢ N \in ℕ \to N \in ℝ$
57	56	adantl	$⊢ (M \in ℕ \land N \in ℕ) \to N \in ℝ$
58		nngt0	$⊢ N \in ℕ \to 0 < N$
59	58	adantl	$⊢ (M \in ℕ \land N \in ℕ) \to 0 < N$
60	57 46 59 49	divgt0d	$⊢ (M \in ℕ \land N \in ℕ) \to 0 < \frac{N}{M \gcd N}$
61		elnnz	$⊢ \frac{N}{M \gcd N} \in ℕ \leftrightarrow (\frac{N}{M \gcd N} \in ℤ \land 0 < \frac{N}{M \gcd N})$
62	55 60 61	sylanbrc	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{N}{M \gcd N} \in ℕ$
63		2nn	$⊢ 2 \in ℕ$
64		rppwr	$⊢ (\frac{M}{M \gcd N} \in ℕ \land \frac{N}{M \gcd N} \in ℕ \land 2 \in ℕ) \to ((\frac{M}{M \gcd N}) \gcd (\frac{N}{M \gcd N}) = 1 \to {(\frac{M}{M \gcd N})}^{2} \gcd {(\frac{N}{M \gcd N})}^{2} = 1)$
65	63 64	mp3an3	$⊢ (\frac{M}{M \gcd N} \in ℕ \land \frac{N}{M \gcd N} \in ℕ) \to ((\frac{M}{M \gcd N}) \gcd (\frac{N}{M \gcd N}) = 1 \to {(\frac{M}{M \gcd N})}^{2} \gcd {(\frac{N}{M \gcd N})}^{2} = 1)$
66	52 62 65	syl2anc	$⊢ (M \in ℕ \land N \in ℕ) \to ((\frac{M}{M \gcd N}) \gcd (\frac{N}{M \gcd N}) = 1 \to {(\frac{M}{M \gcd N})}^{2} \gcd {(\frac{N}{M \gcd N})}^{2} = 1)$
67	40 66	mpd	$⊢ (M \in ℕ \land N \in ℕ) \to {(\frac{M}{M \gcd N})}^{2} \gcd {(\frac{N}{M \gcd N})}^{2} = 1$
68	27 36 67	3eqtr2d	$⊢ (M \in ℕ \land N \in ℕ) \to \frac{M^{2} \gcd N^{2}}{{(M \gcd N)}^{2}} = 1$
69	6 9	anim12i	$⊢ (M \in ℕ \land N \in ℕ) \to (M^{2} \in ℤ \land N^{2} \in ℤ)$
70	5	nnne0d	$⊢ M \in ℕ \to M^{2} \neq 0$
71	70	neneqd	$⊢ M \in ℕ \to \neg M^{2} = 0$
72	71	intnanrd	$⊢ M \in ℕ \to \neg (M^{2} = 0 \land N^{2} = 0)$
73	72	adantr	$⊢ (M \in ℕ \land N \in ℕ) \to \neg (M^{2} = 0 \land N^{2} = 0)$
74		gcdn0cl	$⊢ ((M^{2} \in ℤ \land N^{2} \in ℤ) \land \neg (M^{2} = 0 \land N^{2} = 0)) \to M^{2} \gcd N^{2} \in ℕ$
75	69 73 74	syl2anc	$⊢ (M \in ℕ \land N \in ℕ) \to M^{2} \gcd N^{2} \in ℕ$
76	75	nncnd	$⊢ (M \in ℕ \land N \in ℕ) \to M^{2} \gcd N^{2} \in ℂ$
77	2	nnne0d	$⊢ (M \in ℕ \land N \in ℕ) \to {(M \gcd N)}^{2} \neq 0$
78		ax-1cn	$⊢ 1 \in ℂ$
79		divmul	$⊢ (M^{2} \gcd N^{2} \in ℂ \land 1 \in ℂ \land ({(M \gcd N)}^{2} \in ℂ \land {(M \gcd N)}^{2} \neq 0)) \to (\frac{M^{2} \gcd N^{2}}{{(M \gcd N)}^{2}} = 1 \leftrightarrow {(M \gcd N)}^{2} \cdot 1 = M^{2} \gcd N^{2})$
80	78 79	mp3an2	$⊢ (M^{2} \gcd N^{2} \in ℂ \land ({(M \gcd N)}^{2} \in ℂ \land {(M \gcd N)}^{2} \neq 0)) \to (\frac{M^{2} \gcd N^{2}}{{(M \gcd N)}^{2}} = 1 \leftrightarrow {(M \gcd N)}^{2} \cdot 1 = M^{2} \gcd N^{2})$
81	76 3 77 80	syl12anc	$⊢ (M \in ℕ \land N \in ℕ) \to (\frac{M^{2} \gcd N^{2}}{{(M \gcd N)}^{2}} = 1 \leftrightarrow {(M \gcd N)}^{2} \cdot 1 = M^{2} \gcd N^{2})$
82	68 81	mpbid	$⊢ (M \in ℕ \land N \in ℕ) \to {(M \gcd N)}^{2} \cdot 1 = M^{2} \gcd N^{2}$
83	4 82	eqtr3d	$⊢ (M \in ℕ \land N \in ℕ) \to {(M \gcd N)}^{2} = M^{2} \gcd N^{2}$

Metamath Proof Explorer

Theorem sqgcd

Proof