abvgt0

Description: The absolute value of a nonzero number is strictly positive. (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	abvgt0	$⊢ (F \in A \land X \in B \land X \neq \underset{˙}{0}) \to 0 < F (X)$

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	abvcl	$⊢ (F \in A \land X \in B) \to F (X) \in ℝ$
5	4	3adant3	$⊢ (F \in A \land X \in B \land X \neq \underset{˙}{0}) \to F (X) \in ℝ$
6	1 2	abvge0	$⊢ (F \in A \land X \in B) \to 0 \leq F (X)$
7	6	3adant3	$⊢ (F \in A \land X \in B \land X \neq \underset{˙}{0}) \to 0 \leq F (X)$
8	1 2 3	abvne0	$⊢ (F \in A \land X \in B \land X \neq \underset{˙}{0}) \to F (X) \neq 0$
9	5 7 8	ne0gt0d	$⊢ (F \in A \land X \in B \land X \neq \underset{˙}{0}) \to 0 < F (X)$

Metamath Proof Explorer