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 ) )