Step |
Hyp |
Ref |
Expression |
1 |
|
xmulgt0 |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 < 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
2 |
1
|
an4s |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → 0 < ( 𝐴 ·e 𝐵 ) ) |
3 |
|
0xr |
⊢ 0 ∈ ℝ* |
4 |
|
xmulcl |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 ·e 𝐵 ) ∈ ℝ* ) |
5 |
4
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → ( 𝐴 ·e 𝐵 ) ∈ ℝ* ) |
6 |
|
xrltle |
⊢ ( ( 0 ∈ ℝ* ∧ ( 𝐴 ·e 𝐵 ) ∈ ℝ* ) → ( 0 < ( 𝐴 ·e 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) ) |
7 |
3 5 6
|
sylancr |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → ( 0 < ( 𝐴 ·e 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) ) |
8 |
2 7
|
mpd |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 0 < 𝐴 ∧ 0 < 𝐵 ) ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) |
9 |
8
|
ex |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 0 < 𝐴 ∧ 0 < 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) ) |
10 |
9
|
ad2ant2r |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → ( ( 0 < 𝐴 ∧ 0 < 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) ) |
11 |
10
|
impl |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 < 𝐴 ) ∧ 0 < 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) |
12 |
|
0le0 |
⊢ 0 ≤ 0 |
13 |
|
oveq2 |
⊢ ( 0 = 𝐵 → ( 𝐴 ·e 0 ) = ( 𝐴 ·e 𝐵 ) ) |
14 |
13
|
eqcomd |
⊢ ( 0 = 𝐵 → ( 𝐴 ·e 𝐵 ) = ( 𝐴 ·e 0 ) ) |
15 |
|
xmul01 |
⊢ ( 𝐴 ∈ ℝ* → ( 𝐴 ·e 0 ) = 0 ) |
16 |
15
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → ( 𝐴 ·e 0 ) = 0 ) |
17 |
14 16
|
sylan9eqr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 = 𝐵 ) → ( 𝐴 ·e 𝐵 ) = 0 ) |
18 |
12 17
|
breqtrrid |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 = 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) |
19 |
18
|
adantlr |
⊢ ( ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 < 𝐴 ) ∧ 0 = 𝐵 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) |
20 |
|
xrleloe |
⊢ ( ( 0 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 0 ≤ 𝐵 ↔ ( 0 < 𝐵 ∨ 0 = 𝐵 ) ) ) |
21 |
3 20
|
mpan |
⊢ ( 𝐵 ∈ ℝ* → ( 0 ≤ 𝐵 ↔ ( 0 < 𝐵 ∨ 0 = 𝐵 ) ) ) |
22 |
21
|
biimpa |
⊢ ( ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) → ( 0 < 𝐵 ∨ 0 = 𝐵 ) ) |
23 |
22
|
ad2antlr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 < 𝐴 ) → ( 0 < 𝐵 ∨ 0 = 𝐵 ) ) |
24 |
11 19 23
|
mpjaodan |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 < 𝐴 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) |
25 |
|
oveq1 |
⊢ ( 0 = 𝐴 → ( 0 ·e 𝐵 ) = ( 𝐴 ·e 𝐵 ) ) |
26 |
25
|
eqcomd |
⊢ ( 0 = 𝐴 → ( 𝐴 ·e 𝐵 ) = ( 0 ·e 𝐵 ) ) |
27 |
|
xmul02 |
⊢ ( 𝐵 ∈ ℝ* → ( 0 ·e 𝐵 ) = 0 ) |
28 |
27
|
ad2antrl |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → ( 0 ·e 𝐵 ) = 0 ) |
29 |
26 28
|
sylan9eqr |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 = 𝐴 ) → ( 𝐴 ·e 𝐵 ) = 0 ) |
30 |
12 29
|
breqtrrid |
⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) ∧ 0 = 𝐴 ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) |
31 |
|
xrleloe |
⊢ ( ( 0 ∈ ℝ* ∧ 𝐴 ∈ ℝ* ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) ) |
32 |
3 31
|
mpan |
⊢ ( 𝐴 ∈ ℝ* → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) ) |
33 |
32
|
biimpa |
⊢ ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) → ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) |
34 |
33
|
adantr |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) |
35 |
24 30 34
|
mpjaodan |
⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 0 ≤ 𝐴 ) ∧ ( 𝐵 ∈ ℝ* ∧ 0 ≤ 𝐵 ) ) → 0 ≤ ( 𝐴 ·e 𝐵 ) ) |