Step | Hyp | Ref
| Expression |
1 | | stoweidlem17.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nnnn0d 11228 |
. 2
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
3 | | nn0uz 11598 |
. . . . 5
⊢
ℕ0 = (ℤ≥‘0) |
4 | 2, 3 | syl6eleq 2698 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
5 | | eluzfz2 12220 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘0) → 𝑁 ∈ (0...𝑁)) |
6 | 4, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (0...𝑁)) |
7 | 6 | ancli 572 |
. 2
⊢ (𝜑 → (𝜑 ∧ 𝑁 ∈ (0...𝑁))) |
8 | | eleq1 2676 |
. . . . 5
⊢ (𝑛 = 0 → (𝑛 ∈ (0...𝑁) ↔ 0 ∈ (0...𝑁))) |
9 | 8 | anbi2d 736 |
. . . 4
⊢ (𝑛 = 0 → ((𝜑 ∧ 𝑛 ∈ (0...𝑁)) ↔ (𝜑 ∧ 0 ∈ (0...𝑁)))) |
10 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑛 = 0 → (0...𝑛) = (0...0)) |
11 | 10 | sumeq1d 14279 |
. . . . . 6
⊢ (𝑛 = 0 → Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...0)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
12 | 11 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑛 = 0 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 · ((𝑋‘𝑖)‘𝑡)))) |
13 | 12 | eleq1d 2672 |
. . . 4
⊢ (𝑛 = 0 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) |
14 | 9, 13 | imbi12d 333 |
. . 3
⊢ (𝑛 = 0 → (((𝜑 ∧ 𝑛 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) ↔ ((𝜑 ∧ 0 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴))) |
15 | | eleq1 2676 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝑛 ∈ (0...𝑁) ↔ 𝑚 ∈ (0...𝑁))) |
16 | 15 | anbi2d 736 |
. . . 4
⊢ (𝑛 = 𝑚 → ((𝜑 ∧ 𝑛 ∈ (0...𝑁)) ↔ (𝜑 ∧ 𝑚 ∈ (0...𝑁)))) |
17 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑛 = 𝑚 → (0...𝑛) = (0...𝑚)) |
18 | 17 | sumeq1d 14279 |
. . . . . 6
⊢ (𝑛 = 𝑚 → Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
19 | 18 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑛 = 𝑚 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))) |
20 | 19 | eleq1d 2672 |
. . . 4
⊢ (𝑛 = 𝑚 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) |
21 | 16, 20 | imbi12d 333 |
. . 3
⊢ (𝑛 = 𝑚 → (((𝜑 ∧ 𝑛 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) ↔ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴))) |
22 | | eleq1 2676 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (𝑛 ∈ (0...𝑁) ↔ (𝑚 + 1) ∈ (0...𝑁))) |
23 | 22 | anbi2d 736 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → ((𝜑 ∧ 𝑛 ∈ (0...𝑁)) ↔ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) |
24 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → (0...𝑛) = (0...(𝑚 + 1))) |
25 | 24 | sumeq1d 14279 |
. . . . . 6
⊢ (𝑛 = (𝑚 + 1) → Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
26 | 25 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑛 = (𝑚 + 1) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)))) |
27 | 26 | eleq1d 2672 |
. . . 4
⊢ (𝑛 = (𝑚 + 1) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) |
28 | 23, 27 | imbi12d 333 |
. . 3
⊢ (𝑛 = (𝑚 + 1) → (((𝜑 ∧ 𝑛 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) ↔ ((𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴))) |
29 | | eleq1 2676 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑛 ∈ (0...𝑁) ↔ 𝑁 ∈ (0...𝑁))) |
30 | 29 | anbi2d 736 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝜑 ∧ 𝑛 ∈ (0...𝑁)) ↔ (𝜑 ∧ 𝑁 ∈ (0...𝑁)))) |
31 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑛 = 𝑁 → (0...𝑛) = (0...𝑁)) |
32 | 31 | sumeq1d 14279 |
. . . . . 6
⊢ (𝑛 = 𝑁 → Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
33 | 32 | mpteq2dv 4673 |
. . . . 5
⊢ (𝑛 = 𝑁 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡)))) |
34 | 33 | eleq1d 2672 |
. . . 4
⊢ (𝑛 = 𝑁 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) |
35 | 30, 34 | imbi12d 333 |
. . 3
⊢ (𝑛 = 𝑁 → (((𝜑 ∧ 𝑛 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑛)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) ↔ ((𝜑 ∧ 𝑁 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴))) |
36 | | 0z 11265 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
37 | | fzsn 12254 |
. . . . . . . . 9
⊢ (0 ∈
ℤ → (0...0) = {0}) |
38 | 36, 37 | ax-mp 5 |
. . . . . . . 8
⊢ (0...0) =
{0} |
39 | 38 | sumeq1i 14276 |
. . . . . . 7
⊢
Σ𝑖 ∈
(0...0)(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ {0} (𝐸 · ((𝑋‘𝑖)‘𝑡)) |
40 | 39 | mpteq2i 4669 |
. . . . . 6
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ {0} (𝐸 · ((𝑋‘𝑖)‘𝑡))) |
41 | | stoweidlem17.1 |
. . . . . . 7
⊢
Ⅎ𝑡𝜑 |
42 | | stoweidlem17.7 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℝ) |
43 | 42 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐸 ∈ ℝ) |
44 | 43 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝐸 ∈ ℂ) |
45 | | stoweidlem17.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑋:(0...𝑁)⟶𝐴) |
46 | | nnz 11276 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℤ) |
47 | | nngt0 10926 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → 0 <
𝑁) |
48 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
49 | | nnre 10904 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ → 𝑁 ∈
ℝ) |
50 | | ltle 10005 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℝ ∧ 𝑁
∈ ℝ) → (0 < 𝑁 → 0 ≤ 𝑁)) |
51 | 48, 49, 50 | sylancr 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ ℕ → (0 <
𝑁 → 0 ≤ 𝑁)) |
52 | 47, 51 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑁 ∈ ℕ → 0 ≤
𝑁) |
53 | 46, 52 | jca 553 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ → (𝑁 ∈ ℤ ∧ 0 ≤
𝑁)) |
54 | 1, 53 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁)) |
55 | 36 | eluz1i 11571 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈
(ℤ≥‘0) ↔ (𝑁 ∈ ℤ ∧ 0 ≤ 𝑁)) |
56 | 54, 55 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) |
57 | | eluzfz1 12219 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑁)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈ (0...𝑁)) |
59 | 45, 58 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑋‘0) ∈ 𝐴) |
60 | | feq1 5939 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝑋‘0) → (𝑓:𝑇⟶ℝ ↔ (𝑋‘0):𝑇⟶ℝ)) |
61 | 60 | imbi2d 329 |
. . . . . . . . . . . . 13
⊢ (𝑓 = (𝑋‘0) → ((𝜑 → 𝑓:𝑇⟶ℝ) ↔ (𝜑 → (𝑋‘0):𝑇⟶ℝ))) |
62 | | stoweidlem17.8 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
63 | 62 | expcom 450 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ 𝐴 → (𝜑 → 𝑓:𝑇⟶ℝ)) |
64 | 61, 63 | vtoclga 3245 |
. . . . . . . . . . . 12
⊢ ((𝑋‘0) ∈ 𝐴 → (𝜑 → (𝑋‘0):𝑇⟶ℝ)) |
65 | 59, 64 | mpcom 37 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑋‘0):𝑇⟶ℝ) |
66 | 65 | fnvinran 38196 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑋‘0)‘𝑡) ∈ ℝ) |
67 | 66 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑋‘0)‘𝑡) ∈ ℂ) |
68 | 44, 67 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝐸 · ((𝑋‘0)‘𝑡)) ∈ ℂ) |
69 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑖 = 0 → (𝑋‘𝑖) = (𝑋‘0)) |
70 | 69 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑖 = 0 → ((𝑋‘𝑖)‘𝑡) = ((𝑋‘0)‘𝑡)) |
71 | 70 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑖 = 0 → (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘0)‘𝑡))) |
72 | 71 | sumsn 14319 |
. . . . . . . 8
⊢ ((0
∈ ℤ ∧ (𝐸
· ((𝑋‘0)‘𝑡)) ∈ ℂ) → Σ𝑖 ∈ {0} (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘0)‘𝑡))) |
73 | 36, 68, 72 | sylancr 694 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ {0} (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘0)‘𝑡))) |
74 | 41, 73 | mpteq2da 4671 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ {0} (𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘0)‘𝑡)))) |
75 | 40, 74 | syl5eq 2656 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘0)‘𝑡)))) |
76 | | stoweidlem17.5 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
77 | | stoweidlem17.6 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ) → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) |
78 | 41, 76, 77, 62, 42, 59 | stoweidlem2 38895 |
. . . . 5
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘0)‘𝑡))) ∈ 𝐴) |
79 | 75, 78 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) |
80 | 79 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 0 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...0)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) |
81 | | eqidd 2611 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑡 → 𝐸 = 𝐸) |
82 | 81 | cbvmptv 4678 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ 𝑇 ↦ 𝐸) = (𝑡 ∈ 𝑇 ↦ 𝐸) |
83 | 82 | eqcomi 2619 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝑇 ↦ 𝐸) = (𝑟 ∈ 𝑇 ↦ 𝐸) |
84 | 83 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (𝑡 ∈ 𝑇 ↦ 𝐸) = (𝑟 ∈ 𝑇 ↦ 𝐸)) |
85 | | eqidd 2611 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑡 ∈ 𝑇) ∧ 𝑟 = 𝑡) → 𝐸 = 𝐸) |
86 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
87 | 84, 85, 86, 43 | fvmptd 6197 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) = 𝐸) |
88 | 87 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · ((𝑋‘(𝑚 + 1))‘𝑡)) = (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) |
89 | 41, 88 | mpteq2da 4671 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · ((𝑋‘(𝑚 + 1))‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))) |
90 | 89 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · ((𝑋‘(𝑚 + 1))‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))) |
91 | 45 | fnvinran 38196 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑋‘(𝑚 + 1)) ∈ 𝐴) |
92 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → 𝜑) |
93 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝐸 → 𝑥 = 𝐸) |
94 | 93 | mpteq2dv 4673 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝐸 → (𝑡 ∈ 𝑇 ↦ 𝑥) = (𝑡 ∈ 𝑇 ↦ 𝐸)) |
95 | 94 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝐸 → ((𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)) |
96 | 95 | imbi2d 329 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝐸 → ((𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴) ↔ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴))) |
97 | 77 | expcom 450 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℝ → (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝑥) ∈ 𝐴)) |
98 | 96, 97 | vtoclga 3245 |
. . . . . . . . . . . 12
⊢ (𝐸 ∈ ℝ → (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴)) |
99 | 42, 98 | mpcom 37 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) |
100 | 99 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) |
101 | | fveq1 6102 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = (𝑋‘(𝑚 + 1)) → (𝑔‘𝑡) = ((𝑋‘(𝑚 + 1))‘𝑡)) |
102 | 101 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑋‘(𝑚 + 1)) → (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡)) = (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · ((𝑋‘(𝑚 + 1))‘𝑡))) |
103 | 102 | mpteq2dv 4673 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑋‘(𝑚 + 1)) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · ((𝑋‘(𝑚 + 1))‘𝑡)))) |
104 | 103 | eleq1d 2672 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑋‘(𝑚 + 1)) → ((𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · ((𝑋‘(𝑚 + 1))‘𝑡))) ∈ 𝐴)) |
105 | 104 | imbi2d 329 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑋‘(𝑚 + 1)) → (((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) ↔ ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · ((𝑋‘(𝑚 + 1))‘𝑡))) ∈ 𝐴))) |
106 | 82 | eleq1i 2679 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) |
107 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ 𝐸) → (𝑓‘𝑡) = ((𝑟 ∈ 𝑇 ↦ 𝐸)‘𝑡)) |
108 | 82 | fveq1i 6104 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑟 ∈ 𝑇 ↦ 𝐸)‘𝑡) = ((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) |
109 | 107, 108 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ 𝐸) → (𝑓‘𝑡) = ((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡)) |
110 | 109 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ 𝐸) → ((𝑓‘𝑡) · (𝑔‘𝑡)) = (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) |
111 | 110 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ 𝐸) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡)))) |
112 | 111 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ 𝐸) → ((𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)) |
113 | 112 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ 𝐸) → (((𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) ↔ ((𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴))) |
114 | 76 | 3com12 1261 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑓 ∈ 𝐴 ∧ 𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
115 | 114 | 3expib 1260 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 ∈ 𝐴 → ((𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)) |
116 | 113, 115 | vtoclga 3245 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑟 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 → ((𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)) |
117 | 106, 116 | sylbir 224 |
. . . . . . . . . . . . . . 15
⊢ ((𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 → ((𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)) |
118 | 117 | 3impib 1254 |
. . . . . . . . . . . . . 14
⊢ (((𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴 ∧ 𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
119 | 118 | 3com13 1262 |
. . . . . . . . . . . . 13
⊢ ((𝑔 ∈ 𝐴 ∧ 𝜑 ∧ (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴) |
120 | 119 | 3expib 1260 |
. . . . . . . . . . . 12
⊢ (𝑔 ∈ 𝐴 → ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · (𝑔‘𝑡))) ∈ 𝐴)) |
121 | 105, 120 | vtoclga 3245 |
. . . . . . . . . . 11
⊢ ((𝑋‘(𝑚 + 1)) ∈ 𝐴 → ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · ((𝑋‘(𝑚 + 1))‘𝑡))) ∈ 𝐴)) |
122 | 121 | 3impib 1254 |
. . . . . . . . . 10
⊢ (((𝑋‘(𝑚 + 1)) ∈ 𝐴 ∧ 𝜑 ∧ (𝑡 ∈ 𝑇 ↦ 𝐸) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · ((𝑋‘(𝑚 + 1))‘𝑡))) ∈ 𝐴) |
123 | 91, 92, 100, 122 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ 𝐸)‘𝑡) · ((𝑋‘(𝑚 + 1))‘𝑡))) ∈ 𝐴) |
124 | 90, 123 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) ∈ 𝐴) |
125 | 124 | ad2antll 761 |
. . . . . . 7
⊢ (((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) ∧ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) → (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) ∈ 𝐴) |
126 | | simprrl 800 |
. . . . . . 7
⊢ (((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) ∧ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) → 𝜑) |
127 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → 𝑚 ∈ ℕ0) |
128 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → 𝜑) |
129 | 1 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → 𝑁 ∈ ℕ) |
130 | 129 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → 𝑁 ∈
ℕ0) |
131 | | nn0re 11178 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) |
132 | 131 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → 𝑚 ∈ ℝ) |
133 | | peano2nn0 11210 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℕ0) |
134 | 133 | nn0red 11229 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℕ0
→ (𝑚 + 1) ∈
ℝ) |
135 | 134 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → (𝑚 + 1) ∈ ℝ) |
136 | 1 | nnred 10912 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁 ∈ ℝ) |
137 | 136 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → 𝑁 ∈ ℝ) |
138 | | lep1 10741 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ℝ → 𝑚 ≤ (𝑚 + 1)) |
139 | 127, 131,
138 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → 𝑚 ≤ (𝑚 + 1)) |
140 | | elfzle2 12216 |
. . . . . . . . . . . . 13
⊢ ((𝑚 + 1) ∈ (0...𝑁) → (𝑚 + 1) ≤ 𝑁) |
141 | 140 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → (𝑚 + 1) ≤ 𝑁) |
142 | 132, 135,
137, 139, 141 | letrd 10073 |
. . . . . . . . . . 11
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → 𝑚 ≤ 𝑁) |
143 | | elfz2nn0 12300 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ (0...𝑁) ↔ (𝑚 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0
∧ 𝑚 ≤ 𝑁)) |
144 | 127, 130,
142, 143 | syl3anbrc 1239 |
. . . . . . . . . 10
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → 𝑚 ∈ (0...𝑁)) |
145 | 127, 128,
144 | jca32 556 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ 𝑚 ∈ (0...𝑁)))) |
146 | 145 | adantl 481 |
. . . . . . . 8
⊢ (((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) ∧ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) → (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ 𝑚 ∈ (0...𝑁)))) |
147 | | pm3.31 460 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) → ((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ 𝑚 ∈ (0...𝑁))) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) |
148 | 147 | adantr 480 |
. . . . . . . 8
⊢ (((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) ∧ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) → ((𝑚 ∈ ℕ0 ∧ (𝜑 ∧ 𝑚 ∈ (0...𝑁))) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) |
149 | 146, 148 | mpd 15 |
. . . . . . 7
⊢ (((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) ∧ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) |
150 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑟 = 𝑡 → ((𝑋‘(𝑚 + 1))‘𝑟) = ((𝑋‘(𝑚 + 1))‘𝑡)) |
151 | 150 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝑟 = 𝑡 → (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟)) = (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) |
152 | 151 | cbvmptv 4678 |
. . . . . . . . . 10
⊢ (𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟))) = (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) |
153 | 152 | eleq1i 2679 |
. . . . . . . . 9
⊢ ((𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) ∈ 𝐴) |
154 | | fveq1 6102 |
. . . . . . . . . . . . . . 15
⊢ (𝑔 = (𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟))) → (𝑔‘𝑡) = ((𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟)))‘𝑡)) |
155 | 152 | fveq1i 6104 |
. . . . . . . . . . . . . . 15
⊢ ((𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟)))‘𝑡) = ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡) |
156 | 154, 155 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ (𝑔 = (𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟))) → (𝑔‘𝑡) = ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡)) |
157 | 156 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝑔 = (𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟))) → (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡)) = (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡))) |
158 | 157 | mpteq2dv 4673 |
. . . . . . . . . . . 12
⊢ (𝑔 = (𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟))) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡)))) |
159 | 158 | eleq1d 2672 |
. . . . . . . . . . 11
⊢ (𝑔 = (𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟))) → ((𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡))) ∈ 𝐴)) |
160 | 159 | imbi2d 329 |
. . . . . . . . . 10
⊢ (𝑔 = (𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟))) → (((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) ↔ ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡))) ∈ 𝐴))) |
161 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑟 = 𝑡 → ((𝑋‘𝑖)‘𝑟) = ((𝑋‘𝑖)‘𝑡)) |
162 | 161 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑟 = 𝑡 → (𝐸 · ((𝑋‘𝑖)‘𝑟)) = (𝐸 · ((𝑋‘𝑖)‘𝑡))) |
163 | 162 | sumeq2sdv 14282 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 = 𝑡 → Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟)) = Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
164 | 163 | cbvmptv 4678 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
165 | 164 | eleq1i 2679 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) |
166 | | fveq1 6102 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟))) → (𝑓‘𝑡) = ((𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟)))‘𝑡)) |
167 | 164 | fveq1i 6104 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟)))‘𝑡) = ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) |
168 | 166, 167 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟))) → (𝑓‘𝑡) = ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡)) |
169 | 168 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟))) → ((𝑓‘𝑡) + (𝑔‘𝑡)) = (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) |
170 | 169 | mpteq2dv 4673 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟))) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡)))) |
171 | 170 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟))) → ((𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)) |
172 | 171 | imbi2d 329 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟))) → (((𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) ↔ ((𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴))) |
173 | | stoweidlem17.4 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
174 | 173 | 3com12 1261 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑓 ∈ 𝐴 ∧ 𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
175 | 174 | 3expib 1260 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ∈ 𝐴 → ((𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)) |
176 | 172, 175 | vtoclga 3245 |
. . . . . . . . . . . . . 14
⊢ ((𝑟 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑟))) ∈ 𝐴 → ((𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)) |
177 | 165, 176 | sylbir 224 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴 → ((𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)) |
178 | 177 | 3impib 1254 |
. . . . . . . . . . . 12
⊢ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴 ∧ 𝜑 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
179 | 178 | 3com13 1262 |
. . . . . . . . . . 11
⊢ ((𝑔 ∈ 𝐴 ∧ 𝜑 ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
180 | 179 | 3expib 1260 |
. . . . . . . . . 10
⊢ (𝑔 ∈ 𝐴 → ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴)) |
181 | 160, 180 | vtoclga 3245 |
. . . . . . . . 9
⊢ ((𝑟 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑟))) ∈ 𝐴 → ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡))) ∈ 𝐴)) |
182 | 153, 181 | sylbir 224 |
. . . . . . . 8
⊢ ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) ∈ 𝐴 → ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡))) ∈ 𝐴)) |
183 | 182 | 3impib 1254 |
. . . . . . 7
⊢ (((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) ∈ 𝐴 ∧ 𝜑 ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡))) ∈ 𝐴) |
184 | 125, 126,
149, 183 | syl3anc 1318 |
. . . . . 6
⊢ (((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) ∧ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡))) ∈ 𝐴) |
185 | | 3anass 1035 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ↔ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) |
186 | 185 | biimpri 217 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ0
∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) → (𝑚 ∈ ℕ0 ∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) |
187 | 186 | adantl 481 |
. . . . . . 7
⊢ (((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) ∧ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) → (𝑚 ∈ ℕ0 ∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) |
188 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑡 𝑚 ∈
ℕ0 |
189 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑡(𝑚 + 1) ∈ (0...𝑁) |
190 | 188, 41, 189 | nf3an 1819 |
. . . . . . . . 9
⊢
Ⅎ𝑡(𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) |
191 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
192 | | fzfid 12634 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → (0...𝑚) ∈ Fin) |
193 | 42 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → 𝐸 ∈ ℝ) |
194 | 193 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → 𝐸 ∈ ℝ) |
195 | 194 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (0...𝑚)) → 𝐸 ∈ ℝ) |
196 | | fzelp1 12263 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (0...𝑚) → 𝑖 ∈ (0...(𝑚 + 1))) |
197 | 196 | anim2i 591 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (0...𝑚)) → (((𝑚 ∈ ℕ0 ∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (0...(𝑚 + 1)))) |
198 | | an32 835 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (0...(𝑚 + 1))) ↔ (((𝑚 ∈ ℕ0 ∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(𝑚 + 1))) ∧ 𝑡 ∈ 𝑇)) |
199 | 197, 198 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (0...𝑚)) → (((𝑚 ∈ ℕ0 ∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(𝑚 + 1))) ∧ 𝑡 ∈ 𝑇)) |
200 | 45 | 3ad2ant2 1076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → 𝑋:(0...𝑁)⟶𝐴) |
201 | 200 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(𝑚 + 1))) → 𝑋:(0...𝑁)⟶𝐴) |
202 | | elfzuz3 12210 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑚 + 1) ∈ (0...𝑁) → 𝑁 ∈ (ℤ≥‘(𝑚 + 1))) |
203 | | fzss2 12252 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑁 ∈
(ℤ≥‘(𝑚 + 1)) → (0...(𝑚 + 1)) ⊆ (0...𝑁)) |
204 | 202, 203 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 + 1) ∈ (0...𝑁) → (0...(𝑚 + 1)) ⊆ (0...𝑁)) |
205 | 204 | sselda 3568 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑚 + 1) ∈ (0...𝑁) ∧ 𝑖 ∈ (0...(𝑚 + 1))) → 𝑖 ∈ (0...𝑁)) |
206 | 205 | 3ad2antl3 1218 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(𝑚 + 1))) → 𝑖 ∈ (0...𝑁)) |
207 | 201, 206 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(𝑚 + 1))) → (𝑋‘𝑖) ∈ 𝐴) |
208 | | simpl2 1058 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(𝑚 + 1))) → 𝜑) |
209 | | feq1 5939 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝑋‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝑋‘𝑖):𝑇⟶ℝ)) |
210 | 209 | imbi2d 329 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑋‘𝑖) → ((𝜑 → 𝑓:𝑇⟶ℝ) ↔ (𝜑 → (𝑋‘𝑖):𝑇⟶ℝ))) |
211 | 210, 63 | vtoclga 3245 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑋‘𝑖) ∈ 𝐴 → (𝜑 → (𝑋‘𝑖):𝑇⟶ℝ)) |
212 | 207, 208,
211 | sylc 63 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(𝑚 + 1))) → (𝑋‘𝑖):𝑇⟶ℝ) |
213 | 212 | fnvinran 38196 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑖 ∈ (0...(𝑚 + 1))) ∧ 𝑡 ∈ 𝑇) → ((𝑋‘𝑖)‘𝑡) ∈ ℝ) |
214 | 199, 213 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (0...𝑚)) → ((𝑋‘𝑖)‘𝑡) ∈ ℝ) |
215 | 195, 214 | remulcld 9949 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (0...𝑚)) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℝ) |
216 | 192, 215 | fsumrecl 14312 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℝ) |
217 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
218 | 217 | fvmpt2 6200 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝑇 ∧ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℝ) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) = Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
219 | 191, 216,
218 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) = Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
220 | 219 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) = (Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)) + (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))) |
221 | | 3simpc 1053 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) |
222 | 221 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁))) |
223 | | feq1 5939 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝑋‘(𝑚 + 1)) → (𝑓:𝑇⟶ℝ ↔ (𝑋‘(𝑚 + 1)):𝑇⟶ℝ)) |
224 | 223 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝑋‘(𝑚 + 1)) → ((𝜑 → 𝑓:𝑇⟶ℝ) ↔ (𝜑 → (𝑋‘(𝑚 + 1)):𝑇⟶ℝ))) |
225 | 224, 63 | vtoclga 3245 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑋‘(𝑚 + 1)) ∈ 𝐴 → (𝜑 → (𝑋‘(𝑚 + 1)):𝑇⟶ℝ)) |
226 | 91, 92, 225 | sylc 63 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑋‘(𝑚 + 1)):𝑇⟶ℝ) |
227 | 222, 226 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → (𝑋‘(𝑚 + 1)):𝑇⟶ℝ) |
228 | 227, 191 | ffvelrnd 6268 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → ((𝑋‘(𝑚 + 1))‘𝑡) ∈ ℝ) |
229 | 194, 228 | remulcld 9949 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)) ∈ ℝ) |
230 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) |
231 | 230 | fvmpt2 6200 |
. . . . . . . . . . . 12
⊢ ((𝑡 ∈ 𝑇 ∧ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)) ∈ ℝ) → ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡) = (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) |
232 | 191, 229,
231 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡) = (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) |
233 | 232 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡)) = (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))) |
234 | | elfzuz 12209 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 + 1) ∈ (0...𝑁) → (𝑚 + 1) ∈
(ℤ≥‘0)) |
235 | 234 | 3ad2ant3 1077 |
. . . . . . . . . . . . 13
⊢ ((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑚 + 1) ∈
(ℤ≥‘0)) |
236 | 235 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → (𝑚 + 1) ∈
(ℤ≥‘0)) |
237 | 194 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (0...(𝑚 + 1))) → 𝐸 ∈ ℝ) |
238 | 213 | an32s 842 |
. . . . . . . . . . . . 13
⊢ ((((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (0...(𝑚 + 1))) → ((𝑋‘𝑖)‘𝑡) ∈ ℝ) |
239 | | remulcl 9900 |
. . . . . . . . . . . . . 14
⊢ ((𝐸 ∈ ℝ ∧ ((𝑋‘𝑖)‘𝑡) ∈ ℝ) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℝ) |
240 | 239 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝐸 ∈ ℝ ∧ ((𝑋‘𝑖)‘𝑡) ∈ ℝ) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℂ) |
241 | 237, 238,
240 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (0...(𝑚 + 1))) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) ∈ ℂ) |
242 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑖 = (𝑚 + 1) → (𝑋‘𝑖) = (𝑋‘(𝑚 + 1))) |
243 | 242 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑚 + 1) → ((𝑋‘𝑖)‘𝑡) = ((𝑋‘(𝑚 + 1))‘𝑡)) |
244 | 243 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑚 + 1) → (𝐸 · ((𝑋‘𝑖)‘𝑡)) = (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) |
245 | 236, 241,
244 | fsumm1 14324 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) = (Σ𝑖 ∈ (0...((𝑚 + 1) − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) + (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))) |
246 | | nn0cn 11179 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℂ) |
247 | 246 | 3ad2ant1 1075 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → 𝑚 ∈ ℂ) |
248 | 247 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → 𝑚 ∈ ℂ) |
249 | | 1cnd 9935 |
. . . . . . . . . . . . . . 15
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → 1 ∈ ℂ) |
250 | 248, 249 | pncand 10272 |
. . . . . . . . . . . . . 14
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → ((𝑚 + 1) − 1) = 𝑚) |
251 | 250 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → (0...((𝑚 + 1) − 1)) = (0...𝑚)) |
252 | 251 | sumeq1d 14279 |
. . . . . . . . . . . 12
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (0...((𝑚 + 1) − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) = Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) |
253 | 252 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → (Σ𝑖 ∈ (0...((𝑚 + 1) − 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) + (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡))) = (Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)) + (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))) |
254 | 245, 253 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) = (Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)) + (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))) |
255 | 220, 233,
254 | 3eqtr4rd 2655 |
. . . . . . . . 9
⊢ (((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡)) = (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡))) |
256 | 190, 255 | mpteq2da 4671 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡)))) |
257 | 256 | eleq1d 2672 |
. . . . . . 7
⊢ ((𝑚 ∈ ℕ0
∧ 𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡))) ∈ 𝐴)) |
258 | 187, 257 | syl 17 |
. . . . . 6
⊢ (((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) ∧ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡)))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ (𝐸 · ((𝑋‘(𝑚 + 1))‘𝑡)))‘𝑡))) ∈ 𝐴)) |
259 | 184, 258 | mpbird 246 |
. . . . 5
⊢ (((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) ∧ (𝑚 ∈ ℕ0 ∧ (𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)))) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) |
260 | 259 | exp32 629 |
. . . 4
⊢ ((𝑚 ∈ ℕ0
→ ((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) → (𝑚 ∈ ℕ0 → ((𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴))) |
261 | 260 | pm2.86i 107 |
. . 3
⊢ (𝑚 ∈ ℕ0
→ (((𝜑 ∧ 𝑚 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑚)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) → ((𝜑 ∧ (𝑚 + 1) ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...(𝑚 + 1))(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴))) |
262 | 14, 21, 28, 35, 80, 261 | nn0ind 11348 |
. 2
⊢ (𝑁 ∈ ℕ0
→ ((𝜑 ∧ 𝑁 ∈ (0...𝑁)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴)) |
263 | 2, 7, 262 | sylc 63 |
1
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (0...𝑁)(𝐸 · ((𝑋‘𝑖)‘𝑡))) ∈ 𝐴) |