Metamath Proof Explorer

Theorem 0nn0m1nnn0

Description: A number is zero if and only if it's a nonnegative integer that becomes negative after subtracting 1. (Contributed by BTernaryTau, 30-Sep-2023)

Ref Expression
Assertion 0nn0m1nnn0 ( 𝑁 = 0 ↔ ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) )

Proof

Step Hyp Ref Expression
1 0nn0 ⊢ 0 ∈ ℕ0
2 eleq1 ⊢ ( 𝑁 = 0 → ( 𝑁 ∈ ℕ0 ↔ 0 ∈ ℕ0 ) )
3 1 2 mpbiri ⊢ ( 𝑁 = 0 → 𝑁 ∈ ℕ0 )
4 1nn ⊢ 1 ∈ ℕ
5 0mnnnnn0 ⊢ ( 1 ∈ ℕ → ( 0 − 1 ) ∉ ℕ0 )
6 4 5 ax-mp ⊢ ( 0 − 1 ) ∉ ℕ0
7 oveq1 ⊢ ( 𝑁 = 0 → ( 𝑁 − 1 ) = ( 0 − 1 ) )
8 neleq1 ⊢ ( ( 𝑁 − 1 ) = ( 0 − 1 ) → ( ( 𝑁 − 1 ) ∉ ℕ0 ↔ ( 0 − 1 ) ∉ ℕ0 ) )
9 7 8 syl ⊢ ( 𝑁 = 0 → ( ( 𝑁 − 1 ) ∉ ℕ0 ↔ ( 0 − 1 ) ∉ ℕ0 ) )
10 6 9 mpbiri ⊢ ( 𝑁 = 0 → ( 𝑁 − 1 ) ∉ ℕ0 )
11 df-nel ⊢ ( ( 𝑁 − 1 ) ∉ ℕ0 ↔ ¬ ( 𝑁 − 1 ) ∈ ℕ0 )
12 10 11 sylib ⊢ ( 𝑁 = 0 → ¬ ( 𝑁 − 1 ) ∈ ℕ0 )
13 3 12 jca ⊢ ( 𝑁 = 0 → ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) )
14 nn0z ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℤ )
15 peano2zm ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
16 14 15 syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 1 ) ∈ ℤ )
17 elnn0z ⊢ ( ( 𝑁 − 1 ) ∈ ℕ0 ↔ ( ( 𝑁 − 1 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 − 1 ) ) )
18 17 notbii ⊢ ( ¬ ( 𝑁 − 1 ) ∈ ℕ0 ↔ ¬ ( ( 𝑁 − 1 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 − 1 ) ) )
19 18 biimpi ⊢ ( ¬ ( 𝑁 − 1 ) ∈ ℕ0 → ¬ ( ( 𝑁 − 1 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 − 1 ) ) )
20 annotanannot ⊢ ( ( ( 𝑁 − 1 ) ∈ ℤ ∧ ¬ ( ( 𝑁 − 1 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 − 1 ) ) ) ↔ ( ( 𝑁 − 1 ) ∈ ℤ ∧ ¬ 0 ≤ ( 𝑁 − 1 ) ) )
21 20 simprbi ⊢ ( ( ( 𝑁 − 1 ) ∈ ℤ ∧ ¬ ( ( 𝑁 − 1 ) ∈ ℤ ∧ 0 ≤ ( 𝑁 − 1 ) ) ) → ¬ 0 ≤ ( 𝑁 − 1 ) )
22 16 19 21 syl2an ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) → ¬ 0 ≤ ( 𝑁 − 1 ) )
23 zre ⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ℝ )
24 14 15 23 3syl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 − 1 ) ∈ ℝ )
25 0red ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ℝ )
26 24 25 ltnled ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) < 0 ↔ ¬ 0 ≤ ( 𝑁 − 1 ) ) )
27 26 biimprd ⊢ ( 𝑁 ∈ ℕ0 → ( ¬ 0 ≤ ( 𝑁 − 1 ) → ( 𝑁 − 1 ) < 0 ) )
28 27 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( ¬ 0 ≤ ( 𝑁 − 1 ) → ( 𝑁 − 1 ) < 0 ) )
29 22 28 mpd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( 𝑁 − 1 ) < 0 )
30 0z ⊢ 0 ∈ ℤ
31 zlem1lt ⊢ ( ( 𝑁 ∈ ℤ ∧ 0 ∈ ℤ ) → ( 𝑁 ≤ 0 ↔ ( 𝑁 − 1 ) < 0 ) )
32 14 30 31 sylancl ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 ≤ 0 ↔ ( 𝑁 − 1 ) < 0 ) )
33 32 biimprd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 − 1 ) < 0 → 𝑁 ≤ 0 ) )
34 33 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( ( 𝑁 − 1 ) < 0 → 𝑁 ≤ 0 ) )
35 29 34 mpd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) → 𝑁 ≤ 0 )
36 nn0ge0 ⊢ ( 𝑁 ∈ ℕ0 → 0 ≤ 𝑁 )
37 36 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) → 0 ≤ 𝑁 )
38 nn0re ⊢ ( 𝑁 ∈ ℕ0 → 𝑁 ∈ ℝ )
39 38 25 letri3d ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 = 0 ↔ ( 𝑁 ≤ 0 ∧ 0 ≤ 𝑁 ) ) )
40 39 biimprd ⊢ ( 𝑁 ∈ ℕ0 → ( ( 𝑁 ≤ 0 ∧ 0 ≤ 𝑁 ) → 𝑁 = 0 ) )
41 40 adantr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) → ( ( 𝑁 ≤ 0 ∧ 0 ≤ 𝑁 ) → 𝑁 = 0 ) )
42 35 37 41 mp2and ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) → 𝑁 = 0 )
43 13 42 impbii ⊢ ( 𝑁 = 0 ↔ ( 𝑁 ∈ ℕ0 ∧ ¬ ( 𝑁 − 1 ) ∈ ℕ0 ) )