gcdneg

Description: Negating one operand of the gcd operator does not alter the result. (Contributed by Paul Chapman, 21-Mar-2011)

		Ref	Expression
	Assertion	gcdneg	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd -N = M \gcd N$

Proof

Step	Hyp	Ref	Expression
1		oveq12	$⊢ (M = 0 \land N = 0) \to M \gcd N = 0 \gcd 0$
2	1	adantl	$⊢ ((M \in ℤ \land N \in ℤ) \land (M = 0 \land N = 0)) \to M \gcd N = 0 \gcd 0$
3		zcn	$⊢ N \in ℤ \to N \in ℂ$
4	3	negeq0d	$⊢ N \in ℤ \to (N = 0 \leftrightarrow - N = 0)$
5	4	anbi2d	$⊢ N \in ℤ \to ((M = 0 \land N = 0) \leftrightarrow (M = 0 \land - N = 0))$
6	5	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to ((M = 0 \land N = 0) \leftrightarrow (M = 0 \land - N = 0))$
7		oveq12	$⊢ (M = 0 \land - N = 0) \to M \gcd -N = 0 \gcd 0$
8	6 7	biimtrdi	$⊢ (M \in ℤ \land N \in ℤ) \to ((M = 0 \land N = 0) \to M \gcd -N = 0 \gcd 0)$
9	8	imp	$⊢ ((M \in ℤ \land N \in ℤ) \land (M = 0 \land N = 0)) \to M \gcd -N = 0 \gcd 0$
10	2 9	eqtr4d	$⊢ ((M \in ℤ \land N \in ℤ) \land (M = 0 \land N = 0)) \to M \gcd N = M \gcd -N$
11		gcddvds	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ N)$
12		gcdcl	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℕ_{0}$
13	12	nn0zd	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℤ$
14		dvdsnegb	$⊢ (M \gcd N \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ N \leftrightarrow (M \gcd N) ∥ -N)$
15	13 14	sylancom	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ N \leftrightarrow (M \gcd N) ∥ -N)$
16	15	anbi2d	$⊢ (M \in ℤ \land N \in ℤ) \to (((M \gcd N) ∥ M \land (M \gcd N) ∥ N) \leftrightarrow ((M \gcd N) ∥ M \land (M \gcd N) ∥ -N))$
17	11 16	mpbid	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd N) ∥ M \land (M \gcd N) ∥ -N)$
18	6	notbid	$⊢ (M \in ℤ \land N \in ℤ) \to (\neg (M = 0 \land N = 0) \leftrightarrow \neg (M = 0 \land - N = 0))$
19		simpl	$⊢ (M \in ℤ \land N \in ℤ) \to M \in ℤ$
20		znegcl	$⊢ N \in ℤ \to - N \in ℤ$
21	20	adantl	$⊢ (M \in ℤ \land N \in ℤ) \to - N \in ℤ$
22		dvdslegcd	$⊢ ((M \gcd N \in ℤ \land M \in ℤ \land - N \in ℤ) \land \neg (M = 0 \land - N = 0)) \to (((M \gcd N) ∥ M \land (M \gcd N) ∥ -N) \to M \gcd N \leq M \gcd -N)$
23	22	ex	$⊢ (M \gcd N \in ℤ \land M \in ℤ \land - N \in ℤ) \to (\neg (M = 0 \land - N = 0) \to (((M \gcd N) ∥ M \land (M \gcd N) ∥ -N) \to M \gcd N \leq M \gcd -N))$
24	13 19 21 23	syl3anc	$⊢ (M \in ℤ \land N \in ℤ) \to (\neg (M = 0 \land - N = 0) \to (((M \gcd N) ∥ M \land (M \gcd N) ∥ -N) \to M \gcd N \leq M \gcd -N))$
25	18 24	sylbid	$⊢ (M \in ℤ \land N \in ℤ) \to (\neg (M = 0 \land N = 0) \to (((M \gcd N) ∥ M \land (M \gcd N) ∥ -N) \to M \gcd N \leq M \gcd -N))$
26	25	com12	$⊢ \neg (M = 0 \land N = 0) \to ((M \in ℤ \land N \in ℤ) \to (((M \gcd N) ∥ M \land (M \gcd N) ∥ -N) \to M \gcd N \leq M \gcd -N))$
27	17 26	mpdi	$⊢ \neg (M = 0 \land N = 0) \to ((M \in ℤ \land N \in ℤ) \to M \gcd N \leq M \gcd -N)$
28	27	impcom	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N \leq M \gcd -N$
29		gcddvds	$⊢ (M \in ℤ \land - N \in ℤ) \to ((M \gcd -N) ∥ M \land (M \gcd -N) ∥ -N)$
30	20 29	sylan2	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd -N) ∥ M \land (M \gcd -N) ∥ -N)$
31		gcdcl	$⊢ (M \in ℤ \land - N \in ℤ) \to M \gcd -N \in ℕ_{0}$
32	31	nn0zd	$⊢ (M \in ℤ \land - N \in ℤ) \to M \gcd -N \in ℤ$
33	20 32	sylan2	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd -N \in ℤ$
34		dvdsnegb	$⊢ (M \gcd -N \in ℤ \land N \in ℤ) \to ((M \gcd -N) ∥ N \leftrightarrow (M \gcd -N) ∥ -N)$
35	33 34	sylancom	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd -N) ∥ N \leftrightarrow (M \gcd -N) ∥ -N)$
36	35	anbi2d	$⊢ (M \in ℤ \land N \in ℤ) \to (((M \gcd -N) ∥ M \land (M \gcd -N) ∥ N) \leftrightarrow ((M \gcd -N) ∥ M \land (M \gcd -N) ∥ -N))$
37	30 36	mpbird	$⊢ (M \in ℤ \land N \in ℤ) \to ((M \gcd -N) ∥ M \land (M \gcd -N) ∥ N)$
38		simpr	$⊢ (M \in ℤ \land N \in ℤ) \to N \in ℤ$
39		dvdslegcd	$⊢ ((M \gcd -N \in ℤ \land M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (((M \gcd -N) ∥ M \land (M \gcd -N) ∥ N) \to M \gcd -N \leq M \gcd N)$
40	39	ex	$⊢ (M \gcd -N \in ℤ \land M \in ℤ \land N \in ℤ) \to (\neg (M = 0 \land N = 0) \to (((M \gcd -N) ∥ M \land (M \gcd -N) ∥ N) \to M \gcd -N \leq M \gcd N))$
41	33 19 38 40	syl3anc	$⊢ (M \in ℤ \land N \in ℤ) \to (\neg (M = 0 \land N = 0) \to (((M \gcd -N) ∥ M \land (M \gcd -N) ∥ N) \to M \gcd -N \leq M \gcd N))$
42	41	com12	$⊢ \neg (M = 0 \land N = 0) \to ((M \in ℤ \land N \in ℤ) \to (((M \gcd -N) ∥ M \land (M \gcd -N) ∥ N) \to M \gcd -N \leq M \gcd N))$
43	37 42	mpdi	$⊢ \neg (M = 0 \land N = 0) \to ((M \in ℤ \land N \in ℤ) \to M \gcd -N \leq M \gcd N)$
44	43	impcom	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd -N \leq M \gcd N$
45	13	zred	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N \in ℝ$
46	33	zred	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd -N \in ℝ$
47	45 46	letri3d	$⊢ (M \in ℤ \land N \in ℤ) \to (M \gcd N = M \gcd -N \leftrightarrow (M \gcd N \leq M \gcd -N \land M \gcd -N \leq M \gcd N))$
48	47	adantr	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to (M \gcd N = M \gcd -N \leftrightarrow (M \gcd N \leq M \gcd -N \land M \gcd -N \leq M \gcd N))$
49	28 44 48	mpbir2and	$⊢ ((M \in ℤ \land N \in ℤ) \land \neg (M = 0 \land N = 0)) \to M \gcd N = M \gcd -N$
50	10 49	pm2.61dan	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd N = M \gcd -N$
51	50	eqcomd	$⊢ (M \in ℤ \land N \in ℤ) \to M \gcd -N = M \gcd N$

Metamath Proof Explorer

Theorem gcdneg

Proof