Proof of Theorem xmulge0
| Step | Hyp | Ref
| Expression |
| 1 | | xmulgt0 13325 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 0 < 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 < 𝐵)) → 0 < (𝐴 ·e 𝐵)) |
| 2 | 1 | an4s 660 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (0 < 𝐴 ∧ 0 < 𝐵)) → 0 < (𝐴 ·e 𝐵)) |
| 3 | | 0xr 11308 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
| 4 | | xmulcl 13315 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (𝐴 ·e 𝐵) ∈
ℝ*) |
| 5 | 4 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (0 < 𝐴 ∧ 0 < 𝐵)) → (𝐴 ·e 𝐵) ∈
ℝ*) |
| 6 | | xrltle 13191 |
. . . . . . . 8
⊢ ((0
∈ ℝ* ∧ (𝐴 ·e 𝐵) ∈ ℝ*) → (0 <
(𝐴 ·e
𝐵) → 0 ≤ (𝐴 ·e 𝐵))) |
| 7 | 3, 5, 6 | sylancr 587 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (0 < 𝐴 ∧ 0 < 𝐵)) → (0 < (𝐴 ·e 𝐵) → 0 ≤ (𝐴 ·e 𝐵))) |
| 8 | 2, 7 | mpd 15 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) ∧ (0 < 𝐴 ∧ 0 < 𝐵)) → 0 ≤ (𝐴 ·e 𝐵)) |
| 9 | 8 | ex 412 |
. . . . 5
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 ≤ (𝐴 ·e 𝐵))) |
| 10 | 9 | ad2ant2r 747 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) → ((0 < 𝐴 ∧ 0 < 𝐵) → 0 ≤ (𝐴 ·e 𝐵))) |
| 11 | 10 | impl 455 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤
𝐵)) ∧ 0 < 𝐴) ∧ 0 < 𝐵) → 0 ≤ (𝐴 ·e 𝐵)) |
| 12 | | 0le0 12367 |
. . . . 5
⊢ 0 ≤
0 |
| 13 | | oveq2 7439 |
. . . . . . 7
⊢ (0 =
𝐵 → (𝐴 ·e 0) = (𝐴 ·e 𝐵)) |
| 14 | 13 | eqcomd 2743 |
. . . . . 6
⊢ (0 =
𝐵 → (𝐴 ·e 𝐵) = (𝐴 ·e 0)) |
| 15 | | xmul01 13309 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ*
→ (𝐴
·e 0) = 0) |
| 16 | 15 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) → (𝐴 ·e 0) =
0) |
| 17 | 14, 16 | sylan9eqr 2799 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) ∧ 0 = 𝐵) → (𝐴 ·e 𝐵) = 0) |
| 18 | 12, 17 | breqtrrid 5181 |
. . . 4
⊢ ((((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) ∧ 0 = 𝐵) → 0 ≤ (𝐴 ·e 𝐵)) |
| 19 | 18 | adantlr 715 |
. . 3
⊢
(((((𝐴 ∈
ℝ* ∧ 0 ≤ 𝐴) ∧ (𝐵 ∈ ℝ* ∧ 0 ≤
𝐵)) ∧ 0 < 𝐴) ∧ 0 = 𝐵) → 0 ≤ (𝐴 ·e 𝐵)) |
| 20 | | xrleloe 13186 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (0 ≤
𝐵 ↔ (0 < 𝐵 ∨ 0 = 𝐵))) |
| 21 | 3, 20 | mpan 690 |
. . . . 5
⊢ (𝐵 ∈ ℝ*
→ (0 ≤ 𝐵 ↔ (0
< 𝐵 ∨ 0 = 𝐵))) |
| 22 | 21 | biimpa 476 |
. . . 4
⊢ ((𝐵 ∈ ℝ*
∧ 0 ≤ 𝐵) → (0
< 𝐵 ∨ 0 = 𝐵)) |
| 23 | 22 | ad2antlr 727 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) ∧ 0 < 𝐴) → (0 < 𝐵 ∨ 0 = 𝐵)) |
| 24 | 11, 19, 23 | mpjaodan 961 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) ∧ 0 < 𝐴) → 0 ≤ (𝐴 ·e 𝐵)) |
| 25 | | oveq1 7438 |
. . . . 5
⊢ (0 =
𝐴 → (0
·e 𝐵) =
(𝐴 ·e
𝐵)) |
| 26 | 25 | eqcomd 2743 |
. . . 4
⊢ (0 =
𝐴 → (𝐴 ·e 𝐵) = (0 ·e 𝐵)) |
| 27 | | xmul02 13310 |
. . . . 5
⊢ (𝐵 ∈ ℝ*
→ (0 ·e 𝐵) = 0) |
| 28 | 27 | ad2antrl 728 |
. . . 4
⊢ (((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) → (0 ·e 𝐵) = 0) |
| 29 | 26, 28 | sylan9eqr 2799 |
. . 3
⊢ ((((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) ∧ 0 = 𝐴) → (𝐴 ·e 𝐵) = 0) |
| 30 | 12, 29 | breqtrrid 5181 |
. 2
⊢ ((((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) ∧ 0 = 𝐴) → 0 ≤ (𝐴 ·e 𝐵)) |
| 31 | | xrleloe 13186 |
. . . . 5
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ*) → (0 ≤
𝐴 ↔ (0 < 𝐴 ∨ 0 = 𝐴))) |
| 32 | 3, 31 | mpan 690 |
. . . 4
⊢ (𝐴 ∈ ℝ*
→ (0 ≤ 𝐴 ↔ (0
< 𝐴 ∨ 0 = 𝐴))) |
| 33 | 32 | biimpa 476 |
. . 3
⊢ ((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) → (0
< 𝐴 ∨ 0 = 𝐴)) |
| 34 | 33 | adantr 480 |
. 2
⊢ (((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) → (0 < 𝐴 ∨ 0 = 𝐴)) |
| 35 | 24, 30, 34 | mpjaodan 961 |
1
⊢ (((𝐴 ∈ ℝ*
∧ 0 ≤ 𝐴) ∧
(𝐵 ∈
ℝ* ∧ 0 ≤ 𝐵)) → 0 ≤ (𝐴 ·e 𝐵)) |