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 >_ 0

Proof

Step	Hyp	Ref	Expression
1		0le0	|- 0 <_ 0
2		c0ex	|- 0 e. _V
3	2 2	gte-lteh	|- ( 0 >_ 0 <-> 0 <_ 0 )
4	1 3	mpbir	|- 0 >_ 0