Proof of Theorem prodgt0
Step | Hyp | Ref
| Expression |
1 | | 0red 10367 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 0 ∈
ℝ) |
2 | | simpl 476 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐴 ∈
ℝ) |
3 | 1, 2 | leloed 10506 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤
𝐴 ↔ (0 < 𝐴 ∨ 0 = 𝐴))) |
4 | | simpll 783 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 𝐴 ∈ ℝ) |
5 | | simplr 785 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 𝐵 ∈ ℝ) |
6 | 4, 5 | remulcld 10394 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → (𝐴 · 𝐵) ∈ ℝ) |
7 | | simprl 787 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐴) |
8 | 7 | gt0ne0d 10923 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 𝐴 ≠ 0) |
9 | 4, 8 | rereccld 11185 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → (1 / 𝐴) ∈ ℝ) |
10 | | simprr 789 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < (𝐴 · 𝐵)) |
11 | | recgt0 11204 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 0 <
𝐴) → 0 < (1 / 𝐴)) |
12 | 11 | ad2ant2r 753 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < (1 / 𝐴)) |
13 | 6, 9, 10, 12 | mulgt0d 10518 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < ((𝐴 · 𝐵) · (1 / 𝐴))) |
14 | 6 | recnd 10392 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → (𝐴 · 𝐵) ∈ ℂ) |
15 | 4 | recnd 10392 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 𝐴 ∈ ℂ) |
16 | 14, 15, 8 | divrecd 11137 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → ((𝐴 · 𝐵) / 𝐴) = ((𝐴 · 𝐵) · (1 / 𝐴))) |
17 | | simpr 479 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈
ℝ) |
18 | 17 | recnd 10392 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → 𝐵 ∈
ℂ) |
19 | 18 | adantr 474 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 𝐵 ∈ ℂ) |
20 | 19, 15, 8 | divcan3d 11139 |
. . . . . . 7
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → ((𝐴 · 𝐵) / 𝐴) = 𝐵) |
21 | 16, 20 | eqtr3d 2863 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → ((𝐴 · 𝐵) · (1 / 𝐴)) = 𝐵) |
22 | 13, 21 | breqtrd 4901 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 <
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵) |
23 | 22 | exp32 413 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 <
𝐴 → (0 < (𝐴 · 𝐵) → 0 < 𝐵))) |
24 | | 0re 10365 |
. . . . . . . 8
⊢ 0 ∈
ℝ |
25 | 24 | ltnri 10472 |
. . . . . . 7
⊢ ¬ 0
< 0 |
26 | 18 | mul02d 10560 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0
· 𝐵) =
0) |
27 | 26 | breq2d 4887 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 <
(0 · 𝐵) ↔ 0
< 0)) |
28 | 25, 27 | mtbiri 319 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ¬ 0
< (0 · 𝐵)) |
29 | 28 | pm2.21d 119 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 <
(0 · 𝐵) → 0
< 𝐵)) |
30 | | oveq1 6917 |
. . . . . . 7
⊢ (0 =
𝐴 → (0 · 𝐵) = (𝐴 · 𝐵)) |
31 | 30 | breq2d 4887 |
. . . . . 6
⊢ (0 =
𝐴 → (0 < (0
· 𝐵) ↔ 0 <
(𝐴 · 𝐵))) |
32 | 31 | imbi1d 333 |
. . . . 5
⊢ (0 =
𝐴 → ((0 < (0
· 𝐵) → 0 <
𝐵) ↔ (0 < (𝐴 · 𝐵) → 0 < 𝐵))) |
33 | 29, 32 | syl5ibcom 237 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 =
𝐴 → (0 < (𝐴 · 𝐵) → 0 < 𝐵))) |
34 | 23, 33 | jaod 890 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <
𝐴 ∨ 0 = 𝐴) → (0 < (𝐴 · 𝐵) → 0 < 𝐵))) |
35 | 3, 34 | sylbid 232 |
. 2
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 ≤
𝐴 → (0 < (𝐴 · 𝐵) → 0 < 𝐵))) |
36 | 35 | imp32 411 |
1
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (0 ≤
𝐴 ∧ 0 < (𝐴 · 𝐵))) → 0 < 𝐵) |