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

Metamath Proof Explorer

Theorem ene0

Description: _e is not 0. (Contributed by David A. Wheeler, 17-Oct-2017)

		Ref	Expression
	Assertion	ene0	$⊢ e \neq 0$

Step	Hyp	Ref	Expression
1		ere	$⊢ e \in ℝ$
2		epos	$⊢ 0 < e$
3	1 2	gt0ne0ii	$⊢ e \neq 0$