Metamath Proof Explorer

Theorem qnumdencoprm

Description: The canonical representation of a rational is fully reduced. (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion qnumdencoprm ⊢ A ∈ ℚ → numer ⁡ A gcd denom ⁡ A = 1

Proof

Step Hyp Ref Expression
1 eqidd ⊢ A ∈ ℚ → numer ⁡ A = numer ⁡ A
2 eqid ⊢ denom ⁡ A = denom ⁡ A
3 1 2 jctir ⊢ A ∈ ℚ → numer ⁡ A = numer ⁡ A ∧ denom ⁡ A = denom ⁡ A
4 qnumcl ⊢ A ∈ ℚ → numer ⁡ A ∈ ℤ
5 qdencl ⊢ A ∈ ℚ → denom ⁡ A ∈ ℕ
6 qnumdenbi ⊢ A ∈ ℚ ∧ numer ⁡ A ∈ ℤ ∧ denom ⁡ A ∈ ℕ → numer ⁡ A gcd denom ⁡ A = 1 ∧ A = numer ⁡ A denom ⁡ A ↔ numer ⁡ A = numer ⁡ A ∧ denom ⁡ A = denom ⁡ A
7 4 5 6 mpd3an23 ⊢ A ∈ ℚ → numer ⁡ A gcd denom ⁡ A = 1 ∧ A = numer ⁡ A denom ⁡ A ↔ numer ⁡ A = numer ⁡ A ∧ denom ⁡ A = denom ⁡ A
8 3 7 mpbird ⊢ A ∈ ℚ → numer ⁡ A gcd denom ⁡ A = 1 ∧ A = numer ⁡ A denom ⁡ A
9 8 simpld ⊢ A ∈ ℚ → numer ⁡ A gcd denom ⁡ A = 1