Theorem nn1m1nn

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

	Ref	Expression
Assertion	nn1m1nn	⊢ ( 𝐴 ∈ ℕ → ( 𝐴 = 1 ∨ ( 𝐴 − 1 ) ∈ ℕ ) )

Proof

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