Metamath Proof Explorer

Theorem n0sge0

Description: A non-negative integer is greater than or equal to zero. (Contributed by Scott Fenton, 15-Apr-2025)

Ref Expression
Assertion n0sge0 
|- ( A e. NN0_s -> 0s <_s A )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( n = 0s -> ( 0s <_s n <-> 0s <_s 0s ) )
2 breq2 
 |-  ( n = m -> ( 0s <_s n <-> 0s <_s m ) )
3 breq2 
 |-  ( n = ( m +s 1s ) -> ( 0s <_s n <-> 0s <_s ( m +s 1s ) ) )
4 breq2 
 |-  ( n = A -> ( 0s <_s n <-> 0s <_s A ) )
5 0sno 
 |-  0s e. No
6 slerflex 
 |-  ( 0s e. No -> 0s <_s 0s )
7 5 6 ax-mp 
 |-  0s <_s 0s
8 5 a1i 
 |-  ( ( m e. NN0_s /\ 0s <_s m ) -> 0s e. No )
9 n0sno 
 |-  ( m e. NN0_s -> m e. No )
10 9 adantr 
 |-  ( ( m e. NN0_s /\ 0s <_s m ) -> m e. No )
11 peano2no 
 |-  ( m e. No -> ( m +s 1s ) e. No )
12 9 11 syl 
 |-  ( m e. NN0_s -> ( m +s 1s ) e. No )
13 12 adantr 
 |-  ( ( m e. NN0_s /\ 0s <_s m ) -> ( m +s 1s ) e. No )
14 simpr 
 |-  ( ( m e. NN0_s /\ 0s <_s m ) -> 0s <_s m )
15 9 addsridd 
 |-  ( m e. NN0_s -> ( m +s 0s ) = m )
16 15 adantr 
 |-  ( ( m e. NN0_s /\ 0s <_s m ) -> ( m +s 0s ) = m )
17 5 a1i 
 |-  ( T. -> 0s e. No )
18 1sno 
 |-  1s e. No
19 18 a1i 
 |-  ( T. -> 1s e. No )
20 0slt1s 
 |-  0s
21 20 a1i 
 |-  ( T. -> 0s
22 17 19 21 sltled 
 |-  ( T. -> 0s <_s 1s )
23 22 mptru 
 |-  0s <_s 1s
24 5 a1i 
 |-  ( m e. NN0_s -> 0s e. No )
25 18 a1i 
 |-  ( m e. NN0_s -> 1s e. No )
26 24 25 9 sleadd2d 
 |-  ( m e. NN0_s -> ( 0s <_s 1s <-> ( m +s 0s ) <_s ( m +s 1s ) ) )
27 23 26 mpbii 
 |-  ( m e. NN0_s -> ( m +s 0s ) <_s ( m +s 1s ) )
28 27 adantr 
 |-  ( ( m e. NN0_s /\ 0s <_s m ) -> ( m +s 0s ) <_s ( m +s 1s ) )
29 16 28 eqbrtrrd 
 |-  ( ( m e. NN0_s /\ 0s <_s m ) -> m <_s ( m +s 1s ) )
30 8 10 13 14 29 sletrd 
 |-  ( ( m e. NN0_s /\ 0s <_s m ) -> 0s <_s ( m +s 1s ) )
31 30 ex 
 |-  ( m e. NN0_s -> ( 0s <_s m -> 0s <_s ( m +s 1s ) ) )
32 1 2 3 4 7 31 n0sind 
 |-  ( A e. NN0_s -> 0s <_s A )