Step | Hyp | Ref
| Expression |
1 | | fmul01.6 |
. 2
⊢ (𝜑 → 𝐾 ∈ (𝐿...𝑀)) |
2 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝐿 → (𝐴‘𝑘) = (𝐴‘𝐿)) |
3 | 2 | breq2d 4595 |
. . . . 5
⊢ (𝑘 = 𝐿 → (0 ≤ (𝐴‘𝑘) ↔ 0 ≤ (𝐴‘𝐿))) |
4 | 2 | breq1d 4593 |
. . . . 5
⊢ (𝑘 = 𝐿 → ((𝐴‘𝑘) ≤ 1 ↔ (𝐴‘𝐿) ≤ 1)) |
5 | 3, 4 | anbi12d 743 |
. . . 4
⊢ (𝑘 = 𝐿 → ((0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1) ↔ (0 ≤ (𝐴‘𝐿) ∧ (𝐴‘𝐿) ≤ 1))) |
6 | 5 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝐿 → ((𝜑 → (0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1)) ↔ (𝜑 → (0 ≤ (𝐴‘𝐿) ∧ (𝐴‘𝐿) ≤ 1)))) |
7 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗)) |
8 | 7 | breq2d 4595 |
. . . . 5
⊢ (𝑘 = 𝑗 → (0 ≤ (𝐴‘𝑘) ↔ 0 ≤ (𝐴‘𝑗))) |
9 | 7 | breq1d 4593 |
. . . . 5
⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘) ≤ 1 ↔ (𝐴‘𝑗) ≤ 1)) |
10 | 8, 9 | anbi12d 743 |
. . . 4
⊢ (𝑘 = 𝑗 → ((0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1) ↔ (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1))) |
11 | 10 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝑗 → ((𝜑 → (0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1)) ↔ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)))) |
12 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = (𝑗 + 1) → (𝐴‘𝑘) = (𝐴‘(𝑗 + 1))) |
13 | 12 | breq2d 4595 |
. . . . 5
⊢ (𝑘 = (𝑗 + 1) → (0 ≤ (𝐴‘𝑘) ↔ 0 ≤ (𝐴‘(𝑗 + 1)))) |
14 | 12 | breq1d 4593 |
. . . . 5
⊢ (𝑘 = (𝑗 + 1) → ((𝐴‘𝑘) ≤ 1 ↔ (𝐴‘(𝑗 + 1)) ≤ 1)) |
15 | 13, 14 | anbi12d 743 |
. . . 4
⊢ (𝑘 = (𝑗 + 1) → ((0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1) ↔ (0 ≤ (𝐴‘(𝑗 + 1)) ∧ (𝐴‘(𝑗 + 1)) ≤ 1))) |
16 | 15 | imbi2d 329 |
. . 3
⊢ (𝑘 = (𝑗 + 1) → ((𝜑 → (0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1)) ↔ (𝜑 → (0 ≤ (𝐴‘(𝑗 + 1)) ∧ (𝐴‘(𝑗 + 1)) ≤ 1)))) |
17 | | fveq2 6103 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾)) |
18 | 17 | breq2d 4595 |
. . . . 5
⊢ (𝑘 = 𝐾 → (0 ≤ (𝐴‘𝑘) ↔ 0 ≤ (𝐴‘𝐾))) |
19 | 17 | breq1d 4593 |
. . . . 5
⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘) ≤ 1 ↔ (𝐴‘𝐾) ≤ 1)) |
20 | 18, 19 | anbi12d 743 |
. . . 4
⊢ (𝑘 = 𝐾 → ((0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1) ↔ (0 ≤ (𝐴‘𝐾) ∧ (𝐴‘𝐾) ≤ 1))) |
21 | 20 | imbi2d 329 |
. . 3
⊢ (𝑘 = 𝐾 → ((𝜑 → (0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1)) ↔ (𝜑 → (0 ≤ (𝐴‘𝐾) ∧ (𝐴‘𝐾) ≤ 1)))) |
22 | | fmul01.4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ ℤ) |
23 | 22 | zred 11358 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ ℝ) |
24 | 23 | leidd 10473 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ≤ 𝐿) |
25 | | fmul01.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐿)) |
26 | | eluzelz 11573 |
. . . . . . . . . . 11
⊢ (𝑀 ∈
(ℤ≥‘𝐿) → 𝑀 ∈ ℤ) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑀 ∈ ℤ) |
28 | | eluz 11577 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ∈
(ℤ≥‘𝐿) ↔ 𝐿 ≤ 𝑀)) |
29 | 22, 27, 28 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ∈ (ℤ≥‘𝐿) ↔ 𝐿 ≤ 𝑀)) |
30 | 25, 29 | mpbid 221 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ≤ 𝑀) |
31 | | elfz 12203 |
. . . . . . . . 9
⊢ ((𝐿 ∈ ℤ ∧ 𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝐿 ∈ (𝐿...𝑀) ↔ (𝐿 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀))) |
32 | 22, 22, 27, 31 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (𝐿 ∈ (𝐿...𝑀) ↔ (𝐿 ≤ 𝐿 ∧ 𝐿 ≤ 𝑀))) |
33 | 24, 30, 32 | mpbir2and 959 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (𝐿...𝑀)) |
34 | 33 | ancli 572 |
. . . . . . 7
⊢ (𝜑 → (𝜑 ∧ 𝐿 ∈ (𝐿...𝑀))) |
35 | | fmul01.2 |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝜑 |
36 | | nfv 1830 |
. . . . . . . . . 10
⊢
Ⅎ𝑖 𝐿 ∈ (𝐿...𝑀) |
37 | 35, 36 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) |
38 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑖0 |
39 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑖
≤ |
40 | | fmul01.1 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖𝐵 |
41 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖𝐿 |
42 | 40, 41 | nffv 6110 |
. . . . . . . . . 10
⊢
Ⅎ𝑖(𝐵‘𝐿) |
43 | 38, 39, 42 | nfbr 4629 |
. . . . . . . . 9
⊢
Ⅎ𝑖0 ≤
(𝐵‘𝐿) |
44 | 37, 43 | nfim 1813 |
. . . . . . . 8
⊢
Ⅎ𝑖((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝐿)) |
45 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐿 → (𝑖 ∈ (𝐿...𝑀) ↔ 𝐿 ∈ (𝐿...𝑀))) |
46 | 45 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑖 = 𝐿 → ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) ↔ (𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)))) |
47 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐿 → (𝐵‘𝑖) = (𝐵‘𝐿)) |
48 | 47 | breq2d 4595 |
. . . . . . . . 9
⊢ (𝑖 = 𝐿 → (0 ≤ (𝐵‘𝑖) ↔ 0 ≤ (𝐵‘𝐿))) |
49 | 46, 48 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑖 = 𝐿 → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖)) ↔ ((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝐿)))) |
50 | | fmul01.8 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖)) |
51 | 44, 49, 50 | vtoclg1f 3238 |
. . . . . . 7
⊢ (𝐿 ∈ (𝐿...𝑀) → ((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝐿))) |
52 | 33, 34, 51 | sylc 63 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐵‘𝐿)) |
53 | | fmul01.3 |
. . . . . . . 8
⊢ 𝐴 = seq𝐿( · , 𝐵) |
54 | 53 | fveq1i 6104 |
. . . . . . 7
⊢ (𝐴‘𝐿) = (seq𝐿( · , 𝐵)‘𝐿) |
55 | | seq1 12676 |
. . . . . . . 8
⊢ (𝐿 ∈ ℤ → (seq𝐿( · , 𝐵)‘𝐿) = (𝐵‘𝐿)) |
56 | 22, 55 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (seq𝐿( · , 𝐵)‘𝐿) = (𝐵‘𝐿)) |
57 | 54, 56 | syl5eq 2656 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝐿) = (𝐵‘𝐿)) |
58 | 52, 57 | breqtrrd 4611 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐴‘𝐿)) |
59 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑖1 |
60 | 42, 39, 59 | nfbr 4629 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝐵‘𝐿) ≤ 1 |
61 | 37, 60 | nfim 1813 |
. . . . . . . 8
⊢
Ⅎ𝑖((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → (𝐵‘𝐿) ≤ 1) |
62 | 47 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑖 = 𝐿 → ((𝐵‘𝑖) ≤ 1 ↔ (𝐵‘𝐿) ≤ 1)) |
63 | 46, 62 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑖 = 𝐿 → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1) ↔ ((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → (𝐵‘𝐿) ≤ 1))) |
64 | | fmul01.9 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1) |
65 | 61, 63, 64 | vtoclg1f 3238 |
. . . . . . 7
⊢ (𝐿 ∈ (𝐿...𝑀) → ((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → (𝐵‘𝐿) ≤ 1)) |
66 | 33, 34, 65 | sylc 63 |
. . . . . 6
⊢ (𝜑 → (𝐵‘𝐿) ≤ 1) |
67 | 57, 66 | eqbrtrd 4605 |
. . . . 5
⊢ (𝜑 → (𝐴‘𝐿) ≤ 1) |
68 | 58, 67 | jca 553 |
. . . 4
⊢ (𝜑 → (0 ≤ (𝐴‘𝐿) ∧ (𝐴‘𝐿) ≤ 1)) |
69 | 68 | a1i 11 |
. . 3
⊢ (𝑀 ∈
(ℤ≥‘𝐿) → (𝜑 → (0 ≤ (𝐴‘𝐿) ∧ (𝐴‘𝐿) ≤ 1))) |
70 | | elfzouz 12343 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝐿..^𝑀) → 𝑗 ∈ (ℤ≥‘𝐿)) |
71 | 70 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 𝑗 ∈ (ℤ≥‘𝐿)) |
72 | | simpl3 1059 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) ∧ 𝑘 ∈ (𝐿...𝑗)) → 𝜑) |
73 | | elfzouz2 12353 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (𝐿..^𝑀) → 𝑀 ∈ (ℤ≥‘𝑗)) |
74 | | fzss2 12252 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈
(ℤ≥‘𝑗) → (𝐿...𝑗) ⊆ (𝐿...𝑀)) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (𝐿..^𝑀) → (𝐿...𝑗) ⊆ (𝐿...𝑀)) |
76 | 75 | 3ad2ant1 1075 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝐿...𝑗) ⊆ (𝐿...𝑀)) |
77 | 76 | sselda 3568 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) ∧ 𝑘 ∈ (𝐿...𝑗)) → 𝑘 ∈ (𝐿...𝑀)) |
78 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖 𝑘 ∈ (𝐿...𝑀) |
79 | 35, 78 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝜑 ∧ 𝑘 ∈ (𝐿...𝑀)) |
80 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖𝑘 |
81 | 40, 80 | nffv 6110 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖(𝐵‘𝑘) |
82 | 81 | nfel1 2765 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝐵‘𝑘) ∈ ℝ |
83 | 79, 82 | nfim 1813 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖((𝜑 ∧ 𝑘 ∈ (𝐿...𝑀)) → (𝐵‘𝑘) ∈ ℝ) |
84 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (𝑖 ∈ (𝐿...𝑀) ↔ 𝑘 ∈ (𝐿...𝑀))) |
85 | 84 | anbi2d 736 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) ↔ (𝜑 ∧ 𝑘 ∈ (𝐿...𝑀)))) |
86 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (𝐵‘𝑖) = (𝐵‘𝑘)) |
87 | 86 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → ((𝐵‘𝑖) ∈ ℝ ↔ (𝐵‘𝑘) ∈ ℝ)) |
88 | 85, 87 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑘 ∈ (𝐿...𝑀)) → (𝐵‘𝑘) ∈ ℝ))) |
89 | | fmul01.7 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) |
90 | 83, 88, 89 | chvar 2250 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐿...𝑀)) → (𝐵‘𝑘) ∈ ℝ) |
91 | 72, 77, 90 | syl2anc 691 |
. . . . . . . . 9
⊢ (((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) ∧ 𝑘 ∈ (𝐿...𝑗)) → (𝐵‘𝑘) ∈ ℝ) |
92 | | remulcl 9900 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧ 𝑙 ∈ ℝ) → (𝑘 · 𝑙) ∈ ℝ) |
93 | 92 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) ∧ (𝑘 ∈ ℝ ∧ 𝑙 ∈ ℝ)) → (𝑘 · 𝑙) ∈ ℝ) |
94 | 71, 91, 93 | seqcl 12683 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (seq𝐿( · , 𝐵)‘𝑗) ∈ ℝ) |
95 | | simp3 1056 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 𝜑) |
96 | | fzofzp1 12431 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝐿..^𝑀) → (𝑗 + 1) ∈ (𝐿...𝑀)) |
97 | 96 | 3ad2ant1 1075 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝑗 + 1) ∈ (𝐿...𝑀)) |
98 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖(𝑗 + 1) ∈ (𝐿...𝑀) |
99 | 35, 98 | nfan 1816 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) |
100 | | nfcv 2751 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖(𝑗 + 1) |
101 | 40, 100 | nffv 6110 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖(𝐵‘(𝑗 + 1)) |
102 | 101 | nfel1 2765 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝐵‘(𝑗 + 1)) ∈ ℝ |
103 | 99, 102 | nfim 1813 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
104 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑗 + 1) → (𝑖 ∈ (𝐿...𝑀) ↔ (𝑗 + 1) ∈ (𝐿...𝑀))) |
105 | 104 | anbi2d 736 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 1) → ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) ↔ (𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)))) |
106 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑗 + 1) → (𝐵‘𝑖) = (𝐵‘(𝑗 + 1))) |
107 | 106 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 1) → ((𝐵‘𝑖) ∈ ℝ ↔ (𝐵‘(𝑗 + 1)) ∈ ℝ)) |
108 | 105, 107 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 + 1) → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ∈ ℝ))) |
109 | 103, 108,
89 | vtoclg1f 3238 |
. . . . . . . . . 10
⊢ ((𝑗 + 1) ∈ (𝐿...𝑀) → ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ∈ ℝ)) |
110 | 109 | anabsi7 856 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
111 | 95, 97, 110 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
112 | | pm3.35 609 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1))) → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) |
113 | 112 | ancoms 468 |
. . . . . . . . . . 11
⊢ (((𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) |
114 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((0 ≤
(𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1) → 0 ≤ (𝐴‘𝑗)) |
115 | 113, 114 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (𝐴‘𝑗)) |
116 | 115 | 3adant1 1072 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (𝐴‘𝑗)) |
117 | 53 | fveq1i 6104 |
. . . . . . . . 9
⊢ (𝐴‘𝑗) = (seq𝐿( · , 𝐵)‘𝑗) |
118 | 116, 117 | syl6breq 4624 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (seq𝐿( · , 𝐵)‘𝑗)) |
119 | | simp1 1054 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 𝑗 ∈ (𝐿..^𝑀)) |
120 | 96 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐿..^𝑀)) → (𝑗 + 1) ∈ (𝐿...𝑀)) |
121 | | simpl 472 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐿..^𝑀)) → 𝜑) |
122 | 121, 120 | jca 553 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐿..^𝑀)) → (𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀))) |
123 | 38, 39, 101 | nfbr 4629 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖0 ≤
(𝐵‘(𝑗 + 1)) |
124 | 99, 123 | nfim 1813 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘(𝑗 + 1))) |
125 | 106 | breq2d 4595 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 1) → (0 ≤ (𝐵‘𝑖) ↔ 0 ≤ (𝐵‘(𝑗 + 1)))) |
126 | 105, 125 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 + 1) → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖)) ↔ ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘(𝑗 + 1))))) |
127 | 124, 126,
50 | vtoclg1f 3238 |
. . . . . . . . . 10
⊢ ((𝑗 + 1) ∈ (𝐿...𝑀) → ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘(𝑗 + 1)))) |
128 | 120, 122,
127 | sylc 63 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐿..^𝑀)) → 0 ≤ (𝐵‘(𝑗 + 1))) |
129 | 95, 119, 128 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (𝐵‘(𝑗 + 1))) |
130 | 94, 111, 118, 129 | mulge0d 10483 |
. . . . . . 7
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1)))) |
131 | | seqp1 12678 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘𝐿) → (seq𝐿( · , 𝐵)‘(𝑗 + 1)) = ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1)))) |
132 | 71, 131 | syl 17 |
. . . . . . 7
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (seq𝐿( · , 𝐵)‘(𝑗 + 1)) = ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1)))) |
133 | 130, 132 | breqtrrd 4611 |
. . . . . 6
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (seq𝐿( · , 𝐵)‘(𝑗 + 1))) |
134 | 53 | fveq1i 6104 |
. . . . . 6
⊢ (𝐴‘(𝑗 + 1)) = (seq𝐿( · , 𝐵)‘(𝑗 + 1)) |
135 | 133, 134 | syl6breqr 4625 |
. . . . 5
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (𝐴‘(𝑗 + 1))) |
136 | 94, 111 | remulcld 9949 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1))) ∈ ℝ) |
137 | | 1red 9934 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 1 ∈ ℝ) |
138 | 95, 97 | jca 553 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀))) |
139 | 101, 39, 59 | nfbr 4629 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖(𝐵‘(𝑗 + 1)) ≤ 1 |
140 | 99, 139 | nfim 1813 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ≤ 1) |
141 | 106 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑗 + 1) → ((𝐵‘𝑖) ≤ 1 ↔ (𝐵‘(𝑗 + 1)) ≤ 1)) |
142 | 105, 141 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 1) → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1) ↔ ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ≤ 1))) |
143 | 140, 142,
64 | vtoclg1f 3238 |
. . . . . . . . . . 11
⊢ ((𝑗 + 1) ∈ (𝐿...𝑀) → ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ≤ 1)) |
144 | 97, 138, 143 | sylc 63 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝐵‘(𝑗 + 1)) ≤ 1) |
145 | 111, 137,
94, 118, 144 | lemul2ad 10843 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1))) ≤ ((seq𝐿( · , 𝐵)‘𝑗) · 1)) |
146 | 94 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (seq𝐿( · , 𝐵)‘𝑗) ∈ ℂ) |
147 | 146 | mulid1d 9936 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → ((seq𝐿( · , 𝐵)‘𝑗) · 1) = (seq𝐿( · , 𝐵)‘𝑗)) |
148 | 145, 147 | breqtrd 4609 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1))) ≤ (seq𝐿( · , 𝐵)‘𝑗)) |
149 | | simp2 1055 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1))) |
150 | 112 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1))) → (𝐴‘𝑗) ≤ 1) |
151 | 95, 149, 150 | syl2anc 691 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝐴‘𝑗) ≤ 1) |
152 | 117, 151 | syl5eqbrr 4619 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (seq𝐿( · , 𝐵)‘𝑗) ≤ 1) |
153 | 136, 94, 137, 148, 152 | letrd 10073 |
. . . . . . 7
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1))) ≤ 1) |
154 | 132, 153 | eqbrtrd 4605 |
. . . . . 6
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (seq𝐿( · , 𝐵)‘(𝑗 + 1)) ≤ 1) |
155 | 134, 154 | syl5eqbr 4618 |
. . . . 5
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝐴‘(𝑗 + 1)) ≤ 1) |
156 | 135, 155 | jca 553 |
. . . 4
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (0 ≤ (𝐴‘(𝑗 + 1)) ∧ (𝐴‘(𝑗 + 1)) ≤ 1)) |
157 | 156 | 3exp 1256 |
. . 3
⊢ (𝑗 ∈ (𝐿..^𝑀) → ((𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) → (𝜑 → (0 ≤ (𝐴‘(𝑗 + 1)) ∧ (𝐴‘(𝑗 + 1)) ≤ 1)))) |
158 | 6, 11, 16, 21, 69, 157 | fzind2 12448 |
. 2
⊢ (𝐾 ∈ (𝐿...𝑀) → (𝜑 → (0 ≤ (𝐴‘𝐾) ∧ (𝐴‘𝐾) ≤ 1))) |
159 | 1, 158 | mpcom 37 |
1
⊢ (𝜑 → (0 ≤ (𝐴‘𝐾) ∧ (𝐴‘𝐾) ≤ 1)) |