Metamath Proof Explorer

Theorem zdend

Description: Denominator of an integer. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypothesis znumd.1 ⊢ φ → Z ∈ ℤ
Assertion zdend ⊢ φ → denom ⁡ Z = 1

Proof

Step Hyp Ref Expression
1 znumd.1 ⊢ φ → Z ∈ ℤ
2 zq ⊢ Z ∈ ℤ → Z ∈ ℚ
3 1 2 syl ⊢ φ → Z ∈ ℚ
4 1nn ⊢ 1 ∈ ℕ
5 4 a1i ⊢ φ → 1 ∈ ℕ
6 gcd1 ⊢ Z ∈ ℤ → Z gcd 1 = 1
7 1 6 syl ⊢ φ → Z gcd 1 = 1
8 1 zcnd ⊢ φ → Z ∈ ℂ
9 8 div1d ⊢ φ → Z 1 = Z
10 9 eqcomd ⊢ φ → Z = Z 1
11 qnumdenbi ⊢ Z ∈ ℚ ∧ Z ∈ ℤ ∧ 1 ∈ ℕ → Z gcd 1 = 1 ∧ Z = Z 1 ↔ numer ⁡ Z = Z ∧ denom ⁡ Z = 1
12 11 biimpa ⊢ Z ∈ ℚ ∧ Z ∈ ℤ ∧ 1 ∈ ℕ ∧ Z gcd 1 = 1 ∧ Z = Z 1 → numer ⁡ Z = Z ∧ denom ⁡ Z = 1
13 3 1 5 7 10 12 syl32anc ⊢ φ → numer ⁡ Z = Z ∧ denom ⁡ Z = 1
14 13 simprd ⊢ φ → denom ⁡ Z = 1