Theorem abvne0

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

	Ref	Expression
Hypotheses	abvf.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	abvf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	abveq0.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	abvne0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 𝐹 ‘ 𝑋 ) ≠ 0 )

Proof

Step	Hyp	Ref	Expression
1		abvf.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abvf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		abveq0.z	⊢ 0 = ( 0g ‘ 𝑅 )
4	1 2 3	abveq0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) = 0 ↔ 𝑋 = 0 ) )
5	4	necon3bid	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑋 ) ≠ 0 ↔ 𝑋 ≠ 0 ) )
6	5	biimp3ar	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 𝐹 ‘ 𝑋 ) ≠ 0 )