Theorem zindbi

Description: Inductively transfer a property to the integers if it holds for zero and passes between adjacent integers in either direction. (Contributed by Stefan O'Rear, 1-Oct-2014)

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

Proof

Step	Hyp	Ref	Expression
1		zindbi.1	$$⊢y\in \mathbb{Z}\to \left(\psi \leftrightarrow \chi \right)$$
2		zindbi.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
3		zindbi.3	$$⊢x=y+1\to \left(\phi \leftrightarrow \chi \right)$$
4		zindbi.4	$$⊢x=0\to \left(\phi \leftrightarrow \theta \right)$$
5		zindbi.5	$$⊢x=A\to \left(\phi \leftrightarrow \tau \right)$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7	6 4	sbcie	$$⊢\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \theta$$
8		0z	$$⊢0\in \mathbb{Z}$$
9		eleq1	$$⊢y=0\to \left(y\in \mathbb{Z}\leftrightarrow 0\in \mathbb{Z}\right)$$
10		breq1	$$⊢y=0\to \left(y\le b\leftrightarrow 0\le b\right)$$
11	9 10	3anbi13d	$$⊢y=0\to \left(\left(y\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge y\le b\right)\leftrightarrow \left(0\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge 0\le b\right)\right)$$
12		dfsbcq	$$⊢y=0\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \right)$$
13	12	bibi1d	$$⊢y=0\to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\right)$$
14	11 13	imbi12d	$$⊢y=0\to \left(\left(\left(y\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge y\le b\right)\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(\left(0\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge 0\le b\right)\to \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\right)\right)$$
15		eleq1	$$⊢b=A\to \left(b\in \mathbb{Z}\leftrightarrow A\in \mathbb{Z}\right)$$
16		breq2	$$⊢b=A\to \left(0\le b\leftrightarrow 0\le A\right)$$
17	15 16	3anbi23d	$$⊢b=A\to \left(\left(0\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge 0\le b\right)\leftrightarrow \left(0\in \mathbb{Z}\wedge A\in \mathbb{Z}\wedge 0\le A\right)\right)$$
18		dfsbcq	$$⊢b=A\to \left(\underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
19	18	bibi2d	$$⊢b=A\to \left(\left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
20	17 19	imbi12d	$$⊢b=A\to \left(\left(\left(0\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge 0\le b\right)\to \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(\left(0\in \mathbb{Z}\wedge A\in \mathbb{Z}\wedge 0\le A\right)\to \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)\right)$$
21		dfsbcq	$$⊢a=y\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
22	21	bibi2d	$$⊢a=y\to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)\right)$$
23		dfsbcq	$$⊢a=b\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)$$
24	23	bibi2d	$$⊢a=b\to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\right)$$
25		dfsbcq	$$⊢a=b+1\to \left(\underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(b+1\right)/x\underset{\dot{}}{]}\phi \right)$$
26	25	bibi2d	$$⊢a=b+1\to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}a/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(b+1\right)/x\underset{\dot{}}{]}\phi \right)\right)$$
27		biidd	$$⊢y\in \mathbb{Z}\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \right)$$
28		vex	$$⊢y\in \mathrm{V}$$
29	28 2	sbcie	$$⊢\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \psi$$
30		dfsbcq	$$⊢y=b\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)$$
31	29 30	bitr3id	$$⊢y=b\to \left(\psi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)$$
32		ovex	$$⊢y+1\in \mathrm{V}$$
33	32 3	sbcie	$$⊢\underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \chi$$
34		oveq1	$$⊢y=b\to y+1=b+1$$
35	34	sbceq1d	$$⊢y=b\to \left(\underset{\dot{}}{[}\left(y+1\right)/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(b+1\right)/x\underset{\dot{}}{]}\phi \right)$$
36	33 35	bitr3id	$$⊢y=b\to \left(\chi \leftrightarrow \underset{\dot{}}{[}\left(b+1\right)/x\underset{\dot{}}{]}\phi \right)$$
37	31 36	bibi12d	$$⊢y=b\to \left(\left(\psi \leftrightarrow \chi \right)\leftrightarrow \left(\underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(b+1\right)/x\underset{\dot{}}{]}\phi \right)\right)$$
38	37 1	vtoclga	$$⊢b\in \mathbb{Z}\to \left(\underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(b+1\right)/x\underset{\dot{}}{]}\phi \right)$$
39	38	3ad2ant2	$$⊢\left(y\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge y\le b\right)\to \left(\underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(b+1\right)/x\underset{\dot{}}{]}\phi \right)$$
40	39	bibi2d	$$⊢\left(y\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge y\le b\right)\to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(b+1\right)/x\underset{\dot{}}{]}\phi \right)\right)$$
41	40	biimpd	$$⊢\left(y\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge y\le b\right)\to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}\left(b+1\right)/x\underset{\dot{}}{]}\phi \right)\right)$$
42	22 24 26 24 27 41	uzind	$$⊢\left(y\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge y\le b\right)\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)$$
43	14 20 42	vtocl2g	$$⊢\left(0\in \mathbb{Z}\wedge A\in \mathbb{Z}\right)\to \left(\left(0\in \mathbb{Z}\wedge A\in \mathbb{Z}\wedge 0\le A\right)\to \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
44	43	3adant3	$$⊢\left(0\in \mathbb{Z}\wedge A\in \mathbb{Z}\wedge 0\le A\right)\to \left(\left(0\in \mathbb{Z}\wedge A\in \mathbb{Z}\wedge 0\le A\right)\to \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)\right)$$
45	44	pm2.43i	$$⊢\left(0\in \mathbb{Z}\wedge A\in \mathbb{Z}\wedge 0\le A\right)\to \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
46	8 45	mp3an1	$$⊢\left(A\in \mathbb{Z}\wedge 0\le A\right)\to \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
47		eleq1	$$⊢y=A\to \left(y\in \mathbb{Z}\leftrightarrow A\in \mathbb{Z}\right)$$
48		breq1	$$⊢y=A\to \left(y\le b\leftrightarrow A\le b\right)$$
49	47 48	3anbi13d	$$⊢y=A\to \left(\left(y\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge y\le b\right)\leftrightarrow \left(A\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge A\le b\right)\right)$$
50		dfsbcq	$$⊢y=A\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
51	50	bibi1d	$$⊢y=A\to \left(\left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\right)$$
52	49 51	imbi12d	$$⊢y=A\to \left(\left(\left(y\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge y\le b\right)\to \left(\underset{\dot{}}{[}y/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(\left(A\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge A\le b\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\right)\right)$$
53		eleq1	$$⊢b=0\to \left(b\in \mathbb{Z}\leftrightarrow 0\in \mathbb{Z}\right)$$
54		breq2	$$⊢b=0\to \left(A\le b\leftrightarrow A\le 0\right)$$
55	53 54	3anbi23d	$$⊢b=0\to \left(\left(A\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge A\le b\right)\leftrightarrow \left(A\in \mathbb{Z}\wedge 0\in \mathbb{Z}\wedge A\le 0\right)\right)$$
56		dfsbcq	$$⊢b=0\to \left(\underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \right)$$
57	56	bibi2d	$$⊢b=0\to \left(\left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \right)\right)$$
58	55 57	imbi12d	$$⊢b=0\to \left(\left(\left(A\in \mathbb{Z}\wedge b\in \mathbb{Z}\wedge A\le b\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}b/x\underset{\dot{}}{]}\phi \right)\right)\leftrightarrow \left(\left(A\in \mathbb{Z}\wedge 0\in \mathbb{Z}\wedge A\le 0\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \right)\right)\right)$$
59	52 58 42	vtocl2g	$$⊢\left(A\in \mathbb{Z}\wedge 0\in \mathbb{Z}\right)\to \left(\left(A\in \mathbb{Z}\wedge 0\in \mathbb{Z}\wedge A\le 0\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \right)\right)$$
60	59	3adant3	$$⊢\left(A\in \mathbb{Z}\wedge 0\in \mathbb{Z}\wedge A\le 0\right)\to \left(\left(A\in \mathbb{Z}\wedge 0\in \mathbb{Z}\wedge A\le 0\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \right)\right)$$
61	60	pm2.43i	$$⊢\left(A\in \mathbb{Z}\wedge 0\in \mathbb{Z}\wedge A\le 0\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \right)$$
62	8 61	mp3an2	$$⊢\left(A\in \mathbb{Z}\wedge A\le 0\right)\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \right)$$
63	62	bicomd	$$⊢\left(A\in \mathbb{Z}\wedge A\le 0\right)\to \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
64		0re	$$⊢0\in ℝ$$
65		zre	$$⊢A\in \mathbb{Z}\to A\in ℝ$$
66		letric	$$⊢\left(0\in ℝ\wedge A\in ℝ\right)\to \left(0\le A\vee A\le 0\right)$$
67	64 65 66	sylancr	$$⊢A\in \mathbb{Z}\to \left(0\le A\vee A\le 0\right)$$
68	46 63 67	mpjaodan	$$⊢A\in \mathbb{Z}\to \left(\underset{\dot{}}{[}0/x\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
69	7 68	bitr3id	$$⊢A\in \mathbb{Z}\to \left(\theta \leftrightarrow \underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \right)$$
70	5	sbcieg	$$⊢A\in \mathbb{Z}\to \left(\underset{\dot{}}{[}A/x\underset{\dot{}}{]}\phi \leftrightarrow \tau \right)$$
71	69 70	bitrd	$$⊢A\in \mathbb{Z}\to \left(\theta \leftrightarrow \tau \right)$$