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	syl5bbr	⊢ ( 𝑦 = ( 𝐴 − 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	⊢ ( 𝐴 ∈ ℕ → 𝜃 )