Theorem fztpval

Description: Two ways of defining the first three values of a sequence on NN . (Contributed by NM, 13-Sep-2011)

	Ref	Expression
Assertion	fztpval	$$⊢\forall x\in \left(1\dots 3\right)F\left(x\right)=if\left(x=1,A,if\left(x=2,B,C\right)\right)\leftrightarrow \left(F\left(1\right)=A\wedge F\left(2\right)=B\wedge F\left(3\right)=C\right)$$

Proof

Step	Hyp	Ref	Expression
1		1z	$$⊢1\in \mathbb{Z}$$
2		fztp	$$⊢1\in \mathbb{Z}\to \left(1\dots 1+2\right)=\left\{1,1+1,1+2\right\}$$
3	1 2	ax-mp	$$⊢\left(1\dots 1+2\right)=\left\{1,1+1,1+2\right\}$$
4		df-3	$$⊢3=2+1$$
5		2cn	$$⊢2\in ℂ$$
6		ax-1cn	$$⊢1\in ℂ$$
7	5 6	addcomi	$$⊢2+1=1+2$$
8	4 7	eqtri	$$⊢3=1+2$$
9	8	oveq2i	$$⊢\left(1\dots 3\right)=\left(1\dots 1+2\right)$$
10		tpeq3	$$⊢3=1+2\to \left\{1,2,3\right\}=\left\{1,2,1+2\right\}$$
11	8 10	ax-mp	$$⊢\left\{1,2,3\right\}=\left\{1,2,1+2\right\}$$
12		df-2	$$⊢2=1+1$$
13		tpeq2	$$⊢2=1+1\to \left\{1,2,1+2\right\}=\left\{1,1+1,1+2\right\}$$
14	12 13	ax-mp	$$⊢\left\{1,2,1+2\right\}=\left\{1,1+1,1+2\right\}$$
15	11 14	eqtri	$$⊢\left\{1,2,3\right\}=\left\{1,1+1,1+2\right\}$$
16	3 9 15	3eqtr4i	$$⊢\left(1\dots 3\right)=\left\{1,2,3\right\}$$
17	16	raleqi	$$⊢\forall x\in \left(1\dots 3\right)F\left(x\right)=if\left(x=1,A,if\left(x=2,B,C\right)\right)\leftrightarrow \forall x\in \left\{1,2,3\right\}F\left(x\right)=if\left(x=1,A,if\left(x=2,B,C\right)\right)$$
18		1ex	$$⊢1\in \mathrm{V}$$
19		2ex	$$⊢2\in \mathrm{V}$$
20		3ex	$$⊢3\in \mathrm{V}$$
21		fveq2	$$⊢x=1\to F\left(x\right)=F\left(1\right)$$
22		iftrue	$$⊢x=1\to if\left(x=1,A,if\left(x=2,B,C\right)\right)=A$$
23	21 22	eqeq12d	$$⊢x=1\to \left(F\left(x\right)=if\left(x=1,A,if\left(x=2,B,C\right)\right)\leftrightarrow F\left(1\right)=A\right)$$
24		fveq2	$$⊢x=2\to F\left(x\right)=F\left(2\right)$$
25		1re	$$⊢1\in ℝ$$
26		1lt2	$$⊢1<2$$
27	25 26	gtneii	$$⊢2\ne 1$$
28		neeq1	$$⊢x=2\to \left(x\ne 1\leftrightarrow 2\ne 1\right)$$
29	27 28	mpbiri	$$⊢x=2\to x\ne 1$$
30		ifnefalse	$$⊢x\ne 1\to if\left(x=1,A,if\left(x=2,B,C\right)\right)=if\left(x=2,B,C\right)$$
31	29 30	syl	$$⊢x=2\to if\left(x=1,A,if\left(x=2,B,C\right)\right)=if\left(x=2,B,C\right)$$
32		iftrue	$$⊢x=2\to if\left(x=2,B,C\right)=B$$
33	31 32	eqtrd	$$⊢x=2\to if\left(x=1,A,if\left(x=2,B,C\right)\right)=B$$
34	24 33	eqeq12d	$$⊢x=2\to \left(F\left(x\right)=if\left(x=1,A,if\left(x=2,B,C\right)\right)\leftrightarrow F\left(2\right)=B\right)$$
35		fveq2	$$⊢x=3\to F\left(x\right)=F\left(3\right)$$
36		1lt3	$$⊢1<3$$
37	25 36	gtneii	$$⊢3\ne 1$$
38		neeq1	$$⊢x=3\to \left(x\ne 1\leftrightarrow 3\ne 1\right)$$
39	37 38	mpbiri	$$⊢x=3\to x\ne 1$$
40	39 30	syl	$$⊢x=3\to if\left(x=1,A,if\left(x=2,B,C\right)\right)=if\left(x=2,B,C\right)$$
41		2re	$$⊢2\in ℝ$$
42		2lt3	$$⊢2<3$$
43	41 42	gtneii	$$⊢3\ne 2$$
44		neeq1	$$⊢x=3\to \left(x\ne 2\leftrightarrow 3\ne 2\right)$$
45	43 44	mpbiri	$$⊢x=3\to x\ne 2$$
46		ifnefalse	$$⊢x\ne 2\to if\left(x=2,B,C\right)=C$$
47	45 46	syl	$$⊢x=3\to if\left(x=2,B,C\right)=C$$
48	40 47	eqtrd	$$⊢x=3\to if\left(x=1,A,if\left(x=2,B,C\right)\right)=C$$
49	35 48	eqeq12d	$$⊢x=3\to \left(F\left(x\right)=if\left(x=1,A,if\left(x=2,B,C\right)\right)\leftrightarrow F\left(3\right)=C\right)$$
50	18 19 20 23 34 49	raltp	$$⊢\forall x\in \left\{1,2,3\right\}F\left(x\right)=if\left(x=1,A,if\left(x=2,B,C\right)\right)\leftrightarrow \left(F\left(1\right)=A\wedge F\left(2\right)=B\wedge F\left(3\right)=C\right)$$
51	17 50	bitri	$$⊢\forall x\in \left(1\dots 3\right)F\left(x\right)=if\left(x=1,A,if\left(x=2,B,C\right)\right)\leftrightarrow \left(F\left(1\right)=A\wedge F\left(2\right)=B\wedge F\left(3\right)=C\right)$$