qnumdenbi

Description: Two numbers are the canonical representation of a rational iff they are coprime and have the right quotient. (Contributed by Stefan O'Rear, 13-Sep-2014)

		Ref	Expression
	Assertion	qnumdenbi	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝐵 gcd 𝐶 ) = 1 ∧ 𝐴 = ( 𝐵 / 𝐶 ) ) ↔ ( ( 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		1st2nd2	⊢ ( ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 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 ‘ 𝑎 ) ) ) ) ) ⟩ )
4	1 2 3	3syl	⊢ ( 𝐴 ∈ ℚ → ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 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		qdenval	⊢ ( 𝐴 ∈ ℚ → ( denom ‘ 𝐴 ) = ( 2^nd ‘ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) ) )
7	5 6	opeq12d	⊢ ( 𝐴 ∈ ℚ → ⟨ ( 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 ‘ 𝑎 ) ) ) ) ) ⟩ )
8	4 7	eqtr4d	⊢ ( 𝐴 ∈ ℚ → ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) = ⟨ ( numer ‘ 𝐴 ) , ( denom ‘ 𝐴 ) ⟩ )
9	8	eqeq1d	⊢ ( 𝐴 ∈ ℚ → ( ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) = ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ ( numer ‘ 𝐴 ) , ( denom ‘ 𝐴 ) ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) )
10	9	3ad2ant1	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) = ⟨ 𝐵 , 𝐶 ⟩ ↔ ⟨ ( numer ‘ 𝐴 ) , ( denom ‘ 𝐴 ) ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ) )
11		fvex	⊢ ( numer ‘ 𝐴 ) ∈ V
12		fvex	⊢ ( denom ‘ 𝐴 ) ∈ V
13	11 12	opth	⊢ ( ⟨ ( numer ‘ 𝐴 ) , ( denom ‘ 𝐴 ) ⟩ = ⟨ 𝐵 , 𝐶 ⟩ ↔ ( ( numer ‘ 𝐴 ) = 𝐵 ∧ ( denom ‘ 𝐴 ) = 𝐶 ) )
14	10 13	bitr2di	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( numer ‘ 𝐴 ) = 𝐵 ∧ ( denom ‘ 𝐴 ) = 𝐶 ) ↔ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) = ⟨ 𝐵 , 𝐶 ⟩ ) )
15		opelxpi	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ⟨ 𝐵 , 𝐶 ⟩ ∈ ( ℤ × ℕ ) )
16	15	3adant1	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ⟨ 𝐵 , 𝐶 ⟩ ∈ ( ℤ × ℕ ) )
17	1	3ad2ant1	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ∃! 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) )
18		fveq2	⊢ ( 𝑎 = ⟨ 𝐵 , 𝐶 ⟩ → ( 1^st ‘ 𝑎 ) = ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) )
19		fveq2	⊢ ( 𝑎 = ⟨ 𝐵 , 𝐶 ⟩ → ( 2^nd ‘ 𝑎 ) = ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) )
20	18 19	oveq12d	⊢ ( 𝑎 = ⟨ 𝐵 , 𝐶 ⟩ → ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) gcd ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) )
21	20	eqeq1d	⊢ ( 𝑎 = ⟨ 𝐵 , 𝐶 ⟩ → ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ↔ ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) gcd ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) = 1 ) )
22	18 19	oveq12d	⊢ ( 𝑎 = ⟨ 𝐵 , 𝐶 ⟩ → ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) = ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) / ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) )
23	22	eqeq2d	⊢ ( 𝑎 = ⟨ 𝐵 , 𝐶 ⟩ → ( 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ↔ 𝐴 = ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) / ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) ) )
24	21 23	anbi12d	⊢ ( 𝑎 = ⟨ 𝐵 , 𝐶 ⟩ → ( ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ↔ ( ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) gcd ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) / ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) ) ) )
25	24	riota2	⊢ ( ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( ℤ × ℕ ) ∧ ∃! 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) → ( ( ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) gcd ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) / ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) ) ↔ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) = ⟨ 𝐵 , 𝐶 ⟩ ) )
26	16 17 25	syl2anc	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) gcd ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) / ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) ) ↔ ( ℩ 𝑎 ∈ ( ℤ × ℕ ) ( ( ( 1^st ‘ 𝑎 ) gcd ( 2^nd ‘ 𝑎 ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ 𝑎 ) / ( 2^nd ‘ 𝑎 ) ) ) ) = ⟨ 𝐵 , 𝐶 ⟩ ) )
27		op1stg	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = 𝐵 )
28		op2ndg	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = 𝐶 )
29	27 28	oveq12d	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) gcd ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) = ( 𝐵 gcd 𝐶 ) )
30	29	3adant1	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) gcd ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) = ( 𝐵 gcd 𝐶 ) )
31	30	eqeq1d	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) gcd ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) = 1 ↔ ( 𝐵 gcd 𝐶 ) = 1 ) )
32	27	3adant1	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = 𝐵 )
33	28	3adant1	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) = 𝐶 )
34	32 33	oveq12d	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) / ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) = ( 𝐵 / 𝐶 ) )
35	34	eqeq2d	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐴 = ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) / ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) ↔ 𝐴 = ( 𝐵 / 𝐶 ) ) )
36	31 35	anbi12d	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) gcd ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) = 1 ∧ 𝐴 = ( ( 1^st ‘ ⟨ 𝐵 , 𝐶 ⟩ ) / ( 2^nd ‘ ⟨ 𝐵 , 𝐶 ⟩ ) ) ) ↔ ( ( 𝐵 gcd 𝐶 ) = 1 ∧ 𝐴 = ( 𝐵 / 𝐶 ) ) ) )
37	14 26 36	3bitr2rd	⊢ ( ( 𝐴 ∈ ℚ ∧ 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( ( ( 𝐵 gcd 𝐶 ) = 1 ∧ 𝐴 = ( 𝐵 / 𝐶 ) ) ↔ ( ( numer ‘ 𝐴 ) = 𝐵 ∧ ( denom ‘ 𝐴 ) = 𝐶 ) ) )

Metamath Proof Explorer

Theorem qnumdenbi

Proof