Step |
Hyp |
Ref |
Expression |
1 |
|
ax-i2m1 |
⊢ ( ( i · i ) + 1 ) = 0 |
2 |
|
1re |
⊢ 1 ∈ ℝ |
3 |
|
renegid2 |
⊢ ( 1 ∈ ℝ → ( ( 0 −ℝ 1 ) + 1 ) = 0 ) |
4 |
2 3
|
ax-mp |
⊢ ( ( 0 −ℝ 1 ) + 1 ) = 0 |
5 |
1 4
|
eqtr4i |
⊢ ( ( i · i ) + 1 ) = ( ( 0 −ℝ 1 ) + 1 ) |
6 |
|
ax-icn |
⊢ i ∈ ℂ |
7 |
6 6
|
mulcli |
⊢ ( i · i ) ∈ ℂ |
8 |
7
|
a1i |
⊢ ( ⊤ → ( i · i ) ∈ ℂ ) |
9 |
|
rernegcl |
⊢ ( 1 ∈ ℝ → ( 0 −ℝ 1 ) ∈ ℝ ) |
10 |
9
|
recnd |
⊢ ( 1 ∈ ℝ → ( 0 −ℝ 1 ) ∈ ℂ ) |
11 |
2 10
|
mp1i |
⊢ ( ⊤ → ( 0 −ℝ 1 ) ∈ ℂ ) |
12 |
|
1cnd |
⊢ ( ⊤ → 1 ∈ ℂ ) |
13 |
8 11 12
|
sn-addcan2d |
⊢ ( ⊤ → ( ( ( i · i ) + 1 ) = ( ( 0 −ℝ 1 ) + 1 ) ↔ ( i · i ) = ( 0 −ℝ 1 ) ) ) |
14 |
5 13
|
mpbii |
⊢ ( ⊤ → ( i · i ) = ( 0 −ℝ 1 ) ) |
15 |
14
|
mptru |
⊢ ( i · i ) = ( 0 −ℝ 1 ) |