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

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 ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ↔ ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 enrer ⊢ ~R Er ( P × P )
2 1 a1i ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ~R Er ( P × P ) )
3 opelxpi ⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( P × P ) )
4 3 adantr ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( P × P ) )
5 2 4 erth ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ~R ⟨ 𝐶 , 𝐷 ⟩ ↔ [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ) )
6 enrbreq ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( ⟨ 𝐴 , 𝐵 ⟩ ~R ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ) )
7 5 6 bitr3d ⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐶 ∈ P ∧ 𝐷 ∈ P ) ) → ( [ ⟨ 𝐴 , 𝐵 ⟩ ] ~R = [ ⟨ 𝐶 , 𝐷 ⟩ ] ~R ↔ ( 𝐴 +P 𝐷 ) = ( 𝐵 +P 𝐶 ) ) )