Metamath Proof Explorer


Theorem re1m1e0m0

Description: Equality of two left-additive identities. See resubidaddid1 . 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 )