Step | Hyp | Ref
| Expression |
1 | | supxrge.b |
. . . . 5
|
2 | | pnfge 11964 |
. . . . 5
|
3 | 1, 2 | syl 17 |
. . . 4
|
4 | 3 | adantr 481 |
. . 3
|
5 | | supxrge.a |
. . . . . 6
|
6 | 5 | adantr 481 |
. . . . 5
|
7 | | simpr 477 |
. . . . 5
|
8 | | supxrpnf 12148 |
. . . . 5
|
9 | 6, 7, 8 | syl2anc 693 |
. . . 4
|
10 | 9 | eqcomd 2628 |
. . 3
|
11 | 4, 10 | breqtrd 4679 |
. 2
|
12 | | simpr 477 |
. . . . 5
|
13 | | supxrcl 12145 |
. . . . . . . 8
|
14 | 5, 13 | syl 17 |
. . . . . . 7
|
15 | | mnfle 11969 |
. . . . . . 7
|
16 | 14, 15 | syl 17 |
. . . . . 6
|
17 | 16 | adantr 481 |
. . . . 5
|
18 | 12, 17 | eqbrtrd 4675 |
. . . 4
|
19 | 18 | adantlr 751 |
. . 3
|
20 | | simpl 473 |
. . . 4
|
21 | | neqne 2802 |
. . . . 5
|
22 | 21 | adantl 482 |
. . . 4
|
23 | | nfv 1843 |
. . . . 5
|
24 | 5 | adantr 481 |
. . . . . 6
|
25 | 24 | adantr 481 |
. . . . 5
|
26 | 1 | adantr 481 |
. . . . . 6
|
27 | 26 | adantr 481 |
. . . . 5
|
28 | | simpl 473 |
. . . . . . . . 9
|
29 | | rphalfcl 11858 |
. . . . . . . . . 10
|
30 | 29 | adantl 482 |
. . . . . . . . 9
|
31 | | ovex 6678 |
. . . . . . . . . 10
|
32 | | nfcv 2764 |
. . . . . . . . . . 11
|
33 | | supxrge.xph |
. . . . . . . . . . . . 13
|
34 | | nfv 1843 |
. . . . . . . . . . . . 13
|
35 | 33, 34 | nfan 1828 |
. . . . . . . . . . . 12
|
36 | | nfv 1843 |
. . . . . . . . . . . 12
|
37 | 35, 36 | nfim 1825 |
. . . . . . . . . . 11
|
38 | | eleq1 2689 |
. . . . . . . . . . . . 13
|
39 | 38 | anbi2d 740 |
. . . . . . . . . . . 12
|
40 | | oveq2 6658 |
. . . . . . . . . . . . . 14
|
41 | 40 | breq2d 4665 |
. . . . . . . . . . . . 13
|
42 | 41 | rexbidv 3052 |
. . . . . . . . . . . 12
|
43 | 39, 42 | imbi12d 334 |
. . . . . . . . . . 11
|
44 | | supxrge.y |
. . . . . . . . . . 11
|
45 | 32, 37, 43, 44 | vtoclgf 3264 |
. . . . . . . . . 10
|
46 | 31, 45 | ax-mp 5 |
. . . . . . . . 9
|
47 | 28, 30, 46 | syl2anc 693 |
. . . . . . . 8
|
48 | 47 | adantlr 751 |
. . . . . . 7
|
49 | 48 | adantlr 751 |
. . . . . 6
|
50 | | nfv 1843 |
. . . . . . 7
|
51 | | neneq 2800 |
. . . . . . . . . . . . . . . 16
|
52 | 51 | adantl 482 |
. . . . . . . . . . . . . . 15
|
53 | 1 | adantr 481 |
. . . . . . . . . . . . . . . 16
|
54 | | ngtmnft 11997 |
. . . . . . . . . . . . . . . 16
|
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . . . 15
|
56 | 52, 55 | mtbid 314 |
. . . . . . . . . . . . . 14
|
57 | 56 | notnotrd 128 |
. . . . . . . . . . . . 13
|
58 | 57 | ad4ant13 1292 |
. . . . . . . . . . . 12
|
59 | 58 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
60 | 27 | adantr 481 |
. . . . . . . . . . . . 13
|
61 | 60 | 3ad2ant1 1082 |
. . . . . . . . . . . 12
|
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
|
63 | | mnfxr 10096 |
. . . . . . . . . . . . . . . . . . . 20
|
64 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
|
65 | | simpl3 1066 |
. . . . . . . . . . . . . . . . . . . 20
|
66 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
67 | 5 | sselda 3603 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
|
68 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
69 | | ngtmnft 11997 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
71 | 66, 70 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
72 | 71 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
73 | 72 | adantllr 755 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
74 | 29 | rpxrd 11873 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
75 | 29 | rpred 11872 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
76 | | renepnf 10087 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
|
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
78 | | xaddmnf2 12060 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
|
79 | 74, 77, 78 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
|
80 | 79 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
81 | 80 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
82 | 73, 81 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
83 | 82 | adantlllr 39199 |
. . . . . . . . . . . . . . . . . . . . . 22
|
84 | 83 | adantlllr 39199 |
. . . . . . . . . . . . . . . . . . . . 21
|
85 | 84 | 3adantl3 1219 |
. . . . . . . . . . . . . . . . . . . 20
|
86 | 65, 85 | breqtrd 4679 |
. . . . . . . . . . . . . . . . . . 19
|
87 | | mnfle 11969 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
88 | 1, 87 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
|
89 | 88 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
90 | 89 | ad3antrrr 766 |
. . . . . . . . . . . . . . . . . . . 20
|
91 | 90 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . . 19
|
92 | 62, 64, 86, 91 | xrletrid 11986 |
. . . . . . . . . . . . . . . . . 18
|
93 | | simpllr 799 |
. . . . . . . . . . . . . . . . . . . 20
|
94 | 93 | 3ad2antl1 1223 |
. . . . . . . . . . . . . . . . . . 19
|
95 | 94 | neneqd 2799 |
. . . . . . . . . . . . . . . . . 18
|
96 | 92, 95 | condan 835 |
. . . . . . . . . . . . . . . . 17
|
97 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
98 | 67 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
99 | | nltpnft 11995 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
101 | 97, 100 | mpbird 247 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
102 | 101 | eqcomd 2628 |
. . . . . . . . . . . . . . . . . . . . . 22
|
103 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
104 | 103 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
|
105 | 102, 104 | eqeltrd 2701 |
. . . . . . . . . . . . . . . . . . . . 21
|
106 | 105 | 3adantl2 1218 |
. . . . . . . . . . . . . . . . . . . 20
|
107 | | simpl2 1065 |
. . . . . . . . . . . . . . . . . . . 20
|
108 | 106, 107 | condan 835 |
. . . . . . . . . . . . . . . . . . 19
|
109 | 108 | ad5ant125 1312 |
. . . . . . . . . . . . . . . . . 18
|
110 | 109 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
|
111 | 96, 110 | jca 554 |
. . . . . . . . . . . . . . . 16
|
112 | 67 | ad5ant15 1303 |
. . . . . . . . . . . . . . . . . 18
|
113 | 112 | 3adant3 1081 |
. . . . . . . . . . . . . . . . 17
|
114 | | xrrebnd 11999 |
. . . . . . . . . . . . . . . . 17
|
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . 16
|
116 | 111, 115 | mpbird 247 |
. . . . . . . . . . . . . . 15
|
117 | 75 | adantl 482 |
. . . . . . . . . . . . . . . 16
|
118 | 117 | 3ad2ant1 1082 |
. . . . . . . . . . . . . . 15
|
119 | | rexadd 12063 |
. . . . . . . . . . . . . . 15
|
120 | 116, 118,
119 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
121 | 116, 118 | readdcld 10069 |
. . . . . . . . . . . . . 14
|
122 | 120, 121 | eqeltrd 2701 |
. . . . . . . . . . . . 13
|
123 | 122 | rexrd 10089 |
. . . . . . . . . . . 12
|
124 | | pnfxr 10092 |
. . . . . . . . . . . . 13
|
125 | 124 | a1i 11 |
. . . . . . . . . . . 12
|
126 | | simp3 1063 |
. . . . . . . . . . . 12
|
127 | 122 | ltpnfd 11955 |
. . . . . . . . . . . 12
|
128 | 61, 123, 125, 126, 127 | xrlelttrd 11991 |
. . . . . . . . . . 11
|
129 | 59, 128 | jca 554 |
. . . . . . . . . 10
|
130 | | xrrebnd 11999 |
. . . . . . . . . . 11
|
131 | 61, 130 | syl 17 |
. . . . . . . . . 10
|
132 | 129, 131 | mpbird 247 |
. . . . . . . . 9
|
133 | | rpre 11839 |
. . . . . . . . . . . . 13
|
134 | 133 | adantl 482 |
. . . . . . . . . . . 12
|
135 | 134 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
136 | | rexadd 12063 |
. . . . . . . . . . 11
|
137 | 116, 135,
136 | syl2anc 693 |
. . . . . . . . . 10
|
138 | 116, 135 | readdcld 10069 |
. . . . . . . . . 10
|
139 | 137, 138 | eqeltrd 2701 |
. . . . . . . . 9
|
140 | | rphalflt 11860 |
. . . . . . . . . . . . 13
|
141 | 140 | adantl 482 |
. . . . . . . . . . . 12
|
142 | 141 | 3ad2ant1 1082 |
. . . . . . . . . . 11
|
143 | 118, 135,
116, 142 | ltadd2dd 10196 |
. . . . . . . . . 10
|
144 | 120, 137 | breq12d 4666 |
. . . . . . . . . 10
|
145 | 143, 144 | mpbird 247 |
. . . . . . . . 9
|
146 | 132, 122,
139, 126, 145 | lelttrd 10195 |
. . . . . . . 8
|
147 | 146 | 3exp 1264 |
. . . . . . 7
|
148 | 50, 147 | reximdai 3012 |
. . . . . 6
|
149 | 49, 148 | mpd 15 |
. . . . 5
|
150 | 23, 25, 27, 149 | supxrgelem 39553 |
. . . 4
|
151 | 20, 22, 150 | syl2anc 693 |
. . 3
|
152 | 19, 151 | pm2.61dan 832 |
. 2
|
153 | 11, 152 | pm2.61dan 832 |
1
|