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 A B * A 𝑠 * B = A 𝑒 B

Proof

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