Metamath Proof Explorer


Theorem sn-00idlem3

Description: Lemma for sn-00id . (Contributed by SN, 25-Dec-2023)

Ref Expression
Assertion sn-00idlem3 0 - 0 = 1 0 + 0 = 0

Proof

Step Hyp Ref Expression
1 oveq2 0 - 0 = 1 0 0 - 0 = 0 1
2 1 oveq1d 0 - 0 = 1 0 0 - 0 + 0 = 0 1 + 0
3 0re 0
4 sn-00idlem1 0 0 0 - 0 = 0 - 0
5 4 adantr 0 0 0 0 - 0 = 0 - 0
6 5 oveq1d 0 0 0 0 - 0 + 0 = 0 - 0 + 0
7 resubidaddid1 0 0 0 - 0 + 0 = 0
8 6 7 eqtrd 0 0 0 0 - 0 + 0 = 0
9 3 3 8 mp2an 0 0 - 0 + 0 = 0
10 9 a1i 0 - 0 = 1 0 0 - 0 + 0 = 0
11 ax-1rid 0 0 1 = 0
12 3 11 mp1i 0 - 0 = 1 0 1 = 0
13 12 oveq1d 0 - 0 = 1 0 1 + 0 = 0 + 0
14 2 10 13 3eqtr3rd 0 - 0 = 1 0 + 0 = 0