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 ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → A ~ 𝑸 B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B = 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A

Proof

Step Hyp Ref Expression
1 1st2nd2 ⊢ A ∈ 𝑵 × 𝑵 → A = 1 st ⁡ A 2 nd ⁡ A
2 1st2nd2 ⊢ B ∈ 𝑵 × 𝑵 → B = 1 st ⁡ B 2 nd ⁡ B
3 1 2 breqan12d ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → A ~ 𝑸 B ↔ 1 st ⁡ A 2 nd ⁡ A ~ 𝑸 1 st ⁡ B 2 nd ⁡ B
4 xp1st ⊢ A ∈ 𝑵 × 𝑵 → 1 st ⁡ A ∈ 𝑵
5 xp2nd ⊢ A ∈ 𝑵 × 𝑵 → 2 nd ⁡ A ∈ 𝑵
6 4 5 jca ⊢ A ∈ 𝑵 × 𝑵 → 1 st ⁡ A ∈ 𝑵 ∧ 2 nd ⁡ A ∈ 𝑵
7 xp1st ⊢ B ∈ 𝑵 × 𝑵 → 1 st ⁡ B ∈ 𝑵
8 xp2nd ⊢ B ∈ 𝑵 × 𝑵 → 2 nd ⁡ B ∈ 𝑵
9 7 8 jca ⊢ B ∈ 𝑵 × 𝑵 → 1 st ⁡ B ∈ 𝑵 ∧ 2 nd ⁡ B ∈ 𝑵
10 enqbreq ⊢ 1 st ⁡ A ∈ 𝑵 ∧ 2 nd ⁡ A ∈ 𝑵 ∧ 1 st ⁡ B ∈ 𝑵 ∧ 2 nd ⁡ B ∈ 𝑵 → 1 st ⁡ A 2 nd ⁡ A ~ 𝑸 1 st ⁡ B 2 nd ⁡ B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B = 2 nd ⁡ A ⋅ 𝑵 1 st ⁡ B
11 6 9 10 syl2an ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → 1 st ⁡ A 2 nd ⁡ A ~ 𝑸 1 st ⁡ B 2 nd ⁡ B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B = 2 nd ⁡ A ⋅ 𝑵 1 st ⁡ B
12 mulcompi ⊢ 2 nd ⁡ A ⋅ 𝑵 1 st ⁡ B = 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A
13 12 eqeq2i ⊢ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B = 2 nd ⁡ A ⋅ 𝑵 1 st ⁡ B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B = 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A
14 13 a1i ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B = 2 nd ⁡ A ⋅ 𝑵 1 st ⁡ B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B = 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A
15 3 11 14 3bitrd ⊢ A ∈ 𝑵 × 𝑵 ∧ B ∈ 𝑵 × 𝑵 → A ~ 𝑸 B ↔ 1 st ⁡ A ⋅ 𝑵 2 nd ⁡ B = 1 st ⁡ B ⋅ 𝑵 2 nd ⁡ A