Metamath Proof Explorer

Theorem nnne0

Description: A positive integer is nonzero. See nnne0ALT for a shorter proof using ax-pre-mulgt0 . This proof avoids 0lt1 , and thus ax-pre-mulgt0 , by splitting ax-1ne0 into the two separate cases 0 < 1 and 1 < 0 . (Contributed by NM, 27-Sep-1999) Remove dependency on ax-pre-mulgt0 . (Revised by Steven Nguyen, 30-Jan-2023)

Ref Expression
Assertion nnne0 ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )

Proof

Step Hyp Ref Expression
1 ax-1ne0 1 ≠ 0
2 1re 1 ∈ ℝ
3 0re 0 ∈ ℝ
4 2 3 lttri2i ( 1 ≠ 0 ↔ ( 1 < 0 ∨ 0 < 1 ) )
5 1 4 mpbi ( 1 < 0 ∨ 0 < 1 )
6 breq1 ( 𝑥 = 1 → ( 𝑥 < 0 ↔ 1 < 0 ) )
7 6 imbi2d ( 𝑥 = 1 → ( ( 1 < 0 → 𝑥 < 0 ) ↔ ( 1 < 0 → 1 < 0 ) ) )
8 breq1 ( 𝑥 = 𝑦 → ( 𝑥 < 0 ↔ 𝑦 < 0 ) )
9 8 imbi2d ( 𝑥 = 𝑦 → ( ( 1 < 0 → 𝑥 < 0 ) ↔ ( 1 < 0 → 𝑦 < 0 ) ) )
10 breq1 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝑥 < 0 ↔ ( 𝑦 + 1 ) < 0 ) )
11 10 imbi2d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 1 < 0 → 𝑥 < 0 ) ↔ ( 1 < 0 → ( 𝑦 + 1 ) < 0 ) ) )
12 breq1 ( 𝑥 = 𝐴 → ( 𝑥 < 0 ↔ 𝐴 < 0 ) )
13 12 imbi2d ( 𝑥 = 𝐴 → ( ( 1 < 0 → 𝑥 < 0 ) ↔ ( 1 < 0 → 𝐴 < 0 ) ) )
14 id ( 1 < 0 → 1 < 0 )
15 simp1 ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 𝑦 ∈ ℕ )
16 15 nnred ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 𝑦 ∈ ℝ )
17 1red ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 1 ∈ ℝ )
18 16 17 readdcld ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → ( 𝑦 + 1 ) ∈ ℝ )
19 3 2 readdcli ( 0 + 1 ) ∈ ℝ
20 19 a1i ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → ( 0 + 1 ) ∈ ℝ )
21 0red ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 0 ∈ ℝ )
22 simp3 ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 𝑦 < 0 )
23 16 21 17 22 ltadd1dd ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → ( 𝑦 + 1 ) < ( 0 + 1 ) )
24 ax-1cn 1 ∈ ℂ
25 24 addid2i ( 0 + 1 ) = 1
26 simp2 ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → 1 < 0 )
27 25 26 eqbrtrid ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → ( 0 + 1 ) < 0 )
28 18 20 21 23 27 lttrd ( ( 𝑦 ∈ ℕ ∧ 1 < 0 ∧ 𝑦 < 0 ) → ( 𝑦 + 1 ) < 0 )
29 28 3exp ( 𝑦 ∈ ℕ → ( 1 < 0 → ( 𝑦 < 0 → ( 𝑦 + 1 ) < 0 ) ) )
30 29 a2d ( 𝑦 ∈ ℕ → ( ( 1 < 0 → 𝑦 < 0 ) → ( 1 < 0 → ( 𝑦 + 1 ) < 0 ) ) )
31 7 9 11 13 14 30 nnind ( 𝐴 ∈ ℕ → ( 1 < 0 → 𝐴 < 0 ) )
32 31 imp ( ( 𝐴 ∈ ℕ ∧ 1 < 0 ) → 𝐴 < 0 )
33 32 lt0ne0d ( ( 𝐴 ∈ ℕ ∧ 1 < 0 ) → 𝐴 ≠ 0 )
34 33 ex ( 𝐴 ∈ ℕ → ( 1 < 0 → 𝐴 ≠ 0 ) )
35 breq2 ( 𝑥 = 1 → ( 0 < 𝑥 ↔ 0 < 1 ) )
36 35 imbi2d ( 𝑥 = 1 → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < 1 ) ) )
37 breq2 ( 𝑥 = 𝑦 → ( 0 < 𝑥 ↔ 0 < 𝑦 ) )
38 37 imbi2d ( 𝑥 = 𝑦 → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < 𝑦 ) ) )
39 breq2 ( 𝑥 = ( 𝑦 + 1 ) → ( 0 < 𝑥 ↔ 0 < ( 𝑦 + 1 ) ) )
40 39 imbi2d ( 𝑥 = ( 𝑦 + 1 ) → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < ( 𝑦 + 1 ) ) ) )
41 breq2 ( 𝑥 = 𝐴 → ( 0 < 𝑥 ↔ 0 < 𝐴 ) )
42 41 imbi2d ( 𝑥 = 𝐴 → ( ( 0 < 1 → 0 < 𝑥 ) ↔ ( 0 < 1 → 0 < 𝐴 ) ) )
43 id ( 0 < 1 → 0 < 1 )
44 simp1 ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 𝑦 ∈ ℕ )
45 44 nnred ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 𝑦 ∈ ℝ )
46 1red ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 1 ∈ ℝ )
47 simp3 ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 0 < 𝑦 )
48 simp2 ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 0 < 1 )
49 45 46 47 48 addgt0d ( ( 𝑦 ∈ ℕ ∧ 0 < 1 ∧ 0 < 𝑦 ) → 0 < ( 𝑦 + 1 ) )
50 49 3exp ( 𝑦 ∈ ℕ → ( 0 < 1 → ( 0 < 𝑦 → 0 < ( 𝑦 + 1 ) ) ) )
51 50 a2d ( 𝑦 ∈ ℕ → ( ( 0 < 1 → 0 < 𝑦 ) → ( 0 < 1 → 0 < ( 𝑦 + 1 ) ) ) )
52 36 38 40 42 43 51 nnind ( 𝐴 ∈ ℕ → ( 0 < 1 → 0 < 𝐴 ) )
53 52 imp ( ( 𝐴 ∈ ℕ ∧ 0 < 1 ) → 0 < 𝐴 )
54 53 gt0ne0d ( ( 𝐴 ∈ ℕ ∧ 0 < 1 ) → 𝐴 ≠ 0 )
55 54 ex ( 𝐴 ∈ ℕ → ( 0 < 1 → 𝐴 ≠ 0 ) )
56 34 55 jaod ( 𝐴 ∈ ℕ → ( ( 1 < 0 ∨ 0 < 1 ) → 𝐴 ≠ 0 ) )
57 5 56 mpi ( 𝐴 ∈ ℕ → 𝐴 ≠ 0 )