**Description:** The GCD of one and an integer is one. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref | Expression | ||
---|---|---|---|

Assertion | 1gcd | ⊢ ( 𝑀 ∈ ℤ → ( 1 gcd 𝑀 ) = 1 ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | 1z | ⊢ 1 ∈ ℤ | |

2 | gcdcom | ⊢ ( ( 1 ∈ ℤ ∧ 𝑀 ∈ ℤ ) → ( 1 gcd 𝑀 ) = ( 𝑀 gcd 1 ) ) | |

3 | 1 2 | mpan | ⊢ ( 𝑀 ∈ ℤ → ( 1 gcd 𝑀 ) = ( 𝑀 gcd 1 ) ) |

4 | gcd1 | ⊢ ( 𝑀 ∈ ℤ → ( 𝑀 gcd 1 ) = 1 ) | |

5 | 3 4 | eqtrd | ⊢ ( 𝑀 ∈ ℤ → ( 1 gcd 𝑀 ) = 1 ) |