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	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$

Proof

Step	Hyp	Ref	Expression
1		1st2nd2	$⊢ A \in (𝑵 \times 𝑵) \to A = ⟨1^{st} (A), 2^{nd} (A)⟩$
2		1st2nd2	$⊢ B \in (𝑵 \times 𝑵) \to B = ⟨1^{st} (B), 2^{nd} (B)⟩$
3	1 2	breqan12d	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow ⟨1^{st} (A), 2^{nd} (A)⟩ ~_{𝑸} ⟨1^{st} (B), 2^{nd} (B)⟩)$
4		xp1st	$⊢ A \in (𝑵 \times 𝑵) \to 1^{st} (A) \in 𝑵$
5		xp2nd	$⊢ A \in (𝑵 \times 𝑵) \to 2^{nd} (A) \in 𝑵$
6	4 5	jca	$⊢ A \in (𝑵 \times 𝑵) \to (1^{st} (A) \in 𝑵 \land 2^{nd} (A) \in 𝑵)$
7		xp1st	$⊢ B \in (𝑵 \times 𝑵) \to 1^{st} (B) \in 𝑵$
8		xp2nd	$⊢ B \in (𝑵 \times 𝑵) \to 2^{nd} (B) \in 𝑵$
9	7 8	jca	$⊢ B \in (𝑵 \times 𝑵) \to (1^{st} (B) \in 𝑵 \land 2^{nd} (B) \in 𝑵)$
10		enqbreq	$⊢ ((1^{st} (A) \in 𝑵 \land 2^{nd} (A) \in 𝑵) \land (1^{st} (B) \in 𝑵 \land 2^{nd} (B) \in 𝑵)) \to (⟨1^{st} (A), 2^{nd} (A)⟩ ~_{𝑸} ⟨1^{st} (B), 2^{nd} (B)⟩ \leftrightarrow 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 2^{nd} (A) \cdot_{𝑵} 1^{st} (B))$
11	6 9 10	syl2an	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (⟨1^{st} (A), 2^{nd} (A)⟩ ~_{𝑸} ⟨1^{st} (B), 2^{nd} (B)⟩ \leftrightarrow 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 2^{nd} (A) \cdot_{𝑵} 1^{st} (B))$
12		mulcompi	$⊢ 2^{nd} (A) \cdot_{𝑵} 1^{st} (B) = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A)$
13	12	eqeq2i	$⊢ 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 2^{nd} (A) \cdot_{𝑵} 1^{st} (B) \leftrightarrow 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A)$
14	13	a1i	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 2^{nd} (A) \cdot_{𝑵} 1^{st} (B) \leftrightarrow 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$
15	3 11 14	3bitrd	$⊢ (A \in (𝑵 \times 𝑵) \land B \in (𝑵 \times 𝑵)) \to (A ~_{𝑸} B \leftrightarrow 1^{st} (A) \cdot_{𝑵} 2^{nd} (B) = 1^{st} (B) \cdot_{𝑵} 2^{nd} (A))$