Proof of Theorem xadddi
| Step | Hyp | Ref
| Expression |
| 1 | | xadddilem 13336 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 < 𝐴) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
| 2 | | simpl2 1193 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → 𝐵 ∈
ℝ*) |
| 3 | | simpl3 1194 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → 𝐶 ∈
ℝ*) |
| 4 | | xaddcl 13281 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 5 | 2, 3, 4 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 6 | | xmul02 13310 |
. . . . 5
⊢ ((𝐵 +𝑒 𝐶) ∈ ℝ*
→ (0 ·e (𝐵 +𝑒 𝐶)) = 0) |
| 7 | 5, 6 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → (0 ·e (𝐵 +𝑒 𝐶)) = 0) |
| 8 | | 0xr 11308 |
. . . . 5
⊢ 0 ∈
ℝ* |
| 9 | | xaddrid 13283 |
. . . . 5
⊢ (0 ∈
ℝ* → (0 +𝑒 0) = 0) |
| 10 | 8, 9 | ax-mp 5 |
. . . 4
⊢ (0
+𝑒 0) = 0 |
| 11 | 7, 10 | eqtr4di 2795 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → (0 ·e (𝐵 +𝑒 𝐶)) = (0 +𝑒
0)) |
| 12 | | simpr 484 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → 0 = 𝐴) |
| 13 | 12 | oveq1d 7446 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → (0 ·e (𝐵 +𝑒 𝐶)) = (𝐴 ·e (𝐵 +𝑒 𝐶))) |
| 14 | | xmul02 13310 |
. . . . . 6
⊢ (𝐵 ∈ ℝ*
→ (0 ·e 𝐵) = 0) |
| 15 | 2, 14 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → (0 ·e 𝐵) = 0) |
| 16 | 12 | oveq1d 7446 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → (0 ·e 𝐵) = (𝐴 ·e 𝐵)) |
| 17 | 15, 16 | eqtr3d 2779 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → 0 = (𝐴 ·e 𝐵)) |
| 18 | | xmul02 13310 |
. . . . . 6
⊢ (𝐶 ∈ ℝ*
→ (0 ·e 𝐶) = 0) |
| 19 | 3, 18 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → (0 ·e 𝐶) = 0) |
| 20 | 12 | oveq1d 7446 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → (0 ·e 𝐶) = (𝐴 ·e 𝐶)) |
| 21 | 19, 20 | eqtr3d 2779 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → 0 = (𝐴 ·e 𝐶)) |
| 22 | 17, 21 | oveq12d 7449 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → (0 +𝑒 0) =
((𝐴 ·e
𝐵) +𝑒
(𝐴 ·e
𝐶))) |
| 23 | 11, 13, 22 | 3eqtr3d 2785 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 0 = 𝐴) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
| 24 | | simp1 1137 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → 𝐴 ∈ ℝ) |
| 25 | 24 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → 𝐴 ∈ ℝ) |
| 26 | | rexneg 13253 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ →
-𝑒𝐴 =
-𝐴) |
| 27 | | renegcl 11572 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → -𝐴 ∈
ℝ) |
| 28 | 26, 27 | eqeltrd 2841 |
. . . . . 6
⊢ (𝐴 ∈ ℝ →
-𝑒𝐴
∈ ℝ) |
| 29 | 25, 28 | syl 17 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → -𝑒𝐴 ∈
ℝ) |
| 30 | | simpl2 1193 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → 𝐵 ∈
ℝ*) |
| 31 | | simpl3 1194 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → 𝐶 ∈
ℝ*) |
| 32 | 24 | rexrd 11311 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → 𝐴 ∈
ℝ*) |
| 33 | | xlt0neg1 13261 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (𝐴 < 0 ↔ 0
< -𝑒𝐴)) |
| 34 | 32, 33 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 < 0 ↔ 0 <
-𝑒𝐴)) |
| 35 | 34 | biimpa 476 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → 0 <
-𝑒𝐴) |
| 36 | | xadddilem 13336 |
. . . . 5
⊢
(((-𝑒𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ*)
∧ 0 < -𝑒𝐴) → (-𝑒𝐴 ·e (𝐵 +𝑒 𝐶)) =
((-𝑒𝐴
·e 𝐵)
+𝑒 (-𝑒𝐴 ·e 𝐶))) |
| 37 | 29, 30, 31, 35, 36 | syl31anc 1375 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → (-𝑒𝐴 ·e (𝐵 +𝑒 𝐶)) =
((-𝑒𝐴
·e 𝐵)
+𝑒 (-𝑒𝐴 ·e 𝐶))) |
| 38 | 32 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → 𝐴 ∈
ℝ*) |
| 39 | 30, 31, 4 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → (𝐵 +𝑒 𝐶) ∈
ℝ*) |
| 40 | | xmulneg1 13311 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵
+𝑒 𝐶)
∈ ℝ*) → (-𝑒𝐴 ·e (𝐵 +𝑒 𝐶)) = -𝑒(𝐴 ·e (𝐵 +𝑒 𝐶))) |
| 41 | 38, 39, 40 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → (-𝑒𝐴 ·e (𝐵 +𝑒 𝐶)) = -𝑒(𝐴 ·e (𝐵 +𝑒 𝐶))) |
| 42 | | xmulneg1 13311 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (-𝑒𝐴 ·e 𝐵) = -𝑒(𝐴 ·e 𝐵)) |
| 43 | 38, 30, 42 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → (-𝑒𝐴 ·e 𝐵) = -𝑒(𝐴 ·e 𝐵)) |
| 44 | | xmulneg1 13311 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (-𝑒𝐴 ·e 𝐶) = -𝑒(𝐴 ·e 𝐶)) |
| 45 | 38, 31, 44 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → (-𝑒𝐴 ·e 𝐶) = -𝑒(𝐴 ·e 𝐶)) |
| 46 | 43, 45 | oveq12d 7449 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → ((-𝑒𝐴 ·e 𝐵) +𝑒
(-𝑒𝐴
·e 𝐶)) =
(-𝑒(𝐴
·e 𝐵)
+𝑒 -𝑒(𝐴 ·e 𝐶))) |
| 47 | | xmulcl 13315 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 ·e 𝐵) ∈
ℝ*) |
| 48 | 38, 30, 47 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → (𝐴 ·e 𝐵) ∈
ℝ*) |
| 49 | | xmulcl 13315 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 ·e 𝐶) ∈
ℝ*) |
| 50 | 38, 31, 49 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → (𝐴 ·e 𝐶) ∈
ℝ*) |
| 51 | | xnegdi 13290 |
. . . . . 6
⊢ (((𝐴 ·e 𝐵) ∈ ℝ*
∧ (𝐴
·e 𝐶)
∈ ℝ*) → -𝑒((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) = (-𝑒(𝐴 ·e 𝐵) +𝑒
-𝑒(𝐴
·e 𝐶))) |
| 52 | 48, 50, 51 | syl2anc 584 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → -𝑒((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) =
(-𝑒(𝐴
·e 𝐵)
+𝑒 -𝑒(𝐴 ·e 𝐶))) |
| 53 | 46, 52 | eqtr4d 2780 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → ((-𝑒𝐴 ·e 𝐵) +𝑒
(-𝑒𝐴
·e 𝐶)) =
-𝑒((𝐴
·e 𝐵)
+𝑒 (𝐴
·e 𝐶))) |
| 54 | 37, 41, 53 | 3eqtr3d 2785 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → -𝑒(𝐴 ·e (𝐵 +𝑒 𝐶)) =
-𝑒((𝐴
·e 𝐵)
+𝑒 (𝐴
·e 𝐶))) |
| 55 | | xmulcl 13315 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ (𝐵
+𝑒 𝐶)
∈ ℝ*) → (𝐴 ·e (𝐵 +𝑒 𝐶)) ∈
ℝ*) |
| 56 | 38, 39, 55 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → (𝐴 ·e (𝐵 +𝑒 𝐶)) ∈
ℝ*) |
| 57 | | xaddcl 13281 |
. . . . 5
⊢ (((𝐴 ·e 𝐵) ∈ ℝ*
∧ (𝐴
·e 𝐶)
∈ ℝ*) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) ∈
ℝ*) |
| 58 | 48, 50, 57 | syl2anc 584 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) ∈
ℝ*) |
| 59 | | xneg11 13257 |
. . . 4
⊢ (((𝐴 ·e (𝐵 +𝑒 𝐶)) ∈ ℝ*
∧ ((𝐴
·e 𝐵)
+𝑒 (𝐴
·e 𝐶))
∈ ℝ*) → (-𝑒(𝐴 ·e (𝐵 +𝑒 𝐶)) = -𝑒((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)) ↔ (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶)))) |
| 60 | 56, 58, 59 | syl2anc 584 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → (-𝑒(𝐴 ·e (𝐵 +𝑒 𝐶)) =
-𝑒((𝐴
·e 𝐵)
+𝑒 (𝐴
·e 𝐶))
↔ (𝐴
·e (𝐵
+𝑒 𝐶)) =
((𝐴 ·e
𝐵) +𝑒
(𝐴 ·e
𝐶)))) |
| 61 | 54, 60 | mpbid 232 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) ∧ 𝐴 < 0) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |
| 62 | | 0re 11263 |
. . 3
⊢ 0 ∈
ℝ |
| 63 | | lttri4 11345 |
. . 3
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 < 𝐴 ∨ 0 = 𝐴 ∨ 𝐴 < 0)) |
| 64 | 62, 24, 63 | sylancr 587 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (0 < 𝐴 ∨ 0 = 𝐴 ∨ 𝐴 < 0)) |
| 65 | 1, 23, 61, 64 | mpjao3dan 1434 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ*) → (𝐴 ·e (𝐵 +𝑒 𝐶)) = ((𝐴 ·e 𝐵) +𝑒 (𝐴 ·e 𝐶))) |