Theorem redivne0bd

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

	Ref	Expression
Hypotheses	redivcan2d.a	|- ( ph -> A e. RR )
	redivcan2d.b	|- ( ph -> B e. RR )
	redivcan2d.z	|- ( ph -> B =/= 0 )
Assertion	redivne0bd	|- ( ph -> ( A =/= 0 <-> ( A /R B ) =/= 0 ) )

Proof

Step	Hyp	Ref	Expression
1		redivcan2d.a	|- ( ph -> A e. RR )
2		redivcan2d.b	|- ( ph -> B e. RR )
3		redivcan2d.z	|- ( ph -> B =/= 0 )
4	1 2 3	rediveq0d	|- ( ph -> ( ( A /R B ) = 0 <-> A = 0 ) )
5	4	bicomd	|- ( ph -> ( A = 0 <-> ( A /R B ) = 0 ) )
6	5	necon3bid	|- ( ph -> ( A =/= 0 <-> ( A /R B ) =/= 0 ) )