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

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 3	abveq0	$$⊢\left(F\in A\wedge X\in B\right)\to \left(F\left(X\right)=0\leftrightarrow X=\underset{\dot{}}{0}\right)$$
5	4	necon3bid	$$⊢\left(F\in A\wedge X\in B\right)\to \left(F\left(X\right)\ne 0\leftrightarrow X\ne \underset{\dot{}}{0}\right)$$
6	5	biimp3ar	$$⊢\left(F\in A\wedge X\in B\wedge X\ne \underset{\dot{}}{0}\right)\to F\left(X\right)\ne 0$$