Step | Hyp | Ref
| Expression |
1 | | oveq1 6697 |
. . . 4
⊢ (𝑛 = 0 → (𝑛(.g‘ℝ*𝑠)𝐵) =
(0(.g‘ℝ*𝑠)𝐵)) |
2 | | oveq1 6697 |
. . . 4
⊢ (𝑛 = 0 → (𝑛 ·e 𝐵) = (0 ·e 𝐵)) |
3 | 1, 2 | eqeq12d 2666 |
. . 3
⊢ (𝑛 = 0 → ((𝑛(.g‘ℝ*𝑠)𝐵) = (𝑛 ·e 𝐵) ↔
(0(.g‘ℝ*𝑠)𝐵) = (0 ·e 𝐵))) |
4 | | oveq1 6697 |
. . . 4
⊢ (𝑛 = 𝑚 → (𝑛(.g‘ℝ*𝑠)𝐵) = (𝑚(.g‘ℝ*𝑠)𝐵)) |
5 | | oveq1 6697 |
. . . 4
⊢ (𝑛 = 𝑚 → (𝑛 ·e 𝐵) = (𝑚 ·e 𝐵)) |
6 | 4, 5 | eqeq12d 2666 |
. . 3
⊢ (𝑛 = 𝑚 → ((𝑛(.g‘ℝ*𝑠)𝐵) = (𝑛 ·e 𝐵) ↔ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵))) |
7 | | oveq1 6697 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → (𝑛(.g‘ℝ*𝑠)𝐵) = ((𝑚 +
1)(.g‘ℝ*𝑠)𝐵)) |
8 | | oveq1 6697 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → (𝑛 ·e 𝐵) = ((𝑚 + 1) ·e 𝐵)) |
9 | 7, 8 | eqeq12d 2666 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → ((𝑛(.g‘ℝ*𝑠)𝐵) = (𝑛 ·e 𝐵) ↔ ((𝑚
+ 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚 + 1)
·e 𝐵))) |
10 | | oveq1 6697 |
. . . 4
⊢ (𝑛 = -𝑚 → (𝑛(.g‘ℝ*𝑠)𝐵) = (-𝑚(.g‘ℝ*𝑠)𝐵)) |
11 | | oveq1 6697 |
. . . 4
⊢ (𝑛 = -𝑚 → (𝑛 ·e 𝐵) = (-𝑚 ·e 𝐵)) |
12 | 10, 11 | eqeq12d 2666 |
. . 3
⊢ (𝑛 = -𝑚 → ((𝑛(.g‘ℝ*𝑠)𝐵) = (𝑛 ·e 𝐵) ↔ (-𝑚(.g‘ℝ*𝑠)𝐵) = (-𝑚 ·e 𝐵))) |
13 | | oveq1 6697 |
. . . 4
⊢ (𝑛 = 𝐴 → (𝑛(.g‘ℝ*𝑠)𝐵) = (𝐴(.g‘ℝ*𝑠)𝐵)) |
14 | | oveq1 6697 |
. . . 4
⊢ (𝑛 = 𝐴 → (𝑛 ·e 𝐵) = (𝐴 ·e 𝐵)) |
15 | 13, 14 | eqeq12d 2666 |
. . 3
⊢ (𝑛 = 𝐴 → ((𝑛(.g‘ℝ*𝑠)𝐵) = (𝑛 ·e 𝐵) ↔ (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵))) |
16 | | xrsbas 19810 |
. . . . 5
⊢
ℝ* =
(Base‘ℝ*𝑠) |
17 | | xrs0 29803 |
. . . . 5
⊢ 0 =
(0g‘ℝ*𝑠) |
18 | | eqid 2651 |
. . . . 5
⊢
(.g‘ℝ*𝑠) =
(.g‘ℝ*𝑠) |
19 | 16, 17, 18 | mulg0 17593 |
. . . 4
⊢ (𝐵 ∈ ℝ*
→ (0(.g‘ℝ*𝑠)𝐵) = 0) |
20 | | xmul02 12136 |
. . . 4
⊢ (𝐵 ∈ ℝ*
→ (0 ·e 𝐵) = 0) |
21 | 19, 20 | eqtr4d 2688 |
. . 3
⊢ (𝐵 ∈ ℝ*
→ (0(.g‘ℝ*𝑠)𝐵) = (0 ·e
𝐵)) |
22 | | simpr 476 |
. . . . . 6
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) |
23 | 22 | oveq1d 6705 |
. . . . 5
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵) = ((𝑚
·e 𝐵) +𝑒
𝐵)) |
24 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ 𝑚 ∈ ℕ) → 𝑚 ∈ ℕ) |
25 | | simpll 805 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ 𝑚 ∈ ℕ) → 𝐵 ∈
ℝ*) |
26 | | xrsadd 19811 |
. . . . . . . . 9
⊢
+𝑒 =
(+g‘ℝ*𝑠) |
27 | 16, 18, 26 | mulgnnp1 17596 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ*)
→ ((𝑚 +
1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵)) |
28 | 24, 25, 27 | syl2anc 694 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ 𝑚 ∈ ℕ) → ((𝑚 +
1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵)) |
29 | | simpr 476 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ 𝑚 = 0) → 𝑚 = 0) |
30 | | simpll 805 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ 𝑚 = 0) → 𝐵 ∈
ℝ*) |
31 | | xaddid2 12111 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℝ*
→ (0 +𝑒 𝐵) = 𝐵) |
32 | 31 | adantl 481 |
. . . . . . . . 9
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (0
+𝑒 𝐵) =
𝐵) |
33 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → 𝑚 = 0) |
34 | 33 | oveq1d 6705 |
. . . . . . . . . . 11
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (𝑚(.g‘ℝ*𝑠)𝐵) =
(0(.g‘ℝ*𝑠)𝐵)) |
35 | 19 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) →
(0(.g‘ℝ*𝑠)𝐵) = 0) |
36 | 34, 35 | eqtrd 2685 |
. . . . . . . . . 10
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (𝑚(.g‘ℝ*𝑠)𝐵) = 0) |
37 | 36 | oveq1d 6705 |
. . . . . . . . 9
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵) = (0 +𝑒 𝐵)) |
38 | 33 | oveq1d 6705 |
. . . . . . . . . . . 12
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (𝑚 + 1) = (0 +
1)) |
39 | | 0p1e1 11170 |
. . . . . . . . . . . 12
⊢ (0 + 1) =
1 |
40 | 38, 39 | syl6eq 2701 |
. . . . . . . . . . 11
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → (𝑚 + 1) = 1) |
41 | 40 | oveq1d 6705 |
. . . . . . . . . 10
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → ((𝑚 +
1)(.g‘ℝ*𝑠)𝐵) =
(1(.g‘ℝ*𝑠)𝐵)) |
42 | 16, 18 | mulg1 17595 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ ℝ*
→ (1(.g‘ℝ*𝑠)𝐵) = 𝐵) |
43 | 42 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) →
(1(.g‘ℝ*𝑠)𝐵) = 𝐵) |
44 | 41, 43 | eqtrd 2685 |
. . . . . . . . 9
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → ((𝑚 +
1)(.g‘ℝ*𝑠)𝐵) = 𝐵) |
45 | 32, 37, 44 | 3eqtr4rd 2696 |
. . . . . . . 8
⊢ ((𝑚 = 0 ∧ 𝐵 ∈ ℝ*) → ((𝑚 +
1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵)) |
46 | 29, 30, 45 | syl2anc 694 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ 𝑚 = 0) → ((𝑚 +
1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵)) |
47 | | simpr 476 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) → 𝑚 ∈ ℕ0) |
48 | | elnn0 11332 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
↔ (𝑚 ∈ ℕ
∨ 𝑚 =
0)) |
49 | 47, 48 | sylib 208 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) → (𝑚 ∈ ℕ ∨ 𝑚 = 0)) |
50 | 28, 46, 49 | mpjaodan 844 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) → ((𝑚 +
1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵)) |
51 | 50 | adantr 480 |
. . . . 5
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚
+ 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚(.g‘ℝ*𝑠)𝐵) +𝑒 𝐵)) |
52 | | nn0ssre 11334 |
. . . . . . . . 9
⊢
ℕ0 ⊆ ℝ |
53 | | ressxr 10121 |
. . . . . . . . 9
⊢ ℝ
⊆ ℝ* |
54 | 52, 53 | sstri 3645 |
. . . . . . . 8
⊢
ℕ0 ⊆ ℝ* |
55 | 47 | adantr 480 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 𝑚
∈ ℕ0) |
56 | 54, 55 | sseldi 3634 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 𝑚
∈ ℝ*) |
57 | | nn0ge0 11356 |
. . . . . . . 8
⊢ (𝑚 ∈ ℕ0
→ 0 ≤ 𝑚) |
58 | 57 | ad2antlr 763 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 0 ≤ 𝑚) |
59 | | 1re 10077 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
60 | 59 | rexri 10135 |
. . . . . . . 8
⊢ 1 ∈
ℝ* |
61 | 60 | a1i 11 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 1 ∈ ℝ*) |
62 | | 0le1 10589 |
. . . . . . . 8
⊢ 0 ≤
1 |
63 | 62 | a1i 11 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 0 ≤ 1) |
64 | | simpll 805 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 𝐵
∈ ℝ*) |
65 | | xadddi2r 12166 |
. . . . . . 7
⊢ (((𝑚 ∈ ℝ*
∧ 0 ≤ 𝑚) ∧ (1
∈ ℝ* ∧ 0 ≤ 1) ∧ 𝐵 ∈ ℝ*) → ((𝑚 +𝑒 1)
·e 𝐵) =
((𝑚 ·e
𝐵) +𝑒 (1
·e 𝐵))) |
66 | 56, 58, 61, 63, 64, 65 | syl221anc 1377 |
. . . . . 6
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚
+𝑒 1) ·e 𝐵)
= ((𝑚 ·e 𝐵) +𝑒 (1 ·e 𝐵))) |
67 | 52, 55 | sseldi 3634 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 𝑚
∈ ℝ) |
68 | 59 | a1i 11 |
. . . . . . . 8
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → 1 ∈ ℝ) |
69 | | rexadd 12101 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℝ ∧ 1 ∈
ℝ) → (𝑚
+𝑒 1) = (𝑚 + 1)) |
70 | 67, 68, 69 | syl2anc 694 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (𝑚
+𝑒 1) = (𝑚 +
1)) |
71 | 70 | oveq1d 6705 |
. . . . . 6
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚
+𝑒 1) ·e 𝐵)
= ((𝑚 + 1) ·e 𝐵)) |
72 | | xmulid2 12148 |
. . . . . . . 8
⊢ (𝐵 ∈ ℝ*
→ (1 ·e 𝐵) = 𝐵) |
73 | 64, 72 | syl 17 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (1 ·e 𝐵) = 𝐵) |
74 | 73 | oveq2d 6706 |
. . . . . 6
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚
·e 𝐵) +𝑒 (1
·e 𝐵)) = ((𝑚 ·e 𝐵) +𝑒 𝐵)) |
75 | 66, 71, 74 | 3eqtr3d 2693 |
. . . . 5
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚
+ 1) ·e 𝐵) = ((𝑚 ·e 𝐵) +𝑒 𝐵)) |
76 | 23, 51, 75 | 3eqtr4d 2695 |
. . . 4
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈
ℕ0) ∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → ((𝑚
+ 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚 + 1)
·e 𝐵)) |
77 | 76 | exp31 629 |
. . 3
⊢ (𝐵 ∈ ℝ*
→ (𝑚 ∈
ℕ0 → ((𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵) → ((𝑚
+ 1)(.g‘ℝ*𝑠)𝐵) = ((𝑚 + 1)
·e 𝐵)))) |
78 | | xnegeq 12076 |
. . . . . 6
⊢ ((𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵) → -𝑒(𝑚(.g‘ℝ*𝑠)𝐵) = -𝑒(𝑚 ·e 𝐵)) |
79 | 78 | adantl 481 |
. . . . 5
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → -𝑒(𝑚(.g‘ℝ*𝑠)𝐵) = -𝑒(𝑚 ·e 𝐵)) |
80 | | eqid 2651 |
. . . . . . . . 9
⊢
(invg‘ℝ*𝑠) =
(invg‘ℝ*𝑠) |
81 | 16, 18, 80 | mulgnegnn 17598 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ*)
→ (-𝑚(.g‘ℝ*𝑠)𝐵) =
((invg‘ℝ*𝑠)‘(𝑚(.g‘ℝ*𝑠)𝐵))) |
82 | 81 | ancoms 468 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ (-𝑚(.g‘ℝ*𝑠)𝐵) =
((invg‘ℝ*𝑠)‘(𝑚(.g‘ℝ*𝑠)𝐵))) |
83 | | xrsex 19809 |
. . . . . . . . . . . 12
⊢
ℝ*𝑠 ∈ V |
84 | 83 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ →
ℝ*𝑠 ∈ V) |
85 | | ssid 3657 |
. . . . . . . . . . . 12
⊢
ℝ* ⊆ ℝ* |
86 | 85 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ →
ℝ* ⊆ ℝ*) |
87 | | simp2 1082 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ 𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → 𝑥 ∈ ℝ*) |
88 | | simp3 1083 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ ∧ 𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → 𝑦 ∈ ℝ*) |
89 | 87, 88 | xaddcld 12169 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ ∧ 𝑥 ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → (𝑥 +𝑒 𝑦) ∈
ℝ*) |
90 | 16, 18, 26, 84, 86, 89 | mulgnnsubcl 17600 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ ∧ 𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ*)
→ (𝑚(.g‘ℝ*𝑠)𝐵) ∈ ℝ*) |
91 | 90 | 3anidm12 1423 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ ∧ 𝐵 ∈ ℝ*)
→ (𝑚(.g‘ℝ*𝑠)𝐵) ∈ ℝ*) |
92 | 91 | ancoms 468 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ (𝑚(.g‘ℝ*𝑠)𝐵) ∈ ℝ*) |
93 | | xrsinvgval 29805 |
. . . . . . . 8
⊢ ((𝑚(.g‘ℝ*𝑠)𝐵) ∈ ℝ* →
((invg‘ℝ*𝑠)‘(𝑚(.g‘ℝ*𝑠)𝐵)) = -𝑒(𝑚(.g‘ℝ*𝑠)𝐵)) |
94 | 92, 93 | syl 17 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→
((invg‘ℝ*𝑠)‘(𝑚(.g‘ℝ*𝑠)𝐵)) = -𝑒(𝑚(.g‘ℝ*𝑠)𝐵)) |
95 | 82, 94 | eqtrd 2685 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ (-𝑚(.g‘ℝ*𝑠)𝐵) = -𝑒(𝑚(.g‘ℝ*𝑠)𝐵)) |
96 | 95 | adantr 480 |
. . . . 5
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (-𝑚(.g‘ℝ*𝑠)𝐵) = -𝑒(𝑚(.g‘ℝ*𝑠)𝐵)) |
97 | | nnre 11065 |
. . . . . . . . . 10
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ) |
98 | 97 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ 𝑚 ∈
ℝ) |
99 | | rexneg 12080 |
. . . . . . . . 9
⊢ (𝑚 ∈ ℝ →
-𝑒𝑚 =
-𝑚) |
100 | 98, 99 | syl 17 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ -𝑒𝑚 = -𝑚) |
101 | 100 | oveq1d 6705 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ (-𝑒𝑚 ·e 𝐵) = (-𝑚 ·e 𝐵)) |
102 | | nnssre 11062 |
. . . . . . . . . 10
⊢ ℕ
⊆ ℝ |
103 | 102, 53 | sstri 3645 |
. . . . . . . . 9
⊢ ℕ
⊆ ℝ* |
104 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ 𝑚 ∈
ℕ) |
105 | 103, 104 | sseldi 3634 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ 𝑚 ∈
ℝ*) |
106 | | simpl 472 |
. . . . . . . 8
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ 𝐵 ∈
ℝ*) |
107 | | xmulneg1 12137 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℝ*
∧ 𝐵 ∈
ℝ*) → (-𝑒𝑚 ·e 𝐵) = -𝑒(𝑚 ·e 𝐵)) |
108 | 105, 106,
107 | syl2anc 694 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ (-𝑒𝑚 ·e 𝐵) = -𝑒(𝑚 ·e 𝐵)) |
109 | 101, 108 | eqtr3d 2687 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
→ (-𝑚
·e 𝐵) =
-𝑒(𝑚
·e 𝐵)) |
110 | 109 | adantr 480 |
. . . . 5
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (-𝑚
·e 𝐵) =
-𝑒(𝑚 ·e
𝐵)) |
111 | 79, 96, 110 | 3eqtr4d 2695 |
. . . 4
⊢ (((𝐵 ∈ ℝ*
∧ 𝑚 ∈ ℕ)
∧ (𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵)) → (-𝑚(.g‘ℝ*𝑠)𝐵) = (-𝑚 ·e 𝐵)) |
112 | 111 | exp31 629 |
. . 3
⊢ (𝐵 ∈ ℝ*
→ (𝑚 ∈ ℕ
→ ((𝑚(.g‘ℝ*𝑠)𝐵) = (𝑚 ·e 𝐵) → (-𝑚(.g‘ℝ*𝑠)𝐵) = (-𝑚 ·e 𝐵)))) |
113 | 3, 6, 9, 12, 15, 21, 77, 112 | zindd 11516 |
. 2
⊢ (𝐵 ∈ ℝ*
→ (𝐴 ∈ ℤ
→ (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵))) |
114 | 113 | impcom 445 |
1
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℝ*)
→ (𝐴(.g‘ℝ*𝑠)𝐵) = (𝐴 ·e 𝐵)) |