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 ) ) |