Theorem i4

Description: _i to the fourth power. (Contributed by NM, 31-Jan-2007)

	Ref	Expression
Assertion	i4	⊢ ( i ↑ 4 ) = 1

Proof

Step	Hyp	Ref	Expression
1		ax-icn	⊢ i ∈ ℂ
2		2nn0	⊢ 2 ∈ ℕ0
3		expadd	⊢ ( ( i ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 2 ∈ ℕ0 ) → ( i ↑ ( 2 + 2 ) ) = ( ( i ↑ 2 ) · ( i ↑ 2 ) ) )
4	1 2 2 3	mp3an	⊢ ( i ↑ ( 2 + 2 ) ) = ( ( i ↑ 2 ) · ( i ↑ 2 ) )
5		2p2e4	⊢ ( 2 + 2 ) = 4
6	5	oveq2i	⊢ ( i ↑ ( 2 + 2 ) ) = ( i ↑ 4 )
7		i2	⊢ ( i ↑ 2 ) = - 1
8	7 7	oveq12i	⊢ ( ( i ↑ 2 ) · ( i ↑ 2 ) ) = ( - 1 · - 1 )
9		ax-1cn	⊢ 1 ∈ ℂ
10	9 9	mul2negi	⊢ ( - 1 · - 1 ) = ( 1 · 1 )
11		1t1e1	⊢ ( 1 · 1 ) = 1
12	8 10 11	3eqtri	⊢ ( ( i ↑ 2 ) · ( i ↑ 2 ) ) = 1
13	4 6 12	3eqtr3i	⊢ ( i ↑ 4 ) = 1