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∈ℕ