Metamath Proof Explorer


Theorem xlemul1a

Description: Extended real version of lemul1a . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xlemul1a A * B * C * 0 C A B A 𝑒 C B 𝑒 C

Proof

Step Hyp Ref Expression
1 0xr 0 *
2 simpr A * B * C * C *
3 xrleloe 0 * C * 0 C 0 < C 0 = C
4 1 2 3 sylancr A * B * C * 0 C 0 < C 0 = C
5 simpllr A * B * C * 0 < C A B A B C *
6 elxr C * C C = +∞ C = −∞
7 5 6 sylib A * B * C * 0 < C A B A B C C = +∞ C = −∞
8 simplrr A * B * C * 0 < C A B A B C A B
9 simprll A * B * C * 0 < C A B A B C A
10 simprlr A * B * C * 0 < C A B A B C B
11 simprr A * B * C * 0 < C A B A B C C
12 simplrl A * B * C * 0 < C A B A B C 0 < C
13 lemul1 A B C 0 < C A B A C B C
14 9 10 11 12 13 syl112anc A * B * C * 0 < C A B A B C A B A C B C
15 8 14 mpbid A * B * C * 0 < C A B A B C A C B C
16 rexmul A C A 𝑒 C = A C
17 9 11 16 syl2anc A * B * C * 0 < C A B A B C A 𝑒 C = A C
18 rexmul B C B 𝑒 C = B C
19 10 11 18 syl2anc A * B * C * 0 < C A B A B C B 𝑒 C = B C
20 15 17 19 3brtr4d A * B * C * 0 < C A B A B C A 𝑒 C B 𝑒 C
21 20 expr A * B * C * 0 < C A B A B C A 𝑒 C B 𝑒 C
22 simprl A * B * C * 0 < C A B A B A
23 0re 0
24 lttri4 A 0 A < 0 A = 0 0 < A
25 22 23 24 sylancl A * B * C * 0 < C A B A B A < 0 A = 0 0 < A
26 simplll A * B * C * 0 < C A B A *
27 26 adantr A * B * C * 0 < C A B A B A *
28 xmulpnf1n A * A < 0 A 𝑒 +∞ = −∞
29 27 28 sylan A * B * C * 0 < C A B A B A < 0 A 𝑒 +∞ = −∞
30 simpllr A * B * C * 0 < C A B B *
31 30 adantr A * B * C * 0 < C A B A B B *
32 31 adantr A * B * C * 0 < C A B A B A < 0 B *
33 pnfxr +∞ *
34 xmulcl B * +∞ * B 𝑒 +∞ *
35 32 33 34 sylancl A * B * C * 0 < C A B A B A < 0 B 𝑒 +∞ *
36 mnfle B 𝑒 +∞ * −∞ B 𝑒 +∞
37 35 36 syl A * B * C * 0 < C A B A B A < 0 −∞ B 𝑒 +∞
38 29 37 eqbrtrd A * B * C * 0 < C A B A B A < 0 A 𝑒 +∞ B 𝑒 +∞
39 38 ex A * B * C * 0 < C A B A B A < 0 A 𝑒 +∞ B 𝑒 +∞
40 oveq1 A = 0 A 𝑒 +∞ = 0 𝑒 +∞
41 xmul02 +∞ * 0 𝑒 +∞ = 0
42 33 41 ax-mp 0 𝑒 +∞ = 0
43 40 42 eqtrdi A = 0 A 𝑒 +∞ = 0
44 43 adantl A * B * C * 0 < C A B A B A = 0 A 𝑒 +∞ = 0
45 simplrr A * B * C * 0 < C A B A B A B
46 breq1 A = 0 A B 0 B
47 45 46 syl5ibcom A * B * C * 0 < C A B A B A = 0 0 B
48 simprr A * B * C * 0 < C A B A B B
49 leloe 0 B 0 B 0 < B 0 = B
50 23 48 49 sylancr A * B * C * 0 < C A B A B 0 B 0 < B 0 = B
51 47 50 sylibd A * B * C * 0 < C A B A B A = 0 0 < B 0 = B
52 51 imp A * B * C * 0 < C A B A B A = 0 0 < B 0 = B
53 pnfge 0 * 0 +∞
54 1 53 ax-mp 0 +∞
55 xmulpnf1 B * 0 < B B 𝑒 +∞ = +∞
56 31 55 sylan A * B * C * 0 < C A B A B 0 < B B 𝑒 +∞ = +∞
57 54 56 breqtrrid A * B * C * 0 < C A B A B 0 < B 0 B 𝑒 +∞
58 xrleid 0 * 0 0
59 1 58 ax-mp 0 0
60 59 42 breqtrri 0 0 𝑒 +∞
61 simpr A * B * C * 0 < C A B A B 0 = B 0 = B
62 61 oveq1d A * B * C * 0 < C A B A B 0 = B 0 𝑒 +∞ = B 𝑒 +∞
63 60 62 breqtrid A * B * C * 0 < C A B A B 0 = B 0 B 𝑒 +∞
64 57 63 jaodan A * B * C * 0 < C A B A B 0 < B 0 = B 0 B 𝑒 +∞
65 52 64 syldan A * B * C * 0 < C A B A B A = 0 0 B 𝑒 +∞
66 44 65 eqbrtrd A * B * C * 0 < C A B A B A = 0 A 𝑒 +∞ B 𝑒 +∞
67 66 ex A * B * C * 0 < C A B A B A = 0 A 𝑒 +∞ B 𝑒 +∞
68 pnfge +∞ * +∞ +∞
69 33 68 ax-mp +∞ +∞
70 26 adantr A * B * C * 0 < C A B A B 0 < A A *
71 simprr A * B * C * 0 < C A B A B 0 < A 0 < A
72 xmulpnf1 A * 0 < A A 𝑒 +∞ = +∞
73 70 71 72 syl2anc A * B * C * 0 < C A B A B 0 < A A 𝑒 +∞ = +∞
74 30 adantr A * B * C * 0 < C A B A B 0 < A B *
75 ltletr 0 A B 0 < A A B 0 < B
76 23 75 mp3an1 A B 0 < A A B 0 < B
77 76 adantl A * B * C * 0 < C A B A B 0 < A A B 0 < B
78 45 77 mpan2d A * B * C * 0 < C A B A B 0 < A 0 < B
79 78 impr A * B * C * 0 < C A B A B 0 < A 0 < B
80 74 79 55 syl2anc A * B * C * 0 < C A B A B 0 < A B 𝑒 +∞ = +∞
81 73 80 breq12d A * B * C * 0 < C A B A B 0 < A A 𝑒 +∞ B 𝑒 +∞ +∞ +∞
82 69 81 mpbiri A * B * C * 0 < C A B A B 0 < A A 𝑒 +∞ B 𝑒 +∞
83 82 expr A * B * C * 0 < C A B A B 0 < A A 𝑒 +∞ B 𝑒 +∞
84 39 67 83 3jaod A * B * C * 0 < C A B A B A < 0 A = 0 0 < A A 𝑒 +∞ B 𝑒 +∞
85 25 84 mpd A * B * C * 0 < C A B A B A 𝑒 +∞ B 𝑒 +∞
86 oveq2 C = +∞ A 𝑒 C = A 𝑒 +∞
87 oveq2 C = +∞ B 𝑒 C = B 𝑒 +∞
88 86 87 breq12d C = +∞ A 𝑒 C B 𝑒 C A 𝑒 +∞ B 𝑒 +∞
89 85 88 syl5ibrcom A * B * C * 0 < C A B A B C = +∞ A 𝑒 C B 𝑒 C
90 nltmnf 0 * ¬ 0 < −∞
91 1 90 ax-mp ¬ 0 < −∞
92 breq2 C = −∞ 0 < C 0 < −∞
93 91 92 mtbiri C = −∞ ¬ 0 < C
94 93 con2i 0 < C ¬ C = −∞
95 94 ad2antrl A * B * C * 0 < C A B ¬ C = −∞
96 95 adantr A * B * C * 0 < C A B A B ¬ C = −∞
97 96 pm2.21d A * B * C * 0 < C A B A B C = −∞ A 𝑒 C B 𝑒 C
98 21 89 97 3jaod A * B * C * 0 < C A B A B C C = +∞ C = −∞ A 𝑒 C B 𝑒 C
99 7 98 mpd A * B * C * 0 < C A B A B A 𝑒 C B 𝑒 C
100 99 anassrs A * B * C * 0 < C A B A B A 𝑒 C B 𝑒 C
101 xmulcl A * C * A 𝑒 C *
102 101 adantlr A * B * C * A 𝑒 C *
103 102 ad2antrr A * B * C * 0 < C A B B = +∞ A 𝑒 C *
104 pnfge A 𝑒 C * A 𝑒 C +∞
105 103 104 syl A * B * C * 0 < C A B B = +∞ A 𝑒 C +∞
106 oveq1 B = +∞ B 𝑒 C = +∞ 𝑒 C
107 xmulpnf2 C * 0 < C +∞ 𝑒 C = +∞
108 107 ad2ant2lr A * B * C * 0 < C A B +∞ 𝑒 C = +∞
109 106 108 sylan9eqr A * B * C * 0 < C A B B = +∞ B 𝑒 C = +∞
110 105 109 breqtrrd A * B * C * 0 < C A B B = +∞ A 𝑒 C B 𝑒 C
111 110 adantlr A * B * C * 0 < C A B A B = +∞ A 𝑒 C B 𝑒 C
112 simplrr A * B * C * 0 < C A B B = −∞ A B
113 simpr A * B * C * 0 < C A B B = −∞ B = −∞
114 26 adantr A * B * C * 0 < C A B B = −∞ A *
115 mnfle A * −∞ A
116 114 115 syl A * B * C * 0 < C A B B = −∞ −∞ A
117 113 116 eqbrtrd A * B * C * 0 < C A B B = −∞ B A
118 xrletri3 A * B * A = B A B B A
119 118 ad3antrrr A * B * C * 0 < C A B B = −∞ A = B A B B A
120 112 117 119 mpbir2and A * B * C * 0 < C A B B = −∞ A = B
121 120 oveq1d A * B * C * 0 < C A B B = −∞ A 𝑒 C = B 𝑒 C
122 xmulcl B * C * B 𝑒 C *
123 122 adantll A * B * C * B 𝑒 C *
124 123 ad2antrr A * B * C * 0 < C A B B = −∞ B 𝑒 C *
125 xrleid B 𝑒 C * B 𝑒 C B 𝑒 C
126 124 125 syl A * B * C * 0 < C A B B = −∞ B 𝑒 C B 𝑒 C
127 121 126 eqbrtrd A * B * C * 0 < C A B B = −∞ A 𝑒 C B 𝑒 C
128 127 adantlr A * B * C * 0 < C A B A B = −∞ A 𝑒 C B 𝑒 C
129 elxr B * B B = +∞ B = −∞
130 30 129 sylib A * B * C * 0 < C A B B B = +∞ B = −∞
131 130 adantr A * B * C * 0 < C A B A B B = +∞ B = −∞
132 100 111 128 131 mpjao3dan A * B * C * 0 < C A B A A 𝑒 C B 𝑒 C
133 simplrr A * B * C * 0 < C A B A = +∞ A B
134 30 adantr A * B * C * 0 < C A B A = +∞ B *
135 pnfge B * B +∞
136 134 135 syl A * B * C * 0 < C A B A = +∞ B +∞
137 simpr A * B * C * 0 < C A B A = +∞ A = +∞
138 136 137 breqtrrd A * B * C * 0 < C A B A = +∞ B A
139 118 ad3antrrr A * B * C * 0 < C A B A = +∞ A = B A B B A
140 133 138 139 mpbir2and A * B * C * 0 < C A B A = +∞ A = B
141 140 oveq1d A * B * C * 0 < C A B A = +∞ A 𝑒 C = B 𝑒 C
142 123 125 syl A * B * C * B 𝑒 C B 𝑒 C
143 142 ad2antrr A * B * C * 0 < C A B A = +∞ B 𝑒 C B 𝑒 C
144 141 143 eqbrtrd A * B * C * 0 < C A B A = +∞ A 𝑒 C B 𝑒 C
145 oveq1 A = −∞ A 𝑒 C = −∞ 𝑒 C
146 xmulmnf2 C * 0 < C −∞ 𝑒 C = −∞
147 146 ad2ant2lr A * B * C * 0 < C A B −∞ 𝑒 C = −∞
148 145 147 sylan9eqr A * B * C * 0 < C A B A = −∞ A 𝑒 C = −∞
149 123 ad2antrr A * B * C * 0 < C A B A = −∞ B 𝑒 C *
150 mnfle B 𝑒 C * −∞ B 𝑒 C
151 149 150 syl A * B * C * 0 < C A B A = −∞ −∞ B 𝑒 C
152 148 151 eqbrtrd A * B * C * 0 < C A B A = −∞ A 𝑒 C B 𝑒 C
153 elxr A * A A = +∞ A = −∞
154 26 153 sylib A * B * C * 0 < C A B A A = +∞ A = −∞
155 132 144 152 154 mpjao3dan A * B * C * 0 < C A B A 𝑒 C B 𝑒 C
156 155 exp32 A * B * C * 0 < C A B A 𝑒 C B 𝑒 C
157 xmul01 A * A 𝑒 0 = 0
158 157 ad2antrr A * B * C * A 𝑒 0 = 0
159 xmul01 B * B 𝑒 0 = 0
160 159 ad2antlr A * B * C * B 𝑒 0 = 0
161 158 160 breq12d A * B * C * A 𝑒 0 B 𝑒 0 0 0
162 59 161 mpbiri A * B * C * A 𝑒 0 B 𝑒 0
163 oveq2 0 = C A 𝑒 0 = A 𝑒 C
164 oveq2 0 = C B 𝑒 0 = B 𝑒 C
165 163 164 breq12d 0 = C A 𝑒 0 B 𝑒 0 A 𝑒 C B 𝑒 C
166 162 165 syl5ibcom A * B * C * 0 = C A 𝑒 C B 𝑒 C
167 166 a1dd A * B * C * 0 = C A B A 𝑒 C B 𝑒 C
168 156 167 jaod A * B * C * 0 < C 0 = C A B A 𝑒 C B 𝑒 C
169 4 168 sylbid A * B * C * 0 C A B A 𝑒 C B 𝑒 C
170 169 expimpd A * B * C * 0 C A B A 𝑒 C B 𝑒 C
171 170 3impia A * B * C * 0 C A B A 𝑒 C B 𝑒 C
172 171 imp A * B * C * 0 C A B A 𝑒 C B 𝑒 C