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 \mathbb{Z}\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\leftrightarrow 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\leftrightarrow 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\leftrightarrow \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\leftrightarrow \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\leftrightarrow 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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_0\right)\wedge m\in \mathbb{N}\right)\to m\in \mathbb{N}$$
25		simpll	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_0\right)\wedge m\in \mathbb{N}\right)\to B\in {ℝ}^{*}$$
26		xrsadd	$$⊢{+}_{𝑒}={+}_{{ℝ}_{𝑠}^{*}}$$
27	16 18 26	mulgnnp1	$$⊢\left(m\in \mathbb{N}\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 {\mathbb{N}}_0\right)\wedge m\in \mathbb{N}\right)\to \left(m+1\right){\cdot }_{{ℝ}_{𝑠}^{*}}B=\left(m{\cdot }_{{ℝ}_{𝑠}^{*}}B\right){+}_{𝑒}B$$
29		simpr	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_0\right)\wedge m=0\right)\to m=0$$
30		simpll	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_0\right)\wedge m=0\right)\to B\in {ℝ}^{*}$$
31		xaddlid	$$⊢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	eqtrdi	$$⊢\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 {\mathbb{N}}_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 {\mathbb{N}}_0\right)\to m\in {\mathbb{N}}_0$$
48		elnn0	$$⊢m\in {\mathbb{N}}_0\leftrightarrow \left(m\in \mathbb{N}\vee m=0\right)$$
49	47 48	sylib	$$⊢\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_0\right)\to \left(m\in \mathbb{N}\vee m=0\right)$$
50	28 46 49	mpjaodan	$$⊢\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_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 {\mathbb{N}}_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	$$⊢{\mathbb{N}}_0\subseteq ℝ$$
53		ressxr	$$⊢ℝ\subseteq {ℝ}^{*}$$
54	52 53	sstri	$$⊢{\mathbb{N}}_0\subseteq {ℝ}^{*}$$
55	47	adantr	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_0\right)\wedge m{\cdot }_{{ℝ}_{𝑠}^{*}}B=m{\cdot }_{𝑒}B\right)\to m\in {\mathbb{N}}_0$$
56	54 55	sselid	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_0\right)\wedge m{\cdot }_{{ℝ}_{𝑠}^{*}}B=m{\cdot }_{𝑒}B\right)\to m\in {ℝ}^{*}$$
57		nn0ge0	$$⊢m\in {\mathbb{N}}_0\to 0\le m$$
58	57	ad2antlr	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_0\right)\wedge m{\cdot }_{{ℝ}_{𝑠}^{*}}B=m{\cdot }_{𝑒}B\right)\to 0\le 1$$
63		simpll	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_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 {\mathbb{N}}_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	sselid	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_0\right)\wedge m{\cdot }_{{ℝ}_{𝑠}^{*}}B=m{\cdot }_{𝑒}B\right)\to \left(m{+}_{𝑒}1\right){\cdot }_{𝑒}B=\left(m+1\right){\cdot }_{𝑒}B$$
72		xmullid	$$⊢B\in {ℝ}^{*}\to 1{\cdot }_{𝑒}B=B$$
73	63 72	syl	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_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 {\mathbb{N}}_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 \mathbb{N}\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 \mathbb{N}\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 \mathbb{N}\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 \mathbb{N}\to {ℝ}_{𝑠}^{*}\in \mathrm{V}$$
85		ssidd	$$⊢m\in \mathbb{N}\to {ℝ}^{*}\subseteq {ℝ}^{*}$$
86		simp2	$$⊢\left(m\in \mathbb{N}\wedge x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to x\in {ℝ}^{*}$$
87		simp3	$$⊢\left(m\in \mathbb{N}\wedge x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to y\in {ℝ}^{*}$$
88	86 87	xaddcld	$$⊢\left(m\in \mathbb{N}\wedge x\in {ℝ}^{*}\wedge y\in {ℝ}^{*}\right)\to x{+}_{𝑒}y\in {ℝ}^{*}$$
89	16 18 26 84 85 88	mulgnnsubcl	$$⊢\left(m\in \mathbb{N}\wedge m\in \mathbb{N}\wedge B\in {ℝ}^{*}\right)\to m{\cdot }_{{ℝ}_{𝑠}^{*}}B\in {ℝ}^{*}$$
90	89	3anidm12	$$⊢\left(m\in \mathbb{N}\wedge B\in {ℝ}^{*}\right)\to m{\cdot }_{{ℝ}_{𝑠}^{*}}B\in {ℝ}^{*}$$
91	90	ancoms	$$⊢\left(B\in {ℝ}^{*}\wedge m\in \mathbb{N}\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 \mathbb{N}\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 \mathbb{N}\right)\to \left(-m\right){\cdot }_{{ℝ}_{𝑠}^{*}}B=-\left(m{\cdot }_{{ℝ}_{𝑠}^{*}}B\right)$$
95	94	adantr	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in \mathbb{N}\right)\wedge m{\cdot }_{{ℝ}_{𝑠}^{*}}B=m{\cdot }_{𝑒}B\right)\to \left(-m\right){\cdot }_{{ℝ}_{𝑠}^{*}}B=-\left(m{\cdot }_{{ℝ}_{𝑠}^{*}}B\right)$$
96		nnre	$$⊢m\in \mathbb{N}\to m\in ℝ$$
97	96	adantl	$$⊢\left(B\in {ℝ}^{*}\wedge m\in \mathbb{N}\right)\to m\in ℝ$$
98		rexneg	$$⊢m\in ℝ\to -m=-m$$
99	97 98	syl	$$⊢\left(B\in {ℝ}^{*}\wedge m\in \mathbb{N}\right)\to -m=-m$$
100	99	oveq1d	$$⊢\left(B\in {ℝ}^{*}\wedge m\in \mathbb{N}\right)\to \left(-m\right){\cdot }_{𝑒}B=\left(-m\right){\cdot }_{𝑒}B$$
101		nnssre	$$⊢\mathbb{N}\subseteq ℝ$$
102	101 53	sstri	$$⊢\mathbb{N}\subseteq {ℝ}^{*}$$
103		simpr	$$⊢\left(B\in {ℝ}^{*}\wedge m\in \mathbb{N}\right)\to m\in \mathbb{N}$$
104	102 103	sselid	$$⊢\left(B\in {ℝ}^{*}\wedge m\in \mathbb{N}\right)\to m\in {ℝ}^{*}$$
105		simpl	$$⊢\left(B\in {ℝ}^{*}\wedge m\in \mathbb{N}\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 \mathbb{N}\right)\to \left(-m\right){\cdot }_{𝑒}B=-\left(m{\cdot }_{𝑒}B\right)$$
108	100 107	eqtr3d	$$⊢\left(B\in {ℝ}^{*}\wedge m\in \mathbb{N}\right)\to \left(-m\right){\cdot }_{𝑒}B=-\left(m{\cdot }_{𝑒}B\right)$$
109	108	adantr	$$⊢\left(\left(B\in {ℝ}^{*}\wedge m\in \mathbb{N}\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 \mathbb{N}\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 \mathbb{N}\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 \mathbb{Z}\to A{\cdot }_{{ℝ}_{𝑠}^{*}}B=A{\cdot }_{𝑒}B\right)$$
113	112	impcom	$$⊢\left(A\in \mathbb{Z}\wedge B\in {ℝ}^{*}\right)\to A{\cdot }_{{ℝ}_{𝑠}^{*}}B=A{\cdot }_{𝑒}B$$