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

Theorem xposdif 9866
Description: Extended real version of posdif 8399. (Contributed by Mario Carneiro, 24-Aug-2015.) (Revised by Jim Kingdon, 17-Apr-2023.)
Assertion
Ref Expression
xposdif ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))

Proof of Theorem xposdif
StepHypRef Expression
1 elxr 9760 . . 3 (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
2 elxr 9760 . . . . 5 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
3 posdif 8399 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
4 rexsub 9837 . . . . . . . . . 10 ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (𝐵 +𝑒 -𝑒𝐴) = (𝐵𝐴))
54ancoms 268 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 -𝑒𝐴) = (𝐵𝐴))
65breq2d 4012 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +𝑒 -𝑒𝐴) ↔ 0 < (𝐵𝐴)))
73, 6bitr4d 191 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
87ex 115 . . . . . 6 (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
9 rexr 7990 . . . . . . . . . 10 (𝐵 ∈ ℝ → 𝐵 ∈ ℝ*)
10 pnfnlt 9771 . . . . . . . . . . 11 (𝐵 ∈ ℝ* → ¬ +∞ < 𝐵)
1110adantl 277 . . . . . . . . . 10 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → ¬ +∞ < 𝐵)
129, 11sylan2 286 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ +∞ < 𝐵)
13 simpl 109 . . . . . . . . . 10 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = +∞)
1413breq1d 4010 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
1512, 14mtbird 673 . . . . . . . 8 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 𝐴 < 𝐵)
16 0xr 7991 . . . . . . . . . 10 0 ∈ ℝ*
17 nltmnf 9772 . . . . . . . . . 10 (0 ∈ ℝ* → ¬ 0 < -∞)
1816, 17ax-mp 5 . . . . . . . . 9 ¬ 0 < -∞
19 xnegeq 9811 . . . . . . . . . . . . . 14 (𝐴 = +∞ → -𝑒𝐴 = -𝑒+∞)
2019adantr 276 . . . . . . . . . . . . 13 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -𝑒𝐴 = -𝑒+∞)
21 xnegpnf 9812 . . . . . . . . . . . . 13 -𝑒+∞ = -∞
2220, 21eqtrdi 2226 . . . . . . . . . . . 12 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → -𝑒𝐴 = -∞)
2322oveq2d 5885 . . . . . . . . . . 11 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 -𝑒𝐴) = (𝐵 +𝑒 -∞))
24 renepnf 7992 . . . . . . . . . . . . 13 (𝐵 ∈ ℝ → 𝐵 ≠ +∞)
2524adantl 277 . . . . . . . . . . . 12 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ +∞)
26 xaddmnf1 9832 . . . . . . . . . . . 12 ((𝐵 ∈ ℝ*𝐵 ≠ +∞) → (𝐵 +𝑒 -∞) = -∞)
279, 25, 26syl2an2 594 . . . . . . . . . . 11 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 -∞) = -∞)
2823, 27eqtrd 2210 . . . . . . . . . 10 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 -𝑒𝐴) = -∞)
2928breq2d 4012 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (0 < (𝐵 +𝑒 -𝑒𝐴) ↔ 0 < -∞))
3018, 29mtbiri 675 . . . . . . . 8 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → ¬ 0 < (𝐵 +𝑒 -𝑒𝐴))
3115, 302falsed 702 . . . . . . 7 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
3231ex 115 . . . . . 6 (𝐴 = +∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
33 simpl 109 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 = -∞)
34 mnflt 9767 . . . . . . . . . 10 (𝐵 ∈ ℝ → -∞ < 𝐵)
3534adantl 277 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → -∞ < 𝐵)
3633, 35eqbrtrd 4022 . . . . . . . 8 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐴 < 𝐵)
37 0ltpnf 9766 . . . . . . . . 9 0 < +∞
38 xnegeq 9811 . . . . . . . . . . . . 13 (𝐴 = -∞ → -𝑒𝐴 = -𝑒-∞)
39 xnegmnf 9813 . . . . . . . . . . . . 13 -𝑒-∞ = +∞
4038, 39eqtrdi 2226 . . . . . . . . . . . 12 (𝐴 = -∞ → -𝑒𝐴 = +∞)
4140oveq2d 5885 . . . . . . . . . . 11 (𝐴 = -∞ → (𝐵 +𝑒 -𝑒𝐴) = (𝐵 +𝑒 +∞))
4241adantr 276 . . . . . . . . . 10 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 -𝑒𝐴) = (𝐵 +𝑒 +∞))
43 renemnf 7993 . . . . . . . . . . . 12 (𝐵 ∈ ℝ → 𝐵 ≠ -∞)
4443adantl 277 . . . . . . . . . . 11 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 𝐵 ≠ -∞)
45 xaddpnf1 9830 . . . . . . . . . . 11 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) → (𝐵 +𝑒 +∞) = +∞)
469, 44, 45syl2an2 594 . . . . . . . . . 10 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 +∞) = +∞)
4742, 46eqtrd 2210 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 -𝑒𝐴) = +∞)
4837, 47breqtrrid 4038 . . . . . . . 8 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → 0 < (𝐵 +𝑒 -𝑒𝐴))
4936, 482thd 175 . . . . . . 7 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
5049ex 115 . . . . . 6 (𝐴 = -∞ → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
518, 32, 503jaoi 1303 . . . . 5 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
522, 51sylbi 121 . . . 4 (𝐴 ∈ ℝ* → (𝐵 ∈ ℝ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
53 ltpnf 9764 . . . . . . . . . 10 (𝐴 ∈ ℝ → 𝐴 < +∞)
5453adantr 276 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < +∞)
55 simpr 110 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐵 = +∞)
5654, 55breqtrrd 4028 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
5755oveq1d 5884 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +𝑒 -𝑒𝐴) = (+∞ +𝑒 -𝑒𝐴))
58 rexneg 9814 . . . . . . . . . . . . . 14 (𝐴 ∈ ℝ → -𝑒𝐴 = -𝐴)
59 renegcl 8205 . . . . . . . . . . . . . 14 (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
6058, 59eqeltrd 2254 . . . . . . . . . . . . 13 (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ)
6160rexrd 7994 . . . . . . . . . . . 12 (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ*)
6261adantr 276 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -𝑒𝐴 ∈ ℝ*)
6360renemnfd 7996 . . . . . . . . . . . 12 (𝐴 ∈ ℝ → -𝑒𝐴 ≠ -∞)
6463adantr 276 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -𝑒𝐴 ≠ -∞)
65 xaddpnf2 9831 . . . . . . . . . . 11 ((-𝑒𝐴 ∈ ℝ* ∧ -𝑒𝐴 ≠ -∞) → (+∞ +𝑒 -𝑒𝐴) = +∞)
6662, 64, 65syl2anc 411 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (+∞ +𝑒 -𝑒𝐴) = +∞)
6757, 66eqtrd 2210 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐵 +𝑒 -𝑒𝐴) = +∞)
6837, 67breqtrrid 4038 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → 0 < (𝐵 +𝑒 -𝑒𝐴))
6956, 682thd 175 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
7069ex 115 . . . . . 6 (𝐴 ∈ ℝ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
71 pnfxr 7997 . . . . . . . . . 10 +∞ ∈ ℝ*
72 xrltnr 9763 . . . . . . . . . 10 (+∞ ∈ ℝ* → ¬ +∞ < +∞)
7371, 72ax-mp 5 . . . . . . . . 9 ¬ +∞ < +∞
74 breq12 4005 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ +∞ < +∞))
7573, 74mtbiri 675 . . . . . . . 8 ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 𝐴 < 𝐵)
76 0re 7945 . . . . . . . . . 10 0 ∈ ℝ
7776ltnri 8037 . . . . . . . . 9 ¬ 0 < 0
78 simpr 110 . . . . . . . . . . . 12 ((𝐴 = +∞ ∧ 𝐵 = +∞) → 𝐵 = +∞)
7919, 21eqtrdi 2226 . . . . . . . . . . . . 13 (𝐴 = +∞ → -𝑒𝐴 = -∞)
8079adantr 276 . . . . . . . . . . . 12 ((𝐴 = +∞ ∧ 𝐵 = +∞) → -𝑒𝐴 = -∞)
8178, 80oveq12d 5887 . . . . . . . . . . 11 ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +𝑒 -𝑒𝐴) = (+∞ +𝑒 -∞))
82 pnfaddmnf 9834 . . . . . . . . . . 11 (+∞ +𝑒 -∞) = 0
8381, 82eqtrdi 2226 . . . . . . . . . 10 ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐵 +𝑒 -𝑒𝐴) = 0)
8483breq2d 4012 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 = +∞) → (0 < (𝐵 +𝑒 -𝑒𝐴) ↔ 0 < 0))
8577, 84mtbiri 675 . . . . . . . 8 ((𝐴 = +∞ ∧ 𝐵 = +∞) → ¬ 0 < (𝐵 +𝑒 -𝑒𝐴))
8675, 852falsed 702 . . . . . . 7 ((𝐴 = +∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
8786ex 115 . . . . . 6 (𝐴 = +∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
88 mnfltpnf 9769 . . . . . . . . 9 -∞ < +∞
89 breq12 4005 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ -∞ < +∞))
9088, 89mpbiri 168 . . . . . . . 8 ((𝐴 = -∞ ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
91 oveq1 5876 . . . . . . . . . . 11 (𝐵 = +∞ → (𝐵 +𝑒 +∞) = (+∞ +𝑒 +∞))
9241, 91sylan9eq 2230 . . . . . . . . . 10 ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +𝑒 -𝑒𝐴) = (+∞ +𝑒 +∞))
93 pnfnemnf 7999 . . . . . . . . . . 11 +∞ ≠ -∞
94 xaddpnf1 9830 . . . . . . . . . . 11 ((+∞ ∈ ℝ* ∧ +∞ ≠ -∞) → (+∞ +𝑒 +∞) = +∞)
9571, 93, 94mp2an 426 . . . . . . . . . 10 (+∞ +𝑒 +∞) = +∞
9692, 95eqtrdi 2226 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐵 +𝑒 -𝑒𝐴) = +∞)
9737, 96breqtrrid 4038 . . . . . . . 8 ((𝐴 = -∞ ∧ 𝐵 = +∞) → 0 < (𝐵 +𝑒 -𝑒𝐴))
9890, 972thd 175 . . . . . . 7 ((𝐴 = -∞ ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
9998ex 115 . . . . . 6 (𝐴 = -∞ → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
10070, 87, 993jaoi 1303 . . . . 5 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
1012, 100sylbi 121 . . . 4 (𝐴 ∈ ℝ* → (𝐵 = +∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
102 rexr 7990 . . . . . . . . . . 11 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
103102adantr 276 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ*)
104 nltmnf 9772 . . . . . . . . . 10 (𝐴 ∈ ℝ* → ¬ 𝐴 < -∞)
105103, 104syl 14 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
106 simpr 110 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → 𝐵 = -∞)
107106breq2d 4012 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵𝐴 < -∞))
108105, 107mtbird 673 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
109106oveq1d 5884 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +𝑒 -𝑒𝐴) = (-∞ +𝑒 -𝑒𝐴))
110 rexr 7990 . . . . . . . . . . . . . 14 (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ*)
111 renepnf 7992 . . . . . . . . . . . . . 14 (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ≠ +∞)
112 xaddmnf2 9833 . . . . . . . . . . . . . 14 ((-𝑒𝐴 ∈ ℝ* ∧ -𝑒𝐴 ≠ +∞) → (-∞ +𝑒 -𝑒𝐴) = -∞)
113110, 111, 112syl2anc 411 . . . . . . . . . . . . 13 (-𝑒𝐴 ∈ ℝ → (-∞ +𝑒 -𝑒𝐴) = -∞)
11460, 113syl 14 . . . . . . . . . . . 12 (𝐴 ∈ ℝ → (-∞ +𝑒 -𝑒𝐴) = -∞)
115114adantr 276 . . . . . . . . . . 11 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (-∞ +𝑒 -𝑒𝐴) = -∞)
116109, 115eqtrd 2210 . . . . . . . . . 10 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐵 +𝑒 -𝑒𝐴) = -∞)
117116breq2d 4012 . . . . . . . . 9 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (0 < (𝐵 +𝑒 -𝑒𝐴) ↔ 0 < -∞))
11818, 117mtbiri 675 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +𝑒 -𝑒𝐴))
119108, 1182falsed 702 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
120119ex 115 . . . . . 6 (𝐴 ∈ ℝ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
121 eleq1 2240 . . . . . . . . . . . 12 (𝐴 = +∞ → (𝐴 ∈ ℝ* ↔ +∞ ∈ ℝ*))
12271, 121mpbiri 168 . . . . . . . . . . 11 (𝐴 = +∞ → 𝐴 ∈ ℝ*)
123122adantr 276 . . . . . . . . . 10 ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ*)
124123, 104syl 14 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
125 simpr 110 . . . . . . . . . 10 ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 = -∞)
126125breq2d 4012 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵𝐴 < -∞))
127124, 126mtbird 673 . . . . . . . 8 ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
12879oveq2d 5885 . . . . . . . . . . . 12 (𝐴 = +∞ → (𝐵 +𝑒 -𝑒𝐴) = (𝐵 +𝑒 -∞))
129128adantr 276 . . . . . . . . . . 11 ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +𝑒 -𝑒𝐴) = (𝐵 +𝑒 -∞))
130 mnfxr 8001 . . . . . . . . . . . . 13 -∞ ∈ ℝ*
131 eleq1 2240 . . . . . . . . . . . . 13 (𝐵 = -∞ → (𝐵 ∈ ℝ* ↔ -∞ ∈ ℝ*))
132130, 131mpbiri 168 . . . . . . . . . . . 12 (𝐵 = -∞ → 𝐵 ∈ ℝ*)
133 mnfnepnf 8000 . . . . . . . . . . . . . 14 -∞ ≠ +∞
134 neeq1 2360 . . . . . . . . . . . . . 14 (𝐵 = -∞ → (𝐵 ≠ +∞ ↔ -∞ ≠ +∞))
135133, 134mpbiri 168 . . . . . . . . . . . . 13 (𝐵 = -∞ → 𝐵 ≠ +∞)
136135adantl 277 . . . . . . . . . . . 12 ((𝐴 = +∞ ∧ 𝐵 = -∞) → 𝐵 ≠ +∞)
137132, 136, 26syl2an2 594 . . . . . . . . . . 11 ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +𝑒 -∞) = -∞)
138129, 137eqtrd 2210 . . . . . . . . . 10 ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐵 +𝑒 -𝑒𝐴) = -∞)
139138breq2d 4012 . . . . . . . . 9 ((𝐴 = +∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +𝑒 -𝑒𝐴) ↔ 0 < -∞))
14018, 139mtbiri 675 . . . . . . . 8 ((𝐴 = +∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +𝑒 -𝑒𝐴))
141127, 1402falsed 702 . . . . . . 7 ((𝐴 = +∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
142141ex 115 . . . . . 6 (𝐴 = +∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
143 xrltnr 9763 . . . . . . . . . 10 (-∞ ∈ ℝ* → ¬ -∞ < -∞)
144130, 143ax-mp 5 . . . . . . . . 9 ¬ -∞ < -∞
145 breq12 4005 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ -∞ < -∞))
146144, 145mtbiri 675 . . . . . . . 8 ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
147 oveq1 5876 . . . . . . . . . . . 12 (𝐵 = -∞ → (𝐵 +𝑒 +∞) = (-∞ +𝑒 +∞))
14841, 147sylan9eq 2230 . . . . . . . . . . 11 ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +𝑒 -𝑒𝐴) = (-∞ +𝑒 +∞))
149 mnfaddpnf 9835 . . . . . . . . . . 11 (-∞ +𝑒 +∞) = 0
150148, 149eqtrdi 2226 . . . . . . . . . 10 ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐵 +𝑒 -𝑒𝐴) = 0)
151150breq2d 4012 . . . . . . . . 9 ((𝐴 = -∞ ∧ 𝐵 = -∞) → (0 < (𝐵 +𝑒 -𝑒𝐴) ↔ 0 < 0))
15277, 151mtbiri 675 . . . . . . . 8 ((𝐴 = -∞ ∧ 𝐵 = -∞) → ¬ 0 < (𝐵 +𝑒 -𝑒𝐴))
153146, 1522falsed 702 . . . . . . 7 ((𝐴 = -∞ ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
154153ex 115 . . . . . 6 (𝐴 = -∞ → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
155120, 142, 1543jaoi 1303 . . . . 5 ((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
1562, 155sylbi 121 . . . 4 (𝐴 ∈ ℝ* → (𝐵 = -∞ → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
15752, 101, 1563jaod 1304 . . 3 (𝐴 ∈ ℝ* → ((𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
1581, 157biimtrid 152 . 2 (𝐴 ∈ ℝ* → (𝐵 ∈ ℝ* → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴))))
159158imp 124 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → (𝐴 < 𝐵 ↔ 0 < (𝐵 +𝑒 -𝑒𝐴)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  w3o 977   = wceq 1353  wcel 2148  wne 2347   class class class wbr 4000  (class class class)co 5869  cr 7798  0cc0 7799  +∞cpnf 7976  -∞cmnf 7977  *cxr 7978   < clt 7979  cmin 8115  -cneg 8116  -𝑒cxne 9753   +𝑒 cxad 9754
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 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-setind 4533  ax-cnex 7890  ax-resscn 7891  ax-1cn 7892  ax-1re 7893  ax-icn 7894  ax-addcl 7895  ax-addrcl 7896  ax-mulcl 7897  ax-addcom 7899  ax-addass 7901  ax-distr 7903  ax-i2m1 7904  ax-0id 7907  ax-rnegex 7908  ax-cnre 7910  ax-pre-ltirr 7911  ax-pre-ltadd 7915
This theorem depends on definitions:  df-bi 117  df-dc 835  df-3or 979  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-nel 2443  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-if 3535  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-br 4001  df-opab 4062  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-iota 5174  df-fun 5214  df-fv 5220  df-riota 5825  df-ov 5872  df-oprab 5873  df-mpo 5874  df-pnf 7981  df-mnf 7982  df-xr 7983  df-ltxr 7984  df-sub 8117  df-neg 8118  df-xneg 9756  df-xadd 9757
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator