This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ∀ 𝑥 ∈ ( 1 ... 3 ) ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) ↔ ( ( 𝐹 ‘ 1 ) = 𝐴 ∧ ( 𝐹 ‘ 2 ) = 𝐵 ∧ ( 𝐹 ‘ 3 ) = 𝐶 ) )

Proof

Step Hyp Ref Expression
1 1z ⊢ 1 ∈ ℤ
2 fztp ⊢ ( 1 ∈ ℤ → ( 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 ∈ ℂ
6 ax-1cn ⊢ 1 ∈ ℂ
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 ⊢ ( ∀ 𝑥 ∈ ( 1 ... 3 ) ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) ↔ ∀ 𝑥 ∈ { 1 , 2 , 3 } ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) )
18 1ex ⊢ 1 ∈ V
19 2ex ⊢ 2 ∈ V
20 3ex ⊢ 3 ∈ V
21 fveq2 ⊢ ( 𝑥 = 1 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 1 ) )
22 iftrue ⊢ ( 𝑥 = 1 → if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) = 𝐴 )
23 21 22 eqeq12d ⊢ ( 𝑥 = 1 → ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) ↔ ( 𝐹 ‘ 1 ) = 𝐴 ) )
24 fveq2 ⊢ ( 𝑥 = 2 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 2 ) )
25 1re ⊢ 1 ∈ ℝ
26 1lt2 ⊢ 1 < 2
27 25 26 gtneii ⊢ 2 ≠ 1
28 neeq1 ⊢ ( 𝑥 = 2 → ( 𝑥 ≠ 1 ↔ 2 ≠ 1 ) )
29 27 28 mpbiri ⊢ ( 𝑥 = 2 → 𝑥 ≠ 1 )
30 ifnefalse ⊢ ( 𝑥 ≠ 1 → if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) = if ( 𝑥 = 2 , 𝐵 , 𝐶 ) )
31 29 30 syl ⊢ ( 𝑥 = 2 → if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) = if ( 𝑥 = 2 , 𝐵 , 𝐶 ) )
32 iftrue ⊢ ( 𝑥 = 2 → if ( 𝑥 = 2 , 𝐵 , 𝐶 ) = 𝐵 )
33 31 32 eqtrd ⊢ ( 𝑥 = 2 → if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) = 𝐵 )
34 24 33 eqeq12d ⊢ ( 𝑥 = 2 → ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) ↔ ( 𝐹 ‘ 2 ) = 𝐵 ) )
35 fveq2 ⊢ ( 𝑥 = 3 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 3 ) )
36 1lt3 ⊢ 1 < 3
37 25 36 gtneii ⊢ 3 ≠ 1
38 neeq1 ⊢ ( 𝑥 = 3 → ( 𝑥 ≠ 1 ↔ 3 ≠ 1 ) )
39 37 38 mpbiri ⊢ ( 𝑥 = 3 → 𝑥 ≠ 1 )
40 39 30 syl ⊢ ( 𝑥 = 3 → if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) = if ( 𝑥 = 2 , 𝐵 , 𝐶 ) )
41 2re ⊢ 2 ∈ ℝ
42 2lt3 ⊢ 2 < 3
43 41 42 gtneii ⊢ 3 ≠ 2
44 neeq1 ⊢ ( 𝑥 = 3 → ( 𝑥 ≠ 2 ↔ 3 ≠ 2 ) )
45 43 44 mpbiri ⊢ ( 𝑥 = 3 → 𝑥 ≠ 2 )
46 ifnefalse ⊢ ( 𝑥 ≠ 2 → if ( 𝑥 = 2 , 𝐵 , 𝐶 ) = 𝐶 )
47 45 46 syl ⊢ ( 𝑥 = 3 → if ( 𝑥 = 2 , 𝐵 , 𝐶 ) = 𝐶 )
48 40 47 eqtrd ⊢ ( 𝑥 = 3 → if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) = 𝐶 )
49 35 48 eqeq12d ⊢ ( 𝑥 = 3 → ( ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) ↔ ( 𝐹 ‘ 3 ) = 𝐶 ) )
50 18 19 20 23 34 49 raltp ⊢ ( ∀ 𝑥 ∈ { 1 , 2 , 3 } ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) ↔ ( ( 𝐹 ‘ 1 ) = 𝐴 ∧ ( 𝐹 ‘ 2 ) = 𝐵 ∧ ( 𝐹 ‘ 3 ) = 𝐶 ) )
51 17 50 bitri ⊢ ( ∀ 𝑥 ∈ ( 1 ... 3 ) ( 𝐹 ‘ 𝑥 ) = if ( 𝑥 = 1 , 𝐴 , if ( 𝑥 = 2 , 𝐵 , 𝐶 ) ) ↔ ( ( 𝐹 ‘ 1 ) = 𝐴 ∧ ( 𝐹 ‘ 2 ) = 𝐵 ∧ ( 𝐹 ‘ 3 ) = 𝐶 ) )