Metamath Proof Explorer

Theorem nn1m1nn

Description: Every positive integer is one or a successor. (Contributed by Mario Carneiro, 16-May-2014)

Ref Expression
Assertion nn1m1nn ⊢ A ∈ ℕ → A = 1 ∨ A − 1 ∈ ℕ

Proof

Step Hyp Ref Expression
1 orc ⊢ x = 1 → x = 1 ∨ x − 1 ∈ ℕ
2 1cnd ⊢ x = 1 → 1 ∈ ℂ
3 1 2 2thd ⊢ x = 1 → x = 1 ∨ x − 1 ∈ ℕ ↔ 1 ∈ ℂ
4 eqeq1 ⊢ x = y → x = 1 ↔ y = 1
5 oveq1 ⊢ x = y → x − 1 = y − 1
6 5 eleq1d ⊢ x = y → x − 1 ∈ ℕ ↔ y − 1 ∈ ℕ
7 4 6 orbi12d ⊢ x = y → x = 1 ∨ x − 1 ∈ ℕ ↔ y = 1 ∨ y − 1 ∈ ℕ
8 eqeq1 ⊢ x = y + 1 → x = 1 ↔ y + 1 = 1
9 oveq1 ⊢ x = y + 1 → x − 1 = y + 1 - 1
10 9 eleq1d ⊢ x = y + 1 → x − 1 ∈ ℕ ↔ y + 1 - 1 ∈ ℕ
11 8 10 orbi12d ⊢ x = y + 1 → x = 1 ∨ x − 1 ∈ ℕ ↔ y + 1 = 1 ∨ y + 1 - 1 ∈ ℕ
12 eqeq1 ⊢ x = A → x = 1 ↔ A = 1
13 oveq1 ⊢ x = A → x − 1 = A − 1
14 13 eleq1d ⊢ x = A → x − 1 ∈ ℕ ↔ A − 1 ∈ ℕ
15 12 14 orbi12d ⊢ x = A → x = 1 ∨ x − 1 ∈ ℕ ↔ A = 1 ∨ A − 1 ∈ ℕ
16 ax-1cn ⊢ 1 ∈ ℂ
17 nncn ⊢ y ∈ ℕ → y ∈ ℂ
18 pncan ⊢ y ∈ ℂ ∧ 1 ∈ ℂ → y + 1 - 1 = y
19 17 16 18 sylancl ⊢ y ∈ ℕ → y + 1 - 1 = y
20 id ⊢ y ∈ ℕ → y ∈ ℕ
21 19 20 eqeltrd ⊢ y ∈ ℕ → y + 1 - 1 ∈ ℕ
22 21 olcd ⊢ y ∈ ℕ → y + 1 = 1 ∨ y + 1 - 1 ∈ ℕ
23 22 a1d ⊢ y ∈ ℕ → y = 1 ∨ y − 1 ∈ ℕ → y + 1 = 1 ∨ y + 1 - 1 ∈ ℕ
24 3 7 11 15 16 23 nnind ⊢ A ∈ ℕ → A = 1 ∨ A − 1 ∈ ℕ