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	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	$$⊢\phi \to A\in ℝ$$
2		redivcan2d.b	$$⊢\phi \to B\in ℝ$$
3		redivcan2d.z	$$⊢\phi \to B\ne 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 |-