# Metamath Proof Explorer

## Theorem xrsmulgzz

Description: The "multiple" function in the extended real numbers structure. (Contributed by Thierry Arnoux, 14-Jun-2017)

Ref Expression
Assertion xrsmulgzz ${⊢}\left({A}\in ℤ\wedge {B}\in {ℝ}^{*}\right)\to {A}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={A}{\cdot }_{𝑒}{B}$

### Proof

Step Hyp Ref Expression
1 oveq1 ${⊢}{n}=0\to {n}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}=0{\cdot }_{{ℝ}_{𝑠}^{*}}{B}$
2 oveq1 ${⊢}{n}=0\to {n}{\cdot }_{𝑒}{B}=0{\cdot }_{𝑒}{B}$
3 1 2 eqeq12d ${⊢}{n}=0\to \left({n}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={n}{\cdot }_{𝑒}{B}↔0{\cdot }_{{ℝ}_{𝑠}^{*}}{B}=0{\cdot }_{𝑒}{B}\right)$
4 oveq1 ${⊢}{n}={m}\to {n}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}$
5 oveq1 ${⊢}{n}={m}\to {n}{\cdot }_{𝑒}{B}={m}{\cdot }_{𝑒}{B}$
6 4 5 eqeq12d ${⊢}{n}={m}\to \left({n}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={n}{\cdot }_{𝑒}{B}↔{m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)$
7 oveq1 ${⊢}{n}={m}+1\to {n}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}$
8 oveq1 ${⊢}{n}={m}+1\to {n}{\cdot }_{𝑒}{B}=\left({m}+1\right){\cdot }_{𝑒}{B}$
9 7 8 eqeq12d ${⊢}{n}={m}+1\to \left({n}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={n}{\cdot }_{𝑒}{B}↔\left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left({m}+1\right){\cdot }_{𝑒}{B}\right)$
10 oveq1 ${⊢}{n}=-{m}\to {n}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left(-{m}\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}$
11 oveq1 ${⊢}{n}=-{m}\to {n}{\cdot }_{𝑒}{B}=\left(-{m}\right){\cdot }_{𝑒}{B}$
12 10 11 eqeq12d ${⊢}{n}=-{m}\to \left({n}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={n}{\cdot }_{𝑒}{B}↔\left(-{m}\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left(-{m}\right){\cdot }_{𝑒}{B}\right)$
13 oveq1 ${⊢}{n}={A}\to {n}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={A}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}$
14 oveq1 ${⊢}{n}={A}\to {n}{\cdot }_{𝑒}{B}={A}{\cdot }_{𝑒}{B}$
15 13 14 eqeq12d ${⊢}{n}={A}\to \left({n}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={n}{\cdot }_{𝑒}{B}↔{A}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={A}{\cdot }_{𝑒}{B}\right)$
16 xrsbas ${⊢}{ℝ}^{*}={\mathrm{Base}}_{{ℝ}_{𝑠}^{*}}$
17 xrs0 ${⊢}0={0}_{{ℝ}_{𝑠}^{*}}$
18 eqid ${⊢}{\cdot }_{{ℝ}_{𝑠}^{*}}={\cdot }_{{ℝ}_{𝑠}^{*}}$
19 16 17 18 mulg0 ${⊢}{B}\in {ℝ}^{*}\to 0{\cdot }_{{ℝ}_{𝑠}^{*}}{B}=0$
20 xmul02 ${⊢}{B}\in {ℝ}^{*}\to 0{\cdot }_{𝑒}{B}=0$
21 19 20 eqtr4d ${⊢}{B}\in {ℝ}^{*}\to 0{\cdot }_{{ℝ}_{𝑠}^{*}}{B}=0{\cdot }_{𝑒}{B}$
22 simpr ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}$
23 22 oveq1d ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to \left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right){+}_{𝑒}{B}=\left({m}{\cdot }_{𝑒}{B}\right){+}_{𝑒}{B}$
24 simpr ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}\in ℕ\right)\to {m}\in ℕ$
25 simpll ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}\in ℕ\right)\to {B}\in {ℝ}^{*}$
26 xrsadd ${⊢}{+}_{𝑒}={+}_{{ℝ}_{𝑠}^{*}}$
27 16 18 26 mulgnnp1 ${⊢}\left({m}\in ℕ\wedge {B}\in {ℝ}^{*}\right)\to \left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right){+}_{𝑒}{B}$
28 24 25 27 syl2anc ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}\in ℕ\right)\to \left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right){+}_{𝑒}{B}$
29 simpr ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}=0\right)\to {m}=0$
30 simpll ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}=0\right)\to {B}\in {ℝ}^{*}$
31 xaddid2 ${⊢}{B}\in {ℝ}^{*}\to 0{+}_{𝑒}{B}={B}$
32 31 adantl ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to 0{+}_{𝑒}{B}={B}$
33 simpl ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to {m}=0$
34 33 oveq1d ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}=0{\cdot }_{{ℝ}_{𝑠}^{*}}{B}$
35 19 adantl ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to 0{\cdot }_{{ℝ}_{𝑠}^{*}}{B}=0$
36 34 35 eqtrd ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}=0$
37 36 oveq1d ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to \left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right){+}_{𝑒}{B}=0{+}_{𝑒}{B}$
38 33 oveq1d ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to {m}+1=0+1$
39 0p1e1 ${⊢}0+1=1$
40 38 39 syl6eq ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to {m}+1=1$
41 40 oveq1d ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to \left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=1{\cdot }_{{ℝ}_{𝑠}^{*}}{B}$
42 16 18 mulg1 ${⊢}{B}\in {ℝ}^{*}\to 1{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={B}$
43 42 adantl ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to 1{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={B}$
44 41 43 eqtrd ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to \left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}={B}$
45 32 37 44 3eqtr4rd ${⊢}\left({m}=0\wedge {B}\in {ℝ}^{*}\right)\to \left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right){+}_{𝑒}{B}$
46 29 30 45 syl2anc ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}=0\right)\to \left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right){+}_{𝑒}{B}$
47 simpr ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\to {m}\in {ℕ}_{0}$
48 elnn0 ${⊢}{m}\in {ℕ}_{0}↔\left({m}\in ℕ\vee {m}=0\right)$
49 47 48 sylib ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\to \left({m}\in ℕ\vee {m}=0\right)$
50 28 46 49 mpjaodan ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\to \left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right){+}_{𝑒}{B}$
51 50 adantr ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to \left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right){+}_{𝑒}{B}$
52 nn0ssre ${⊢}{ℕ}_{0}\subseteq ℝ$
53 ressxr ${⊢}ℝ\subseteq {ℝ}^{*}$
54 52 53 sstri ${⊢}{ℕ}_{0}\subseteq {ℝ}^{*}$
55 47 adantr ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to {m}\in {ℕ}_{0}$
56 54 55 sseldi ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to {m}\in {ℝ}^{*}$
57 nn0ge0 ${⊢}{m}\in {ℕ}_{0}\to 0\le {m}$
58 57 ad2antlr ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to 0\le {m}$
59 1xr ${⊢}1\in {ℝ}^{*}$
60 59 a1i ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to 1\in {ℝ}^{*}$
61 0le1 ${⊢}0\le 1$
62 61 a1i ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to 0\le 1$
63 simpll ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to {B}\in {ℝ}^{*}$
64 xadddi2r ${⊢}\left(\left({m}\in {ℝ}^{*}\wedge 0\le {m}\right)\wedge \left(1\in {ℝ}^{*}\wedge 0\le 1\right)\wedge {B}\in {ℝ}^{*}\right)\to \left({m}{+}_{𝑒}1\right){\cdot }_{𝑒}{B}=\left({m}{\cdot }_{𝑒}{B}\right){+}_{𝑒}\left(1{\cdot }_{𝑒}{B}\right)$
65 56 58 60 62 63 64 syl221anc ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to \left({m}{+}_{𝑒}1\right){\cdot }_{𝑒}{B}=\left({m}{\cdot }_{𝑒}{B}\right){+}_{𝑒}\left(1{\cdot }_{𝑒}{B}\right)$
66 52 55 sseldi ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to {m}\in ℝ$
67 1re ${⊢}1\in ℝ$
68 67 a1i ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to 1\in ℝ$
69 rexadd ${⊢}\left({m}\in ℝ\wedge 1\in ℝ\right)\to {m}{+}_{𝑒}1={m}+1$
70 66 68 69 syl2anc ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to {m}{+}_{𝑒}1={m}+1$
71 70 oveq1d ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to \left({m}{+}_{𝑒}1\right){\cdot }_{𝑒}{B}=\left({m}+1\right){\cdot }_{𝑒}{B}$
72 xmulid2 ${⊢}{B}\in {ℝ}^{*}\to 1{\cdot }_{𝑒}{B}={B}$
73 63 72 syl ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to 1{\cdot }_{𝑒}{B}={B}$
74 73 oveq2d ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to \left({m}{\cdot }_{𝑒}{B}\right){+}_{𝑒}\left(1{\cdot }_{𝑒}{B}\right)=\left({m}{\cdot }_{𝑒}{B}\right){+}_{𝑒}{B}$
75 65 71 74 3eqtr3d ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to \left({m}+1\right){\cdot }_{𝑒}{B}=\left({m}{\cdot }_{𝑒}{B}\right){+}_{𝑒}{B}$
76 23 51 75 3eqtr4d ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in {ℕ}_{0}\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to \left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left({m}+1\right){\cdot }_{𝑒}{B}$
77 76 exp31 ${⊢}{B}\in {ℝ}^{*}\to \left({m}\in {ℕ}_{0}\to \left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\to \left({m}+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left({m}+1\right){\cdot }_{𝑒}{B}\right)\right)$
78 xnegeq ${⊢}{m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\to -\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right)=-\left({m}{\cdot }_{𝑒}{B}\right)$
79 78 adantl ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to -\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right)=-\left({m}{\cdot }_{𝑒}{B}\right)$
80 eqid ${⊢}{inv}_{g}\left({ℝ}_{𝑠}^{*}\right)={inv}_{g}\left({ℝ}_{𝑠}^{*}\right)$
81 16 18 80 mulgnegnn ${⊢}\left({m}\in ℕ\wedge {B}\in {ℝ}^{*}\right)\to \left(-{m}\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}={inv}_{g}\left({ℝ}_{𝑠}^{*}\right)\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right)$
82 81 ancoms ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to \left(-{m}\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}={inv}_{g}\left({ℝ}_{𝑠}^{*}\right)\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right)$
83 xrsex ${⊢}{ℝ}_{𝑠}^{*}\in \mathrm{V}$
84 83 a1i ${⊢}{m}\in ℕ\to {ℝ}_{𝑠}^{*}\in \mathrm{V}$
85 ssidd ${⊢}{m}\in ℕ\to {ℝ}^{*}\subseteq {ℝ}^{*}$
86 simp2 ${⊢}\left({m}\in ℕ\wedge {x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to {x}\in {ℝ}^{*}$
87 simp3 ${⊢}\left({m}\in ℕ\wedge {x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to {y}\in {ℝ}^{*}$
88 86 87 xaddcld ${⊢}\left({m}\in ℕ\wedge {x}\in {ℝ}^{*}\wedge {y}\in {ℝ}^{*}\right)\to {x}{+}_{𝑒}{y}\in {ℝ}^{*}$
89 16 18 26 84 85 88 mulgnnsubcl ${⊢}\left({m}\in ℕ\wedge {m}\in ℕ\wedge {B}\in {ℝ}^{*}\right)\to {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\in {ℝ}^{*}$
90 89 3anidm12 ${⊢}\left({m}\in ℕ\wedge {B}\in {ℝ}^{*}\right)\to {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\in {ℝ}^{*}$
91 90 ancoms ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\in {ℝ}^{*}$
92 xrsinvgval ${⊢}{m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\in {ℝ}^{*}\to {inv}_{g}\left({ℝ}_{𝑠}^{*}\right)\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right)=-\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right)$
93 91 92 syl ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to {inv}_{g}\left({ℝ}_{𝑠}^{*}\right)\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right)=-\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right)$
94 82 93 eqtrd ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to \left(-{m}\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=-\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right)$
95 94 adantr ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to \left(-{m}\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=-\left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}\right)$
96 nnre ${⊢}{m}\in ℕ\to {m}\in ℝ$
97 96 adantl ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to {m}\in ℝ$
98 rexneg ${⊢}{m}\in ℝ\to -{m}=-{m}$
99 97 98 syl ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to -{m}=-{m}$
100 99 oveq1d ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to \left(-{m}\right){\cdot }_{𝑒}{B}=\left(-{m}\right){\cdot }_{𝑒}{B}$
101 nnssre ${⊢}ℕ\subseteq ℝ$
102 101 53 sstri ${⊢}ℕ\subseteq {ℝ}^{*}$
103 simpr ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to {m}\in ℕ$
104 102 103 sseldi ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to {m}\in {ℝ}^{*}$
105 simpl ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to {B}\in {ℝ}^{*}$
106 xmulneg1 ${⊢}\left({m}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(-{m}\right){\cdot }_{𝑒}{B}=-\left({m}{\cdot }_{𝑒}{B}\right)$
107 104 105 106 syl2anc ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to \left(-{m}\right){\cdot }_{𝑒}{B}=-\left({m}{\cdot }_{𝑒}{B}\right)$
108 100 107 eqtr3d ${⊢}\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\to \left(-{m}\right){\cdot }_{𝑒}{B}=-\left({m}{\cdot }_{𝑒}{B}\right)$
109 108 adantr ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to \left(-{m}\right){\cdot }_{𝑒}{B}=-\left({m}{\cdot }_{𝑒}{B}\right)$
110 79 95 109 3eqtr4d ${⊢}\left(\left({B}\in {ℝ}^{*}\wedge {m}\in ℕ\right)\wedge {m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\right)\to \left(-{m}\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left(-{m}\right){\cdot }_{𝑒}{B}$
111 110 exp31 ${⊢}{B}\in {ℝ}^{*}\to \left({m}\in ℕ\to \left({m}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={m}{\cdot }_{𝑒}{B}\to \left(-{m}\right){\cdot }_{{ℝ}_{𝑠}^{*}}{B}=\left(-{m}\right){\cdot }_{𝑒}{B}\right)\right)$
112 3 6 9 12 15 21 77 111 zindd ${⊢}{B}\in {ℝ}^{*}\to \left({A}\in ℤ\to {A}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={A}{\cdot }_{𝑒}{B}\right)$
113 112 impcom ${⊢}\left({A}\in ℤ\wedge {B}\in {ℝ}^{*}\right)\to {A}{\cdot }_{{ℝ}_{𝑠}^{*}}{B}={A}{\cdot }_{𝑒}{B}$