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 ) )