This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )