Metamath Proof Explorer


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
|- ( A. x e. ( 1 ... 3 ) ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( ( F ` 1 ) = A /\ ( F ` 2 ) = B /\ ( F ` 3 ) = C ) )

Proof

Step Hyp Ref Expression
1 1z
 |-  1 e. ZZ
2 fztp
 |-  ( 1 e. ZZ -> ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
3 1 2 ax-mp
 |-  ( 1 ... ( 1 + 2 ) ) = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
4 df-3
 |-  3 = ( 2 + 1 )
5 2cn
 |-  2 e. CC
6 ax-1cn
 |-  1 e. CC
7 5 6 addcomi
 |-  ( 2 + 1 ) = ( 1 + 2 )
8 4 7 eqtri
 |-  3 = ( 1 + 2 )
9 8 oveq2i
 |-  ( 1 ... 3 ) = ( 1 ... ( 1 + 2 ) )
10 tpeq3
 |-  ( 3 = ( 1 + 2 ) -> { 1 , 2 , 3 } = { 1 , 2 , ( 1 + 2 ) } )
11 8 10 ax-mp
 |-  { 1 , 2 , 3 } = { 1 , 2 , ( 1 + 2 ) }
12 df-2
 |-  2 = ( 1 + 1 )
13 tpeq2
 |-  ( 2 = ( 1 + 1 ) -> { 1 , 2 , ( 1 + 2 ) } = { 1 , ( 1 + 1 ) , ( 1 + 2 ) } )
14 12 13 ax-mp
 |-  { 1 , 2 , ( 1 + 2 ) } = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
15 11 14 eqtri
 |-  { 1 , 2 , 3 } = { 1 , ( 1 + 1 ) , ( 1 + 2 ) }
16 3 9 15 3eqtr4i
 |-  ( 1 ... 3 ) = { 1 , 2 , 3 }
17 16 raleqi
 |-  ( A. x e. ( 1 ... 3 ) ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> A. x e. { 1 , 2 , 3 } ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) )
18 1ex
 |-  1 e. _V
19 2ex
 |-  2 e. _V
20 3ex
 |-  3 e. _V
21 fveq2
 |-  ( x = 1 -> ( F ` x ) = ( F ` 1 ) )
22 iftrue
 |-  ( x = 1 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = A )
23 21 22 eqeq12d
 |-  ( x = 1 -> ( ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( F ` 1 ) = A ) )
24 fveq2
 |-  ( x = 2 -> ( F ` x ) = ( F ` 2 ) )
25 1re
 |-  1 e. RR
26 1lt2
 |-  1 < 2
27 25 26 gtneii
 |-  2 =/= 1
28 neeq1
 |-  ( x = 2 -> ( x =/= 1 <-> 2 =/= 1 ) )
29 27 28 mpbiri
 |-  ( x = 2 -> x =/= 1 )
30 ifnefalse
 |-  ( x =/= 1 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = if ( x = 2 , B , C ) )
31 29 30 syl
 |-  ( x = 2 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = if ( x = 2 , B , C ) )
32 iftrue
 |-  ( x = 2 -> if ( x = 2 , B , C ) = B )
33 31 32 eqtrd
 |-  ( x = 2 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = B )
34 24 33 eqeq12d
 |-  ( x = 2 -> ( ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( F ` 2 ) = B ) )
35 fveq2
 |-  ( x = 3 -> ( F ` x ) = ( F ` 3 ) )
36 1lt3
 |-  1 < 3
37 25 36 gtneii
 |-  3 =/= 1
38 neeq1
 |-  ( x = 3 -> ( x =/= 1 <-> 3 =/= 1 ) )
39 37 38 mpbiri
 |-  ( x = 3 -> x =/= 1 )
40 39 30 syl
 |-  ( x = 3 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = if ( x = 2 , B , C ) )
41 2re
 |-  2 e. RR
42 2lt3
 |-  2 < 3
43 41 42 gtneii
 |-  3 =/= 2
44 neeq1
 |-  ( x = 3 -> ( x =/= 2 <-> 3 =/= 2 ) )
45 43 44 mpbiri
 |-  ( x = 3 -> x =/= 2 )
46 ifnefalse
 |-  ( x =/= 2 -> if ( x = 2 , B , C ) = C )
47 45 46 syl
 |-  ( x = 3 -> if ( x = 2 , B , C ) = C )
48 40 47 eqtrd
 |-  ( x = 3 -> if ( x = 1 , A , if ( x = 2 , B , C ) ) = C )
49 35 48 eqeq12d
 |-  ( x = 3 -> ( ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( F ` 3 ) = C ) )
50 18 19 20 23 34 49 raltp
 |-  ( A. x e. { 1 , 2 , 3 } ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( ( F ` 1 ) = A /\ ( F ` 2 ) = B /\ ( F ` 3 ) = C ) )
51 17 50 bitri
 |-  ( A. x e. ( 1 ... 3 ) ( F ` x ) = if ( x = 1 , A , if ( x = 2 , B , C ) ) <-> ( ( F ` 1 ) = A /\ ( F ` 2 ) = B /\ ( F ` 3 ) = C ) )