Step |
Hyp |
Ref |
Expression |
1 |
|
0red |
⊢ ( ⊤ → 0 ∈ ℝ ) |
2 |
|
1re |
⊢ 1 ∈ ℝ |
3 |
|
rersubcl |
⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 −ℝ 1 ) ∈ ℝ ) |
4 |
2 2 3
|
mp2an |
⊢ ( 1 −ℝ 1 ) ∈ ℝ |
5 |
4
|
a1i |
⊢ ( ⊤ → ( 1 −ℝ 1 ) ∈ ℝ ) |
6 |
|
ax-icn |
⊢ i ∈ ℂ |
7 |
6 6
|
mulcli |
⊢ ( i · i ) ∈ ℂ |
8 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
9 |
4
|
recni |
⊢ ( 1 −ℝ 1 ) ∈ ℂ |
10 |
7 8 9
|
addassi |
⊢ ( ( ( i · i ) + 1 ) + ( 1 −ℝ 1 ) ) = ( ( i · i ) + ( 1 + ( 1 −ℝ 1 ) ) ) |
11 |
|
repncan3 |
⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 + ( 1 −ℝ 1 ) ) = 1 ) |
12 |
2 2 11
|
mp2an |
⊢ ( 1 + ( 1 −ℝ 1 ) ) = 1 |
13 |
12
|
oveq2i |
⊢ ( ( i · i ) + ( 1 + ( 1 −ℝ 1 ) ) ) = ( ( i · i ) + 1 ) |
14 |
10 13
|
eqtri |
⊢ ( ( ( i · i ) + 1 ) + ( 1 −ℝ 1 ) ) = ( ( i · i ) + 1 ) |
15 |
|
ax-i2m1 |
⊢ ( ( i · i ) + 1 ) = 0 |
16 |
15
|
oveq1i |
⊢ ( ( ( i · i ) + 1 ) + ( 1 −ℝ 1 ) ) = ( 0 + ( 1 −ℝ 1 ) ) |
17 |
14 16 15
|
3eqtr3i |
⊢ ( 0 + ( 1 −ℝ 1 ) ) = 0 |
18 |
17
|
a1i |
⊢ ( ⊤ → ( 0 + ( 1 −ℝ 1 ) ) = 0 ) |
19 |
1 5 18
|
reladdrsub |
⊢ ( ⊤ → ( 1 −ℝ 1 ) = ( 0 −ℝ 0 ) ) |
20 |
19
|
mptru |
⊢ ( 1 −ℝ 1 ) = ( 0 −ℝ 0 ) |