Metamath Proof Explorer

Theorem enreceq

Description: Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995) (New usage is discouraged.)

		Ref	Expression
	Assertion	enreceq	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to ([⟨A, B⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹} \leftrightarrow A +_{𝑷} D = B +_{𝑷} C)$

Proof

Step	Hyp	Ref	Expression
1		enrer	$⊢ ~_{𝑹} Er (𝑷 \times 𝑷)$
2	1	a1i	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to ~_{𝑹} Er (𝑷 \times 𝑷)$
3		opelxpi	$⊢ (A \in 𝑷 \land B \in 𝑷) \to ⟨A, B⟩ \in (𝑷 \times 𝑷)$
4	3	adantr	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to ⟨A, B⟩ \in (𝑷 \times 𝑷)$
5	2 4	erth	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to (⟨A, B⟩ ~_{𝑹} ⟨C, D⟩ \leftrightarrow [⟨A, B⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹})$
6		enrbreq	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to (⟨A, B⟩ ~_{𝑹} ⟨C, D⟩ \leftrightarrow A +_{𝑷} D = B +_{𝑷} C)$
7	5 6	bitr3d	$⊢ ((A \in 𝑷 \land B \in 𝑷) \land (C \in 𝑷 \land D \in 𝑷)) \to ([⟨A, B⟩] ~_{𝑹} = [⟨C, D⟩] ~_{𝑹} \leftrightarrow A +_{𝑷} D = B +_{𝑷} C)$