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 ) ) = ( 𝐴 −ℝ 𝐴 ) )