This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: The ratio of nonzero numbers is nonzero. (Contributed by NM, 2-Aug-2004)
(Proof shortened by Mario Carneiro, 27-May-2016)
|
|
Ref |
Expression |
|
Assertion |
divne0b |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 ≠ 0 ↔ ( 𝐴 / 𝐵 ) ≠ 0 ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
diveq0 |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( ( 𝐴 / 𝐵 ) = 0 ↔ 𝐴 = 0 ) ) |
| 2 |
1
|
bicomd |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 = 0 ↔ ( 𝐴 / 𝐵 ) = 0 ) ) |
| 3 |
2
|
necon3bid |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 𝐴 ≠ 0 ↔ ( 𝐴 / 𝐵 ) ≠ 0 ) ) |