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

Metamath Proof Explorer

Theorem sn-00idlem1

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

Ref Expression
Assertion sn-00idlem1 ⊢ A ∈ ℝ → A ⁢ 0 - ℝ 0 = A - ℝ A

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 resubdi ⊢ A ∈ ℝ ∧ 1 ∈ ℝ ∧ 1 ∈ ℝ → A ⁢ 1 - ℝ 1 = A ⋅ 1 - ℝ A ⋅ 1
3 1 1 2 mp3an23 ⊢ A ∈ ℝ → A ⁢ 1 - ℝ 1 = A ⋅ 1 - ℝ A ⋅ 1
4 re1m1e0m0 ⊢ 1 - ℝ 1 = 0 - ℝ 0
5 4 oveq2i ⊢ A ⁢ 1 - ℝ 1 = A ⁢ 0 - ℝ 0
6 5 a1i ⊢ A ∈ ℝ → A ⁢ 1 - ℝ 1 = A ⁢ 0 - ℝ 0
7 ax-1rid ⊢ A ∈ ℝ → A ⋅ 1 = A
8 7 7 oveq12d ⊢ A ∈ ℝ → A ⋅ 1 - ℝ A ⋅ 1 = A - ℝ A
9 3 6 8 3eqtr3d ⊢ A ∈ ℝ → A ⁢ 0 - ℝ 0 = A - ℝ A