Theorem gcd1

Description: The gcd of a number with 1 is 1. Theorem 1.4(d)1 in ApostolNT p. 16. (Contributed by Mario Carneiro, 19-Feb-2014)

	Ref	Expression
Assertion	gcd1	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 gcd 1 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		1z	⊢ 1 ∈ ℤ
2		gcddvds	⊢ ( ( 𝑀 ∈ ℤ ∧ 1 ∈ ℤ ) → ( ( 𝑀 gcd 1 ) ∥ 𝑀 ∧ ( 𝑀 gcd 1 ) ∥ 1 ) )
3	1 2	mpan2	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 gcd 1 ) ∥ 𝑀 ∧ ( 𝑀 gcd 1 ) ∥ 1 ) )
4	3	simprd	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 gcd 1 ) ∥ 1 )
5		ax-1ne0	⊢ 1 ≠ 0
6		simpr	⊢ ( ( 𝑀 = 0 ∧ 1 = 0 ) → 1 = 0 )
7	6	necon3ai	⊢ ( 1 ≠ 0 → ¬ ( 𝑀 = 0 ∧ 1 = 0 ) )
8	5 7	ax-mp	⊢ ¬ ( 𝑀 = 0 ∧ 1 = 0 )
9		gcdn0cl	⊢ ( ( ( 𝑀 ∈ ℤ ∧ 1 ∈ ℤ ) ∧ ¬ ( 𝑀 = 0 ∧ 1 = 0 ) ) → ( 𝑀 gcd 1 ) ∈ ℕ )
10	8 9	mpan2	⊢ ( ( 𝑀 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 𝑀 gcd 1 ) ∈ ℕ )
11	1 10	mpan2	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 gcd 1 ) ∈ ℕ )
12	11	nnzd	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 gcd 1 ) ∈ ℤ )
13		1nn	⊢ 1 ∈ ℕ
14		dvdsle	⊢ ( ( ( 𝑀 gcd 1 ) ∈ ℤ ∧ 1 ∈ ℕ ) → ( ( 𝑀 gcd 1 ) ∥ 1 → ( 𝑀 gcd 1 ) ≤ 1 ) )
15	12 13 14	sylancl	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 gcd 1 ) ∥ 1 → ( 𝑀 gcd 1 ) ≤ 1 ) )
16	4 15	mpd	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 gcd 1 ) ≤ 1 )
17		nnle1eq1	⊢ ( ( 𝑀 gcd 1 ) ∈ ℕ → ( ( 𝑀 gcd 1 ) ≤ 1 ↔ ( 𝑀 gcd 1 ) = 1 ) )
18	11 17	syl	⊢ ( 𝑀 ∈ ℤ → ( ( 𝑀 gcd 1 ) ≤ 1 ↔ ( 𝑀 gcd 1 ) = 1 ) )
19	16 18	mpbid	⊢ ( 𝑀 ∈ ℤ → ( 𝑀 gcd 1 ) = 1 )