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

Theorem xltadd1 9863
Description: Extended real version of ltadd1 8376. (Contributed by Mario Carneiro, 23-Aug-2015.) (Revised by Jim Kingdon, 16-Apr-2023.)
Assertion
Ref Expression
xltadd1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))

Proof of Theorem xltadd1
StepHypRef Expression
1 simplr 528 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → 𝐴 ∈ ℝ)
2 simpr 110 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
3 simpll3 1038 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → 𝐶 ∈ ℝ)
4 ltadd1 8376 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶)))
5 simp1 997 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐴 ∈ ℝ)
6 simp3 999 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐶 ∈ ℝ)
75, 6rexaddd 9841 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐶) = (𝐴 + 𝐶))
8 simp2 998 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → 𝐵 ∈ ℝ)
98, 6rexaddd 9841 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶))
107, 9breq12d 4013 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶) ↔ (𝐴 + 𝐶) < (𝐵 + 𝐶)))
114, 10bitr4d 191 . . . 4 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
121, 2, 3, 11syl3anc 1238 . . 3 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
13 ltpnf 9767 . . . . . 6 (𝐴 ∈ ℝ → 𝐴 < +∞)
1413ad2antlr 489 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → 𝐴 < +∞)
15 breq2 4004 . . . . . 6 (𝐵 = +∞ → (𝐴 < 𝐵𝐴 < +∞))
1615adantl 277 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐴 < 𝐵𝐴 < +∞))
1714, 16mpbird 167 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → 𝐴 < 𝐵)
18 simplr 528 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → 𝐴 ∈ ℝ)
19 simpll3 1038 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → 𝐶 ∈ ℝ)
20 rexadd 9839 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐶) = (𝐴 + 𝐶))
21 readdcl 7928 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 + 𝐶) ∈ ℝ)
2220, 21eqeltrd 2254 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 +𝑒 𝐶) ∈ ℝ)
2318, 19, 22syl2anc 411 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) ∈ ℝ)
24 ltpnf 9767 . . . . . 6 ((𝐴 +𝑒 𝐶) ∈ ℝ → (𝐴 +𝑒 𝐶) < +∞)
2523, 24syl 14 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) < +∞)
26 oveq1 5876 . . . . . . 7 (𝐵 = +∞ → (𝐵 +𝑒 𝐶) = (+∞ +𝑒 𝐶))
2726adantl 277 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = (+∞ +𝑒 𝐶))
28 rexr 7993 . . . . . . . 8 (𝐶 ∈ ℝ → 𝐶 ∈ ℝ*)
29 renemnf 7996 . . . . . . . 8 (𝐶 ∈ ℝ → 𝐶 ≠ -∞)
30 xaddpnf2 9834 . . . . . . . 8 ((𝐶 ∈ ℝ*𝐶 ≠ -∞) → (+∞ +𝑒 𝐶) = +∞)
3128, 29, 30syl2anc 411 . . . . . . 7 (𝐶 ∈ ℝ → (+∞ +𝑒 𝐶) = +∞)
3219, 31syl 14 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → (+∞ +𝑒 𝐶) = +∞)
3327, 32eqtrd 2210 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = +∞)
3425, 33breqtrrd 4028 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶))
3517, 342thd 175 . . 3 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
36 mnfle 9779 . . . . . . . 8 (𝐴 ∈ ℝ* → -∞ ≤ 𝐴)
37363ad2ant1 1018 . . . . . . 7 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) → -∞ ≤ 𝐴)
3837ad2antrr 488 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → -∞ ≤ 𝐴)
39 mnfxr 8004 . . . . . . 7 -∞ ∈ ℝ*
40 simpll1 1036 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → 𝐴 ∈ ℝ*)
41 xrlenlt 8012 . . . . . . 7 ((-∞ ∈ ℝ*𝐴 ∈ ℝ*) → (-∞ ≤ 𝐴 ↔ ¬ 𝐴 < -∞))
4239, 40, 41sylancr 414 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → (-∞ ≤ 𝐴 ↔ ¬ 𝐴 < -∞))
4338, 42mpbid 147 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → ¬ 𝐴 < -∞)
44 breq2 4004 . . . . . 6 (𝐵 = -∞ → (𝐴 < 𝐵𝐴 < -∞))
4544adantl 277 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐴 < 𝐵𝐴 < -∞))
4643, 45mtbird 673 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → ¬ 𝐴 < 𝐵)
47283ad2ant3 1020 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) → 𝐶 ∈ ℝ*)
4847ad2antrr 488 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → 𝐶 ∈ ℝ*)
49 xaddcl 9847 . . . . . . . 8 ((𝐴 ∈ ℝ*𝐶 ∈ ℝ*) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
5040, 48, 49syl2anc 411 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) ∈ ℝ*)
51 mnfle 9779 . . . . . . 7 ((𝐴 +𝑒 𝐶) ∈ ℝ* → -∞ ≤ (𝐴 +𝑒 𝐶))
5250, 51syl 14 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → -∞ ≤ (𝐴 +𝑒 𝐶))
53 xrlenlt 8012 . . . . . . 7 ((-∞ ∈ ℝ* ∧ (𝐴 +𝑒 𝐶) ∈ ℝ*) → (-∞ ≤ (𝐴 +𝑒 𝐶) ↔ ¬ (𝐴 +𝑒 𝐶) < -∞))
5439, 50, 53sylancr 414 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → (-∞ ≤ (𝐴 +𝑒 𝐶) ↔ ¬ (𝐴 +𝑒 𝐶) < -∞))
5552, 54mpbid 147 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → ¬ (𝐴 +𝑒 𝐶) < -∞)
56 simpr 110 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → 𝐵 = -∞)
5756oveq1d 5884 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐵 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
58 renepnf 7995 . . . . . . . . . 10 (𝐶 ∈ ℝ → 𝐶 ≠ +∞)
59583ad2ant3 1020 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) → 𝐶 ≠ +∞)
6059ad2antrr 488 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → 𝐶 ≠ +∞)
61 xaddmnf2 9836 . . . . . . . 8 ((𝐶 ∈ ℝ*𝐶 ≠ +∞) → (-∞ +𝑒 𝐶) = -∞)
6248, 60, 61syl2anc 411 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → (-∞ +𝑒 𝐶) = -∞)
6357, 62eqtrd 2210 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐵 +𝑒 𝐶) = -∞)
6463breq2d 4012 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → ((𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶) ↔ (𝐴 +𝑒 𝐶) < -∞))
6555, 64mtbird 673 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → ¬ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶))
6646, 652falsed 702 . . 3 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
67 elxr 9763 . . . . . 6 (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
6867biimpi 120 . . . . 5 (𝐵 ∈ ℝ* → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
69683ad2ant2 1019 . . . 4 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
7069adantr 276 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
7112, 35, 66, 70mpjao3dan 1307 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
72 simpl2 1001 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → 𝐵 ∈ ℝ*)
73 pnfge 9776 . . . . . 6 (𝐵 ∈ ℝ*𝐵 ≤ +∞)
7472, 73syl 14 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → 𝐵 ≤ +∞)
75 pnfxr 8000 . . . . . . 7 +∞ ∈ ℝ*
7675a1i 9 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → +∞ ∈ ℝ*)
77 xrlenlt 8012 . . . . . 6 ((𝐵 ∈ ℝ* ∧ +∞ ∈ ℝ*) → (𝐵 ≤ +∞ ↔ ¬ +∞ < 𝐵))
7872, 76, 77syl2anc 411 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐵 ≤ +∞ ↔ ¬ +∞ < 𝐵))
7974, 78mpbid 147 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → ¬ +∞ < 𝐵)
80 simpr 110 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → 𝐴 = +∞)
8180breq1d 4010 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐴 < 𝐵 ↔ +∞ < 𝐵))
8279, 81mtbird 673 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → ¬ 𝐴 < 𝐵)
8347adantr 276 . . . . . . . 8 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → 𝐶 ∈ ℝ*)
84 xaddcl 9847 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐶 ∈ ℝ*) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
8572, 83, 84syl2anc 411 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐵 +𝑒 𝐶) ∈ ℝ*)
86 pnfge 9776 . . . . . . 7 ((𝐵 +𝑒 𝐶) ∈ ℝ* → (𝐵 +𝑒 𝐶) ≤ +∞)
8785, 86syl 14 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐵 +𝑒 𝐶) ≤ +∞)
88293ad2ant3 1020 . . . . . . . 8 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) → 𝐶 ≠ -∞)
8988adantr 276 . . . . . . 7 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → 𝐶 ≠ -∞)
9083, 89, 30syl2anc 411 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (+∞ +𝑒 𝐶) = +∞)
9187, 90breqtrrd 4028 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐵 +𝑒 𝐶) ≤ (+∞ +𝑒 𝐶))
92 xaddcl 9847 . . . . . . 7 ((+∞ ∈ ℝ*𝐶 ∈ ℝ*) → (+∞ +𝑒 𝐶) ∈ ℝ*)
9375, 83, 92sylancr 414 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (+∞ +𝑒 𝐶) ∈ ℝ*)
94 xrlenlt 8012 . . . . . 6 (((𝐵 +𝑒 𝐶) ∈ ℝ* ∧ (+∞ +𝑒 𝐶) ∈ ℝ*) → ((𝐵 +𝑒 𝐶) ≤ (+∞ +𝑒 𝐶) ↔ ¬ (+∞ +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
9585, 93, 94syl2anc 411 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → ((𝐵 +𝑒 𝐶) ≤ (+∞ +𝑒 𝐶) ↔ ¬ (+∞ +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
9691, 95mpbid 147 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → ¬ (+∞ +𝑒 𝐶) < (𝐵 +𝑒 𝐶))
9780oveq1d 5884 . . . . 5 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐴 +𝑒 𝐶) = (+∞ +𝑒 𝐶))
9897breq1d 4010 . . . 4 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → ((𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶) ↔ (+∞ +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
9996, 98mtbird 673 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → ¬ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶))
10082, 992falsed 702 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = +∞) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
101 simplr 528 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → 𝐴 = -∞)
102 mnflt 9770 . . . . . 6 (𝐵 ∈ ℝ → -∞ < 𝐵)
103102adantl 277 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → -∞ < 𝐵)
104101, 103eqbrtrd 4022 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → 𝐴 < 𝐵)
105101oveq1d 5884 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
106 simpll3 1038 . . . . . . . 8 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → 𝐶 ∈ ℝ)
107106, 28syl 14 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → 𝐶 ∈ ℝ*)
108106, 58syl 14 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → 𝐶 ≠ +∞)
109107, 108, 61syl2anc 411 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → (-∞ +𝑒 𝐶) = -∞)
110105, 109eqtrd 2210 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) = -∞)
111 simpr 110 . . . . . . 7 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ℝ)
112 rexadd 9839 . . . . . . . 8 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) = (𝐵 + 𝐶))
113 readdcl 7928 . . . . . . . 8 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 + 𝐶) ∈ ℝ)
114112, 113eqeltrd 2254 . . . . . . 7 ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵 +𝑒 𝐶) ∈ ℝ)
115111, 106, 114syl2anc 411 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → (𝐵 +𝑒 𝐶) ∈ ℝ)
116 mnflt 9770 . . . . . 6 ((𝐵 +𝑒 𝐶) ∈ ℝ → -∞ < (𝐵 +𝑒 𝐶))
117115, 116syl 14 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → -∞ < (𝐵 +𝑒 𝐶))
118110, 117eqbrtrd 4022 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶))
119104, 1182thd 175 . . 3 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
120 simplr 528 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐴 = -∞)
121 simpr 110 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → 𝐵 = +∞)
122120, 121breq12d 4013 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ -∞ < +∞))
123 oveq1 5876 . . . . . . 7 (𝐴 = -∞ → (𝐴 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
12447, 59, 61syl2anc 411 . . . . . . 7 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) → (-∞ +𝑒 𝐶) = -∞)
125123, 124sylan9eqr 2232 . . . . . 6 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 +𝑒 𝐶) = -∞)
126125adantr 276 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐶) = -∞)
12726adantl 277 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = (+∞ +𝑒 𝐶))
12847, 88, 30syl2anc 411 . . . . . . 7 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) → (+∞ +𝑒 𝐶) = +∞)
129128ad2antrr 488 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (+∞ +𝑒 𝐶) = +∞)
130127, 129eqtrd 2210 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐵 +𝑒 𝐶) = +∞)
131126, 130breq12d 4013 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → ((𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶) ↔ -∞ < +∞))
132122, 131bitr4d 191 . . 3 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = +∞) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
133 simplr 528 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = -∞) → 𝐴 = -∞)
134 simpr 110 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = -∞) → 𝐵 = -∞)
135133, 134breq12d 4013 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ -∞ < -∞))
136124ad2antrr 488 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = -∞) → (-∞ +𝑒 𝐶) = -∞)
137123eqeq1d 2186 . . . . . . 7 (𝐴 = -∞ → ((𝐴 +𝑒 𝐶) = -∞ ↔ (-∞ +𝑒 𝐶) = -∞))
138137ad2antlr 489 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = -∞) → ((𝐴 +𝑒 𝐶) = -∞ ↔ (-∞ +𝑒 𝐶) = -∞))
139136, 138mpbird 167 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐶) = -∞)
140134oveq1d 5884 . . . . . 6 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = -∞) → (𝐵 +𝑒 𝐶) = (-∞ +𝑒 𝐶))
141140, 136eqtrd 2210 . . . . 5 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = -∞) → (𝐵 +𝑒 𝐶) = -∞)
142139, 141breq12d 4013 . . . 4 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = -∞) → ((𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶) ↔ -∞ < -∞))
143135, 142bitr4d 191 . . 3 ((((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) ∧ 𝐵 = -∞) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
14469adantr 276 . . 3 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
145119, 132, 143, 144mpjao3dan 1307 . 2 (((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) ∧ 𝐴 = -∞) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
146 elxr 9763 . . . 4 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
147146biimpi 120 . . 3 (𝐴 ∈ ℝ* → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
1481473ad2ant1 1018 . 2 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) → (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
14971, 100, 145, 148mpjao3dan 1307 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*𝐶 ∈ ℝ) → (𝐴 < 𝐵 ↔ (𝐴 +𝑒 𝐶) < (𝐵 +𝑒 𝐶)))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 104  wb 105  w3o 977  w3a 978   = wceq 1353  wcel 2148  wne 2347   class class class wbr 4000  (class class class)co 5869  cr 7801   + caddc 7805  +∞cpnf 7979  -∞cmnf 7980  *cxr 7981   < clt 7982  cle 7983   +𝑒 cxad 9757
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 7893  ax-resscn 7894  ax-1cn 7895  ax-1re 7896  ax-icn 7897  ax-addcl 7898  ax-addrcl 7899  ax-mulcl 7900  ax-addcom 7902  ax-addass 7904  ax-i2m1 7907  ax-0id 7910  ax-rnegex 7911  ax-pre-ltadd 7918
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-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  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-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-fv 5220  df-ov 5872  df-oprab 5873  df-mpo 5874  df-1st 6135  df-2nd 6136  df-pnf 7984  df-mnf 7985  df-xr 7986  df-ltxr 7987  df-le 7988  df-xadd 9760
This theorem is referenced by:  xltadd2  9864  xlt2add  9867  xrmaxaddlem  11252
  Copyright terms: Public domain W3C validator