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 e. ZZ /\ B e. RR* ) -> ( A ( .g ` RR*s ) B ) = ( A *e B ) )

Proof

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