Theorem nn0ind-raph

Description: Principle of Mathematical Induction (inference schema) on nonnegative integers. The first four hypotheses give us the substitution instances we need; the last two are the basis and the induction step. Raph Levien remarks: "This seems a bit painful. I wonder if an explicit substitution version would be easier." (Contributed by Raph Levien, 10-Apr-2004)

	Ref	Expression
Hypotheses	nn0ind-raph.1	$$⊢x=0\to \left(\phi \leftrightarrow \psi \right)$$
	nn0ind-raph.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
	nn0ind-raph.3	$$⊢x=y+1\to \left(\phi \leftrightarrow \theta \right)$$
	nn0ind-raph.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
	nn0ind-raph.5	$$⊢\psi$$
	nn0ind-raph.6	$$⊢y\in {\mathbb{N}}_0\to \left(\chi \to \theta \right)$$
Assertion	nn0ind-raph	$$⊢A\in {\mathbb{N}}_0\to \tau$$

Proof

Step	Hyp	Ref	Expression
1		nn0ind-raph.1	$$⊢x=0\to \left(\phi \leftrightarrow \psi \right)$$
2		nn0ind-raph.2	$$⊢x=y\to \left(\phi \leftrightarrow \chi \right)$$
3		nn0ind-raph.3	$$⊢x=y+1\to \left(\phi \leftrightarrow \theta \right)$$
4		nn0ind-raph.4	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
5		nn0ind-raph.5	$$⊢\psi$$
6		nn0ind-raph.6	$$⊢y\in {\mathbb{N}}_0\to \left(\chi \to \theta \right)$$
7		elnn0	$$⊢A\in {\mathbb{N}}_0\leftrightarrow \left(A\in \mathbb{N}\vee A=0\right)$$
8		dfsbcq2	$$⊢z=1\to \left(\left[z/x\right]\phi \leftrightarrow \underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi \right)$$
9		nfv	$$⊢Ⅎx\chi$$
10	9 2	sbhypf	$$⊢z=y\to \left(\left[z/x\right]\phi \leftrightarrow \chi \right)$$
11		nfv	$$⊢Ⅎx\theta$$
12	11 3	sbhypf	$$⊢z=y+1\to \left(\left[z/x\right]\phi \leftrightarrow \theta \right)$$
13		nfv	$$⊢Ⅎx\tau$$
14	13 4	sbhypf	$$⊢z=A\to \left(\left[z/x\right]\phi \leftrightarrow \tau \right)$$
15		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi$$
16		1ex	$$⊢1\in \mathrm{V}$$
17		c0ex	$$⊢0\in \mathrm{V}$$
18		0nn0	$$⊢0\in {\mathbb{N}}_0$$
19		eleq1a	$$⊢0\in {\mathbb{N}}_0\to \left(y=0\to y\in {\mathbb{N}}_0\right)$$
20	18 19	ax-mp	$$⊢y=0\to y\in {\mathbb{N}}_0$$
21	5 1	mpbiri	$$⊢x=0\to \phi$$
22		eqeq2	$$⊢y=0\to \left(x=y\leftrightarrow x=0\right)$$
23	22 2	syl6bir	$$⊢y=0\to \left(x=0\to \left(\phi \leftrightarrow \chi \right)\right)$$
24	23	pm5.74d	$$⊢y=0\to \left(\left(x=0\to \phi \right)\leftrightarrow \left(x=0\to \chi \right)\right)$$
25	21 24	mpbii	$$⊢y=0\to \left(x=0\to \chi \right)$$
26	25	com12	$$⊢x=0\to \left(y=0\to \chi \right)$$
27	17 26	vtocle	$$⊢y=0\to \chi$$
28	20 27 6	sylc	$$⊢y=0\to \theta$$
29	28	adantr	$$⊢\left(y=0\wedge x=1\right)\to \theta$$
30		oveq1	$$⊢y=0\to y+1=0+1$$
31		0p1e1	$$⊢0+1=1$$
32	30 31	eqtrdi	$$⊢y=0\to y+1=1$$
33	32	eqeq2d	$$⊢y=0\to \left(x=y+1\leftrightarrow x=1\right)$$
34	33 3	syl6bir	$$⊢y=0\to \left(x=1\to \left(\phi \leftrightarrow \theta \right)\right)$$
35	34	imp	$$⊢\left(y=0\wedge x=1\right)\to \left(\phi \leftrightarrow \theta \right)$$
36	29 35	mpbird	$$⊢\left(y=0\wedge x=1\right)\to \phi$$
37	36	ex	$$⊢y=0\to \left(x=1\to \phi \right)$$
38	17 37	vtocle	$$⊢x=1\to \phi$$
39		sbceq1a	$$⊢x=1\to \left(\phi \leftrightarrow \underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi \right)$$
40	38 39	mpbid	$$⊢x=1\to \underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi$$
41	15 16 40	vtoclef	$$⊢\underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi$$
42		nnnn0	$$⊢y\in \mathbb{N}\to y\in {\mathbb{N}}_0$$
43	42 6	syl	$$⊢y\in \mathbb{N}\to \left(\chi \to \theta \right)$$
44	8 10 12 14 41 43	nnind	$$⊢A\in \mathbb{N}\to \tau$$
45		nfv	$$⊢Ⅎx\left(0=A\to \tau \right)$$
46		eqeq1	$$⊢x=0\to \left(x=A\leftrightarrow 0=A\right)$$
47	1	bicomd	$$⊢x=0\to \left(\psi \leftrightarrow \phi \right)$$
48	47 4	sylan9bb	$$⊢\left(x=0\wedge x=A\right)\to \left(\psi \leftrightarrow \tau \right)$$
49	5 48	mpbii	$$⊢\left(x=0\wedge x=A\right)\to \tau$$
50	49	ex	$$⊢x=0\to \left(x=A\to \tau \right)$$
51	46 50	sylbird	$$⊢x=0\to \left(0=A\to \tau \right)$$
52	45 17 51	vtoclef	$$⊢0=A\to \tau$$
53	52	eqcoms	$$⊢A=0\to \tau$$
54	44 53	jaoi	$$⊢\left(A\in \mathbb{N}\vee A=0\right)\to \tau$$
55	7 54	sylbi	$$⊢A\in {\mathbb{N}}_0\to \tau$$