Metamath Proof Explorer

Theorem nn1suc

Description: If a statement holds for 1 and also holds for a successor, it holds for all positive integers. The first three hypotheses give us the substitution instances we need; the last two show that it holds for 1 and for a successor. (Contributed by NM, 11-Oct-2004) (Revised by Mario Carneiro, 16-May-2014)

Ref Expression
Hypotheses nn1suc.1 ⊢ x = 1 → φ ↔ ψ
nn1suc.3 ⊢ x = y + 1 → φ ↔ χ
nn1suc.4 ⊢ x = A → φ ↔ θ
nn1suc.5 ⊢ ψ
nn1suc.6 ⊢ y ∈ ℕ → χ
Assertion nn1suc ⊢ A ∈ ℕ → θ

Proof

Step Hyp Ref Expression
1 nn1suc.1 ⊢ x = 1 → φ ↔ ψ
2 nn1suc.3 ⊢ x = y + 1 → φ ↔ χ
3 nn1suc.4 ⊢ x = A → φ ↔ θ
4 nn1suc.5 ⊢ ψ
5 nn1suc.6 ⊢ y ∈ ℕ → χ
6 1ex ⊢ 1 ∈ V
7 6 1 sbcie ⊢ [˙ 1 / x]˙ φ ↔ ψ
8 4 7 mpbir ⊢ [˙ 1 / x]˙ φ
9 1nn ⊢ 1 ∈ ℕ
10 eleq1 ⊢ A = 1 → A ∈ ℕ ↔ 1 ∈ ℕ
11 9 10 mpbiri ⊢ A = 1 → A ∈ ℕ
12 3 sbcieg ⊢ A ∈ ℕ → [˙A / x]˙ φ ↔ θ
13 11 12 syl ⊢ A = 1 → [˙A / x]˙ φ ↔ θ
14 dfsbcq ⊢ A = 1 → [˙A / x]˙ φ ↔ [˙ 1 / x]˙ φ
15 13 14 bitr3d ⊢ A = 1 → θ ↔ [˙ 1 / x]˙ φ
16 8 15 mpbiri ⊢ A = 1 → θ
17 16 a1i ⊢ A ∈ ℕ → A = 1 → θ
18 ovex ⊢ y + 1 ∈ V
19 18 2 sbcie ⊢ [˙y + 1 / x]˙ φ ↔ χ
20 oveq1 ⊢ y = A − 1 → y + 1 = A - 1 + 1
21 20 sbceq1d ⊢ y = A − 1 → [˙y + 1 / x]˙ φ ↔ [˙A - 1 + 1 / x]˙ φ
22 19 21 bitr3id ⊢ y = A − 1 → χ ↔ [˙A - 1 + 1 / x]˙ φ
23 22 5 vtoclga ⊢ A − 1 ∈ ℕ → [˙A - 1 + 1 / x]˙ φ
24 nncn ⊢ A ∈ ℕ → A ∈ ℂ
25 ax-1cn ⊢ 1 ∈ ℂ
26 npcan ⊢ A ∈ ℂ ∧ 1 ∈ ℂ → A - 1 + 1 = A
27 24 25 26 sylancl ⊢ A ∈ ℕ → A - 1 + 1 = A
28 27 sbceq1d ⊢ A ∈ ℕ → [˙A - 1 + 1 / x]˙ φ ↔ [˙A / x]˙ φ
29 28 12 bitrd ⊢ A ∈ ℕ → [˙A - 1 + 1 / x]˙ φ ↔ θ
30 23 29 syl5ib ⊢ A ∈ ℕ → A − 1 ∈ ℕ → θ
31 nn1m1nn ⊢ A ∈ ℕ → A = 1 ∨ A − 1 ∈ ℕ
32 17 30 31 mpjaod ⊢ A ∈ ℕ → θ