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

Metamath Proof Explorer

Theorem redivne0bd

Description: The ratio of nonzero numbers is nonzero. (Contributed by SN, 2-Apr-2026)

Ref Expression
Hypotheses redivcan2d.a ⊢ φ → A ∈ ℝ
redivcan2d.b ⊢ φ → B ∈ ℝ
redivcan2d.z ⊢ φ → B ≠ 0
Assertion redivne0bd Could not format assertion : No typesetting found for |- ( ph -> ( A =/= 0 <-> ( A /R B ) =/= 0 ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 redivcan2d.a ⊢ φ → A ∈ ℝ
2 redivcan2d.b ⊢ φ → B ∈ ℝ
3 redivcan2d.z ⊢ φ → B ≠ 0
4 1 2 3 rediveq0d Could not format ( ph -> ( ( A /R B ) = 0 <-> A = 0 ) ) : No typesetting found for |- ( ph -> ( ( A /R B ) = 0 <-> A = 0 ) ) with typecode |-
5 4 bicomd Could not format ( ph -> ( A = 0 <-> ( A /R B ) = 0 ) ) : No typesetting found for |- ( ph -> ( A = 0 <-> ( A /R B ) = 0 ) ) with typecode |-
6 5 necon3bid Could not format ( ph -> ( A =/= 0 <-> ( A /R B ) =/= 0 ) ) : No typesetting found for |- ( ph -> ( A =/= 0 <-> ( A /R B ) =/= 0 ) ) with typecode |-