Metamath Proof Explorer

Theorem xmullem2

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

Ref Expression
Assertion xmullem2 
|- ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mnfnepnf 
 |-  -oo =/= +oo
2 eqeq1 
 |-  ( A = -oo -> ( A = +oo <-> -oo = +oo ) )
3 2 necon3bbid 
 |-  ( A = -oo -> ( -. A = +oo <-> -oo =/= +oo ) )
4 1 3 mpbiri 
 |-  ( A = -oo -> -. A = +oo )
5 4 con2i 
 |-  ( A = +oo -> -. A = -oo )
6 5 adantl 
 |-  ( ( 0 < B /\ A = +oo ) -> -. A = -oo )
7 0xr 
 |-  0 e. RR*
8 nltmnf 
 |-  ( 0 e. RR* -> -. 0 < -oo )
9 7 8 ax-mp 
 |-  -. 0 < -oo
10 breq2 
 |-  ( A = -oo -> ( 0 < A <-> 0 < -oo ) )
11 9 10 mtbiri 
 |-  ( A = -oo -> -. 0 < A )
12 11 con2i 
 |-  ( 0 < A -> -. A = -oo )
13 12 adantr 
 |-  ( ( 0 < A /\ B = +oo ) -> -. A = -oo )
14 6 13 jaoi 
 |-  ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) -> -. A = -oo )
15 14 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) -> -. A = -oo ) )
16 simpr 
 |-  ( ( A e. RR* /\ B e. RR* ) -> B e. RR* )
17 xrltnsym 
 |-  ( ( B e. RR* /\ 0 e. RR* ) -> ( B < 0 -> -. 0 < B ) )
18 16 7 17 sylancl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( B < 0 -> -. 0 < B ) )
19 18 adantrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( B < 0 /\ A = -oo ) -> -. 0 < B ) )
20 breq2 
 |-  ( B = -oo -> ( 0 < B <-> 0 < -oo ) )
21 9 20 mtbiri 
 |-  ( B = -oo -> -. 0 < B )
22 21 adantl 
 |-  ( ( A < 0 /\ B = -oo ) -> -. 0 < B )
23 22 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A < 0 /\ B = -oo ) -> -. 0 < B ) )
24 19 23 jaod 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) -> -. 0 < B ) )
25 15 24 orim12d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> ( -. A = -oo \/ -. 0 < B ) ) )
26 ianor 
 |-  ( -. ( 0 < B /\ A = -oo ) <-> ( -. 0 < B \/ -. A = -oo ) )
27 orcom 
 |-  ( ( -. 0 < B \/ -. A = -oo ) <-> ( -. A = -oo \/ -. 0 < B ) )
28 26 27 bitri 
 |-  ( -. ( 0 < B /\ A = -oo ) <-> ( -. A = -oo \/ -. 0 < B ) )
29 25 28 imbitrrdi 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> -. ( 0 < B /\ A = -oo ) ) )
30 18 con2d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( 0 < B -> -. B < 0 ) )
31 30 adantrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( 0 < B /\ A = +oo ) -> -. B < 0 ) )
32 pnfnlt 
 |-  ( 0 e. RR* -> -. +oo < 0 )
33 7 32 ax-mp 
 |-  -. +oo < 0
34 simpr 
 |-  ( ( 0 < A /\ B = +oo ) -> B = +oo )
35 34 breq1d 
 |-  ( ( 0 < A /\ B = +oo ) -> ( B < 0 <-> +oo < 0 ) )
36 33 35 mtbiri 
 |-  ( ( 0 < A /\ B = +oo ) -> -. B < 0 )
37 36 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( 0 < A /\ B = +oo ) -> -. B < 0 ) )
38 31 37 jaod 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) -> -. B < 0 ) )
39 4 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A = -oo -> -. A = +oo ) )
40 39 adantld 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( B < 0 /\ A = -oo ) -> -. A = +oo ) )
41 breq1 
 |-  ( A = +oo -> ( A < 0 <-> +oo < 0 ) )
42 33 41 mtbiri 
 |-  ( A = +oo -> -. A < 0 )
43 42 con2i 
 |-  ( A < 0 -> -. A = +oo )
44 43 adantr 
 |-  ( ( A < 0 /\ B = -oo ) -> -. A = +oo )
45 44 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A < 0 /\ B = -oo ) -> -. A = +oo ) )
46 40 45 jaod 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) -> -. A = +oo ) )
47 38 46 orim12d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> ( -. B < 0 \/ -. A = +oo ) ) )
48 ianor 
 |-  ( -. ( B < 0 /\ A = +oo ) <-> ( -. B < 0 \/ -. A = +oo ) )
49 47 48 imbitrrdi 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> -. ( B < 0 /\ A = +oo ) ) )
50 29 49 jcad 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) ) )
51 ioran 
 |-  ( -. ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) <-> ( -. ( 0 < B /\ A = -oo ) /\ -. ( B < 0 /\ A = +oo ) ) )
52 50 51 imbitrrdi 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> -. ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) ) )
53 21 con2i 
 |-  ( 0 < B -> -. B = -oo )
54 53 adantr 
 |-  ( ( 0 < B /\ A = +oo ) -> -. B = -oo )
55 54 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( 0 < B /\ A = +oo ) -> -. B = -oo ) )
56 pnfnemnf 
 |-  +oo =/= -oo
57 eqeq1 
 |-  ( B = +oo -> ( B = -oo <-> +oo = -oo ) )
58 57 necon3bbid 
 |-  ( B = +oo -> ( -. B = -oo <-> +oo =/= -oo ) )
59 56 58 mpbiri 
 |-  ( B = +oo -> -. B = -oo )
60 59 adantl 
 |-  ( ( 0 < A /\ B = +oo ) -> -. B = -oo )
61 60 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( 0 < A /\ B = +oo ) -> -. B = -oo ) )
62 55 61 jaod 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) -> -. B = -oo ) )
63 11 adantl 
 |-  ( ( B < 0 /\ A = -oo ) -> -. 0 < A )
64 63 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( B < 0 /\ A = -oo ) -> -. 0 < A ) )
65 simpl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> A e. RR* )
66 xrltnsym 
 |-  ( ( A e. RR* /\ 0 e. RR* ) -> ( A < 0 -> -. 0 < A ) )
67 65 7 66 sylancl 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( A < 0 -> -. 0 < A ) )
68 67 adantrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A < 0 /\ B = -oo ) -> -. 0 < A ) )
69 64 68 jaod 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) -> -. 0 < A ) )
70 62 69 orim12d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> ( -. B = -oo \/ -. 0 < A ) ) )
71 ianor 
 |-  ( -. ( 0 < A /\ B = -oo ) <-> ( -. 0 < A \/ -. B = -oo ) )
72 orcom 
 |-  ( ( -. 0 < A \/ -. B = -oo ) <-> ( -. B = -oo \/ -. 0 < A ) )
73 71 72 bitri 
 |-  ( -. ( 0 < A /\ B = -oo ) <-> ( -. B = -oo \/ -. 0 < A ) )
74 70 73 imbitrrdi 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> -. ( 0 < A /\ B = -oo ) ) )
75 42 adantl 
 |-  ( ( 0 < B /\ A = +oo ) -> -. A < 0 )
76 75 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( 0 < B /\ A = +oo ) -> -. A < 0 ) )
77 67 con2d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( 0 < A -> -. A < 0 ) )
78 77 adantrd 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( 0 < A /\ B = +oo ) -> -. A < 0 ) )
79 76 78 jaod 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) -> -. A < 0 ) )
80 breq1 
 |-  ( B = +oo -> ( B < 0 <-> +oo < 0 ) )
81 33 80 mtbiri 
 |-  ( B = +oo -> -. B < 0 )
82 81 con2i 
 |-  ( B < 0 -> -. B = +oo )
83 82 adantr 
 |-  ( ( B < 0 /\ A = -oo ) -> -. B = +oo )
84 59 con2i 
 |-  ( B = -oo -> -. B = +oo )
85 84 adantl 
 |-  ( ( A < 0 /\ B = -oo ) -> -. B = +oo )
86 83 85 jaoi 
 |-  ( ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) -> -. B = +oo )
87 86 a1i 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) -> -. B = +oo ) )
88 79 87 orim12d 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> ( -. A < 0 \/ -. B = +oo ) ) )
89 ianor 
 |-  ( -. ( A < 0 /\ B = +oo ) <-> ( -. A < 0 \/ -. B = +oo ) )
90 88 89 imbitrrdi 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> -. ( A < 0 /\ B = +oo ) ) )
91 74 90 jcad 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) ) )
92 ioran 
 |-  ( -. ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) <-> ( -. ( 0 < A /\ B = -oo ) /\ -. ( A < 0 /\ B = +oo ) ) )
93 91 92 imbitrrdi 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> -. ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) )
94 52 93 jcad 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) -> ( -. ( ( 0 < B /\ A = -oo ) \/ ( B < 0 /\ A = +oo ) ) /\ -. ( ( 0 < A /\ B = -oo ) \/ ( A < 0 /\ B = +oo ) ) ) ) )
95 or4 
 |-  ( ( ( ( 0 < B /\ A = +oo ) \/ ( B < 0 /\ A = -oo ) ) \/ ( ( 0 < A /\ B = +oo ) \/ ( A < 0 /\ B = -oo ) ) ) <-> ( ( ( 0 < B /\ A = +oo ) \/ ( 0 < A /\ B = +oo ) ) \/ ( ( B < 0 /\ A = -oo ) \/ ( A < 0 /\ B = -oo ) ) ) )
96 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 ) ) ) )
97 94 95 96 3imtr4g 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( ( ( 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 ) ) ) ) )