This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem absne0d

Description: The absolute value of a number is zero iff the number is zero. Proposition 10-3.7(c) of Gleason p. 133. (Contributed by Mario Carneiro, 29-May-2016)

	Ref	Expression
Hypotheses	abscld.1	$⊢ φ \to A \in ℂ$
	absne0d.2	$⊢ φ \to A \neq 0$
Assertion	absne0d	$⊢ φ \to \|A\| \neq 0$

Proof

Step	Hyp	Ref	Expression
1		abscld.1	$⊢ φ \to A \in ℂ$
2		absne0d.2	$⊢ φ \to A \neq 0$
3	1	abs00ad	$⊢ φ \to (\|A\| = 0 \leftrightarrow A = 0)$
4	3	necon3bid	$⊢ φ \to (\|A\| \neq 0 \leftrightarrow A \neq 0)$
5	2 4	mpbird	$⊢ φ \to \|A\| \neq 0$