Theorem 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=\mathrm{AbsVal}\left(R\right)$$
	abvf.b	$$⊢B={\mathrm{Base}}_R$$
	abveq0.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	abvgt0	$$⊢\left(F\in A\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to 0<F\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		abvf.a	$$⊢A=\mathrm{AbsVal}\left(R\right)$$
2		abvf.b	$$⊢B={\mathrm{Base}}_R$$
3		abveq0.z	$$⊢\underset{\dot{}}{0}=0_R$$
4	1 2	abvcl	$$⊢\left(F\in A\wedge X\in B\right)\to F\left(X\right)\in ℝ$$
5	4	3adant3	$$⊢\left(F\in A\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to F\left(X\right)\in ℝ$$
6	1 2	abvge0	$$⊢\left(F\in A\wedge X\in B\right)\to 0\le F\left(X\right)$$
7	6	3adant3	$$⊢\left(F\in A\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to 0\le F\left(X\right)$$
8	1 2 3	abvne0	$$⊢\left(F\in A\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to F\left(X\right)\ne 0$$
9	5 7 8	ne0gt0d	$$⊢\left(F\in A\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to 0<F\left(X\right)$$