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

Metamath Proof Explorer

Theorem re1m1e0m0

Description: Equality of two left-additive identities. See resubidaddlid . Uses ax-i2m1 . (Contributed by SN, 25-Dec-2023)

Ref Expression
Assertion re1m1e0m0 ( 1 −ℝ 1 ) = ( 0 −ℝ 0 )

Proof

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 )