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