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 ∈ V
3	2 2	gte-lteh	⊢ ( 0 ≥ 0 ↔ 0 ≤ 0 )
4	1 3	mpbir	⊢ 0 ≥ 0