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

Metamath Proof Explorer

Theorem abvne0

Description: The absolute value of a nonzero number is nonzero. (Contributed by Mario Carneiro, 8-Sep-2014)

	Ref	Expression
Hypotheses	abvf.a	$⊢ A = AbsVal (R)$
	abvf.b	$⊢ B = {Base}_{R}$
	abveq0.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	abvne0	$⊢ (F \in A \land X \in B \land X \neq \underset{˙}{0}) \to F (X) \neq 0$

Step	Hyp	Ref	Expression
1		abvf.a	$⊢ A = AbsVal (R)$
2		abvf.b	$⊢ B = {Base}_{R}$
3		abveq0.z	$⊢ \underset{˙}{0} = 0_{R}$
4	1 2 3	abveq0	$⊢ (F \in A \land X \in B) \to (F (X) = 0 \leftrightarrow X = \underset{˙}{0})$
5	4	necon3bid	$⊢ (F \in A \land X \in B) \to (F (X) \neq 0 \leftrightarrow X \neq \underset{˙}{0})$
6	5	biimp3ar	$⊢ (F \in A \land X \in B \land X \neq \underset{˙}{0}) \to F (X) \neq 0$