Step |
Hyp |
Ref |
Expression |
1 |
|
3z |
⊢ 3 ∈ ℤ |
2 |
|
fzoval |
⊢ ( 3 ∈ ℤ → ( 1 ..^ 3 ) = ( 1 ... ( 3 − 1 ) ) ) |
3 |
1 2
|
ax-mp |
⊢ ( 1 ..^ 3 ) = ( 1 ... ( 3 − 1 ) ) |
4 |
|
3m1e2 |
⊢ ( 3 − 1 ) = 2 |
5 |
|
1p1e2 |
⊢ ( 1 + 1 ) = 2 |
6 |
4 5
|
eqtr4i |
⊢ ( 3 − 1 ) = ( 1 + 1 ) |
7 |
6
|
oveq2i |
⊢ ( 1 ... ( 3 − 1 ) ) = ( 1 ... ( 1 + 1 ) ) |
8 |
|
1z |
⊢ 1 ∈ ℤ |
9 |
|
fzpr |
⊢ ( 1 ∈ ℤ → ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } ) |
10 |
8 9
|
ax-mp |
⊢ ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } |
11 |
3 7 10
|
3eqtri |
⊢ ( 1 ..^ 3 ) = { 1 , ( 1 + 1 ) } |
12 |
5
|
preq2i |
⊢ { 1 , ( 1 + 1 ) } = { 1 , 2 } |
13 |
11 12
|
eqtri |
⊢ ( 1 ..^ 3 ) = { 1 , 2 } |