Theorem 2nn0ind

Description: Induction on nonnegative integers with two base cases, for use with Lucas-type sequences. (Contributed by Stefan O'Rear, 1-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		2nn0ind.1	$$⊢\psi$$
2		2nn0ind.2	$$⊢\chi$$
3		2nn0ind.3	$$⊢y\in \mathbb{N}\to \left(\left(\theta \wedge \tau \right)\to \eta \right)$$
4		2nn0ind.4	$$⊢x=0\to \left(\phi \leftrightarrow \psi \right)$$
5		2nn0ind.5	$$⊢x=1\to \left(\phi \leftrightarrow \chi \right)$$
6		2nn0ind.6	$$⊢x=y-1\to \left(\phi \leftrightarrow \theta \right)$$
7		2nn0ind.7	$$⊢x=y\to \left(\phi \leftrightarrow \tau \right)$$
8		2nn0ind.8	$$⊢x=y+1\to \left(\phi \leftrightarrow \eta \right)$$
9		2nn0ind.9	$$⊢x=A\to \left(\phi \leftrightarrow \rho \right)$$
10		nn0p1nn	$$⊢A\in {\mathbb{N}}_0\to A+1\in \mathbb{N}$$
11		oveq1	$$⊢a=1\to a-1=1-1$$
12	11	sbceq1d	$$⊢a=1\to \left(\underset{\dot{}}{[}\left(a-1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(1-1\right)/x\underset{\dot{}}{]}\phi \right)$$
13		dfsbcq	$$⊢a=1\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi \right)$$
14	12 13	anbi12d	$$⊢a=1\to \left(\left(\underset{\dot{}}{[}\left(a-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(1-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi \right)\right)$$
15		oveq1	$$⊢a=y\to a-1=y-1$$
16	15	sbceq1d	$$⊢a=y\to \left(\underset{\dot{}}{[}\left(a-1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \right)$$
17		dfsbcq	$$⊢a=y\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
18	16 17	anbi12d	$$⊢a=y\to \left(\left(\underset{\dot{}}{[}\left(a-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
19		oveq1	$$⊢a=y+1\to a-1=y+1-1$$
20	19	sbceq1d	$$⊢a=y+1\to \left(\underset{\dot{}}{[}\left(a-1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(y+1-1\right)/x\underset{\dot{}}{]}\phi \right)$$
21		dfsbcq	$$⊢a=y+1\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi \right)$$
22	20 21	anbi12d	$$⊢a=y+1\to \left(\left(\underset{\dot{}}{[}\left(a-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(y+1-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi \right)\right)$$
23		oveq1	$$⊢a=A+1\to a-1=A+1-1$$
24	23	sbceq1d	$$⊢a=A+1\to \left(\underset{\dot{}}{[}\left(a-1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(A+1-1\right)/x\underset{\dot{}}{]}\phi \right)$$
25		dfsbcq	$$⊢a=A+1\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(A+1\right)/x\underset{\dot{}}{]}\phi \right)$$
26	24 25	anbi12d	$$⊢a=A+1\to \left(\left(\underset{\dot{}}{[}\left(a-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}\left(A+1-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}\left(A+1\right)/x\underset{\dot{}}{]}\phi \right)\right)$$
27		ovex	$$⊢1-1\in \mathrm{V}$$
28		1m1e0	$$⊢1-1=0$$
29	28	eqeq2i	$$⊢x=1-1\leftrightarrow x=0$$
30	29 4	sylbi	$$⊢x=1-1\to \left(\phi \leftrightarrow \psi \right)$$
31	27 30	sbcie	$$⊢\underset{\dot{}}{[}\left(1-1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
32	1 31	mpbir	$$⊢\underset{\dot{}}{[}\left(1-1\right)/x\underset{\dot{}}{]}\phi$$
33		1ex	$$⊢1\in \mathrm{V}$$
34	33 5	sbcie	$$⊢\underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi \leftrightarrow \chi$$
35	2 34	mpbir	$$⊢\underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi$$
36	32 35	pm3.2i	$$⊢\left(\underset{\dot{}}{[}\left(1-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}1/x\underset{\dot{}}{]}\phi \right)$$
37		simprr	$$⊢\left(y\in \mathbb{N}\wedge \left(\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\to \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi$$
38		nncn	$$⊢y\in \mathbb{N}\to y\in ℂ$$
39		ax-1cn	$$⊢1\in ℂ$$
40		pncan	$$⊢\left(y\in ℂ\wedge 1\in ℂ\right)\to y+1-1=y$$
41	38 39 40	sylancl	$$⊢y\in \mathbb{N}\to y+1-1=y$$
42	41	adantr	$$⊢\left(y\in \mathbb{N}\wedge \left(\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\to y+1-1=y$$
43	42	sbceq1d	$$⊢\left(y\in \mathbb{N}\wedge \left(\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\to \left(\underset{\dot{}}{[}\left(y+1-1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
44	37 43	mpbird	$$⊢\left(y\in \mathbb{N}\wedge \left(\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\to \underset{\dot{}}{[}\left(y+1-1\right)/x\underset{\dot{}}{]}\phi$$
45		ovex	$$⊢y-1\in \mathrm{V}$$
46	45 6	sbcie	$$⊢\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \theta$$
47		vex	$$⊢y\in \mathrm{V}$$
48	47 7	sbcie	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \tau$$
49	46 48	anbi12i	$$⊢\left(\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\theta \wedge \tau \right)$$
50		ovex	$$⊢y+1\in \mathrm{V}$$
51	50 8	sbcie	$$⊢\underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \eta$$
52	3 49 51	3imtr4g	$$⊢y\in \mathbb{N}\to \left(\left(\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\to \underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi \right)$$
53	52	imp	$$⊢\left(y\in \mathbb{N}\wedge \left(\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\to \underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi$$
54	44 53	jca	$$⊢\left(y\in \mathbb{N}\wedge \left(\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)\to \left(\underset{\dot{}}{[}\left(y+1-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi \right)$$
55	54	ex	$$⊢y\in \mathbb{N}\to \left(\left(\underset{\dot{}}{[}\left(y-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\to \left(\underset{\dot{}}{[}\left(y+1-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi \right)\right)$$
56	14 18 22 26 36 55	nnind	$$⊢A+1\in \mathbb{N}\to \left(\underset{\dot{}}{[}\left(A+1-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}\left(A+1\right)/x\underset{\dot{}}{]}\phi \right)$$
57	10 56	syl	$$⊢A\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left(A+1-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}\left(A+1\right)/x\underset{\dot{}}{]}\phi \right)$$
58		nn0cn	$$⊢A\in {\mathbb{N}}_0\to A\in ℂ$$
59		pncan	$$⊢\left(A\in ℂ\wedge 1\in ℂ\right)\to A+1-1=A$$
60	58 39 59	sylancl	$$⊢A\in {\mathbb{N}}_0\to A+1-1=A$$
61	60	sbceq1d	$$⊢A\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}\left(A+1-1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
62	61	biimpa	$$⊢\left(A\in {\mathbb{N}}_0\wedge \underset{\dot{}}{[}\left(A+1-1\right)/x\underset{\dot{}}{]}\phi \right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
63	62	adantrr	$$⊢\left(A\in {\mathbb{N}}_0\wedge \left(\underset{\dot{}}{[}\left(A+1-1\right)/x\underset{\dot{}}{]}\phi \wedge \underset{\dot{}}{[}\left(A+1\right)/x\underset{\dot{}}{]}\phi \right)\right)\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
64	57 63	mpdan	$$⊢A\in {\mathbb{N}}_0\to \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi$$
65	9	sbcieg	$$⊢A\in {\mathbb{N}}_0\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \rho \right)$$
66	64 65	mpbid	$$⊢A\in {\mathbb{N}}_0\to \rho$$