Theorem redivne0bd

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

	Ref	Expression
Hypotheses	redivcan2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	redivcan2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	redivcan2d.z	⊢ ( 𝜑 → 𝐵 ≠ 0 )
Assertion	redivne0bd	⊢ ( 𝜑 → ( 𝐴 ≠ 0 ↔ ( 𝐴 /ℝ 𝐵 ) ≠ 0 ) )

Proof

Step	Hyp	Ref	Expression
1		redivcan2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		redivcan2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		redivcan2d.z	⊢ ( 𝜑 → 𝐵 ≠ 0 )
4	1 2 3	rediveq0d	⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐵 ) = 0 ↔ 𝐴 = 0 ) )
5	4	bicomd	⊢ ( 𝜑 → ( 𝐴 = 0 ↔ ( 𝐴 /ℝ 𝐵 ) = 0 ) )
6	5	necon3bid	⊢ ( 𝜑 → ( 𝐴 ≠ 0 ↔ ( 𝐴 /ℝ 𝐵 ) ≠ 0 ) )