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

Metamath Proof Explorer

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 sn-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