nn0gcdsq

Description: Squaring commutes with GCD, in particular two coprime numbers have coprime squares. (Contributed by Stefan O'Rear, 15-Sep-2014)

		Ref	Expression
	Assertion	nn0gcdsq	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to {(A \gcd B)}^{2} = A^{2} \gcd B^{2}$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ A \in ℕ_{0} \leftrightarrow (A \in ℕ \lor A = 0)$
2		elnn0	$⊢ B \in ℕ_{0} \leftrightarrow (B \in ℕ \lor B = 0)$
3		sqgcd	$⊢ (A \in ℕ \land B \in ℕ) \to {(A \gcd B)}^{2} = A^{2} \gcd B^{2}$
4		nncn	$⊢ B \in ℕ \to B \in ℂ$
5		abssq	$⊢ B \in ℂ \to {\|B\|}^{2} = \|B^{2}\|$
6	4 5	syl	$⊢ B \in ℕ \to {\|B\|}^{2} = \|B^{2}\|$
7		nnz	$⊢ B \in ℕ \to B \in ℤ$
8		gcd0id	$⊢ B \in ℤ \to 0 \gcd B = \|B\|$
9	7 8	syl	$⊢ B \in ℕ \to 0 \gcd B = \|B\|$
10	9	oveq1d	$⊢ B \in ℕ \to {(0 \gcd B)}^{2} = {\|B\|}^{2}$
11		sq0	$⊢ 0^{2} = 0$
12	11	a1i	$⊢ B \in ℕ \to 0^{2} = 0$
13	12	oveq1d	$⊢ B \in ℕ \to 0^{2} \gcd B^{2} = 0 \gcd B^{2}$
14		zsqcl	$⊢ B \in ℤ \to B^{2} \in ℤ$
15		gcd0id	$⊢ B^{2} \in ℤ \to 0 \gcd B^{2} = \|B^{2}\|$
16	7 14 15	3syl	$⊢ B \in ℕ \to 0 \gcd B^{2} = \|B^{2}\|$
17	13 16	eqtrd	$⊢ B \in ℕ \to 0^{2} \gcd B^{2} = \|B^{2}\|$
18	6 10 17	3eqtr4d	$⊢ B \in ℕ \to {(0 \gcd B)}^{2} = 0^{2} \gcd B^{2}$
19	18	adantl	$⊢ (A = 0 \land B \in ℕ) \to {(0 \gcd B)}^{2} = 0^{2} \gcd B^{2}$
20		oveq1	$⊢ A = 0 \to A \gcd B = 0 \gcd B$
21	20	oveq1d	$⊢ A = 0 \to {(A \gcd B)}^{2} = {(0 \gcd B)}^{2}$
22		oveq1	$⊢ A = 0 \to A^{2} = 0^{2}$
23	22	oveq1d	$⊢ A = 0 \to A^{2} \gcd B^{2} = 0^{2} \gcd B^{2}$
24	21 23	eqeq12d	$⊢ A = 0 \to ({(A \gcd B)}^{2} = A^{2} \gcd B^{2} \leftrightarrow {(0 \gcd B)}^{2} = 0^{2} \gcd B^{2})$
25	24	adantr	$⊢ (A = 0 \land B \in ℕ) \to ({(A \gcd B)}^{2} = A^{2} \gcd B^{2} \leftrightarrow {(0 \gcd B)}^{2} = 0^{2} \gcd B^{2})$
26	19 25	mpbird	$⊢ (A = 0 \land B \in ℕ) \to {(A \gcd B)}^{2} = A^{2} \gcd B^{2}$
27		nncn	$⊢ A \in ℕ \to A \in ℂ$
28		abssq	$⊢ A \in ℂ \to {\|A\|}^{2} = \|A^{2}\|$
29	27 28	syl	$⊢ A \in ℕ \to {\|A\|}^{2} = \|A^{2}\|$
30		nnz	$⊢ A \in ℕ \to A \in ℤ$
31		gcdid0	$⊢ A \in ℤ \to A \gcd 0 = \|A\|$
32	30 31	syl	$⊢ A \in ℕ \to A \gcd 0 = \|A\|$
33	32	oveq1d	$⊢ A \in ℕ \to {(A \gcd 0)}^{2} = {\|A\|}^{2}$
34	11	a1i	$⊢ A \in ℕ \to 0^{2} = 0$
35	34	oveq2d	$⊢ A \in ℕ \to A^{2} \gcd 0^{2} = A^{2} \gcd 0$
36		zsqcl	$⊢ A \in ℤ \to A^{2} \in ℤ$
37		gcdid0	$⊢ A^{2} \in ℤ \to A^{2} \gcd 0 = \|A^{2}\|$
38	30 36 37	3syl	$⊢ A \in ℕ \to A^{2} \gcd 0 = \|A^{2}\|$
39	35 38	eqtrd	$⊢ A \in ℕ \to A^{2} \gcd 0^{2} = \|A^{2}\|$
40	29 33 39	3eqtr4d	$⊢ A \in ℕ \to {(A \gcd 0)}^{2} = A^{2} \gcd 0^{2}$
41	40	adantr	$⊢ (A \in ℕ \land B = 0) \to {(A \gcd 0)}^{2} = A^{2} \gcd 0^{2}$
42		oveq2	$⊢ B = 0 \to A \gcd B = A \gcd 0$
43	42	oveq1d	$⊢ B = 0 \to {(A \gcd B)}^{2} = {(A \gcd 0)}^{2}$
44		oveq1	$⊢ B = 0 \to B^{2} = 0^{2}$
45	44	oveq2d	$⊢ B = 0 \to A^{2} \gcd B^{2} = A^{2} \gcd 0^{2}$
46	43 45	eqeq12d	$⊢ B = 0 \to ({(A \gcd B)}^{2} = A^{2} \gcd B^{2} \leftrightarrow {(A \gcd 0)}^{2} = A^{2} \gcd 0^{2})$
47	46	adantl	$⊢ (A \in ℕ \land B = 0) \to ({(A \gcd B)}^{2} = A^{2} \gcd B^{2} \leftrightarrow {(A \gcd 0)}^{2} = A^{2} \gcd 0^{2})$
48	41 47	mpbird	$⊢ (A \in ℕ \land B = 0) \to {(A \gcd B)}^{2} = A^{2} \gcd B^{2}$
49		gcd0val	$⊢ 0 \gcd 0 = 0$
50	49	oveq1i	$⊢ {(0 \gcd 0)}^{2} = 0^{2}$
51	11 11	oveq12i	$⊢ 0^{2} \gcd 0^{2} = 0 \gcd 0$
52	51 49	eqtri	$⊢ 0^{2} \gcd 0^{2} = 0$
53	11 50 52	3eqtr4i	$⊢ {(0 \gcd 0)}^{2} = 0^{2} \gcd 0^{2}$
54		oveq12	$⊢ (A = 0 \land B = 0) \to A \gcd B = 0 \gcd 0$
55	54	oveq1d	$⊢ (A = 0 \land B = 0) \to {(A \gcd B)}^{2} = {(0 \gcd 0)}^{2}$
56	22 44	oveqan12d	$⊢ (A = 0 \land B = 0) \to A^{2} \gcd B^{2} = 0^{2} \gcd 0^{2}$
57	53 55 56	3eqtr4a	$⊢ (A = 0 \land B = 0) \to {(A \gcd B)}^{2} = A^{2} \gcd B^{2}$
58	3 26 48 57	ccase	$⊢ ((A \in ℕ \lor A = 0) \land (B \in ℕ \lor B = 0)) \to {(A \gcd B)}^{2} = A^{2} \gcd B^{2}$
59	1 2 58	syl2anb	$⊢ (A \in ℕ_{0} \land B \in ℕ_{0}) \to {(A \gcd B)}^{2} = A^{2} \gcd B^{2}$

Metamath Proof Explorer

Theorem nn0gcdsq

Proof