Theorem ex-gt

Description: Simple example of > , in this case, 0 is not greater than 0. This is useful as an example, and helps us gain confidence that we've correctly defined the symbol. (Contributed by David A. Wheeler, 1-Jan-2017) (New usage is discouraged.)

	Ref	Expression
Assertion	ex-gt	$$⊢\neg 0>0$$

Proof

Step	Hyp	Ref	Expression
1		0re	$$⊢0\in ℝ$$
2	1	ltnri	$$⊢\neg 0<0$$
3		c0ex	$$⊢0\in \mathrm{V}$$
4	3 3	gt-lth	$$⊢0>0\leftrightarrow 0<0$$
5	2 4	mtbir	$$⊢\neg 0>0$$