This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nn2ge

Description: There exists a positive integer greater than or equal to any two others. (Contributed by NM, 18-Aug-1999)

Ref Expression
Assertion nn2ge 
|- ( ( A e. NN /\ B e. NN ) -> E. x e. NN ( A <_ x /\ B <_ x ) )

Proof

Step Hyp Ref Expression
1 nnre 
 |-  ( A e. NN -> A e. RR )
2 1 adantr 
 |-  ( ( A e. NN /\ B e. NN ) -> A e. RR )
3 nnre 
 |-  ( B e. NN -> B e. RR )
4 3 adantl 
 |-  ( ( A e. NN /\ B e. NN ) -> B e. RR )
5 leid 
 |-  ( B e. RR -> B <_ B )
6 5 anim1ci 
 |-  ( ( B e. RR /\ A <_ B ) -> ( A <_ B /\ B <_ B ) )
7 3 6 sylan 
 |-  ( ( B e. NN /\ A <_ B ) -> ( A <_ B /\ B <_ B ) )
8 breq2 
 |-  ( x = B -> ( A <_ x <-> A <_ B ) )
9 breq2 
 |-  ( x = B -> ( B <_ x <-> B <_ B ) )
10 8 9 anbi12d 
 |-  ( x = B -> ( ( A <_ x /\ B <_ x ) <-> ( A <_ B /\ B <_ B ) ) )
11 10 rspcev 
 |-  ( ( B e. NN /\ ( A <_ B /\ B <_ B ) ) -> E. x e. NN ( A <_ x /\ B <_ x ) )
12 7 11 syldan 
 |-  ( ( B e. NN /\ A <_ B ) -> E. x e. NN ( A <_ x /\ B <_ x ) )
13 12 adantll 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ A <_ B ) -> E. x e. NN ( A <_ x /\ B <_ x ) )
14 leid 
 |-  ( A e. RR -> A <_ A )
15 14 anim1i 
 |-  ( ( A e. RR /\ B <_ A ) -> ( A <_ A /\ B <_ A ) )
16 1 15 sylan 
 |-  ( ( A e. NN /\ B <_ A ) -> ( A <_ A /\ B <_ A ) )
17 breq2 
 |-  ( x = A -> ( A <_ x <-> A <_ A ) )
18 breq2 
 |-  ( x = A -> ( B <_ x <-> B <_ A ) )
19 17 18 anbi12d 
 |-  ( x = A -> ( ( A <_ x /\ B <_ x ) <-> ( A <_ A /\ B <_ A ) ) )
20 19 rspcev 
 |-  ( ( A e. NN /\ ( A <_ A /\ B <_ A ) ) -> E. x e. NN ( A <_ x /\ B <_ x ) )
21 16 20 syldan 
 |-  ( ( A e. NN /\ B <_ A ) -> E. x e. NN ( A <_ x /\ B <_ x ) )
22 21 adantlr 
 |-  ( ( ( A e. NN /\ B e. NN ) /\ B <_ A ) -> E. x e. NN ( A <_ x /\ B <_ x ) )
23 2 4 13 22 lecasei 
 |-  ( ( A e. NN /\ B e. NN ) -> E. x e. NN ( A <_ x /\ B <_ x ) )