MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xnegdi Structured version   Visualization version   GIF version

Theorem xnegdi 13167
Description: Extended real version of negdi 11458. (Contributed by Mario Carneiro, 20-Aug-2015.)
Assertion
Ref Expression
xnegdi ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))

Proof of Theorem xnegdi
StepHypRef Expression
1 elxr 13037 . 2 (𝐴 ∈ ℝ* ↔ (𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞))
2 elxr 13037 . . . 4 (𝐵 ∈ ℝ* ↔ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞))
3 recn 11141 . . . . . . . 8 (𝐴 ∈ ℝ → 𝐴 ∈ ℂ)
4 recn 11141 . . . . . . . 8 (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
5 negdi 11458 . . . . . . . 8 ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
63, 4, 5syl2an 596 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -(𝐴 + 𝐵) = (-𝐴 + -𝐵))
7 readdcl 11134 . . . . . . . 8 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
8 rexneg 13130 . . . . . . . 8 ((𝐴 + 𝐵) ∈ ℝ → -𝑒(𝐴 + 𝐵) = -(𝐴 + 𝐵))
97, 8syl 17 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 + 𝐵) = -(𝐴 + 𝐵))
10 renegcl 11464 . . . . . . . 8 (𝐴 ∈ ℝ → -𝐴 ∈ ℝ)
11 renegcl 11464 . . . . . . . 8 (𝐵 ∈ ℝ → -𝐵 ∈ ℝ)
12 rexadd 13151 . . . . . . . 8 ((-𝐴 ∈ ℝ ∧ -𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵))
1310, 11, 12syl2an 596 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝐴 +𝑒 -𝐵) = (-𝐴 + -𝐵))
146, 9, 133eqtr4d 2786 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 + 𝐵) = (-𝐴 +𝑒 -𝐵))
15 rexadd 13151 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 +𝑒 𝐵) = (𝐴 + 𝐵))
16 xnegeq 13126 . . . . . . 7 ((𝐴 +𝑒 𝐵) = (𝐴 + 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(𝐴 + 𝐵))
1715, 16syl 17 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(𝐴 + 𝐵))
18 rexneg 13130 . . . . . . 7 (𝐴 ∈ ℝ → -𝑒𝐴 = -𝐴)
19 rexneg 13130 . . . . . . 7 (𝐵 ∈ ℝ → -𝑒𝐵 = -𝐵)
2018, 19oveqan12d 7376 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝐴 +𝑒 -𝐵))
2114, 17, 203eqtr4d 2786 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
22 xnegpnf 13128 . . . . . 6 -𝑒+∞ = -∞
23 oveq2 7365 . . . . . . . 8 (𝐵 = +∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 +∞))
24 rexr 11201 . . . . . . . . 9 (𝐴 ∈ ℝ → 𝐴 ∈ ℝ*)
25 renemnf 11204 . . . . . . . . 9 (𝐴 ∈ ℝ → 𝐴 ≠ -∞)
26 xaddpnf1 13145 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐴 ≠ -∞) → (𝐴 +𝑒 +∞) = +∞)
2724, 25, 26syl2anc 584 . . . . . . . 8 (𝐴 ∈ ℝ → (𝐴 +𝑒 +∞) = +∞)
2823, 27sylan9eqr 2798 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (𝐴 +𝑒 𝐵) = +∞)
29 xnegeq 13126 . . . . . . 7 ((𝐴 +𝑒 𝐵) = +∞ → -𝑒(𝐴 +𝑒 𝐵) = -𝑒+∞)
3028, 29syl 17 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒+∞)
31 xnegeq 13126 . . . . . . . . 9 (𝐵 = +∞ → -𝑒𝐵 = -𝑒+∞)
3231, 22eqtrdi 2792 . . . . . . . 8 (𝐵 = +∞ → -𝑒𝐵 = -∞)
3332oveq2d 7373 . . . . . . 7 (𝐵 = +∞ → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒 -∞))
3418, 10eqeltrd 2838 . . . . . . . 8 (𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ)
35 rexr 11201 . . . . . . . . 9 (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ∈ ℝ*)
36 renepnf 11203 . . . . . . . . 9 (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ≠ +∞)
37 xaddmnf1 13147 . . . . . . . . 9 ((-𝑒𝐴 ∈ ℝ* ∧ -𝑒𝐴 ≠ +∞) → (-𝑒𝐴 +𝑒 -∞) = -∞)
3835, 36, 37syl2anc 584 . . . . . . . 8 (-𝑒𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 -∞) = -∞)
3934, 38syl 17 . . . . . . 7 (𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 -∞) = -∞)
4033, 39sylan9eqr 2798 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = -∞)
4122, 30, 403eqtr4a 2802 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 = +∞) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
42 xnegmnf 13129 . . . . . 6 -𝑒-∞ = +∞
43 oveq2 7365 . . . . . . . 8 (𝐵 = -∞ → (𝐴 +𝑒 𝐵) = (𝐴 +𝑒 -∞))
44 renepnf 11203 . . . . . . . . 9 (𝐴 ∈ ℝ → 𝐴 ≠ +∞)
45 xaddmnf1 13147 . . . . . . . . 9 ((𝐴 ∈ ℝ*𝐴 ≠ +∞) → (𝐴 +𝑒 -∞) = -∞)
4624, 44, 45syl2anc 584 . . . . . . . 8 (𝐴 ∈ ℝ → (𝐴 +𝑒 -∞) = -∞)
4743, 46sylan9eqr 2798 . . . . . . 7 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (𝐴 +𝑒 𝐵) = -∞)
48 xnegeq 13126 . . . . . . 7 ((𝐴 +𝑒 𝐵) = -∞ → -𝑒(𝐴 +𝑒 𝐵) = -𝑒-∞)
4947, 48syl 17 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒-∞)
50 xnegeq 13126 . . . . . . . . 9 (𝐵 = -∞ → -𝑒𝐵 = -𝑒-∞)
5150, 42eqtrdi 2792 . . . . . . . 8 (𝐵 = -∞ → -𝑒𝐵 = +∞)
5251oveq2d 7373 . . . . . . 7 (𝐵 = -∞ → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-𝑒𝐴 +𝑒 +∞))
53 renemnf 11204 . . . . . . . . 9 (-𝑒𝐴 ∈ ℝ → -𝑒𝐴 ≠ -∞)
54 xaddpnf1 13145 . . . . . . . . 9 ((-𝑒𝐴 ∈ ℝ* ∧ -𝑒𝐴 ≠ -∞) → (-𝑒𝐴 +𝑒 +∞) = +∞)
5535, 53, 54syl2anc 584 . . . . . . . 8 (-𝑒𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 +∞) = +∞)
5634, 55syl 17 . . . . . . 7 (𝐴 ∈ ℝ → (-𝑒𝐴 +𝑒 +∞) = +∞)
5752, 56sylan9eqr 2798 . . . . . 6 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = +∞)
5842, 49, 573eqtr4a 2802 . . . . 5 ((𝐴 ∈ ℝ ∧ 𝐵 = -∞) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
5921, 41, 583jaodan 1430 . . . 4 ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∨ 𝐵 = +∞ ∨ 𝐵 = -∞)) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
602, 59sylan2b 594 . . 3 ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
61 xneg0 13131 . . . . . . 7 -𝑒0 = 0
62 simpr 485 . . . . . . . . . 10 ((𝐵 ∈ ℝ*𝐵 = -∞) → 𝐵 = -∞)
6362oveq2d 7373 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐵 = -∞) → (+∞ +𝑒 𝐵) = (+∞ +𝑒 -∞))
64 pnfaddmnf 13149 . . . . . . . . 9 (+∞ +𝑒 -∞) = 0
6563, 64eqtrdi 2792 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐵 = -∞) → (+∞ +𝑒 𝐵) = 0)
66 xnegeq 13126 . . . . . . . 8 ((+∞ +𝑒 𝐵) = 0 → -𝑒(+∞ +𝑒 𝐵) = -𝑒0)
6765, 66syl 17 . . . . . . 7 ((𝐵 ∈ ℝ*𝐵 = -∞) → -𝑒(+∞ +𝑒 𝐵) = -𝑒0)
6851adantl 482 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐵 = -∞) → -𝑒𝐵 = +∞)
6968oveq2d 7373 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐵 = -∞) → (-∞ +𝑒 -𝑒𝐵) = (-∞ +𝑒 +∞))
70 mnfaddpnf 13150 . . . . . . . 8 (-∞ +𝑒 +∞) = 0
7169, 70eqtrdi 2792 . . . . . . 7 ((𝐵 ∈ ℝ*𝐵 = -∞) → (-∞ +𝑒 -𝑒𝐵) = 0)
7261, 67, 713eqtr4a 2802 . . . . . 6 ((𝐵 ∈ ℝ*𝐵 = -∞) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
73 xaddpnf2 13146 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) → (+∞ +𝑒 𝐵) = +∞)
74 xnegeq 13126 . . . . . . . 8 ((+∞ +𝑒 𝐵) = +∞ → -𝑒(+∞ +𝑒 𝐵) = -𝑒+∞)
7573, 74syl 17 . . . . . . 7 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) → -𝑒(+∞ +𝑒 𝐵) = -𝑒+∞)
76 xnegcl 13132 . . . . . . . 8 (𝐵 ∈ ℝ* → -𝑒𝐵 ∈ ℝ*)
77 xnegeq 13126 . . . . . . . . . . . 12 (-𝑒𝐵 = +∞ → -𝑒-𝑒𝐵 = -𝑒+∞)
7877, 22eqtrdi 2792 . . . . . . . . . . 11 (-𝑒𝐵 = +∞ → -𝑒-𝑒𝐵 = -∞)
79 xnegneg 13133 . . . . . . . . . . . 12 (𝐵 ∈ ℝ* → -𝑒-𝑒𝐵 = 𝐵)
8079eqeq1d 2738 . . . . . . . . . . 11 (𝐵 ∈ ℝ* → (-𝑒-𝑒𝐵 = -∞ ↔ 𝐵 = -∞))
8178, 80imbitrid 243 . . . . . . . . . 10 (𝐵 ∈ ℝ* → (-𝑒𝐵 = +∞ → 𝐵 = -∞))
8281necon3d 2964 . . . . . . . . 9 (𝐵 ∈ ℝ* → (𝐵 ≠ -∞ → -𝑒𝐵 ≠ +∞))
8382imp 407 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) → -𝑒𝐵 ≠ +∞)
84 xaddmnf2 13148 . . . . . . . 8 ((-𝑒𝐵 ∈ ℝ* ∧ -𝑒𝐵 ≠ +∞) → (-∞ +𝑒 -𝑒𝐵) = -∞)
8576, 83, 84syl2an2r 683 . . . . . . 7 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) → (-∞ +𝑒 -𝑒𝐵) = -∞)
8622, 75, 853eqtr4a 2802 . . . . . 6 ((𝐵 ∈ ℝ*𝐵 ≠ -∞) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
8772, 86pm2.61dane 3032 . . . . 5 (𝐵 ∈ ℝ* → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
8887adantl 482 . . . 4 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(+∞ +𝑒 𝐵) = (-∞ +𝑒 -𝑒𝐵))
89 simpl 483 . . . . . 6 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → 𝐴 = +∞)
9089oveq1d 7372 . . . . 5 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵))
91 xnegeq 13126 . . . . 5 ((𝐴 +𝑒 𝐵) = (+∞ +𝑒 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞ +𝑒 𝐵))
9290, 91syl 17 . . . 4 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(+∞ +𝑒 𝐵))
93 xnegeq 13126 . . . . . . 7 (𝐴 = +∞ → -𝑒𝐴 = -𝑒+∞)
9493adantr 481 . . . . . 6 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -𝑒+∞)
9594, 22eqtrdi 2792 . . . . 5 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -∞)
9695oveq1d 7372 . . . 4 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (-∞ +𝑒 -𝑒𝐵))
9788, 92, 963eqtr4d 2786 . . 3 ((𝐴 = +∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
98 simpr 485 . . . . . . . . . 10 ((𝐵 ∈ ℝ*𝐵 = +∞) → 𝐵 = +∞)
9998oveq2d 7373 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐵 = +∞) → (-∞ +𝑒 𝐵) = (-∞ +𝑒 +∞))
10099, 70eqtrdi 2792 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐵 = +∞) → (-∞ +𝑒 𝐵) = 0)
101 xnegeq 13126 . . . . . . . 8 ((-∞ +𝑒 𝐵) = 0 → -𝑒(-∞ +𝑒 𝐵) = -𝑒0)
102100, 101syl 17 . . . . . . 7 ((𝐵 ∈ ℝ*𝐵 = +∞) → -𝑒(-∞ +𝑒 𝐵) = -𝑒0)
10332adantl 482 . . . . . . . . 9 ((𝐵 ∈ ℝ*𝐵 = +∞) → -𝑒𝐵 = -∞)
104103oveq2d 7373 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐵 = +∞) → (+∞ +𝑒 -𝑒𝐵) = (+∞ +𝑒 -∞))
105104, 64eqtrdi 2792 . . . . . . 7 ((𝐵 ∈ ℝ*𝐵 = +∞) → (+∞ +𝑒 -𝑒𝐵) = 0)
10661, 102, 1053eqtr4a 2802 . . . . . 6 ((𝐵 ∈ ℝ*𝐵 = +∞) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
107 xaddmnf2 13148 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐵 ≠ +∞) → (-∞ +𝑒 𝐵) = -∞)
108 xnegeq 13126 . . . . . . . 8 ((-∞ +𝑒 𝐵) = -∞ → -𝑒(-∞ +𝑒 𝐵) = -𝑒-∞)
109107, 108syl 17 . . . . . . 7 ((𝐵 ∈ ℝ*𝐵 ≠ +∞) → -𝑒(-∞ +𝑒 𝐵) = -𝑒-∞)
110 xnegeq 13126 . . . . . . . . . . . 12 (-𝑒𝐵 = -∞ → -𝑒-𝑒𝐵 = -𝑒-∞)
111110, 42eqtrdi 2792 . . . . . . . . . . 11 (-𝑒𝐵 = -∞ → -𝑒-𝑒𝐵 = +∞)
11279eqeq1d 2738 . . . . . . . . . . 11 (𝐵 ∈ ℝ* → (-𝑒-𝑒𝐵 = +∞ ↔ 𝐵 = +∞))
113111, 112imbitrid 243 . . . . . . . . . 10 (𝐵 ∈ ℝ* → (-𝑒𝐵 = -∞ → 𝐵 = +∞))
114113necon3d 2964 . . . . . . . . 9 (𝐵 ∈ ℝ* → (𝐵 ≠ +∞ → -𝑒𝐵 ≠ -∞))
115114imp 407 . . . . . . . 8 ((𝐵 ∈ ℝ*𝐵 ≠ +∞) → -𝑒𝐵 ≠ -∞)
116 xaddpnf2 13146 . . . . . . . 8 ((-𝑒𝐵 ∈ ℝ* ∧ -𝑒𝐵 ≠ -∞) → (+∞ +𝑒 -𝑒𝐵) = +∞)
11776, 115, 116syl2an2r 683 . . . . . . 7 ((𝐵 ∈ ℝ*𝐵 ≠ +∞) → (+∞ +𝑒 -𝑒𝐵) = +∞)
11842, 109, 1173eqtr4a 2802 . . . . . 6 ((𝐵 ∈ ℝ*𝐵 ≠ +∞) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
119106, 118pm2.61dane 3032 . . . . 5 (𝐵 ∈ ℝ* → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
120119adantl 482 . . . 4 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(-∞ +𝑒 𝐵) = (+∞ +𝑒 -𝑒𝐵))
121 simpl 483 . . . . . 6 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → 𝐴 = -∞)
122121oveq1d 7372 . . . . 5 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → (𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵))
123 xnegeq 13126 . . . . 5 ((𝐴 +𝑒 𝐵) = (-∞ +𝑒 𝐵) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞ +𝑒 𝐵))
124122, 123syl 17 . . . 4 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = -𝑒(-∞ +𝑒 𝐵))
125 xnegeq 13126 . . . . . . 7 (𝐴 = -∞ → -𝑒𝐴 = -𝑒-∞)
126125adantr 481 . . . . . 6 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = -𝑒-∞)
127126, 42eqtrdi 2792 . . . . 5 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒𝐴 = +∞)
128127oveq1d 7372 . . . 4 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → (-𝑒𝐴 +𝑒 -𝑒𝐵) = (+∞ +𝑒 -𝑒𝐵))
129120, 124, 1283eqtr4d 2786 . . 3 ((𝐴 = -∞ ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
13060, 97, 1293jaoian 1429 . 2 (((𝐴 ∈ ℝ ∨ 𝐴 = +∞ ∨ 𝐴 = -∞) ∧ 𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
1311, 130sylanb 581 1 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ*) → -𝑒(𝐴 +𝑒 𝐵) = (-𝑒𝐴 +𝑒 -𝑒𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3o 1086   = wceq 1541  wcel 2106  wne 2943  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051   + caddc 11054  +∞cpnf 11186  -∞cmnf 11187  *cxr 11188  -cneg 11386  -𝑒cxne 13030   +𝑒 cxad 13031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-po 5545  df-so 5546  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-sub 11387  df-neg 11388  df-xneg 13033  df-xadd 13034
This theorem is referenced by:  xaddass2  13169  xposdif  13181  xadddi  13214  xrsxmet  24172
  Copyright terms: Public domain W3C validator