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