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\to \left(\phi \leftrightarrow \psi \right)$$
	nn1suc.3	$$⊢x=y+1\to \left(\phi \leftrightarrow \chi \right)$$
	nn1suc.4	$$⊢x=A\to \left(\phi \leftrightarrow \theta \right)$$
	nn1suc.5	$$⊢\psi$$
	nn1suc.6	$$⊢y\in \mathbb{N}\to \chi$$
Assertion	nn1suc	$$⊢A\in \mathbb{N}\to \theta$$

Proof

Step	Hyp	Ref	Expression
1		nn1suc.1	$$⊢x=1\to \left(\phi \leftrightarrow \psi \right)$$
2		nn1suc.3	$$⊢x=y+1\to \left(\phi \leftrightarrow \chi \right)$$
3		nn1suc.4	$$⊢x=A\to \left(\phi \leftrightarrow \theta \right)$$
4		nn1suc.5	$$⊢\psi$$
5		nn1suc.6	$$⊢y\in \mathbb{N}\to \chi$$
6		1ex	$$⊢1\in \mathrm{V}$$
7	6 1	sbcie	$$⊢\underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
8	4 7	mpbir	$$⊢\underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi$$
9		1nn	$$⊢1\in \mathbb{N}$$
10		eleq1	$$⊢A=1\to \left(A\in \mathbb{N}\leftrightarrow 1\in \mathbb{N}\right)$$
11	9 10	mpbiri	$$⊢A=1\to A\in \mathbb{N}$$
12	3	sbcieg	$$⊢A\in \mathbb{N}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \theta \right)$$
13	11 12	syl	$$⊢A=1\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \theta \right)$$
14		dfsbcq	$$⊢A=1\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi \right)$$
15	13 14	bitr3d	$$⊢A=1\to \left(\theta \leftrightarrow \underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi \right)$$
16	8 15	mpbiri	$$⊢A=1\to \theta$$
17	16	a1i	$$⊢A\in \mathbb{N}\to \left(A=1\to \theta \right)$$
18		ovex	$$⊢y+1\in \mathrm{V}$$
19	18 2	sbcie	$$⊢\underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \chi$$
20		oveq1	$$⊢y=A-1\to y+1=A-1+1$$
21	20	sbceq1d	$$⊢y=A-1\to \left(\underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(A-1+1\right)/x\underset{\dot{}}{]}\phi \right)$$
22	19 21	bitr3id	$$⊢y=A-1\to \left(\chi \leftrightarrow \underset{\dot{}}{[}\left(A-1+1\right)/x\underset{\dot{}}{]}\phi \right)$$
23	22 5	vtoclga	$$⊢A-1\in \mathbb{N}\to \underset{\dot{}}{[}\left(A-1+1\right)/x\underset{\dot{}}{]}\phi$$
24		nncn	$$⊢A\in \mathbb{N}\to A\in ℂ$$
25		ax-1cn	$$⊢1\in ℂ$$
26		npcan	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to A-1+1=A$$
27	24 25 26	sylancl	$$⊢A\in \mathbb{N}\to A-1+1=A$$
28	27	sbceq1d	$$⊢A\in \mathbb{N}\to \left(\underset{\dot{}}{[}\left(A-1+1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
29	28 12	bitrd	$$⊢A\in \mathbb{N}\to \left(\underset{\dot{}}{[}\left(A-1+1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \theta \right)$$
30	23 29	imbitrid	$$⊢A\in \mathbb{N}\to \left(A-1\in \mathbb{N}\to \theta \right)$$
31		nn1m1nn	$$⊢A\in \mathbb{N}\to \left(A=1\vee A-1\in \mathbb{N}\right)$$
32	17 30 31	mpjaod	$$⊢A\in \mathbb{N}\to \theta$$