Metamath Proof Explorer


Theorem xmullem

Description: Lemma for rexmul . (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion xmullem
|- ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> A e. RR )

Proof

Step Hyp Ref Expression
1 ioran
 |-  ( -. ( A = 0 \/ B = 0 ) <-> ( -. A = 0 /\ -. B = 0 ) )
2 1 anbi2i
 |-  ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) <-> ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) )
3 ioran
 |-  ( -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) <-> ( -. ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) /\ -. ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) )
4 ioran
 |-  ( -. ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) <-> ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) )
5 ioran
 |-  ( -. ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) <-> ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) )
6 4 5 anbi12i
 |-  ( ( -. ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) /\ -. ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) <-> ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) )
7 3 6 bitri
 |-  ( -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) <-> ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) )
8 ioran
 |-  ( -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) <-> ( -. ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) /\ -. ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) )
9 ioran
 |-  ( -. ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) <-> ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) )
10 ioran
 |-  ( -. ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) <-> ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) )
11 9 10 anbi12i
 |-  ( ( -. ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) /\ -. ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) <-> ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) )
12 8 11 bitri
 |-  ( -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) <-> ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) )
13 7 12 anbi12i
 |-  ( ( -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) <-> ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) )
14 simplll
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> A e. RR* )
15 elxr
 |-  ( A e. RR* <-> ( A e. RR \/ A = +oo \/ A = -oo ) )
16 14 15 sylib
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( A e. RR \/ A = +oo \/ A = -oo ) )
17 idd
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( A e. RR -> A e. RR ) )
18 simprlr
 |-  ( ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) -> -. ( B < 0 /\ A = +oo ) )
19 18 adantl
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> -. ( B < 0 /\ A = +oo ) )
20 19 pm2.21d
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( ( B < 0 /\ A = +oo ) -> A e. RR ) )
21 20 expdimp
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) /\ B < 0 ) -> ( A = +oo -> A e. RR ) )
22 simplrr
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> -. B = 0 )
23 22 pm2.21d
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( B = 0 -> ( A = +oo -> A e. RR ) ) )
24 23 imp
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) /\ B = 0 ) -> ( A = +oo -> A e. RR ) )
25 simplll
 |-  ( ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) -> -. ( 0 < B /\ A = +oo ) )
26 25 adantl
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> -. ( 0 < B /\ A = +oo ) )
27 26 pm2.21d
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( ( 0 < B /\ A = +oo ) -> A e. RR ) )
28 27 expdimp
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) /\ 0 < B ) -> ( A = +oo -> A e. RR ) )
29 simpllr
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> B e. RR* )
30 0xr
 |-  0 e. RR*
31 xrltso
 |-  < Or RR*
32 solin
 |-  ( ( < Or RR* /\ ( B e. RR* /\ 0 e. RR* ) ) -> ( B < 0 \/ B = 0 \/ 0 < B ) )
33 31 32 mpan
 |-  ( ( B e. RR* /\ 0 e. RR* ) -> ( B < 0 \/ B = 0 \/ 0 < B ) )
34 29 30 33 sylancl
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( B < 0 \/ B = 0 \/ 0 < B ) )
35 21 24 28 34 mpjao3dan
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( A = +oo -> A e. RR ) )
36 simpllr
 |-  ( ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) -> -. ( B < 0 /\ A = -oo ) )
37 36 adantl
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> -. ( B < 0 /\ A = -oo ) )
38 37 pm2.21d
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( ( B < 0 /\ A = -oo ) -> A e. RR ) )
39 38 expdimp
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) /\ B < 0 ) -> ( A = -oo -> A e. RR ) )
40 22 pm2.21d
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( B = 0 -> ( A = -oo -> A e. RR ) ) )
41 40 imp
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) /\ B = 0 ) -> ( A = -oo -> A e. RR ) )
42 simprll
 |-  ( ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) -> -. ( 0 < B /\ A = -oo ) )
43 42 adantl
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> -. ( 0 < B /\ A = -oo ) )
44 43 pm2.21d
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( ( 0 < B /\ A = -oo ) -> A e. RR ) )
45 44 expdimp
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) /\ 0 < B ) -> ( A = -oo -> A e. RR ) )
46 39 41 45 34 mpjao3dan
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( A = -oo -> A e. RR ) )
47 17 35 46 3jaod
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> ( ( A e. RR \/ A = +oo \/ A = -oo ) -> A e. RR ) )
48 16 47 mpd
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ ( -. A = 0 /\ -. B = 0 ) ) /\ ( ( ( -. ( 0 < B /\ A = +oo ) /\ -. ( B < 0 /\ A = -oo ) ) /\ ( -. ( 0 < A /\ B = +oo ) /\ -. ( A < 0 /\ B = -oo ) ) ) /\ ( ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) /\ ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) ) ) -> A e. RR )
49 2 13 48 syl2anb
 |-  ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ ( -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) ) -> A e. RR )
50 49 anassrs
 |-  ( ( ( ( ( A e. RR* /\ B e. RR* ) /\ -. ( A = 0 \/ B = 0 ) ) /\ -. ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) ) /\ -. ( ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) \/ ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) -> A e. RR )