Metamath Proof Explorer


Theorem ltresr

Description: Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996) (New usage is discouraged.)

Ref Expression
Assertion ltresr A 0 𝑹 < B 0 𝑹 A < 𝑹 B

Proof

Step Hyp Ref Expression
1 ltrelre < 2
2 1 brel A 0 𝑹 < B 0 𝑹 A 0 𝑹 B 0 𝑹
3 opelreal A 0 𝑹 A 𝑹
4 opelreal B 0 𝑹 B 𝑹
5 3 4 anbi12i A 0 𝑹 B 0 𝑹 A 𝑹 B 𝑹
6 2 5 sylib A 0 𝑹 < B 0 𝑹 A 𝑹 B 𝑹
7 ltrelsr < 𝑹 𝑹 × 𝑹
8 7 brel A < 𝑹 B A 𝑹 B 𝑹
9 opex A 0 𝑹 V
10 opex B 0 𝑹 V
11 eleq1 x = A 0 𝑹 x A 0 𝑹
12 11 anbi1d x = A 0 𝑹 x y A 0 𝑹 y
13 eqeq1 x = A 0 𝑹 x = z 0 𝑹 A 0 𝑹 = z 0 𝑹
14 13 anbi1d x = A 0 𝑹 x = z 0 𝑹 y = w 0 𝑹 A 0 𝑹 = z 0 𝑹 y = w 0 𝑹
15 14 anbi1d x = A 0 𝑹 x = z 0 𝑹 y = w 0 𝑹 z < 𝑹 w A 0 𝑹 = z 0 𝑹 y = w 0 𝑹 z < 𝑹 w
16 15 2exbidv x = A 0 𝑹 z w x = z 0 𝑹 y = w 0 𝑹 z < 𝑹 w z w A 0 𝑹 = z 0 𝑹 y = w 0 𝑹 z < 𝑹 w
17 12 16 anbi12d x = A 0 𝑹 x y z w x = z 0 𝑹 y = w 0 𝑹 z < 𝑹 w A 0 𝑹 y z w A 0 𝑹 = z 0 𝑹 y = w 0 𝑹 z < 𝑹 w
18 eleq1 y = B 0 𝑹 y B 0 𝑹
19 18 anbi2d y = B 0 𝑹 A 0 𝑹 y A 0 𝑹 B 0 𝑹
20 eqeq1 y = B 0 𝑹 y = w 0 𝑹 B 0 𝑹 = w 0 𝑹
21 20 anbi2d y = B 0 𝑹 A 0 𝑹 = z 0 𝑹 y = w 0 𝑹 A 0 𝑹 = z 0 𝑹 B 0 𝑹 = w 0 𝑹
22 21 anbi1d y = B 0 𝑹 A 0 𝑹 = z 0 𝑹 y = w 0 𝑹 z < 𝑹 w A 0 𝑹 = z 0 𝑹 B 0 𝑹 = w 0 𝑹 z < 𝑹 w
23 22 2exbidv y = B 0 𝑹 z w A 0 𝑹 = z 0 𝑹 y = w 0 𝑹 z < 𝑹 w z w A 0 𝑹 = z 0 𝑹 B 0 𝑹 = w 0 𝑹 z < 𝑹 w
24 19 23 anbi12d y = B 0 𝑹 A 0 𝑹 y z w A 0 𝑹 = z 0 𝑹 y = w 0 𝑹 z < 𝑹 w A 0 𝑹 B 0 𝑹 z w A 0 𝑹 = z 0 𝑹 B 0 𝑹 = w 0 𝑹 z < 𝑹 w
25 df-lt < = x y | x y z w x = z 0 𝑹 y = w 0 𝑹 z < 𝑹 w
26 9 10 17 24 25 brab A 0 𝑹 < B 0 𝑹 A 0 𝑹 B 0 𝑹 z w A 0 𝑹 = z 0 𝑹 B 0 𝑹 = w 0 𝑹 z < 𝑹 w
27 26 baib A 0 𝑹 B 0 𝑹 A 0 𝑹 < B 0 𝑹 z w A 0 𝑹 = z 0 𝑹 B 0 𝑹 = w 0 𝑹 z < 𝑹 w
28 vex z V
29 28 eqresr z 0 𝑹 = A 0 𝑹 z = A
30 eqcom A 0 𝑹 = z 0 𝑹 z 0 𝑹 = A 0 𝑹
31 eqcom A = z z = A
32 29 30 31 3bitr4i A 0 𝑹 = z 0 𝑹 A = z
33 vex w V
34 33 eqresr w 0 𝑹 = B 0 𝑹 w = B
35 eqcom B 0 𝑹 = w 0 𝑹 w 0 𝑹 = B 0 𝑹
36 eqcom B = w w = B
37 34 35 36 3bitr4i B 0 𝑹 = w 0 𝑹 B = w
38 32 37 anbi12i A 0 𝑹 = z 0 𝑹 B 0 𝑹 = w 0 𝑹 A = z B = w
39 28 33 opth2 A B = z w A = z B = w
40 38 39 bitr4i A 0 𝑹 = z 0 𝑹 B 0 𝑹 = w 0 𝑹 A B = z w
41 40 anbi1i A 0 𝑹 = z 0 𝑹 B 0 𝑹 = w 0 𝑹 z < 𝑹 w A B = z w z < 𝑹 w
42 41 2exbii z w A 0 𝑹 = z 0 𝑹 B 0 𝑹 = w 0 𝑹 z < 𝑹 w z w A B = z w z < 𝑹 w
43 27 42 bitrdi A 0 𝑹 B 0 𝑹 A 0 𝑹 < B 0 𝑹 z w A B = z w z < 𝑹 w
44 3 4 43 syl2anbr A 𝑹 B 𝑹 A 0 𝑹 < B 0 𝑹 z w A B = z w z < 𝑹 w
45 breq12 z = A w = B z < 𝑹 w A < 𝑹 B
46 45 copsex2g A 𝑹 B 𝑹 z w A B = z w z < 𝑹 w A < 𝑹 B
47 44 46 bitrd A 𝑹 B 𝑹 A 0 𝑹 < B 0 𝑹 A < 𝑹 B
48 6 8 47 pm5.21nii A 0 𝑹 < B 0 𝑹 A < 𝑹 B