Proof of Theorem xrlttr
Step | Hyp | Ref
| Expression |
1 | | elxr 9593 |
. 2
![( (](lp.gif)
![( (](lp.gif) ![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) |
2 | | elxr 9593 |
. . 3
![( (](lp.gif)
![( (](lp.gif) ![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) |
3 | | elxr 9593 |
. . . . . . . . 9
![( (](lp.gif)
![( (](lp.gif) ![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) |
4 | | lttr 7862 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![RR RR](bbr.gif) ![( (](lp.gif) ![(
(](lp.gif)
![C C](_cc.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
5 | 4 | 3expa 1182 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
6 | 5 | an32s 558 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
7 | | rexr 7835 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![RR* RR*](_bbrast.gif) ![) )](rp.gif) |
8 | | pnfnlt 9603 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) |
9 | 7, 8 | syl 14 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) |
10 | 9 | adantr 274 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![C C](_cc.gif) ![)
)](rp.gif) |
11 | | breq1 3940 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
12 | 11 | adantl 275 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
13 | 10, 12 | mtbird 663 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![C C](_cc.gif) ![)
)](rp.gif) |
14 | 13 | pm2.21d 609 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
15 | 14 | adantll 468 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![+oo +oo](_pinf.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
16 | 15 | adantld 276 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![+oo +oo](_pinf.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
17 | | rexr 7835 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif) ![RR* RR*](_bbrast.gif) ![) )](rp.gif) |
18 | | nltmnf 9604 |
. . . . . . . . . . . . . . . 16
![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) |
19 | 17, 18 | syl 14 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![-oo -oo](_minf.gif) ![) )](rp.gif) |
20 | 19 | adantr 274 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![-oo -oo](_minf.gif) ![) )](rp.gif) |
21 | | breq2 3941 |
. . . . . . . . . . . . . . 15
![( (](lp.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) |
22 | 21 | adantl 275 |
. . . . . . . . . . . . . 14
![( (](lp.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![( (](lp.gif) ![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) |
23 | 20, 22 | mtbird 663 |
. . . . . . . . . . . . 13
![( (](lp.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![B B](_cb.gif) ![)
)](rp.gif) |
24 | 23 | pm2.21d 609 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
25 | 24 | adantlr 469 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![-oo -oo](_minf.gif) ![( (](lp.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
26 | 25 | adantrd 277 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![-oo -oo](_minf.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
27 | 6, 16, 26 | 3jaodan 1285 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![( (](lp.gif) ![-oo -oo](_minf.gif) ![) )](rp.gif) ![(
(](lp.gif) ![( (](lp.gif)
![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
28 | 3, 27 | sylan2b 285 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR RR](bbr.gif) ![RR* RR*](_bbrast.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
29 | 28 | an32s 558 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif)
![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
30 | | ltpnf 9597 |
. . . . . . . . . . 11
![( (](lp.gif) ![+oo +oo](_pinf.gif) ![) )](rp.gif) |
31 | 30 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![+oo +oo](_pinf.gif) ![) )](rp.gif) |
32 | | breq2 3941 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![) )](rp.gif) ![) )](rp.gif) |
33 | 32 | adantl 275 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![( (](lp.gif) ![+oo +oo](_pinf.gif) ![) )](rp.gif) ![) )](rp.gif) |
34 | 31, 33 | mpbird 166 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![C C](_cc.gif) ![) )](rp.gif) |
35 | 34 | adantlr 469 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif)
![+oo +oo](_pinf.gif) ![C C](_cc.gif) ![)
)](rp.gif) |
36 | 35 | a1d 22 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif)
![+oo +oo](_pinf.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
37 | | nltmnf 9604 |
. . . . . . . . . . . 12
![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) |
38 | 37 | adantr 274 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![-oo -oo](_minf.gif) ![-oo -oo](_minf.gif) ![) )](rp.gif) |
39 | | breq2 3941 |
. . . . . . . . . . . 12
![( (](lp.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) |
40 | 39 | adantl 275 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif) ![-oo -oo](_minf.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) |
41 | 38, 40 | mtbird 663 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif) ![-oo -oo](_minf.gif) ![C C](_cc.gif) ![) )](rp.gif) |
42 | 41 | pm2.21d 609 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif) ![-oo -oo](_minf.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
43 | 42 | adantld 276 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif) ![-oo -oo](_minf.gif) ![( (](lp.gif) ![(
(](lp.gif)
![C C](_cc.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
44 | 43 | adantll 468 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif)
![-oo -oo](_minf.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
45 | 29, 36, 44 | 3jaodan 1285 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![C C](_cc.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
46 | 45 | anasss 397 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
47 | | pnfnlt 9603 |
. . . . . . . . . 10
![( (](lp.gif)
![B B](_cb.gif) ![) )](rp.gif) |
48 | 47 | adantl 275 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![RR* RR*](_bbrast.gif)
![B B](_cb.gif) ![) )](rp.gif) |
49 | | breq1 3940 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![B B](_cb.gif) ![)
)](rp.gif) ![) )](rp.gif) |
50 | 49 | adantr 274 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![RR* RR*](_bbrast.gif) ![(
(](lp.gif) ![B B](_cb.gif) ![) )](rp.gif) ![) )](rp.gif) |
51 | 48, 50 | mtbird 663 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![RR* RR*](_bbrast.gif)
![B B](_cb.gif) ![) )](rp.gif) |
52 | 51 | pm2.21d 609 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif)
![RR* RR*](_bbrast.gif) ![(
(](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
53 | 52 | adantrd 277 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif)
![RR* RR*](_bbrast.gif) ![(
(](lp.gif) ![( (](lp.gif)
![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
54 | 53 | adantrr 471 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
55 | | mnflt 9599 |
. . . . . . . . . . 11
![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) |
56 | 55 | adantl 275 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![RR RR](bbr.gif)
![C C](_cc.gif) ![) )](rp.gif) |
57 | | breq1 3940 |
. . . . . . . . . . 11
![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
58 | 57 | adantr 274 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![RR RR](bbr.gif) ![( (](lp.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
59 | 56, 58 | mpbird 166 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![RR RR](bbr.gif) ![C C](_cc.gif) ![) )](rp.gif) |
60 | 59 | a1d 22 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
61 | 60 | adantlr 469 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif)
![RR RR](bbr.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
62 | | mnfltpnf 9601 |
. . . . . . . . . 10
![+oo +oo](_pinf.gif) |
63 | | breq12 3942 |
. . . . . . . . . 10
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![( (](lp.gif) ![+oo +oo](_pinf.gif) ![) )](rp.gif) ![) )](rp.gif) |
64 | 62, 63 | mpbiri 167 |
. . . . . . . . 9
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![C C](_cc.gif) ![) )](rp.gif) |
65 | 64 | a1d 22 |
. . . . . . . 8
![( (](lp.gif) ![( (](lp.gif)
![+oo +oo](_pinf.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
66 | 65 | adantlr 469 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif)
![+oo +oo](_pinf.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
67 | 43 | adantll 468 |
. . . . . . 7
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif)
![-oo -oo](_minf.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
68 | 61, 66, 67 | 3jaodan 1285 |
. . . . . 6
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif) ![RR* RR*](_bbrast.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![C C](_cc.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
69 | 68 | anasss 397 |
. . . . 5
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
70 | 46, 54, 69 | 3jaoian 1284 |
. . . 4
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![( (](lp.gif)
![( (](lp.gif) ![-oo -oo](_minf.gif) ![) )](rp.gif) ![) )](rp.gif) ![( (](lp.gif) ![( (](lp.gif) ![C C](_cc.gif) ![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
71 | 70 | 3impb 1178 |
. . 3
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![) )](rp.gif) ![( (](lp.gif) ![(
(](lp.gif)
![C C](_cc.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |
72 | 2, 71 | syl3an3b 1255 |
. 2
![( (](lp.gif) ![( (](lp.gif) ![( (](lp.gif)
![-oo -oo](_minf.gif) ![RR* RR*](_bbrast.gif) ![( (](lp.gif) ![( (](lp.gif)
![C C](_cc.gif)
![C C](_cc.gif) ![) )](rp.gif) ![) )](rp.gif) |
73 | 1, 72 | syl3an1b 1253 |
1
![( (](lp.gif) ![( (](lp.gif) ![RR*
RR*](_bbrast.gif) ![( (](lp.gif) ![(
(](lp.gif)
![C C](_cc.gif) ![C C](_cc.gif) ![)
)](rp.gif) ![) )](rp.gif) |