Metamath Proof Explorer


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