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 ( 𝐴 ∈ ℝ → ( 𝐴 · ( 0 −ℝ 0 ) ) = ( 𝐴 −ℝ 𝐴 ) )

Proof

Step Hyp Ref Expression
1 1re ⊢ 1 ∈ ℝ
2 resubdi ⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 · ( 1 −ℝ 1 ) ) = ( ( 𝐴 · 1 ) −ℝ ( 𝐴 · 1 ) ) )
3 1 1 2 mp3an23 ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · ( 1 −ℝ 1 ) ) = ( ( 𝐴 · 1 ) −ℝ ( 𝐴 · 1 ) ) )
4 re1m1e0m0 ⊢ ( 1 −ℝ 1 ) = ( 0 −ℝ 0 )
5 4 oveq2i ⊢ ( 𝐴 · ( 1 −ℝ 1 ) ) = ( 𝐴 · ( 0 −ℝ 0 ) )
6 5 a1i ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · ( 1 −ℝ 1 ) ) = ( 𝐴 · ( 0 −ℝ 0 ) ) )
7 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
8 7 7 oveq12d ⊢ ( 𝐴 ∈ ℝ → ( ( 𝐴 · 1 ) −ℝ ( 𝐴 · 1 ) ) = ( 𝐴 −ℝ 𝐴 ) )
9 3 6 8 3eqtr3d ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · ( 0 −ℝ 0 ) ) = ( 𝐴 −ℝ 𝐴 ) )