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 ) ) |