This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divne0i

Description: The ratio of nonzero numbers is nonzero. (Contributed by NM, 9-Feb-1995)

Ref Expression
Hypotheses divclz.1 ⊢ 𝐴 ∈ ℂ
divclz.2 ⊢ 𝐵 ∈ ℂ
divneq0.3 ⊢ 𝐴 ≠ 0
divneq0.4 ⊢ 𝐵 ≠ 0
Assertion divne0i ( 𝐴 / 𝐵 ) ≠ 0

Proof

Step Hyp Ref Expression
1 divclz.1 ⊢ 𝐴 ∈ ℂ
2 divclz.2 ⊢ 𝐵 ∈ ℂ
3 divneq0.3 ⊢ 𝐴 ≠ 0
4 divneq0.4 ⊢ 𝐵 ≠ 0
5 divne0 ⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ≠ 0 )
6 1 3 2 4 5 mp4an ⊢ ( 𝐴 / 𝐵 ) ≠ 0