ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xposdif Unicode version

Theorem xposdif 9900
Description: Extended real version of posdif 8430. (Contributed by Mario Carneiro, 24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)
Assertion
Ref Expression
xposdif  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )

Proof of Theorem xposdif
StepHypRef Expression
1 elxr 9794 . . 3  |-  ( B  e.  RR*  <->  ( B  e.  RR  \/  B  = +oo  \/  B  = -oo ) )
2 elxr 9794 . . . . 5  |-  ( A  e.  RR*  <->  ( A  e.  RR  \/  A  = +oo  \/  A  = -oo ) )
3 posdif 8430 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  0  <  ( B  -  A ) ) )
4 rexsub 9871 . . . . . . . . . 10  |-  ( ( B  e.  RR  /\  A  e.  RR )  ->  ( B +e  -e A )  =  ( B  -  A
) )
54ancoms 268 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( B +e  -e A )  =  ( B  -  A
) )
65breq2d 4030 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( 0  <  ( B +e  -e
A )  <->  0  <  ( B  -  A ) ) )
73, 6bitr4d 191 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  e.  RR )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )
87ex 115 . . . . . 6  |-  ( A  e.  RR  ->  ( B  e.  RR  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
9 rexr 8021 . . . . . . . . . 10  |-  ( B  e.  RR  ->  B  e.  RR* )
10 pnfnlt 9805 . . . . . . . . . . 11  |-  ( B  e.  RR*  ->  -. +oo  <  B )
1110adantl 277 . . . . . . . . . 10  |-  ( ( A  = +oo  /\  B  e.  RR* )  ->  -. +oo  <  B )
129, 11sylan2 286 . . . . . . . . 9  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  -. +oo  <  B
)
13 simpl 109 . . . . . . . . . 10  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  A  = +oo )
1413breq1d 4028 . . . . . . . . 9  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  ( A  <  B  <-> +oo 
<  B ) )
1512, 14mtbird 674 . . . . . . . 8  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  -.  A  <  B
)
16 0xr 8022 . . . . . . . . . 10  |-  0  e.  RR*
17 nltmnf 9806 . . . . . . . . . 10  |-  ( 0  e.  RR*  ->  -.  0  < -oo )
1816, 17ax-mp 5 . . . . . . . . 9  |-  -.  0  < -oo
19 xnegeq 9845 . . . . . . . . . . . . . 14  |-  ( A  = +oo  ->  -e
A  =  -e +oo )
2019adantr 276 . . . . . . . . . . . . 13  |-  ( ( A  = +oo  /\  B  e.  RR )  -> 
-e A  = 
-e +oo )
21 xnegpnf 9846 . . . . . . . . . . . . 13  |-  -e +oo  = -oo
2220, 21eqtrdi 2238 . . . . . . . . . . . 12  |-  ( ( A  = +oo  /\  B  e.  RR )  -> 
-e A  = -oo )
2322oveq2d 5907 . . . . . . . . . . 11  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  ( B +e  -e A )  =  ( B +e -oo ) )
24 renepnf 8023 . . . . . . . . . . . . 13  |-  ( B  e.  RR  ->  B  =/= +oo )
2524adantl 277 . . . . . . . . . . . 12  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  B  =/= +oo )
26 xaddmnf1 9866 . . . . . . . . . . . 12  |-  ( ( B  e.  RR*  /\  B  =/= +oo )  ->  ( B +e -oo )  = -oo )
279, 25, 26syl2an2 594 . . . . . . . . . . 11  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  ( B +e -oo )  = -oo )
2823, 27eqtrd 2222 . . . . . . . . . 10  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  ( B +e  -e A )  = -oo )
2928breq2d 4030 . . . . . . . . 9  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  ( 0  <  ( B +e  -e
A )  <->  0  < -oo ) )
3018, 29mtbiri 676 . . . . . . . 8  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  -.  0  <  ( B +e  -e
A ) )
3115, 302falsed 703 . . . . . . 7  |-  ( ( A  = +oo  /\  B  e.  RR )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )
3231ex 115 . . . . . 6  |-  ( A  = +oo  ->  ( B  e.  RR  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
33 simpl 109 . . . . . . . . 9  |-  ( ( A  = -oo  /\  B  e.  RR )  ->  A  = -oo )
34 mnflt 9801 . . . . . . . . . 10  |-  ( B  e.  RR  -> -oo  <  B )
3534adantl 277 . . . . . . . . 9  |-  ( ( A  = -oo  /\  B  e.  RR )  -> -oo  <  B )
3633, 35eqbrtrd 4040 . . . . . . . 8  |-  ( ( A  = -oo  /\  B  e.  RR )  ->  A  <  B )
37 0ltpnf 9800 . . . . . . . . 9  |-  0  < +oo
38 xnegeq 9845 . . . . . . . . . . . . 13  |-  ( A  = -oo  ->  -e
A  =  -e -oo )
39 xnegmnf 9847 . . . . . . . . . . . . 13  |-  -e -oo  = +oo
4038, 39eqtrdi 2238 . . . . . . . . . . . 12  |-  ( A  = -oo  ->  -e
A  = +oo )
4140oveq2d 5907 . . . . . . . . . . 11  |-  ( A  = -oo  ->  ( B +e  -e
A )  =  ( B +e +oo ) )
4241adantr 276 . . . . . . . . . 10  |-  ( ( A  = -oo  /\  B  e.  RR )  ->  ( B +e  -e A )  =  ( B +e +oo ) )
43 renemnf 8024 . . . . . . . . . . . 12  |-  ( B  e.  RR  ->  B  =/= -oo )
4443adantl 277 . . . . . . . . . . 11  |-  ( ( A  = -oo  /\  B  e.  RR )  ->  B  =/= -oo )
45 xaddpnf1 9864 . . . . . . . . . . 11  |-  ( ( B  e.  RR*  /\  B  =/= -oo )  ->  ( B +e +oo )  = +oo )
469, 44, 45syl2an2 594 . . . . . . . . . 10  |-  ( ( A  = -oo  /\  B  e.  RR )  ->  ( B +e +oo )  = +oo )
4742, 46eqtrd 2222 . . . . . . . . 9  |-  ( ( A  = -oo  /\  B  e.  RR )  ->  ( B +e  -e A )  = +oo )
4837, 47breqtrrid 4056 . . . . . . . 8  |-  ( ( A  = -oo  /\  B  e.  RR )  ->  0  <  ( B +e  -e
A ) )
4936, 482thd 175 . . . . . . 7  |-  ( ( A  = -oo  /\  B  e.  RR )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )
5049ex 115 . . . . . 6  |-  ( A  = -oo  ->  ( B  e.  RR  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
518, 32, 503jaoi 1314 . . . . 5  |-  ( ( A  e.  RR  \/  A  = +oo  \/  A  = -oo )  ->  ( B  e.  RR  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
522, 51sylbi 121 . . . 4  |-  ( A  e.  RR*  ->  ( B  e.  RR  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
53 ltpnf 9798 . . . . . . . . . 10  |-  ( A  e.  RR  ->  A  < +oo )
5453adantr 276 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  = +oo )  ->  A  < +oo )
55 simpr 110 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  = +oo )  ->  B  = +oo )
5654, 55breqtrrd 4046 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  = +oo )  ->  A  <  B )
5755oveq1d 5906 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  = +oo )  ->  ( B +e  -e A )  =  ( +oo +e  -e A ) )
58 rexneg 9848 . . . . . . . . . . . . . 14  |-  ( A  e.  RR  ->  -e
A  =  -u A
)
59 renegcl 8236 . . . . . . . . . . . . . 14  |-  ( A  e.  RR  ->  -u A  e.  RR )
6058, 59eqeltrd 2266 . . . . . . . . . . . . 13  |-  ( A  e.  RR  ->  -e
A  e.  RR )
6160rexrd 8025 . . . . . . . . . . . 12  |-  ( A  e.  RR  ->  -e
A  e.  RR* )
6261adantr 276 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  B  = +oo )  -> 
-e A  e. 
RR* )
6360renemnfd 8027 . . . . . . . . . . . 12  |-  ( A  e.  RR  ->  -e
A  =/= -oo )
6463adantr 276 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  B  = +oo )  -> 
-e A  =/= -oo )
65 xaddpnf2 9865 . . . . . . . . . . 11  |-  ( ( 
-e A  e. 
RR*  /\  -e A  =/= -oo )  -> 
( +oo +e  -e A )  = +oo )
6662, 64, 65syl2anc 411 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  = +oo )  ->  ( +oo +e  -e A )  = +oo )
6757, 66eqtrd 2222 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  = +oo )  ->  ( B +e  -e A )  = +oo )
6837, 67breqtrrid 4056 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  = +oo )  ->  0  <  ( B +e  -e
A ) )
6956, 682thd 175 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  = +oo )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )
7069ex 115 . . . . . 6  |-  ( A  e.  RR  ->  ( B  = +oo  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
71 pnfxr 8028 . . . . . . . . . 10  |- +oo  e.  RR*
72 xrltnr 9797 . . . . . . . . . 10  |-  ( +oo  e.  RR*  ->  -. +oo  < +oo )
7371, 72ax-mp 5 . . . . . . . . 9  |-  -. +oo  < +oo
74 breq12 4023 . . . . . . . . 9  |-  ( ( A  = +oo  /\  B  = +oo )  ->  ( A  <  B  <-> +oo 
< +oo ) )
7573, 74mtbiri 676 . . . . . . . 8  |-  ( ( A  = +oo  /\  B  = +oo )  ->  -.  A  <  B
)
76 0re 7975 . . . . . . . . . 10  |-  0  e.  RR
7776ltnri 8068 . . . . . . . . 9  |-  -.  0  <  0
78 simpr 110 . . . . . . . . . . . 12  |-  ( ( A  = +oo  /\  B  = +oo )  ->  B  = +oo )
7919, 21eqtrdi 2238 . . . . . . . . . . . . 13  |-  ( A  = +oo  ->  -e
A  = -oo )
8079adantr 276 . . . . . . . . . . . 12  |-  ( ( A  = +oo  /\  B  = +oo )  -> 
-e A  = -oo )
8178, 80oveq12d 5909 . . . . . . . . . . 11  |-  ( ( A  = +oo  /\  B  = +oo )  ->  ( B +e  -e A )  =  ( +oo +e -oo ) )
82 pnfaddmnf 9868 . . . . . . . . . . 11  |-  ( +oo +e -oo )  =  0
8381, 82eqtrdi 2238 . . . . . . . . . 10  |-  ( ( A  = +oo  /\  B  = +oo )  ->  ( B +e  -e A )  =  0 )
8483breq2d 4030 . . . . . . . . 9  |-  ( ( A  = +oo  /\  B  = +oo )  ->  ( 0  <  ( B +e  -e
A )  <->  0  <  0 ) )
8577, 84mtbiri 676 . . . . . . . 8  |-  ( ( A  = +oo  /\  B  = +oo )  ->  -.  0  <  ( B +e  -e
A ) )
8675, 852falsed 703 . . . . . . 7  |-  ( ( A  = +oo  /\  B  = +oo )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )
8786ex 115 . . . . . 6  |-  ( A  = +oo  ->  ( B  = +oo  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
88 mnfltpnf 9803 . . . . . . . . 9  |- -oo  < +oo
89 breq12 4023 . . . . . . . . 9  |-  ( ( A  = -oo  /\  B  = +oo )  ->  ( A  <  B  <-> -oo 
< +oo ) )
9088, 89mpbiri 168 . . . . . . . 8  |-  ( ( A  = -oo  /\  B  = +oo )  ->  A  <  B )
91 oveq1 5898 . . . . . . . . . . 11  |-  ( B  = +oo  ->  ( B +e +oo )  =  ( +oo +e +oo ) )
9241, 91sylan9eq 2242 . . . . . . . . . 10  |-  ( ( A  = -oo  /\  B  = +oo )  ->  ( B +e  -e A )  =  ( +oo +e +oo ) )
93 pnfnemnf 8030 . . . . . . . . . . 11  |- +oo  =/= -oo
94 xaddpnf1 9864 . . . . . . . . . . 11  |-  ( ( +oo  e.  RR*  /\ +oo  =/= -oo )  ->  ( +oo +e +oo )  = +oo )
9571, 93, 94mp2an 426 . . . . . . . . . 10  |-  ( +oo +e +oo )  = +oo
9692, 95eqtrdi 2238 . . . . . . . . 9  |-  ( ( A  = -oo  /\  B  = +oo )  ->  ( B +e  -e A )  = +oo )
9737, 96breqtrrid 4056 . . . . . . . 8  |-  ( ( A  = -oo  /\  B  = +oo )  ->  0  <  ( B +e  -e
A ) )
9890, 972thd 175 . . . . . . 7  |-  ( ( A  = -oo  /\  B  = +oo )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )
9998ex 115 . . . . . 6  |-  ( A  = -oo  ->  ( B  = +oo  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
10070, 87, 993jaoi 1314 . . . . 5  |-  ( ( A  e.  RR  \/  A  = +oo  \/  A  = -oo )  ->  ( B  = +oo  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
1012, 100sylbi 121 . . . 4  |-  ( A  e.  RR*  ->  ( B  = +oo  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
102 rexr 8021 . . . . . . . . . . 11  |-  ( A  e.  RR  ->  A  e.  RR* )
103102adantr 276 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  A  e.  RR* )
104 nltmnf 9806 . . . . . . . . . 10  |-  ( A  e.  RR*  ->  -.  A  < -oo )
105103, 104syl 14 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  -.  A  < -oo )
106 simpr 110 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  B  = -oo )
107106breq2d 4030 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  ( A  <  B  <->  A  < -oo ) )
108105, 107mtbird 674 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  -.  A  <  B
)
109106oveq1d 5906 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  ( B +e  -e A )  =  ( -oo +e  -e A ) )
110 rexr 8021 . . . . . . . . . . . . . 14  |-  (  -e A  e.  RR  -> 
-e A  e. 
RR* )
111 renepnf 8023 . . . . . . . . . . . . . 14  |-  (  -e A  e.  RR  -> 
-e A  =/= +oo )
112 xaddmnf2 9867 . . . . . . . . . . . . . 14  |-  ( ( 
-e A  e. 
RR*  /\  -e A  =/= +oo )  -> 
( -oo +e  -e A )  = -oo )
113110, 111, 112syl2anc 411 . . . . . . . . . . . . 13  |-  (  -e A  e.  RR  ->  ( -oo +e  -e A )  = -oo )
11460, 113syl 14 . . . . . . . . . . . 12  |-  ( A  e.  RR  ->  ( -oo +e  -e
A )  = -oo )
115114adantr 276 . . . . . . . . . . 11  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  ( -oo +e  -e A )  = -oo )
116109, 115eqtrd 2222 . . . . . . . . . 10  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  ( B +e  -e A )  = -oo )
117116breq2d 4030 . . . . . . . . 9  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  ( 0  <  ( B +e  -e
A )  <->  0  < -oo ) )
11818, 117mtbiri 676 . . . . . . . 8  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  -.  0  <  ( B +e  -e
A ) )
119108, 1182falsed 703 . . . . . . 7  |-  ( ( A  e.  RR  /\  B  = -oo )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )
120119ex 115 . . . . . 6  |-  ( A  e.  RR  ->  ( B  = -oo  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
121 eleq1 2252 . . . . . . . . . . . 12  |-  ( A  = +oo  ->  ( A  e.  RR*  <-> +oo  e.  RR* ) )
12271, 121mpbiri 168 . . . . . . . . . . 11  |-  ( A  = +oo  ->  A  e.  RR* )
123122adantr 276 . . . . . . . . . 10  |-  ( ( A  = +oo  /\  B  = -oo )  ->  A  e.  RR* )
124123, 104syl 14 . . . . . . . . 9  |-  ( ( A  = +oo  /\  B  = -oo )  ->  -.  A  < -oo )
125 simpr 110 . . . . . . . . . 10  |-  ( ( A  = +oo  /\  B  = -oo )  ->  B  = -oo )
126125breq2d 4030 . . . . . . . . 9  |-  ( ( A  = +oo  /\  B  = -oo )  ->  ( A  <  B  <->  A  < -oo ) )
127124, 126mtbird 674 . . . . . . . 8  |-  ( ( A  = +oo  /\  B  = -oo )  ->  -.  A  <  B
)
12879oveq2d 5907 . . . . . . . . . . . 12  |-  ( A  = +oo  ->  ( B +e  -e
A )  =  ( B +e -oo ) )
129128adantr 276 . . . . . . . . . . 11  |-  ( ( A  = +oo  /\  B  = -oo )  ->  ( B +e  -e A )  =  ( B +e -oo ) )
130 mnfxr 8032 . . . . . . . . . . . . 13  |- -oo  e.  RR*
131 eleq1 2252 . . . . . . . . . . . . 13  |-  ( B  = -oo  ->  ( B  e.  RR*  <-> -oo  e.  RR* ) )
132130, 131mpbiri 168 . . . . . . . . . . . 12  |-  ( B  = -oo  ->  B  e.  RR* )
133 mnfnepnf 8031 . . . . . . . . . . . . . 14  |- -oo  =/= +oo
134 neeq1 2373 . . . . . . . . . . . . . 14  |-  ( B  = -oo  ->  ( B  =/= +oo  <-> -oo  =/= +oo )
)
135133, 134mpbiri 168 . . . . . . . . . . . . 13  |-  ( B  = -oo  ->  B  =/= +oo )
136135adantl 277 . . . . . . . . . . . 12  |-  ( ( A  = +oo  /\  B  = -oo )  ->  B  =/= +oo )
137132, 136, 26syl2an2 594 . . . . . . . . . . 11  |-  ( ( A  = +oo  /\  B  = -oo )  ->  ( B +e -oo )  = -oo )
138129, 137eqtrd 2222 . . . . . . . . . 10  |-  ( ( A  = +oo  /\  B  = -oo )  ->  ( B +e  -e A )  = -oo )
139138breq2d 4030 . . . . . . . . 9  |-  ( ( A  = +oo  /\  B  = -oo )  ->  ( 0  <  ( B +e  -e
A )  <->  0  < -oo ) )
14018, 139mtbiri 676 . . . . . . . 8  |-  ( ( A  = +oo  /\  B  = -oo )  ->  -.  0  <  ( B +e  -e
A ) )
141127, 1402falsed 703 . . . . . . 7  |-  ( ( A  = +oo  /\  B  = -oo )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )
142141ex 115 . . . . . 6  |-  ( A  = +oo  ->  ( B  = -oo  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
143 xrltnr 9797 . . . . . . . . . 10  |-  ( -oo  e.  RR*  ->  -. -oo  < -oo )
144130, 143ax-mp 5 . . . . . . . . 9  |-  -. -oo  < -oo
145 breq12 4023 . . . . . . . . 9  |-  ( ( A  = -oo  /\  B  = -oo )  ->  ( A  <  B  <-> -oo 
< -oo ) )
146144, 145mtbiri 676 . . . . . . . 8  |-  ( ( A  = -oo  /\  B  = -oo )  ->  -.  A  <  B
)
147 oveq1 5898 . . . . . . . . . . . 12  |-  ( B  = -oo  ->  ( B +e +oo )  =  ( -oo +e +oo ) )
14841, 147sylan9eq 2242 . . . . . . . . . . 11  |-  ( ( A  = -oo  /\  B  = -oo )  ->  ( B +e  -e A )  =  ( -oo +e +oo ) )
149 mnfaddpnf 9869 . . . . . . . . . . 11  |-  ( -oo +e +oo )  =  0
150148, 149eqtrdi 2238 . . . . . . . . . 10  |-  ( ( A  = -oo  /\  B  = -oo )  ->  ( B +e  -e A )  =  0 )
151150breq2d 4030 . . . . . . . . 9  |-  ( ( A  = -oo  /\  B  = -oo )  ->  ( 0  <  ( B +e  -e
A )  <->  0  <  0 ) )
15277, 151mtbiri 676 . . . . . . . 8  |-  ( ( A  = -oo  /\  B  = -oo )  ->  -.  0  <  ( B +e  -e
A ) )
153146, 1522falsed 703 . . . . . . 7  |-  ( ( A  = -oo  /\  B  = -oo )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )
154153ex 115 . . . . . 6  |-  ( A  = -oo  ->  ( B  = -oo  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
155120, 142, 1543jaoi 1314 . . . . 5  |-  ( ( A  e.  RR  \/  A  = +oo  \/  A  = -oo )  ->  ( B  = -oo  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
1562, 155sylbi 121 . . . 4  |-  ( A  e.  RR*  ->  ( B  = -oo  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
15752, 101, 1563jaod 1315 . . 3  |-  ( A  e.  RR*  ->  ( ( B  e.  RR  \/  B  = +oo  \/  B  = -oo )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
1581, 157biimtrid 152 . 2  |-  ( A  e.  RR*  ->  ( B  e.  RR*  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) ) )
159158imp 124 1  |-  ( ( A  e.  RR*  /\  B  e.  RR* )  ->  ( A  <  B  <->  0  <  ( B +e  -e A ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 104    <-> wb 105    \/ w3o 979    = wceq 1364    e. wcel 2160    =/= wne 2360   class class class wbr 4018  (class class class)co 5891   RRcr 7828   0cc0 7829   +oocpnf 8007   -oocmnf 8008   RR*cxr 8009    < clt 8010    - cmin 8146   -ucneg 8147    -ecxne 9787   +ecxad 9788
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-13 2162  ax-14 2163  ax-ext 2171  ax-sep 4136  ax-pow 4189  ax-pr 4224  ax-un 4448  ax-setind 4551  ax-cnex 7920  ax-resscn 7921  ax-1cn 7922  ax-1re 7923  ax-icn 7924  ax-addcl 7925  ax-addrcl 7926  ax-mulcl 7927  ax-addcom 7929  ax-addass 7931  ax-distr 7933  ax-i2m1 7934  ax-0id 7937  ax-rnegex 7938  ax-cnre 7940  ax-pre-ltirr 7941  ax-pre-ltadd 7945
This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1472  df-sb 1774  df-eu 2041  df-mo 2042  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ne 2361  df-nel 2456  df-ral 2473  df-rex 2474  df-reu 2475  df-rab 2477  df-v 2754  df-sbc 2978  df-dif 3146  df-un 3148  df-in 3150  df-ss 3157  df-if 3550  df-pw 3592  df-sn 3613  df-pr 3614  df-op 3616  df-uni 3825  df-br 4019  df-opab 4080  df-id 4308  df-xp 4647  df-rel 4648  df-cnv 4649  df-co 4650  df-dm 4651  df-iota 5193  df-fun 5233  df-fv 5239  df-riota 5847  df-ov 5894  df-oprab 5895  df-mpo 5896  df-pnf 8012  df-mnf 8013  df-xr 8014  df-ltxr 8015  df-sub 8148  df-neg 8149  df-xneg 9790  df-xadd 9791
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator