| Step |
Hyp |
Ref |
Expression |
| 1 |
|
ax-icn |
⊢ i ∈ ℂ |
| 2 |
1 1
|
mulcli |
⊢ ( i · i ) ∈ ℂ |
| 3 |
2 2 1
|
mulassi |
⊢ ( ( ( i · i ) · ( i · i ) ) · i ) = ( ( i · i ) · ( ( i · i ) · i ) ) |
| 4 |
1 2
|
mulcli |
⊢ ( i · ( i · i ) ) ∈ ℂ |
| 5 |
1 1 4
|
mulassi |
⊢ ( ( i · i ) · ( i · ( i · i ) ) ) = ( i · ( i · ( i · ( i · i ) ) ) ) |
| 6 |
1 1 1
|
mulassi |
⊢ ( ( i · i ) · i ) = ( i · ( i · i ) ) |
| 7 |
6
|
oveq2i |
⊢ ( ( i · i ) · ( ( i · i ) · i ) ) = ( ( i · i ) · ( i · ( i · i ) ) ) |
| 8 |
1 1 2
|
mulassi |
⊢ ( ( i · i ) · ( i · i ) ) = ( i · ( i · ( i · i ) ) ) |
| 9 |
8
|
oveq2i |
⊢ ( i · ( ( i · i ) · ( i · i ) ) ) = ( i · ( i · ( i · ( i · i ) ) ) ) |
| 10 |
5 7 9
|
3eqtr4i |
⊢ ( ( i · i ) · ( ( i · i ) · i ) ) = ( i · ( ( i · i ) · ( i · i ) ) ) |
| 11 |
3 10
|
eqtri |
⊢ ( ( ( i · i ) · ( i · i ) ) · i ) = ( i · ( ( i · i ) · ( i · i ) ) ) |
| 12 |
|
rei4 |
⊢ ( ( i · i ) · ( i · i ) ) = 1 |
| 13 |
12
|
oveq1i |
⊢ ( ( ( i · i ) · ( i · i ) ) · i ) = ( 1 · i ) |
| 14 |
12
|
oveq2i |
⊢ ( i · ( ( i · i ) · ( i · i ) ) ) = ( i · 1 ) |
| 15 |
11 13 14
|
3eqtr3i |
⊢ ( 1 · i ) = ( i · 1 ) |