Theorem redivne0bd

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

	Ref	Expression
Hypotheses	redivcan2d.a	$$⊢\phi \to A\in ℝ$$
	redivcan2d.b	$$⊢\phi \to B\in ℝ$$
	redivcan2d.z	$$⊢\phi \to B\ne 0$$
Assertion	redivne0bd	$$⊢\phi \to \left(A\ne 0\leftrightarrow A{/}_{ℝ}B\ne 0\right)$$

Proof

Step	Hyp	Ref	Expression
1		redivcan2d.a	$$⊢\phi \to A\in ℝ$$
2		redivcan2d.b	$$⊢\phi \to B\in ℝ$$
3		redivcan2d.z	$$⊢\phi \to B\ne 0$$
4	1 2 3	rediveq0d	$$⊢\phi \to \left(A{/}_{ℝ}B=0\leftrightarrow A=0\right)$$
5	4	bicomd	$$⊢\phi \to \left(A=0\leftrightarrow A{/}_{ℝ}B=0\right)$$
6	5	necon3bid	$$⊢\phi \to \left(A\ne 0\leftrightarrow A{/}_{ℝ}B\ne 0\right)$$