Metamath Proof Explorer


Theorem ex-gt

Description: Simple example of > , in this case, 0 is not greater than 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-gt
|- -. 0 > 0

Proof

Step Hyp Ref Expression
1 0re
 |-  0 e. RR
2 1 ltnri
 |-  -. 0 < 0
3 c0ex
 |-  0 e. _V
4 3 3 gt-lth
 |-  ( 0 > 0 <-> 0 < 0 )
5 2 4 mtbir
 |-  -. 0 > 0