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 ( 𝑥 = 1 → ( 𝜑𝜓 ) )
nn1suc.3 ( 𝑥 = ( 𝑦 + 1 ) → ( 𝜑𝜒 ) )
nn1suc.4 ( 𝑥 = 𝐴 → ( 𝜑𝜃 ) )
nn1suc.5 𝜓
nn1suc.6 ( 𝑦 ∈ ℕ → 𝜒 )
Assertion nn1suc ( 𝐴 ∈ ℕ → 𝜃 )

Proof

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