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

Metamath Proof Explorer

Theorem sn-rediv0d

Description: Division into zero is zero. (Contributed by SN, 2-Apr-2026)

Ref Expression
Hypotheses sn-rediv0d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
sn-rediv0d.z ⊢ ( 𝜑 → 𝐴 ≠ 0 )
Assertion sn-rediv0d ( 𝜑 → ( 0 /ℝ 𝐴 ) = 0 )

Proof

Step Hyp Ref Expression
1 sn-rediv0d.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 sn-rediv0d.z ⊢ ( 𝜑 → 𝐴 ≠ 0 )
3 eqidd ⊢ ( 𝜑 → 0 = 0 )
4 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
5 4 1 2 rediveq0d ⊢ ( 𝜑 → ( ( 0 /ℝ 𝐴 ) = 0 ↔ 0 = 0 ) )
6 3 5 mpbird ⊢ ( 𝜑 → ( 0 /ℝ 𝐴 ) = 0 )