Theorem ipiiie0

Description: The multiplicative inverse of _i (per i4 ) is also its additive inverse. (Contributed by SN, 30-Jun-2024)

	Ref	Expression
Assertion	ipiiie0	⊢ ( i + ( i · ( i · i ) ) ) = 0

Proof

Step	Hyp	Ref	Expression
1		it1ei	⊢ ( i · 1 ) = i
2	1	eqcomi	⊢ i = ( i · 1 )
3		reixi	⊢ ( i · i ) = ( 0 −ℝ 1 )
4	3	oveq2i	⊢ ( i · ( i · i ) ) = ( i · ( 0 −ℝ 1 ) )
5	2 4	oveq12i	⊢ ( i + ( i · ( i · i ) ) ) = ( ( i · 1 ) + ( i · ( 0 −ℝ 1 ) ) )
6		ax-icn	⊢ i ∈ ℂ
7		ax-1cn	⊢ 1 ∈ ℂ
8		1re	⊢ 1 ∈ ℝ
9		rernegcl	⊢ ( 1 ∈ ℝ → ( 0 −ℝ 1 ) ∈ ℝ )
10	8 9	ax-mp	⊢ ( 0 −ℝ 1 ) ∈ ℝ
11	10	recni	⊢ ( 0 −ℝ 1 ) ∈ ℂ
12	6 7 11	adddii	⊢ ( i · ( 1 + ( 0 −ℝ 1 ) ) ) = ( ( i · 1 ) + ( i · ( 0 −ℝ 1 ) ) )
13		renegid	⊢ ( 1 ∈ ℝ → ( 1 + ( 0 −ℝ 1 ) ) = 0 )
14	8 13	ax-mp	⊢ ( 1 + ( 0 −ℝ 1 ) ) = 0
15	14	oveq2i	⊢ ( i · ( 1 + ( 0 −ℝ 1 ) ) ) = ( i · 0 )
16		sn-it0e0	⊢ ( i · 0 ) = 0
17	15 16	eqtri	⊢ ( i · ( 1 + ( 0 −ℝ 1 ) ) ) = 0
18	5 12 17	3eqtr2i	⊢ ( i + ( i · ( i · i ) ) ) = 0