Metamath Proof Explorer

Theorem xnn0lenn0nn0

Description: An extended nonnegative integer which is less than or equal to a nonnegative integer is a nonnegative integer. (Contributed by AV, 24-Nov-2021)

Ref Expression
Assertion xnn0lenn0nn0 
|- ( ( M e. NN0* /\ N e. NN0 /\ M <_ N ) -> M e. NN0 )

Proof

Step Hyp Ref Expression
1 elxnn0 
 |-  ( M e. NN0* <-> ( M e. NN0 \/ M = +oo ) )
2 2a1 
 |-  ( M e. NN0 -> ( N e. NN0 -> ( M <_ N -> M e. NN0 ) ) )
3 breq1 
 |-  ( M = +oo -> ( M <_ N <-> +oo <_ N ) )
4 3 adantr 
 |-  ( ( M = +oo /\ N e. NN0 ) -> ( M <_ N <-> +oo <_ N ) )
5 nn0re 
 |-  ( N e. NN0 -> N e. RR )
6 5 rexrd 
 |-  ( N e. NN0 -> N e. RR* )
7 xgepnf 
 |-  ( N e. RR* -> ( +oo <_ N <-> N = +oo ) )
8 6 7 syl 
 |-  ( N e. NN0 -> ( +oo <_ N <-> N = +oo ) )
9 pnfnre 
 |-  +oo e/ RR
10 eleq1 
 |-  ( N = +oo -> ( N e. NN0 <-> +oo e. NN0 ) )
11 nn0re 
 |-  ( +oo e. NN0 -> +oo e. RR )
12 elnelall 
 |-  ( +oo e. RR -> ( +oo e/ RR -> M e. NN0 ) )
13 11 12 syl 
 |-  ( +oo e. NN0 -> ( +oo e/ RR -> M e. NN0 ) )
14 10 13 syl6bi 
 |-  ( N = +oo -> ( N e. NN0 -> ( +oo e/ RR -> M e. NN0 ) ) )
15 14 com13 
 |-  ( +oo e/ RR -> ( N e. NN0 -> ( N = +oo -> M e. NN0 ) ) )
16 9 15 ax-mp 
 |-  ( N e. NN0 -> ( N = +oo -> M e. NN0 ) )
17 8 16 sylbid 
 |-  ( N e. NN0 -> ( +oo <_ N -> M e. NN0 ) )
18 17 adantl 
 |-  ( ( M = +oo /\ N e. NN0 ) -> ( +oo <_ N -> M e. NN0 ) )
19 4 18 sylbid 
 |-  ( ( M = +oo /\ N e. NN0 ) -> ( M <_ N -> M e. NN0 ) )
20 19 ex 
 |-  ( M = +oo -> ( N e. NN0 -> ( M <_ N -> M e. NN0 ) ) )
21 2 20 jaoi 
 |-  ( ( M e. NN0 \/ M = +oo ) -> ( N e. NN0 -> ( M <_ N -> M e. NN0 ) ) )
22 1 21 sylbi 
 |-  ( M e. NN0* -> ( N e. NN0 -> ( M <_ N -> M e. NN0 ) ) )
23 22 3imp 
 |-  ( ( M e. NN0* /\ N e. NN0 /\ M <_ N ) -> M e. NN0 )