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	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
	abvf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	abveq0.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	abvgt0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 0 < ( 𝐹 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		abvf.a	⊢ 𝐴 = ( AbsVal ‘ 𝑅 )
2		abvf.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
3		abveq0.z	⊢ 0 = ( 0g ‘ 𝑅 )
4	1 2	abvcl	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )
5	4	3adant3	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )
6	1 2	abvge0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ) → 0 ≤ ( 𝐹 ‘ 𝑋 ) )
7	6	3adant3	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 0 ≤ ( 𝐹 ‘ 𝑋 ) )
8	1 2 3	abvne0	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ( 𝐹 ‘ 𝑋 ) ≠ 0 )
9	5 7 8	ne0gt0d	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → 0 < ( 𝐹 ‘ 𝑋 ) )