Metamath Proof Explorer

Theorem sn-nnne0

Description: nnne0 without ax-mulcom . (Contributed by SN, 25-Jan-2025)

Ref Expression
Assertion sn-nnne0 
|- ( A e. NN -> A =/= 0 )

Proof

Step Hyp Ref Expression
1 0ne1 
 |-  0 =/= 1
2 0re 
 |-  0 e. RR
3 1re 
 |-  1 e. RR
4 2 3 lttri2i 
 |-  ( 0 =/= 1 <-> ( 0 < 1 \/ 1 < 0 ) )
5 1 4 mpbi 
 |-  ( 0 < 1 \/ 1 < 0 )
6 breq2 
 |-  ( x = 1 -> ( 0 < x <-> 0 < 1 ) )
7 breq2 
 |-  ( x = y -> ( 0 < x <-> 0 < y ) )
8 breq2 
 |-  ( x = ( y + 1 ) -> ( 0 < x <-> 0 < ( y + 1 ) ) )
9 breq2 
 |-  ( x = A -> ( 0 < x <-> 0 < A ) )
10 id 
 |-  ( 0 < 1 -> 0 < 1 )
11 nnre 
 |-  ( y e. NN -> y e. RR )
12 11 ad2antlr 
 |-  ( ( ( 0 < 1 /\ y e. NN ) /\ 0 < y ) -> y e. RR )
13 1red 
 |-  ( ( ( 0 < 1 /\ y e. NN ) /\ 0 < y ) -> 1 e. RR )
14 simpr 
 |-  ( ( ( 0 < 1 /\ y e. NN ) /\ 0 < y ) -> 0 < y )
15 simpll 
 |-  ( ( ( 0 < 1 /\ y e. NN ) /\ 0 < y ) -> 0 < 1 )
16 12 13 14 15 sn-addgt0d 
 |-  ( ( ( 0 < 1 /\ y e. NN ) /\ 0 < y ) -> 0 < ( y + 1 ) )
17 6 7 8 9 10 16 nnindd 
 |-  ( ( 0 < 1 /\ A e. NN ) -> 0 < A )
18 17 gt0ne0d 
 |-  ( ( 0 < 1 /\ A e. NN ) -> A =/= 0 )
19 18 ancoms 
 |-  ( ( A e. NN /\ 0 < 1 ) -> A =/= 0 )
20 breq1 
 |-  ( x = 1 -> ( x < 0 <-> 1 < 0 ) )
21 breq1 
 |-  ( x = y -> ( x < 0 <-> y < 0 ) )
22 breq1 
 |-  ( x = ( y + 1 ) -> ( x < 0 <-> ( y + 1 ) < 0 ) )
23 breq1 
 |-  ( x = A -> ( x < 0 <-> A < 0 ) )
24 id 
 |-  ( 1 < 0 -> 1 < 0 )
25 11 ad2antlr 
 |-  ( ( ( 1 < 0 /\ y e. NN ) /\ y < 0 ) -> y e. RR )
26 1red 
 |-  ( ( ( 1 < 0 /\ y e. NN ) /\ y < 0 ) -> 1 e. RR )
27 simpr 
 |-  ( ( ( 1 < 0 /\ y e. NN ) /\ y < 0 ) -> y < 0 )
28 simpll 
 |-  ( ( ( 1 < 0 /\ y e. NN ) /\ y < 0 ) -> 1 < 0 )
29 25 26 27 28 sn-addlt0d 
 |-  ( ( ( 1 < 0 /\ y e. NN ) /\ y < 0 ) -> ( y + 1 ) < 0 )
30 20 21 22 23 24 29 nnindd 
 |-  ( ( 1 < 0 /\ A e. NN ) -> A < 0 )
31 30 lt0ne0d 
 |-  ( ( 1 < 0 /\ A e. NN ) -> A =/= 0 )
32 31 ancoms 
 |-  ( ( A e. NN /\ 1 < 0 ) -> A =/= 0 )
33 19 32 jaodan 
 |-  ( ( A e. NN /\ ( 0 < 1 \/ 1 < 0 ) ) -> A =/= 0 )
34 5 33 mpan2 
 |-  ( A e. NN -> A =/= 0 )