Theorem ex-gte

Description: Simple example of >_ , in this case, 0 is greater than or equal to 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-gte	$$⊢0\ge 0$$

Proof

Step	Hyp	Ref	Expression
1		0le0	$$⊢0\le 0$$
2		c0ex	$$⊢0\in \mathrm{V}$$
3	2 2	gte-lteh	$$⊢0\ge 0\leftrightarrow 0\le 0$$
4	1 3	mpbir	$$⊢0\ge 0$$