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 )