Metamath Proof Explorer


Theorem sn-nnne0

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

Ref Expression
Assertion sn-nnne0 A A 0

Proof

Step Hyp Ref Expression
1 0ne1 0 1
2 0re 0
3 1re 1
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 y
12 11 ad2antlr 0 < 1 y 0 < y y
13 1red 0 < 1 y 0 < y 1
14 simpr 0 < 1 y 0 < y 0 < y
15 simpll 0 < 1 y 0 < y 0 < 1
16 12 13 14 15 sn-addgt0d 0 < 1 y 0 < y 0 < y + 1
17 6 7 8 9 10 16 nnindd 0 < 1 A 0 < A
18 17 gt0ne0d 0 < 1 A A 0
19 18 ancoms A 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 y < 0 y
26 1red 1 < 0 y y < 0 1
27 simpr 1 < 0 y y < 0 y < 0
28 simpll 1 < 0 y y < 0 1 < 0
29 25 26 27 28 sn-addlt0d 1 < 0 y y < 0 y + 1 < 0
30 20 21 22 23 24 29 nnindd 1 < 0 A A < 0
31 30 lt0ne0d 1 < 0 A A 0
32 31 ancoms A 1 < 0 A 0
33 19 32 jaodan A 0 < 1 1 < 0 A 0
34 5 33 mpan2 A A 0