Theorem rerecne0d

Description: The reciprocal of a nonzero number is nonzero. (Contributed by SN, 4-Apr-2026)

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

Proof

Step	Hyp	Ref	Expression
1		sn-rereccld.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		sn-rereccld.z	⊢ ( 𝜑 → 𝐴 ≠ 0 )
3		ax-1ne0	⊢ 1 ≠ 0
4		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
5	4 1 2	redivne0bd	⊢ ( 𝜑 → ( 1 ≠ 0 ↔ ( 1 /ℝ 𝐴 ) ≠ 0 ) )
6	3 5	mpbii	⊢ ( 𝜑 → ( 1 /ℝ 𝐴 ) ≠ 0 )