Step | Hyp | Ref
| Expression |
1 | | stoweidlem20.2 |
. 2
⊢ 𝐹 = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
2 | | stoweidlem20.3 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℕ) |
3 | 2 | nnred 11988 |
. . . . 5
⊢ (𝜑 → 𝑀 ∈ ℝ) |
4 | 3 | leidd 11541 |
. . . 4
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
5 | 4 | ancli 549 |
. . 3
⊢ (𝜑 → (𝜑 ∧ 𝑀 ≤ 𝑀)) |
6 | | eleq1 2826 |
. . . . 5
⊢ (𝑛 = 𝑀 → (𝑛 ∈ ℕ ↔ 𝑀 ∈ ℕ)) |
7 | | breq1 5077 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (𝑛 ≤ 𝑀 ↔ 𝑀 ≤ 𝑀)) |
8 | 7 | anbi2d 629 |
. . . . . 6
⊢ (𝑛 = 𝑀 → ((𝜑 ∧ 𝑛 ≤ 𝑀) ↔ (𝜑 ∧ 𝑀 ≤ 𝑀))) |
9 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑛 = 𝑀 → (1...𝑛) = (1...𝑀)) |
10 | 9 | sumeq1d 15413 |
. . . . . . . 8
⊢ (𝑛 = 𝑀 → Σ𝑖 ∈ (1...𝑛)((𝐺‘𝑖)‘𝑡) = Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) |
11 | 10 | mpteq2dv 5176 |
. . . . . . 7
⊢ (𝑛 = 𝑀 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡))) |
12 | 11 | eleq1d 2823 |
. . . . . 6
⊢ (𝑛 = 𝑀 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) |
13 | 8, 12 | imbi12d 345 |
. . . . 5
⊢ (𝑛 = 𝑀 → (((𝜑 ∧ 𝑛 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) ↔ ((𝜑 ∧ 𝑀 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴))) |
14 | 6, 13 | imbi12d 345 |
. . . 4
⊢ (𝑛 = 𝑀 → ((𝑛 ∈ ℕ → ((𝜑 ∧ 𝑛 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) ↔ (𝑀 ∈ ℕ → ((𝜑 ∧ 𝑀 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)))) |
15 | | breq1 5077 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑥 ≤ 𝑀 ↔ 1 ≤ 𝑀)) |
16 | 15 | anbi2d 629 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝜑 ∧ 𝑥 ≤ 𝑀) ↔ (𝜑 ∧ 1 ≤ 𝑀))) |
17 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑥 = 1 → (1...𝑥) = (1...1)) |
18 | 17 | sumeq1d 15413 |
. . . . . . . 8
⊢ (𝑥 = 1 → Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡) = Σ𝑖 ∈ (1...1)((𝐺‘𝑖)‘𝑡)) |
19 | 18 | mpteq2dv 5176 |
. . . . . . 7
⊢ (𝑥 = 1 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((𝐺‘𝑖)‘𝑡))) |
20 | 19 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = 1 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) |
21 | 16, 20 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = 1 → (((𝜑 ∧ 𝑥 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) ↔ ((𝜑 ∧ 1 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴))) |
22 | | breq1 5077 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑥 ≤ 𝑀 ↔ 𝑦 ≤ 𝑀)) |
23 | 22 | anbi2d 629 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ≤ 𝑀) ↔ (𝜑 ∧ 𝑦 ≤ 𝑀))) |
24 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (1...𝑥) = (1...𝑦)) |
25 | 24 | sumeq1d 15413 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡) = Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) |
26 | 25 | mpteq2dv 5176 |
. . . . . . 7
⊢ (𝑥 = 𝑦 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))) |
27 | 26 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = 𝑦 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) |
28 | 23, 27 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) ↔ ((𝜑 ∧ 𝑦 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴))) |
29 | | breq1 5077 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (𝑥 ≤ 𝑀 ↔ (𝑦 + 1) ≤ 𝑀)) |
30 | 29 | anbi2d 629 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((𝜑 ∧ 𝑥 ≤ 𝑀) ↔ (𝜑 ∧ (𝑦 + 1) ≤ 𝑀))) |
31 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑥 = (𝑦 + 1) → (1...𝑥) = (1...(𝑦 + 1))) |
32 | 31 | sumeq1d 15413 |
. . . . . . . 8
⊢ (𝑥 = (𝑦 + 1) → Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡) = Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡)) |
33 | 32 | mpteq2dv 5176 |
. . . . . . 7
⊢ (𝑥 = (𝑦 + 1) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡))) |
34 | 33 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = (𝑦 + 1) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) |
35 | 30, 34 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = (𝑦 + 1) → (((𝜑 ∧ 𝑥 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) ↔ ((𝜑 ∧ (𝑦 + 1) ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡)) ∈ 𝐴))) |
36 | | breq1 5077 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑥 ≤ 𝑀 ↔ 𝑛 ≤ 𝑀)) |
37 | 36 | anbi2d 629 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝜑 ∧ 𝑥 ≤ 𝑀) ↔ (𝜑 ∧ 𝑛 ≤ 𝑀))) |
38 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑥 = 𝑛 → (1...𝑥) = (1...𝑛)) |
39 | 38 | sumeq1d 15413 |
. . . . . . . 8
⊢ (𝑥 = 𝑛 → Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡) = Σ𝑖 ∈ (1...𝑛)((𝐺‘𝑖)‘𝑡)) |
40 | 39 | mpteq2dv 5176 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((𝐺‘𝑖)‘𝑡))) |
41 | 40 | eleq1d 2823 |
. . . . . 6
⊢ (𝑥 = 𝑛 → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴 ↔ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) |
42 | 37, 41 | imbi12d 345 |
. . . . 5
⊢ (𝑥 = 𝑛 → (((𝜑 ∧ 𝑥 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑥)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) ↔ ((𝜑 ∧ 𝑛 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴))) |
43 | | stoweidlem20.1 |
. . . . . . . . 9
⊢
Ⅎ𝑡𝜑 |
44 | | 1z 12350 |
. . . . . . . . . 10
⊢ 1 ∈
ℤ |
45 | | stoweidlem20.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐺:(1...𝑀)⟶𝐴) |
46 | | nnuz 12621 |
. . . . . . . . . . . . . . . 16
⊢ ℕ =
(ℤ≥‘1) |
47 | 2, 46 | eleqtrdi 2849 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘1)) |
48 | | eluzfz1 13263 |
. . . . . . . . . . . . . . 15
⊢ (𝑀 ∈
(ℤ≥‘1) → 1 ∈ (1...𝑀)) |
49 | 47, 48 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈ (1...𝑀)) |
50 | 45, 49 | ffvelrnd 6962 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐺‘1) ∈ 𝐴) |
51 | 50 | ancli 549 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝜑 ∧ (𝐺‘1) ∈ 𝐴)) |
52 | | eleq1 2826 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = (𝐺‘1) → (𝑓 ∈ 𝐴 ↔ (𝐺‘1) ∈ 𝐴)) |
53 | 52 | anbi2d 629 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝐺‘1) → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ (𝐺‘1) ∈ 𝐴))) |
54 | | feq1 6581 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 = (𝐺‘1) → (𝑓:𝑇⟶ℝ ↔ (𝐺‘1):𝑇⟶ℝ)) |
55 | 53, 54 | imbi12d 345 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = (𝐺‘1) → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝐺‘1) ∈ 𝐴) → (𝐺‘1):𝑇⟶ℝ))) |
56 | | stoweidlem20.6 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) |
57 | 55, 56 | vtoclg 3505 |
. . . . . . . . . . . . 13
⊢ ((𝐺‘1) ∈ 𝐴 → ((𝜑 ∧ (𝐺‘1) ∈ 𝐴) → (𝐺‘1):𝑇⟶ℝ)) |
58 | 50, 51, 57 | sylc 65 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐺‘1):𝑇⟶ℝ) |
59 | 58 | ffvelrnda 6961 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐺‘1)‘𝑡) ∈ ℝ) |
60 | 59 | recnd 11003 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → ((𝐺‘1)‘𝑡) ∈ ℂ) |
61 | | fveq2 6774 |
. . . . . . . . . . . 12
⊢ (𝑖 = 1 → (𝐺‘𝑖) = (𝐺‘1)) |
62 | 61 | fveq1d 6776 |
. . . . . . . . . . 11
⊢ (𝑖 = 1 → ((𝐺‘𝑖)‘𝑡) = ((𝐺‘1)‘𝑡)) |
63 | 62 | fsum1 15459 |
. . . . . . . . . 10
⊢ ((1
∈ ℤ ∧ ((𝐺‘1)‘𝑡) ∈ ℂ) → Σ𝑖 ∈ (1...1)((𝐺‘𝑖)‘𝑡) = ((𝐺‘1)‘𝑡)) |
64 | 44, 60, 63 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...1)((𝐺‘𝑖)‘𝑡) = ((𝐺‘1)‘𝑡)) |
65 | 43, 64 | mpteq2da 5172 |
. . . . . . . 8
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ ((𝐺‘1)‘𝑡))) |
66 | 58 | feqmptd 6837 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘1) = (𝑡 ∈ 𝑇 ↦ ((𝐺‘1)‘𝑡))) |
67 | 65, 66 | eqtr4d 2781 |
. . . . . . 7
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((𝐺‘𝑖)‘𝑡)) = (𝐺‘1)) |
68 | 67, 50 | eqeltrd 2839 |
. . . . . 6
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) |
69 | 68 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 1 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...1)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) |
70 | | simprl 768 |
. . . . . . 7
⊢ (((𝑦 ∈ ℕ ∧ ((𝜑 ∧ 𝑦 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) ∧ (𝜑 ∧ (𝑦 + 1) ≤ 𝑀)) → 𝜑) |
71 | | simpll 764 |
. . . . . . 7
⊢ (((𝑦 ∈ ℕ ∧ ((𝜑 ∧ 𝑦 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) ∧ (𝜑 ∧ (𝑦 + 1) ≤ 𝑀)) → 𝑦 ∈ ℕ) |
72 | | simprr 770 |
. . . . . . 7
⊢ (((𝑦 ∈ ℕ ∧ ((𝜑 ∧ 𝑦 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) ∧ (𝜑 ∧ (𝑦 + 1) ≤ 𝑀)) → (𝑦 + 1) ≤ 𝑀) |
73 | | simp1 1135 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → 𝜑) |
74 | | nnre 11980 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℕ → 𝑦 ∈
ℝ) |
75 | 74 | 3ad2ant2 1133 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → 𝑦 ∈ ℝ) |
76 | | 1red 10976 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → 1 ∈ ℝ) |
77 | 75, 76 | readdcld 11004 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → (𝑦 + 1) ∈ ℝ) |
78 | 2 | 3ad2ant1 1132 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → 𝑀 ∈ ℕ) |
79 | 78 | nnred 11988 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → 𝑀 ∈ ℝ) |
80 | 75 | lep1d 11906 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → 𝑦 ≤ (𝑦 + 1)) |
81 | | simp3 1137 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → (𝑦 + 1) ≤ 𝑀) |
82 | 75, 77, 79, 80, 81 | letrd 11132 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → 𝑦 ≤ 𝑀) |
83 | 73, 82 | jca 512 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → (𝜑 ∧ 𝑦 ≤ 𝑀)) |
84 | 70, 71, 72, 83 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ ∧ ((𝜑 ∧ 𝑦 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) ∧ (𝜑 ∧ (𝑦 + 1) ≤ 𝑀)) → (𝜑 ∧ 𝑦 ≤ 𝑀)) |
85 | | simplr 766 |
. . . . . . . 8
⊢ (((𝑦 ∈ ℕ ∧ ((𝜑 ∧ 𝑦 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) ∧ (𝜑 ∧ (𝑦 + 1) ≤ 𝑀)) → ((𝜑 ∧ 𝑦 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) |
86 | 84, 85 | mpd 15 |
. . . . . . 7
⊢ (((𝑦 ∈ ℕ ∧ ((𝜑 ∧ 𝑦 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) ∧ (𝜑 ∧ (𝑦 + 1) ≤ 𝑀)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) |
87 | | nfv 1917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡 𝑦 ∈ ℕ |
88 | | nfv 1917 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝑦 + 1) ≤ 𝑀 |
89 | 43, 87, 88 | nf3an 1904 |
. . . . . . . . . 10
⊢
Ⅎ𝑡(𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) |
90 | | simpl2 1191 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → 𝑦 ∈ ℕ) |
91 | 90, 46 | eleqtrdi 2849 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → 𝑦 ∈
(ℤ≥‘1)) |
92 | | simpll1 1211 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 𝜑) |
93 | | 1zzd 12351 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 1 ∈
ℤ) |
94 | 2 | nnzd 12425 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℤ) |
95 | 94 | 3ad2ant1 1132 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → 𝑀 ∈ ℤ) |
96 | 95 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 𝑀 ∈ ℤ) |
97 | | elfzelz 13256 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...(𝑦 + 1)) → 𝑖 ∈ ℤ) |
98 | 97 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 𝑖 ∈ ℤ) |
99 | | elfzle1 13259 |
. . . . . . . . . . . . . . 15
⊢ (𝑖 ∈ (1...(𝑦 + 1)) → 1 ≤ 𝑖) |
100 | 99 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 1 ≤ 𝑖) |
101 | 97 | zred 12426 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...(𝑦 + 1)) → 𝑖 ∈ ℝ) |
102 | 101 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 𝑖 ∈ ℝ) |
103 | 77 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → (𝑦 + 1) ∈ ℝ) |
104 | 79 | ad2antrr 723 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 𝑀 ∈ ℝ) |
105 | | elfzle2 13260 |
. . . . . . . . . . . . . . . 16
⊢ (𝑖 ∈ (1...(𝑦 + 1)) → 𝑖 ≤ (𝑦 + 1)) |
106 | 105 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 𝑖 ≤ (𝑦 + 1)) |
107 | | simpll3 1213 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → (𝑦 + 1) ≤ 𝑀) |
108 | 102, 103,
104, 106, 107 | letrd 11132 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 𝑖 ≤ 𝑀) |
109 | 93, 96, 98, 100, 108 | elfzd 13247 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 𝑖 ∈ (1...𝑀)) |
110 | | simplr 766 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → 𝑡 ∈ 𝑇) |
111 | 45 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀)) → (𝐺‘𝑖) ∈ 𝐴) |
112 | 111 | 3adant3 1131 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (𝐺‘𝑖) ∈ 𝐴) |
113 | | simp1 1135 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → 𝜑) |
114 | 113, 112 | jca 512 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴)) |
115 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝐺‘𝑖) → (𝑓 ∈ 𝐴 ↔ (𝐺‘𝑖) ∈ 𝐴)) |
116 | 115 | anbi2d 629 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝐺‘𝑖) → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴))) |
117 | | feq1 6581 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝐺‘𝑖) → (𝑓:𝑇⟶ℝ ↔ (𝐺‘𝑖):𝑇⟶ℝ)) |
118 | 116, 117 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝐺‘𝑖) → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ))) |
119 | 118, 56 | vtoclg 3505 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘𝑖) ∈ 𝐴 → ((𝜑 ∧ (𝐺‘𝑖) ∈ 𝐴) → (𝐺‘𝑖):𝑇⟶ℝ)) |
120 | 112, 114,
119 | sylc 65 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → (𝐺‘𝑖):𝑇⟶ℝ) |
121 | | simp3 1137 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
122 | 120, 121 | ffvelrnd 6962 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
123 | 122 | recnd 11003 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ (1...𝑀) ∧ 𝑡 ∈ 𝑇) → ((𝐺‘𝑖)‘𝑡) ∈ ℂ) |
124 | 92, 109, 110, 123 | syl3anc 1370 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...(𝑦 + 1))) → ((𝐺‘𝑖)‘𝑡) ∈ ℂ) |
125 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑦 + 1) → (𝐺‘𝑖) = (𝐺‘(𝑦 + 1))) |
126 | 125 | fveq1d 6776 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑦 + 1) → ((𝐺‘𝑖)‘𝑡) = ((𝐺‘(𝑦 + 1))‘𝑡)) |
127 | 91, 124, 126 | fsump1 15468 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡) = (Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡) + ((𝐺‘(𝑦 + 1))‘𝑡))) |
128 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑇) |
129 | | fzfid 13693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → (1...𝑦) ∈ Fin) |
130 | | simpll1 1211 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) → 𝜑) |
131 | | 1zzd 12351 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) → 1 ∈ ℤ) |
132 | 95 | ad2antrr 723 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) → 𝑀 ∈ ℤ) |
133 | | elfzelz 13256 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑦) → 𝑖 ∈ ℤ) |
134 | 133 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) → 𝑖 ∈ ℤ) |
135 | | elfzle1 13259 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑖 ∈ (1...𝑦) → 1 ≤ 𝑖) |
136 | 135 | adantl 482 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) → 1 ≤ 𝑖) |
137 | 133 | zred 12426 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 ∈ (1...𝑦) → 𝑖 ∈ ℝ) |
138 | 137 | adantl 482 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) → 𝑖 ∈ ℝ) |
139 | 77 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) → (𝑦 + 1) ∈ ℝ) |
140 | 79 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) → 𝑀 ∈ ℝ) |
141 | 75 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) → 𝑦 ∈ ℝ) |
142 | | elfzle2 13260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 ∈ (1...𝑦) → 𝑖 ≤ 𝑦) |
143 | 142 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) → 𝑖 ≤ 𝑦) |
144 | | letrp1 11819 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑖 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑖 ≤ 𝑦) → 𝑖 ≤ (𝑦 + 1)) |
145 | 138, 141,
143, 144 | syl3anc 1370 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) → 𝑖 ≤ (𝑦 + 1)) |
146 | | simpl3 1192 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) → (𝑦 + 1) ≤ 𝑀) |
147 | 138, 139,
140, 145, 146 | letrd 11132 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑖 ∈ (1...𝑦)) → 𝑖 ≤ 𝑀) |
148 | 147 | adantlr 712 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) → 𝑖 ≤ 𝑀) |
149 | 131, 132,
134, 136, 148 | elfzd 13247 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) → 𝑖 ∈ (1...𝑀)) |
150 | | simplr 766 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) → 𝑡 ∈ 𝑇) |
151 | 130, 149,
150, 122 | syl3anc 1370 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) ∧ 𝑖 ∈ (1...𝑦)) → ((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
152 | 129, 151 | fsumrecl 15446 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡) ∈ ℝ) |
153 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) |
154 | 153 | fvmpt2 6886 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝑇 ∧ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡) ∈ ℝ) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) = Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) |
155 | 128, 152,
154 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → ((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) = Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) |
156 | 155 | oveq1d 7290 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝐺‘(𝑦 + 1))‘𝑡)) = (Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡) + ((𝐺‘(𝑦 + 1))‘𝑡))) |
157 | 127, 156 | eqtr4d 2781 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡) = (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝐺‘(𝑦 + 1))‘𝑡))) |
158 | 89, 157 | mpteq2da 5172 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝐺‘(𝑦 + 1))‘𝑡)))) |
159 | 158 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡)) = (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝐺‘(𝑦 + 1))‘𝑡)))) |
160 | | 1zzd 12351 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → 1 ∈ ℤ) |
161 | | peano2nn 11985 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℕ) |
162 | 161 | nnzd 12425 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → (𝑦 + 1) ∈
ℤ) |
163 | 162 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → (𝑦 + 1) ∈ ℤ) |
164 | 161 | nnge1d 12021 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ℕ → 1 ≤
(𝑦 + 1)) |
165 | 164 | 3ad2ant2 1133 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → 1 ≤ (𝑦 + 1)) |
166 | 160, 95, 163, 165, 81 | elfzd 13247 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → (𝑦 + 1) ∈ (1...𝑀)) |
167 | 45 | ffvelrnda 6961 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑦 + 1) ∈ (1...𝑀)) → (𝐺‘(𝑦 + 1)) ∈ 𝐴) |
168 | 73, 166, 167 | syl2anc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → (𝐺‘(𝑦 + 1)) ∈ 𝐴) |
169 | | eleq1 2826 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑓 = (𝐺‘(𝑦 + 1)) → (𝑓 ∈ 𝐴 ↔ (𝐺‘(𝑦 + 1)) ∈ 𝐴)) |
170 | 169 | anbi2d 629 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝐺‘(𝑦 + 1)) → ((𝜑 ∧ 𝑓 ∈ 𝐴) ↔ (𝜑 ∧ (𝐺‘(𝑦 + 1)) ∈ 𝐴))) |
171 | | feq1 6581 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑓 = (𝐺‘(𝑦 + 1)) → (𝑓:𝑇⟶ℝ ↔ (𝐺‘(𝑦 + 1)):𝑇⟶ℝ)) |
172 | 170, 171 | imbi12d 345 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = (𝐺‘(𝑦 + 1)) → (((𝜑 ∧ 𝑓 ∈ 𝐴) → 𝑓:𝑇⟶ℝ) ↔ ((𝜑 ∧ (𝐺‘(𝑦 + 1)) ∈ 𝐴) → (𝐺‘(𝑦 + 1)):𝑇⟶ℝ))) |
173 | 172, 56 | vtoclg 3505 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐺‘(𝑦 + 1)) ∈ 𝐴 → ((𝜑 ∧ (𝐺‘(𝑦 + 1)) ∈ 𝐴) → (𝐺‘(𝑦 + 1)):𝑇⟶ℝ)) |
174 | 173 | anabsi7 668 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐺‘(𝑦 + 1)) ∈ 𝐴) → (𝐺‘(𝑦 + 1)):𝑇⟶ℝ) |
175 | 73, 168, 174 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → (𝐺‘(𝑦 + 1)):𝑇⟶ℝ) |
176 | 175 | ffvelrnda 6961 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → ((𝐺‘(𝑦 + 1))‘𝑡) ∈ ℝ) |
177 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡)) = (𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡)) |
178 | 177 | fvmpt2 6886 |
. . . . . . . . . . . . 13
⊢ ((𝑡 ∈ 𝑇 ∧ ((𝐺‘(𝑦 + 1))‘𝑡) ∈ ℝ) → ((𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡))‘𝑡) = ((𝐺‘(𝑦 + 1))‘𝑡)) |
179 | 128, 176,
178 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → ((𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡))‘𝑡) = ((𝐺‘(𝑦 + 1))‘𝑡)) |
180 | 179 | oveq2d 7291 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ 𝑡 ∈ 𝑇) → (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡))‘𝑡)) = (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝐺‘(𝑦 + 1))‘𝑡))) |
181 | 89, 180 | mpteq2da 5172 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡))‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝐺‘(𝑦 + 1))‘𝑡)))) |
182 | 181 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡))‘𝑡))) = (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝐺‘(𝑦 + 1))‘𝑡)))) |
183 | | simpl1 1190 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) → 𝜑) |
184 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) |
185 | 166 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) → (𝑦 + 1) ∈ (1...𝑀)) |
186 | 174 | feqmptd 6837 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐺‘(𝑦 + 1)) ∈ 𝐴) → (𝐺‘(𝑦 + 1)) = (𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡))) |
187 | 167, 186 | syldan 591 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 + 1) ∈ (1...𝑀)) → (𝐺‘(𝑦 + 1)) = (𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡))) |
188 | 187, 167 | eqeltrrd 2840 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑦 + 1) ∈ (1...𝑀)) → (𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡)) ∈ 𝐴) |
189 | 183, 185,
188 | syl2anc 584 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡)) ∈ 𝐴) |
190 | | stoweidlem20.5 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐴 ∧ 𝑔 ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ ((𝑓‘𝑡) + (𝑔‘𝑡))) ∈ 𝐴) |
191 | | nfmpt1 5182 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) |
192 | | nfmpt1 5182 |
. . . . . . . . . . 11
⊢
Ⅎ𝑡(𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡)) |
193 | 190, 191,
192 | stoweidlem8 43549 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴 ∧ (𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡))‘𝑡))) ∈ 𝐴) |
194 | 183, 184,
189, 193 | syl3anc 1370 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝑡 ∈ 𝑇 ↦ ((𝐺‘(𝑦 + 1))‘𝑡))‘𝑡))) ∈ 𝐴) |
195 | 182, 194 | eqeltrrd 2840 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ (((𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡))‘𝑡) + ((𝐺‘(𝑦 + 1))‘𝑡))) ∈ 𝐴) |
196 | 159, 195 | eqeltrd 2839 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ ℕ ∧ (𝑦 + 1) ≤ 𝑀) ∧ (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) |
197 | 70, 71, 72, 86, 196 | syl31anc 1372 |
. . . . . 6
⊢ (((𝑦 ∈ ℕ ∧ ((𝜑 ∧ 𝑦 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) ∧ (𝜑 ∧ (𝑦 + 1) ≤ 𝑀)) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) |
198 | 197 | exp31 420 |
. . . . 5
⊢ (𝑦 ∈ ℕ → (((𝜑 ∧ 𝑦 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑦)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) → ((𝜑 ∧ (𝑦 + 1) ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...(𝑦 + 1))((𝐺‘𝑖)‘𝑡)) ∈ 𝐴))) |
199 | 21, 28, 35, 42, 69, 198 | nnind 11991 |
. . . 4
⊢ (𝑛 ∈ ℕ → ((𝜑 ∧ 𝑛 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑛)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴)) |
200 | 14, 199 | vtoclg 3505 |
. . 3
⊢ (𝑀 ∈ ℕ → (𝑀 ∈ ℕ → ((𝜑 ∧ 𝑀 ≤ 𝑀) → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴))) |
201 | 2, 2, 5, 200 | syl3c 66 |
. 2
⊢ (𝜑 → (𝑡 ∈ 𝑇 ↦ Σ𝑖 ∈ (1...𝑀)((𝐺‘𝑖)‘𝑡)) ∈ 𝐴) |
202 | 1, 201 | eqeltrid 2843 |
1
⊢ (𝜑 → 𝐹 ∈ 𝐴) |