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