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

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 0re ⊢ 0 ∈ ℝ
3 sn-00idlem1 ⊢ 0 ∈ ℝ → 0 ⋅ 0 - ℝ 0 = 0 - ℝ 0
4 2 3 ax-mp ⊢ 0 ⋅ 0 - ℝ 0 = 0 - ℝ 0
5 ax-1rid ⊢ 0 ∈ ℝ → 0 ⋅ 1 = 0
6 2 5 ax-mp ⊢ 0 ⋅ 1 = 0
7 1 4 6 3eqtr3g ⊢ 0 - ℝ 0 = 1 → 0 - ℝ 0 = 0
8 7 oveq1d ⊢ 0 - ℝ 0 = 1 → 0 - ℝ 0 + 0 = 0 + 0
9 resubidaddlid ⊢ 0 ∈ ℝ ∧ 0 ∈ ℝ → 0 - ℝ 0 + 0 = 0
10 2 2 9 mp2an ⊢ 0 - ℝ 0 + 0 = 0
11 8 10 eqtr3di ⊢ 0 - ℝ 0 = 1 → 0 + 0 = 0