This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem enqbreq2

Description: Equivalence relation for positive fractions in terms of positive integers. (Contributed by Mario Carneiro, 8-May-2013) (New usage is discouraged.)

		Ref	Expression
	Assertion	enqbreq2	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ~_Q 𝐵 ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	⊢ ( 𝐴 ∈ ( N × N ) → 𝐴 = ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ )
2		1st2nd2	⊢ ( 𝐵 ∈ ( N × N ) → 𝐵 = ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ )
3	1 2	breqan12d	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ~_Q 𝐵 ↔ ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ~_Q ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ) )
4		xp1st	⊢ ( 𝐴 ∈ ( N × N ) → ( 1^st ‘ 𝐴 ) ∈ N )
5		xp2nd	⊢ ( 𝐴 ∈ ( N × N ) → ( 2^nd ‘ 𝐴 ) ∈ N )
6	4 5	jca	⊢ ( 𝐴 ∈ ( N × N ) → ( ( 1^st ‘ 𝐴 ) ∈ N ∧ ( 2^nd ‘ 𝐴 ) ∈ N ) )
7		xp1st	⊢ ( 𝐵 ∈ ( N × N ) → ( 1^st ‘ 𝐵 ) ∈ N )
8		xp2nd	⊢ ( 𝐵 ∈ ( N × N ) → ( 2^nd ‘ 𝐵 ) ∈ N )
9	7 8	jca	⊢ ( 𝐵 ∈ ( N × N ) → ( ( 1^st ‘ 𝐵 ) ∈ N ∧ ( 2^nd ‘ 𝐵 ) ∈ N ) )
10		enqbreq	⊢ ( ( ( ( 1^st ‘ 𝐴 ) ∈ N ∧ ( 2^nd ‘ 𝐴 ) ∈ N ) ∧ ( ( 1^st ‘ 𝐵 ) ∈ N ∧ ( 2^nd ‘ 𝐵 ) ∈ N ) ) → ( ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ~_Q ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 2^nd ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐵 ) ) ) )
11	6 9 10	syl2an	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ⟨ ( 1^st ‘ 𝐴 ) , ( 2^nd ‘ 𝐴 ) ⟩ ~_Q ⟨ ( 1^st ‘ 𝐵 ) , ( 2^nd ‘ 𝐵 ) ⟩ ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 2^nd ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐵 ) ) ) )
12		mulcompi	⊢ ( ( 2^nd ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐵 ) ) = ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) )
13	12	eqeq2i	⊢ ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 2^nd ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐵 ) ) ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) )
14	13	a1i	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 2^nd ‘ 𝐴 ) ·_N ( 1^st ‘ 𝐵 ) ) ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )
15	3 11 14	3bitrd	⊢ ( ( 𝐴 ∈ ( N × N ) ∧ 𝐵 ∈ ( N × N ) ) → ( 𝐴 ~_Q 𝐵 ↔ ( ( 1^st ‘ 𝐴 ) ·_N ( 2^nd ‘ 𝐵 ) ) = ( ( 1^st ‘ 𝐵 ) ·_N ( 2^nd ‘ 𝐴 ) ) ) )