Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ltresr | Unicode version |
Description: Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
Ref | Expression |
---|---|
ltresr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ltrelre 7807 | . . . 4 | |
2 | 1 | brel 4672 | . . 3 |
3 | opelreal 7801 | . . . 4 | |
4 | opelreal 7801 | . . . 4 | |
5 | 3, 4 | anbi12i 460 | . . 3 |
6 | 2, 5 | sylib 122 | . 2 |
7 | ltrelsr 7712 | . . 3 | |
8 | 7 | brel 4672 | . 2 |
9 | eleq1 2238 | . . . . . . . . 9 | |
10 | 9 | anbi1d 465 | . . . . . . . 8 |
11 | eqeq1 2182 | . . . . . . . . . . 11 | |
12 | 11 | anbi1d 465 | . . . . . . . . . 10 |
13 | 12 | anbi1d 465 | . . . . . . . . 9 |
14 | 13 | 2exbidv 1866 | . . . . . . . 8 |
15 | 10, 14 | anbi12d 473 | . . . . . . 7 |
16 | eleq1 2238 | . . . . . . . . 9 | |
17 | 16 | anbi2d 464 | . . . . . . . 8 |
18 | eqeq1 2182 | . . . . . . . . . . 11 | |
19 | 18 | anbi2d 464 | . . . . . . . . . 10 |
20 | 19 | anbi1d 465 | . . . . . . . . 9 |
21 | 20 | 2exbidv 1866 | . . . . . . . 8 |
22 | 17, 21 | anbi12d 473 | . . . . . . 7 |
23 | df-lt 7799 | . . . . . . 7 | |
24 | 15, 22, 23 | brabg 4263 | . . . . . 6 |
25 | 24 | bianabs 611 | . . . . 5 |
26 | vex 2738 | . . . . . . . . . . 11 | |
27 | 26 | eqresr 7810 | . . . . . . . . . 10 |
28 | eqcom 2177 | . . . . . . . . . 10 | |
29 | eqcom 2177 | . . . . . . . . . 10 | |
30 | 27, 28, 29 | 3bitr4i 212 | . . . . . . . . 9 |
31 | vex 2738 | . . . . . . . . . . 11 | |
32 | 31 | eqresr 7810 | . . . . . . . . . 10 |
33 | eqcom 2177 | . . . . . . . . . 10 | |
34 | eqcom 2177 | . . . . . . . . . 10 | |
35 | 32, 33, 34 | 3bitr4i 212 | . . . . . . . . 9 |
36 | 30, 35 | anbi12i 460 | . . . . . . . 8 |
37 | 26, 31 | opth2 4234 | . . . . . . . 8 |
38 | 36, 37 | bitr4i 187 | . . . . . . 7 |
39 | 38 | anbi1i 458 | . . . . . 6 |
40 | 39 | 2exbii 1604 | . . . . 5 |
41 | 25, 40 | bitrdi 196 | . . . 4 |
42 | 3, 4, 41 | syl2anbr 292 | . . 3 |
43 | breq12 4003 | . . . 4 | |
44 | 43 | copsex2g 4240 | . . 3 |
45 | 42, 44 | bitrd 188 | . 2 |
46 | 6, 8, 45 | pm5.21nii 704 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 104 wb 105 wceq 1353 wex 1490 wcel 2146 cop 3592 class class class wbr 3998 cnr 7271 c0r 7272 cltr 7277 cr 7785 cltrr 7790 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 ax-io 709 ax-5 1445 ax-7 1446 ax-gen 1447 ax-ie1 1491 ax-ie2 1492 ax-8 1502 ax-10 1503 ax-11 1504 ax-i12 1505 ax-bndl 1507 ax-4 1508 ax-17 1524 ax-i9 1528 ax-ial 1532 ax-i5r 1533 ax-13 2148 ax-14 2149 ax-ext 2157 ax-coll 4113 ax-sep 4116 ax-nul 4124 ax-pow 4169 ax-pr 4203 ax-un 4427 ax-setind 4530 ax-iinf 4581 |
This theorem depends on definitions: df-bi 117 df-dc 835 df-3or 979 df-3an 980 df-tru 1356 df-fal 1359 df-nf 1459 df-sb 1761 df-eu 2027 df-mo 2028 df-clab 2162 df-cleq 2168 df-clel 2171 df-nfc 2306 df-ne 2346 df-ral 2458 df-rex 2459 df-reu 2460 df-rab 2462 df-v 2737 df-sbc 2961 df-csb 3056 df-dif 3129 df-un 3131 df-in 3133 df-ss 3140 df-nul 3421 df-pw 3574 df-sn 3595 df-pr 3596 df-op 3598 df-uni 3806 df-int 3841 df-iun 3884 df-br 3999 df-opab 4060 df-mpt 4061 df-tr 4097 df-eprel 4283 df-id 4287 df-po 4290 df-iso 4291 df-iord 4360 df-on 4362 df-suc 4365 df-iom 4584 df-xp 4626 df-rel 4627 df-cnv 4628 df-co 4629 df-dm 4630 df-rn 4631 df-res 4632 df-ima 4633 df-iota 5170 df-fun 5210 df-fn 5211 df-f 5212 df-f1 5213 df-fo 5214 df-f1o 5215 df-fv 5216 df-ov 5868 df-oprab 5869 df-mpo 5870 df-1st 6131 df-2nd 6132 df-recs 6296 df-irdg 6361 df-1o 6407 df-oadd 6411 df-omul 6412 df-er 6525 df-ec 6527 df-qs 6531 df-ni 7278 df-pli 7279 df-mi 7280 df-lti 7281 df-plpq 7318 df-mpq 7319 df-enq 7321 df-nqqs 7322 df-plqqs 7323 df-mqqs 7324 df-1nqqs 7325 df-rq 7326 df-ltnqqs 7327 df-inp 7440 df-i1p 7441 df-enr 7700 df-nr 7701 df-ltr 7704 df-0r 7705 df-r 7796 df-lt 7799 |
This theorem is referenced by: ltresr2 7814 pitoregt0 7823 ltrennb 7828 ax0lt1 7850 axprecex 7854 axpre-ltirr 7856 axpre-ltwlin 7857 axpre-lttrn 7858 axpre-apti 7859 axpre-ltadd 7860 axpre-mulgt0 7861 axpre-mulext 7862 axarch 7865 axcaucvglemcau 7872 axcaucvglemres 7873 axpre-suploclemres 7875 |
Copyright terms: Public domain | W3C validator |