Metamath Proof Explorer

Theorem z2ge

Description: There exists an integer greater than or equal to any two others. (Contributed by NM, 28-Aug-2005)

Ref Expression
Assertion z2ge 
|- ( ( M e. ZZ /\ N e. ZZ ) -> E. k e. ZZ ( M <_ k /\ N <_ k ) )

Proof

Step Hyp Ref Expression
1 ifcl 
 |-  ( ( N e. ZZ /\ M e. ZZ ) -> if ( M <_ N , N , M ) e. ZZ )
2 1 ancoms 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> if ( M <_ N , N , M ) e. ZZ )
3 zre 
 |-  ( M e. ZZ -> M e. RR )
4 zre 
 |-  ( N e. ZZ -> N e. RR )
5 max1 
 |-  ( ( M e. RR /\ N e. RR ) -> M <_ if ( M <_ N , N , M ) )
6 max2 
 |-  ( ( M e. RR /\ N e. RR ) -> N <_ if ( M <_ N , N , M ) )
7 5 6 jca 
 |-  ( ( M e. RR /\ N e. RR ) -> ( M <_ if ( M <_ N , N , M ) /\ N <_ if ( M <_ N , N , M ) ) )
8 3 4 7 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M <_ if ( M <_ N , N , M ) /\ N <_ if ( M <_ N , N , M ) ) )
9 breq2 
 |-  ( k = if ( M <_ N , N , M ) -> ( M <_ k <-> M <_ if ( M <_ N , N , M ) ) )
10 breq2 
 |-  ( k = if ( M <_ N , N , M ) -> ( N <_ k <-> N <_ if ( M <_ N , N , M ) ) )
11 9 10 anbi12d 
 |-  ( k = if ( M <_ N , N , M ) -> ( ( M <_ k /\ N <_ k ) <-> ( M <_ if ( M <_ N , N , M ) /\ N <_ if ( M <_ N , N , M ) ) ) )
12 11 rspcev 
 |-  ( ( if ( M <_ N , N , M ) e. ZZ /\ ( M <_ if ( M <_ N , N , M ) /\ N <_ if ( M <_ N , N , M ) ) ) -> E. k e. ZZ ( M <_ k /\ N <_ k ) )
13 2 8 12 syl2anc 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> E. k e. ZZ ( M <_ k /\ N <_ k ) )