Metamath Proof Explorer

Theorem qnumdencl

Description: Lemma for qnumcl and qdencl . (Contributed by Stefan O'Rear, 13-Sep-2014)

Ref Expression
Assertion qnumdencl ⊢ A ∈ ℚ → numer ⁡ A ∈ ℤ ∧ denom ⁡ A ∈ ℕ

Proof

Step Hyp Ref Expression
1 qredeu ⊢ A ∈ ℚ → ∃! a ∈ ℤ × ℕ 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a
2 riotacl ⊢ ∃! a ∈ ℤ × ℕ 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a → ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℤ × ℕ
3 1 2 syl ⊢ A ∈ ℚ → ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℤ × ℕ
4 elxp6 ⊢ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℤ × ℕ ↔ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a = 1 st ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a 2 nd ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∧ 1 st ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℤ ∧ 2 nd ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℕ
5 qnumval ⊢ A ∈ ℚ → numer ⁡ A = 1 st ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a
6 5 eleq1d ⊢ A ∈ ℚ → numer ⁡ A ∈ ℤ ↔ 1 st ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℤ
7 qdenval ⊢ A ∈ ℚ → denom ⁡ A = 2 nd ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a
8 7 eleq1d ⊢ A ∈ ℚ → denom ⁡ A ∈ ℕ ↔ 2 nd ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℕ
9 6 8 anbi12d ⊢ A ∈ ℚ → numer ⁡ A ∈ ℤ ∧ denom ⁡ A ∈ ℕ ↔ 1 st ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℤ ∧ 2 nd ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℕ
10 9 biimprd ⊢ A ∈ ℚ → 1 st ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℤ ∧ 2 nd ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℕ → numer ⁡ A ∈ ℤ ∧ denom ⁡ A ∈ ℕ
11 10 adantld ⊢ A ∈ ℚ → ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a = 1 st ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a 2 nd ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∧ 1 st ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℤ ∧ 2 nd ⁡ ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℕ → numer ⁡ A ∈ ℤ ∧ denom ⁡ A ∈ ℕ
12 4 11 syl5bi ⊢ A ∈ ℚ → ι a ∈ ℤ × ℕ | 1 st ⁡ a gcd 2 nd ⁡ a = 1 ∧ A = 1 st ⁡ a 2 nd ⁡ a ∈ ℤ × ℕ → numer ⁡ A ∈ ℤ ∧ denom ⁡ A ∈ ℕ
13 3 12 mpd ⊢ A ∈ ℚ → numer ⁡ A ∈ ℤ ∧ denom ⁡ A ∈ ℕ