Metamath Proof Explorer

Theorem qnumdencl

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

		Ref	Expression
	Assertion	qnumdencl	⊢ ( 𝐴 ∈ ℚ → ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		qredeu	⊢ ( 𝐴 ∈ ℚ → ∃! 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) )
2		riotacl	⊢ ( ∃! 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) → ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ∈ ( ℤ × ℕ ) )
3	1 2	syl	⊢ ( 𝐴 ∈ ℚ → ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ∈ ( ℤ × ℕ ) )
4		elxp6	⊢ ( ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ∈ ( ℤ × ℕ ) ↔ ( ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) = ⟨ ( 1^st ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) , ( 2^nd ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ⟩ ∧ ( ( 1^st ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ∈ ℤ ∧ ( 2^nd ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ∈ ℕ ) ) )
5		qnumval	⊢ ( 𝐴 ∈ ℚ → ( numer ‘ 𝐴 ) = ( 1^st ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) )
6	5	eleq1d	⊢ ( 𝐴 ∈ ℚ → ( ( numer ‘ 𝐴 ) ∈ ℤ ↔ ( 1^st ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ∈ ℤ ) )
7		qdenval	⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) = ( 2^nd ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) )
8	7	eleq1d	⊢ ( 𝐴 ∈ ℚ → ( ( denom ‘ 𝐴 ) ∈ ℕ ↔ ( 2^nd ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ∈ ℕ ) )
9	6 8	anbi12d	⊢ ( 𝐴 ∈ ℚ → ( ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℕ ) ↔ ( ( 1^st ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ∈ ℤ ∧ ( 2^nd ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ∈ ℕ ) ) )
10	9	biimprd	⊢ ( 𝐴 ∈ ℚ → ( ( ( 1^st ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ∈ ℤ ∧ ( 2^nd ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ∈ ℕ ) → ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℕ ) ) )
11	10	adantld	⊢ ( 𝐴 ∈ ℚ → ( ( ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) = ⟨ ( 1^st ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) , ( 2^nd ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ⟩ ∧ ( ( 1^st ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ∈ ℤ ∧ ( 2^nd ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) ∈ ℕ ) ) → ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℕ ) ) )
12	4 11	syl5bi	⊢ ( 𝐴 ∈ ℚ → ( ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ∈ ( ℤ × ℕ ) → ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℕ ) ) )
13	3 12	mpd	⊢ ( 𝐴 ∈ ℚ → ( ( numer ‘ 𝐴 ) ∈ ℤ ∧ ( denom ‘ 𝐴 ) ∈ ℕ ) )