Theorem xrsmulgzz 30667

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

Assertion

Ref	Expression
xrsmulgzz	⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵))

Proof of Theorem xrsmulgzz

Dummy variables 𝑛 𝑚 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 7165	. . . 4 ⊢ (𝑛 = 0 → (𝑛(.g‘ℝ*𝑠)𝐵) = (0(.g‘ℝ*𝑠)𝐵))
2		oveq1 7165	. . . 4 ⊢ (𝑛 = 0 → (𝑛 ·e 𝐵) = (0 ·e 𝐵))
3	1, 2	eqeq12d 2839	. . 3 ⊢ (𝑛 = 0 → ((𝑛(.g‘ℝ*𝑠)𝐵) = (𝑛 ·e 𝐵) ↔ (0(.g‘ℝ*𝑠)𝐵) = (0 ·e 𝐵)))
4		oveq1 7165	. . . 4 ⊢ (𝑛 = 𝑚 → (𝑛(.g‘ℝ*𝑠)𝐵) = (𝑚(.g‘ℝ*𝑠)𝐵))
5		oveq1 7165	. . . 4 ⊢ (𝑛 = 𝑚 → (𝑛 ·e 𝐵) = (𝑚 ·e 𝐵))
6	4, 5	eqeq12d 2839	. . 3 ⊢ (𝑛 = 𝑚 → ((𝑛(.g‘ℝ*𝑠)𝐵) = (𝑛 ·e 𝐵) ↔ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)))
7		oveq1 7165	. . . 4 ⊢ (𝑛 = (𝑚 + 1) → (𝑛(.g‘ℝ*𝑠)𝐵) = ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵))
8		oveq1 7165	. . . 4 ⊢ (𝑛 = (𝑚 + 1) → (𝑛 ·e 𝐵) = ((𝑚 + 1) ·e 𝐵))
9	7, 8	eqeq12d 2839	. . 3 ⊢ (𝑛 = (𝑚 + 1) → ((𝑛(.g‘ℝ*𝑠)𝐵) = (𝑛 ·e 𝐵) ↔ ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚 + 1) ·e 𝐵)))
10		oveq1 7165	. . . 4 ⊢ (𝑛 = -𝑚 → (𝑛(.g‘ℝ*𝑠)𝐵) = (-𝑚(.g‘ℝ*𝑠)𝐵))
11		oveq1 7165	. . . 4 ⊢ (𝑛 = -𝑚 → (𝑛 ·e 𝐵) = (-𝑚 ·e 𝐵))
12	10, 11	eqeq12d 2839	. . 3 ⊢ (𝑛 = -𝑚 → ((𝑛(.g‘ℝ*𝑠)𝐵) = (𝑛 ·e 𝐵) ↔ (-𝑚(.g‘ℝ*𝑠)𝐵) = (-𝑚 ·e 𝐵)))
13		oveq1 7165	. . . 4 ⊢ (𝑛 = 𝐴 → (𝑛(.g‘ℝ*𝑠)𝐵) = (𝐴(.g‘ℝ*𝑠)𝐵))
14		oveq1 7165	. . . 4 ⊢ (𝑛 = 𝐴 → (𝑛 ·e 𝐵) = (𝐴 ·e 𝐵))
15	13, 14	eqeq12d 2839	. . 3 ⊢ (𝑛 = 𝐴 → ((𝑛(.g‘ℝ*𝑠)𝐵) = (𝑛 ·e 𝐵) ↔ (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)))
16		xrsbas 20563	. . . . 5 ⊢ ℝ* = (Base‘ℝ*𝑠)
17		xrs0 30664	. . . . 5 ⊢ 0 = (0g‘ℝ*𝑠)
18		eqid 2823	. . . . 5 ⊢ (.g‘ℝ*𝑠) = (.g‘ℝ*𝑠)
19	16, 17, 18	mulg0 18233	. . . 4 ⊢ (𝐵 ∈ ℝ* → (0(.g‘ℝ*𝑠)𝐵) = 0)
20		xmul02 12664	. . . 4 ⊢ (𝐵 ∈ ℝ* → (0 ·e 𝐵) = 0)
21	19, 20	eqtr4d 2861	. . 3 ⊢ (𝐵 ∈ ℝ* → (0(.g‘ℝ*𝑠)𝐵) = (0 ·e 𝐵))
22		simpr 487	. . . . . 6 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵))
23	22	oveq1d 7173	. . . . 5 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵) = ((𝑚 ·e 𝐵) +𝑒 𝐵))
24		simpr 487	. . . . . . . 8 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
25		simpll 765	. . . . . . . 8 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ∈ ℕ) → 𝐵 ∈ ℝ*)
26		xrsadd 20564	. . . . . . . . 9 ⊢ +𝑒 = (+g‘ℝ*𝑠)
27	16, 18, 26	mulgnnp1 18238	. . . . . . . 8 ⊢ ((𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ*) → ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵))
28	24, 25, 27	syl2anc 586	. . . . . . 7 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵))
29		simpr 487	. . . . . . . 8 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 0) → 𝑚 = 0)
30		simpll 765	. . . . . . . 8 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 0) → 𝐵 ∈ ℝ*)
31		xaddid2 12638	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ* → (0 +𝑒 𝐵) = 𝐵)
32	31	adantl 484	. . . . . . . . 9 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (0 +𝑒 𝐵) = 𝐵)
33		simpl 485	. . . . . . . . . . . 12 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → 𝑚 = 0)
34	33	oveq1d 7173	. . . . . . . . . . 11 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (𝑚(.g‘ℝ*𝑠)𝐵) = (0(.g‘ℝ*𝑠)𝐵))
35	19	adantl 484	. . . . . . . . . . 11 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (0(.g‘ℝ*𝑠)𝐵) = 0)
36	34, 35	eqtrd 2858	. . . . . . . . . 10 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (𝑚(.g‘ℝ*𝑠)𝐵) = 0)
37	36	oveq1d 7173	. . . . . . . . 9 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵) = (0 +𝑒 𝐵))
38	33	oveq1d 7173	. . . . . . . . . . . 12 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (𝑚 + 1) = (0 + 1))
39		0p1e1 11762	. . . . . . . . . . . 12 ⊢ (0 + 1) = 1
40	38, 39	syl6eq 2874	. . . . . . . . . . 11 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (𝑚 + 1) = 1)
41	40	oveq1d 7173	. . . . . . . . . 10 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = (1(.g‘ℝ*𝑠)𝐵))
42	16, 18	mulg1 18237	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ* → (1(.g‘ℝ*𝑠)𝐵) = 𝐵)
43	42	adantl 484	. . . . . . . . . 10 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (1(.g‘ℝ*𝑠)𝐵) = 𝐵)
44	41, 43	eqtrd 2858	. . . . . . . . 9 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = 𝐵)
45	32, 37, 44	3eqtr4rd 2869	. . . . . . . 8 ⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵))
46	29, 30, 45	syl2anc 586	. . . . . . 7 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 0) → ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵))
47		simpr 487	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈ ℕ0)
48		elnn0 11902	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ0 ↔ (𝑚 ∈ ℕ ∨ 𝑚 = 0))
49	47, 48	sylib 220	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) → (𝑚 ∈ ℕ ∨ 𝑚 = 0))
50	28, 46, 49	mpjaodan 955	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) → ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵))
51	50	adantr 483	. . . . 5 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵))
52		nn0ssre 11904	. . . . . . . . 9 ⊢ ℕ0 ⊆ ℝ
53		ressxr 10687	. . . . . . . . 9 ⊢ ℝ ⊆ ℝ*
54	52, 53	sstri 3978	. . . . . . . 8 ⊢ ℕ0 ⊆ ℝ*
55	47	adantr 483	. . . . . . . 8 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 𝑚 ∈ ℕ0)
56	54, 55	sseldi 3967	. . . . . . 7 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 𝑚 ∈ ℝ*)
57		nn0ge0 11925	. . . . . . . 8 ⊢ (𝑚 ∈ ℕ0 → 0 ≤ 𝑚)
58	57	ad2antlr 725	. . . . . . 7 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 0 ≤ 𝑚)
59		1xr 10702	. . . . . . . 8 ⊢ 1 ∈ ℝ*
60	59	a1i 11	. . . . . . 7 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 1 ∈ ℝ*)
61		0le1 11165	. . . . . . . 8 ⊢ 0 ≤ 1
62	61	a1i 11	. . . . . . 7 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 0 ≤ 1)
63		simpll 765	. . . . . . 7 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 𝐵 ∈ ℝ*)
64		xadddi2r 12694	. . . . . . 7 ⊢ (((𝑚 ∈ ℝ* ∧ 0 ≤ 𝑚) ∧ (1 ∈ ℝ* ∧ 0 ≤ 1) ∧ 𝐵 ∈ ℝ*) → ((𝑚 +𝑒 1) ·e 𝐵) = ((𝑚 ·e 𝐵) +𝑒 (1 ·e 𝐵)))
65	56, 58, 60, 62, 63, 64	syl221anc 1377	. . . . . 6 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚 +𝑒 1) ·e 𝐵) = ((𝑚 ·e 𝐵) +𝑒 (1 ·e 𝐵)))
66	52, 55	sseldi 3967	. . . . . . . 8 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 𝑚 ∈ ℝ)
67		1re 10643	. . . . . . . . 9 ⊢ 1 ∈ ℝ
68	67	a1i 11	. . . . . . . 8 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 1 ∈ ℝ)
69		rexadd 12628	. . . . . . . 8 ⊢ ((𝑚 ∈ ℝ ∧ 1 ∈ ℝ) → (𝑚 +𝑒 1) = (𝑚 + 1))
70	66, 68, 69	syl2anc 586	. . . . . . 7 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (𝑚 +𝑒 1) = (𝑚 + 1))
71	70	oveq1d 7173	. . . . . 6 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚 +𝑒 1) ·e 𝐵) = ((𝑚 + 1) ·e 𝐵))
72		xmulid2 12676	. . . . . . . 8 ⊢ (𝐵 ∈ ℝ* → (1 ·e 𝐵) = 𝐵)
73	63, 72	syl 17	. . . . . . 7 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (1 ·e 𝐵) = 𝐵)
74	73	oveq2d 7174	. . . . . 6 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚 ·e 𝐵) +𝑒 (1 ·e 𝐵)) = ((𝑚 ·e 𝐵) +𝑒 𝐵))
75	65, 71, 74	3eqtr3d 2866	. . . . 5 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚 + 1) ·e 𝐵) = ((𝑚 ·e 𝐵) +𝑒 𝐵))
76	23, 51, 75	3eqtr4d 2868	. . . 4 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚 + 1) ·e 𝐵))
77	76	exp31 422	. . 3 ⊢ (𝐵 ∈ ℝ* → (𝑚 ∈ ℕ0 → ((𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵) → ((𝑚 + 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚 + 1) ·e 𝐵))))
78		xnegeq 12603	. . . . . 6 ⊢ ((𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵) → -𝑒(𝑚(.g‘ℝ*𝑠)𝐵) = -𝑒(𝑚 ·e 𝐵))
79	78	adantl 484	. . . . 5 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → -𝑒(𝑚(.g‘ℝ*𝑠)𝐵) = -𝑒(𝑚 ·e 𝐵))
80		eqid 2823	. . . . . . . . 9 ⊢ (invg‘ℝ*𝑠) = (invg‘ℝ*𝑠)
81	16, 18, 80	mulgnegnn 18240	. . . . . . . 8 ⊢ ((𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ*) → (-𝑚(.g‘ℝ*𝑠)𝐵) = ((invg‘ℝ*𝑠)‘(𝑚(.g‘ℝ*𝑠)𝐵)))
82	81	ancoms 461	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → (-𝑚(.g‘ℝ*𝑠)𝐵) = ((invg‘ℝ*𝑠)‘(𝑚(.g‘ℝ*𝑠)𝐵)))
83		xrsex 20562	. . . . . . . . . . . 12 ⊢ ℝ*𝑠 ∈ V
84	83	a1i 11	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ → ℝ*𝑠 ∈ V)
85		ssidd 3992	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ℕ → ℝ* ⊆ ℝ*)
86		simp2 1133	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → 𝑥 ∈ ℝ*)
87		simp3 1134	. . . . . . . . . . . 12 ⊢ ((𝑚 ∈ ℕ ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → 𝑦 ∈ ℝ*)
88	86, 87	xaddcld 12697	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ ℕ ∧ 𝑥 ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (𝑥 +𝑒 𝑦) ∈ ℝ*)
89	16, 18, 26, 84, 85, 88	mulgnnsubcl 18242	. . . . . . . . . 10 ⊢ ((𝑚 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ*) → (𝑚(.g‘ℝ*𝑠)𝐵) ∈ ℝ*)
90	89	3anidm12 1415	. . . . . . . . 9 ⊢ ((𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ*) → (𝑚(.g‘ℝ*𝑠)𝐵) ∈ ℝ*)
91	90	ancoms 461	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → (𝑚(.g‘ℝ*𝑠)𝐵) ∈ ℝ*)
92		xrsinvgval 30666	. . . . . . . 8 ⊢ ((𝑚(.g‘ℝ*𝑠)𝐵) ∈ ℝ* → ((invg‘ℝ*𝑠)‘(𝑚(.g‘ℝ*𝑠)𝐵)) = -𝑒(𝑚(.g‘ℝ*𝑠)𝐵))
93	91, 92	syl 17	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → ((invg‘ℝ*𝑠)‘(𝑚(.g‘ℝ*𝑠)𝐵)) = -𝑒(𝑚(.g‘ℝ*𝑠)𝐵))
94	82, 93	eqtrd 2858	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → (-𝑚(.g‘ℝ*𝑠)𝐵) = -𝑒(𝑚(.g‘ℝ*𝑠)𝐵))
95	94	adantr 483	. . . . 5 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (-𝑚(.g‘ℝ*𝑠)𝐵) = -𝑒(𝑚(.g‘ℝ*𝑠)𝐵))
96		nnre 11647	. . . . . . . . . 10 ⊢ (𝑚 ∈ ℕ → 𝑚 ∈ ℝ)
97	96	adantl 484	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ)
98		rexneg 12607	. . . . . . . . 9 ⊢ (𝑚 ∈ ℝ → -𝑒𝑚 = -𝑚)
99	97, 98	syl 17	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → -𝑒𝑚 = -𝑚)
100	99	oveq1d 7173	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → (-𝑒𝑚 ·e 𝐵) = (-𝑚 ·e 𝐵))
101		nnssre 11644	. . . . . . . . . 10 ⊢ ℕ ⊆ ℝ
102	101, 53	sstri 3978	. . . . . . . . 9 ⊢ ℕ ⊆ ℝ*
103		simpr 487	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ)
104	102, 103	sseldi 3967	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℝ*)
105		simpl 485	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → 𝐵 ∈ ℝ*)
106		xmulneg1 12665	. . . . . . . 8 ⊢ ((𝑚 ∈ ℝ* ∧ 𝐵 ∈ ℝ*) → (-𝑒𝑚 ·e 𝐵) = -𝑒(𝑚 ·e 𝐵))
107	104, 105, 106	syl2anc 586	. . . . . . 7 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → (-𝑒𝑚 ·e 𝐵) = -𝑒(𝑚 ·e 𝐵))
108	100, 107	eqtr3d 2860	. . . . . 6 ⊢ ((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) → (-𝑚 ·e 𝐵) = -𝑒(𝑚 ·e 𝐵))
109	108	adantr 483	. . . . 5 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (-𝑚 ·e 𝐵) = -𝑒(𝑚 ·e 𝐵))
110	79, 95, 109	3eqtr4d 2868	. . . 4 ⊢ (((𝐵 ∈ ℝ* ∧ 𝑚 ∈ ℕ) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (-𝑚(.g‘ℝ*𝑠)𝐵) = (-𝑚 ·e 𝐵))
111	110	exp31 422	. . 3 ⊢ (𝐵 ∈ ℝ* → (𝑚 ∈ ℕ → ((𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵) → (-𝑚(.g‘ℝ*𝑠)𝐵) = (-𝑚 ·e 𝐵))))
112	3, 6, 9, 12, 15, 21, 77, 111	zindd 12086	. 2 ⊢ (𝐵 ∈ ℝ* → (𝐴 ∈ ℤ → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)))
113	112	impcom 410	1 ⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*) → (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵))

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114  Vcvv 3496   class class class wbr 5068  ‘cfv 6357  (class class class)co 7158  ℝcr 10538  0cc0 10539  1c1 10540   + caddc 10542  ℝ^*cxr 10676   ≤ cle 10678  -cneg 10873  ℕcn 11640  ℕ₀cn0 11900  ℤcz 11984  -_𝑒cxne 12507   +_𝑒 cxad 12508   ·_e cxmu 12509  ℝ^*_𝑠cxrs 16775  inv_gcminusg 18106  ._gcmg 18226

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pow 5268  ax-pr 5332  ax-un 7463  ax-cnex 10595  ax-resscn 10596  ax-1cn 10597  ax-icn 10598  ax-addcl 10599  ax-addrcl 10600  ax-mulcl 10601  ax-mulrcl 10602  ax-mulcom 10603  ax-addass 10604  ax-mulass 10605  ax-distr 10606  ax-i2m1 10607  ax-1ne0 10608  ax-1rid 10609  ax-rnegex 10610  ax-rrecex 10611  ax-cnre 10612  ax-pre-lttri 10613  ax-pre-lttrn 10614  ax-pre-ltadd 10615  ax-pre-mulgt0 10616

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ne 3019  df-nel 3126  df-ral 3145  df-rex 3146  df-reu 3147  df-rmo 3148  df-rab 3149  df-v 3498  df-sbc 3775  df-csb 3886  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-pss 3956  df-nul 4294  df-if 4470  df-pw 4543  df-sn 4570  df-pr 4572  df-tp 4574  df-op 4576  df-uni 4841  df-int 4879  df-iun 4923  df-br 5069  df-opab 5131  df-mpt 5149  df-tr 5175  df-id 5462  df-eprel 5467  df-po 5476  df-so 5477  df-fr 5516  df-we 5518  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570  df-pred 6150  df-ord 6196  df-on 6197  df-lim 6198  df-suc 6199  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fo 6363  df-f1o 6364  df-fv 6365  df-riota 7116  df-ov 7161  df-oprab 7162  df-mpo 7163  df-om 7583  df-1st 7691  df-2nd 7692  df-wrecs 7949  df-recs 8010  df-rdg 8048  df-1o 8104  df-oadd 8108  df-er 8291  df-en 8512  df-dom 8513  df-sdom 8514  df-fin 8515  df-pnf 10679  df-mnf 10680  df-xr 10681  df-ltxr 10682  df-le 10683  df-sub 10874  df-neg 10875  df-nn 11641  df-2 11703  df-3 11704  df-4 11705  df-5 11706  df-6 11707  df-7 11708  df-8 11709  df-9 11710  df-n0 11901  df-z 11985  df-dec 12102  df-uz 12247  df-xneg 12510  df-xadd 12511  df-xmul 12512  df-fz 12896  df-seq 13373  df-struct 16487  df-ndx 16488  df-slot 16489  df-base 16491  df-plusg 16580  df-mulr 16581  df-tset 16586  df-ple 16587  df-ds 16589  df-0g 16717  df-xrs 16777  df-minusg 18109  df-mulg 18227

This theorem is referenced by:  xrge0mulgnn0  30678  pnfinf  30814