| Step | Hyp | Ref
| Expression |
| 1 | | fmul01.6 |
. 2
⊢ (𝜑 → 𝐾 ∈ (𝐿...𝑀)) |
| 2 | | fveq2 6906 |
. . . . . 6
⊢ (𝑘 = 𝐿 → (𝐴‘𝑘) = (𝐴‘𝐿)) |
| 3 | 2 | breq2d 5155 |
. . . . 5
⊢ (𝑘 = 𝐿 → (0 ≤ (𝐴‘𝑘) ↔ 0 ≤ (𝐴‘𝐿))) |
| 4 | 2 | breq1d 5153 |
. . . . 5
⊢ (𝑘 = 𝐿 → ((𝐴‘𝑘) ≤ 1 ↔ (𝐴‘𝐿) ≤ 1)) |
| 5 | 3, 4 | anbi12d 632 |
. . . 4
⊢ (𝑘 = 𝐿 → ((0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1) ↔ (0 ≤ (𝐴‘𝐿) ∧ (𝐴‘𝐿) ≤ 1))) |
| 6 | 5 | imbi2d 340 |
. . 3
⊢ (𝑘 = 𝐿 → ((𝜑 → (0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1)) ↔ (𝜑 → (0 ≤ (𝐴‘𝐿) ∧ (𝐴‘𝐿) ≤ 1)))) |
| 7 | | fveq2 6906 |
. . . . . 6
⊢ (𝑘 = 𝑗 → (𝐴‘𝑘) = (𝐴‘𝑗)) |
| 8 | 7 | breq2d 5155 |
. . . . 5
⊢ (𝑘 = 𝑗 → (0 ≤ (𝐴‘𝑘) ↔ 0 ≤ (𝐴‘𝑗))) |
| 9 | 7 | breq1d 5153 |
. . . . 5
⊢ (𝑘 = 𝑗 → ((𝐴‘𝑘) ≤ 1 ↔ (𝐴‘𝑗) ≤ 1)) |
| 10 | 8, 9 | anbi12d 632 |
. . . 4
⊢ (𝑘 = 𝑗 → ((0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1) ↔ (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1))) |
| 11 | 10 | imbi2d 340 |
. . 3
⊢ (𝑘 = 𝑗 → ((𝜑 → (0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1)) ↔ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)))) |
| 12 | | fveq2 6906 |
. . . . . 6
⊢ (𝑘 = (𝑗 + 1) → (𝐴‘𝑘) = (𝐴‘(𝑗 + 1))) |
| 13 | 12 | breq2d 5155 |
. . . . 5
⊢ (𝑘 = (𝑗 + 1) → (0 ≤ (𝐴‘𝑘) ↔ 0 ≤ (𝐴‘(𝑗 + 1)))) |
| 14 | 12 | breq1d 5153 |
. . . . 5
⊢ (𝑘 = (𝑗 + 1) → ((𝐴‘𝑘) ≤ 1 ↔ (𝐴‘(𝑗 + 1)) ≤ 1)) |
| 15 | 13, 14 | anbi12d 632 |
. . . 4
⊢ (𝑘 = (𝑗 + 1) → ((0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1) ↔ (0 ≤ (𝐴‘(𝑗 + 1)) ∧ (𝐴‘(𝑗 + 1)) ≤ 1))) |
| 16 | 15 | imbi2d 340 |
. . 3
⊢ (𝑘 = (𝑗 + 1) → ((𝜑 → (0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1)) ↔ (𝜑 → (0 ≤ (𝐴‘(𝑗 + 1)) ∧ (𝐴‘(𝑗 + 1)) ≤ 1)))) |
| 17 | | fveq2 6906 |
. . . . . 6
⊢ (𝑘 = 𝐾 → (𝐴‘𝑘) = (𝐴‘𝐾)) |
| 18 | 17 | breq2d 5155 |
. . . . 5
⊢ (𝑘 = 𝐾 → (0 ≤ (𝐴‘𝑘) ↔ 0 ≤ (𝐴‘𝐾))) |
| 19 | 17 | breq1d 5153 |
. . . . 5
⊢ (𝑘 = 𝐾 → ((𝐴‘𝑘) ≤ 1 ↔ (𝐴‘𝐾) ≤ 1)) |
| 20 | 18, 19 | anbi12d 632 |
. . . 4
⊢ (𝑘 = 𝐾 → ((0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1) ↔ (0 ≤ (𝐴‘𝐾) ∧ (𝐴‘𝐾) ≤ 1))) |
| 21 | 20 | imbi2d 340 |
. . 3
⊢ (𝑘 = 𝐾 → ((𝜑 → (0 ≤ (𝐴‘𝑘) ∧ (𝐴‘𝑘) ≤ 1)) ↔ (𝜑 → (0 ≤ (𝐴‘𝐾) ∧ (𝐴‘𝐾) ≤ 1)))) |
| 22 | | fmul01.4 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ∈ ℤ) |
| 23 | | fmul01.5 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘𝐿)) |
| 24 | | eluzelz 12888 |
. . . . . . . . 9
⊢ (𝑀 ∈
(ℤ≥‘𝐿) → 𝑀 ∈ ℤ) |
| 25 | 23, 24 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 26 | 22 | zred 12722 |
. . . . . . . . 9
⊢ (𝜑 → 𝐿 ∈ ℝ) |
| 27 | 26 | leidd 11829 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ≤ 𝐿) |
| 28 | | eluz 12892 |
. . . . . . . . . 10
⊢ ((𝐿 ∈ ℤ ∧ 𝑀 ∈ ℤ) → (𝑀 ∈
(ℤ≥‘𝐿) ↔ 𝐿 ≤ 𝑀)) |
| 29 | 22, 25, 28 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑀 ∈ (ℤ≥‘𝐿) ↔ 𝐿 ≤ 𝑀)) |
| 30 | 23, 29 | mpbid 232 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ≤ 𝑀) |
| 31 | 22, 25, 22, 27, 30 | elfzd 13555 |
. . . . . . 7
⊢ (𝜑 → 𝐿 ∈ (𝐿...𝑀)) |
| 32 | 31 | ancli 548 |
. . . . . . 7
⊢ (𝜑 → (𝜑 ∧ 𝐿 ∈ (𝐿...𝑀))) |
| 33 | | fmul01.2 |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝜑 |
| 34 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑖 𝐿 ∈ (𝐿...𝑀) |
| 35 | 33, 34 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) |
| 36 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑖0 |
| 37 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑖
≤ |
| 38 | | fmul01.1 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖𝐵 |
| 39 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖𝐿 |
| 40 | 38, 39 | nffv 6916 |
. . . . . . . . . 10
⊢
Ⅎ𝑖(𝐵‘𝐿) |
| 41 | 36, 37, 40 | nfbr 5190 |
. . . . . . . . 9
⊢
Ⅎ𝑖0 ≤
(𝐵‘𝐿) |
| 42 | 35, 41 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑖((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝐿)) |
| 43 | | eleq1 2829 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐿 → (𝑖 ∈ (𝐿...𝑀) ↔ 𝐿 ∈ (𝐿...𝑀))) |
| 44 | 43 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑖 = 𝐿 → ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) ↔ (𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)))) |
| 45 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑖 = 𝐿 → (𝐵‘𝑖) = (𝐵‘𝐿)) |
| 46 | 45 | breq2d 5155 |
. . . . . . . . 9
⊢ (𝑖 = 𝐿 → (0 ≤ (𝐵‘𝑖) ↔ 0 ≤ (𝐵‘𝐿))) |
| 47 | 44, 46 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑖 = 𝐿 → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖)) ↔ ((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝐿)))) |
| 48 | | fmul01.8 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖)) |
| 49 | 42, 47, 48 | vtoclg1f 3570 |
. . . . . . 7
⊢ (𝐿 ∈ (𝐿...𝑀) → ((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝐿))) |
| 50 | 31, 32, 49 | sylc 65 |
. . . . . 6
⊢ (𝜑 → 0 ≤ (𝐵‘𝐿)) |
| 51 | | fmul01.3 |
. . . . . . . 8
⊢ 𝐴 = seq𝐿( · , 𝐵) |
| 52 | 51 | fveq1i 6907 |
. . . . . . 7
⊢ (𝐴‘𝐿) = (seq𝐿( · , 𝐵)‘𝐿) |
| 53 | | seq1 14055 |
. . . . . . . 8
⊢ (𝐿 ∈ ℤ → (seq𝐿( · , 𝐵)‘𝐿) = (𝐵‘𝐿)) |
| 54 | 22, 53 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (seq𝐿( · , 𝐵)‘𝐿) = (𝐵‘𝐿)) |
| 55 | 52, 54 | eqtrid 2789 |
. . . . . 6
⊢ (𝜑 → (𝐴‘𝐿) = (𝐵‘𝐿)) |
| 56 | 50, 55 | breqtrrd 5171 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐴‘𝐿)) |
| 57 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑖1 |
| 58 | 40, 37, 57 | nfbr 5190 |
. . . . . . . . 9
⊢
Ⅎ𝑖(𝐵‘𝐿) ≤ 1 |
| 59 | 35, 58 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑖((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → (𝐵‘𝐿) ≤ 1) |
| 60 | 45 | breq1d 5153 |
. . . . . . . . 9
⊢ (𝑖 = 𝐿 → ((𝐵‘𝑖) ≤ 1 ↔ (𝐵‘𝐿) ≤ 1)) |
| 61 | 44, 60 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑖 = 𝐿 → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1) ↔ ((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → (𝐵‘𝐿) ≤ 1))) |
| 62 | | fmul01.9 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1) |
| 63 | 59, 61, 62 | vtoclg1f 3570 |
. . . . . . 7
⊢ (𝐿 ∈ (𝐿...𝑀) → ((𝜑 ∧ 𝐿 ∈ (𝐿...𝑀)) → (𝐵‘𝐿) ≤ 1)) |
| 64 | 31, 32, 63 | sylc 65 |
. . . . . 6
⊢ (𝜑 → (𝐵‘𝐿) ≤ 1) |
| 65 | 55, 64 | eqbrtrd 5165 |
. . . . 5
⊢ (𝜑 → (𝐴‘𝐿) ≤ 1) |
| 66 | 56, 65 | jca 511 |
. . . 4
⊢ (𝜑 → (0 ≤ (𝐴‘𝐿) ∧ (𝐴‘𝐿) ≤ 1)) |
| 67 | 66 | a1i 11 |
. . 3
⊢ (𝑀 ∈
(ℤ≥‘𝐿) → (𝜑 → (0 ≤ (𝐴‘𝐿) ∧ (𝐴‘𝐿) ≤ 1))) |
| 68 | | elfzouz 13703 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝐿..^𝑀) → 𝑗 ∈ (ℤ≥‘𝐿)) |
| 69 | 68 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 𝑗 ∈ (ℤ≥‘𝐿)) |
| 70 | | simpl3 1194 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) ∧ 𝑘 ∈ (𝐿...𝑗)) → 𝜑) |
| 71 | | elfzouz2 13714 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ (𝐿..^𝑀) → 𝑀 ∈ (ℤ≥‘𝑗)) |
| 72 | | fzss2 13604 |
. . . . . . . . . . . . 13
⊢ (𝑀 ∈
(ℤ≥‘𝑗) → (𝐿...𝑗) ⊆ (𝐿...𝑀)) |
| 73 | 71, 72 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (𝐿..^𝑀) → (𝐿...𝑗) ⊆ (𝐿...𝑀)) |
| 74 | 73 | 3ad2ant1 1134 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝐿...𝑗) ⊆ (𝐿...𝑀)) |
| 75 | 74 | sselda 3983 |
. . . . . . . . . 10
⊢ (((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) ∧ 𝑘 ∈ (𝐿...𝑗)) → 𝑘 ∈ (𝐿...𝑀)) |
| 76 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖 𝑘 ∈ (𝐿...𝑀) |
| 77 | 33, 76 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝜑 ∧ 𝑘 ∈ (𝐿...𝑀)) |
| 78 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖𝑘 |
| 79 | 38, 78 | nffv 6916 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖(𝐵‘𝑘) |
| 80 | 79 | nfel1 2922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝐵‘𝑘) ∈ ℝ |
| 81 | 77, 80 | nfim 1896 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖((𝜑 ∧ 𝑘 ∈ (𝐿...𝑀)) → (𝐵‘𝑘) ∈ ℝ) |
| 82 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (𝑖 ∈ (𝐿...𝑀) ↔ 𝑘 ∈ (𝐿...𝑀))) |
| 83 | 82 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) ↔ (𝜑 ∧ 𝑘 ∈ (𝐿...𝑀)))) |
| 84 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑘 → (𝐵‘𝑖) = (𝐵‘𝑘)) |
| 85 | 84 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑘 → ((𝐵‘𝑖) ∈ ℝ ↔ (𝐵‘𝑘) ∈ ℝ)) |
| 86 | 83, 85 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑖 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ 𝑘 ∈ (𝐿...𝑀)) → (𝐵‘𝑘) ∈ ℝ))) |
| 87 | | fmul01.7 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) |
| 88 | 81, 86, 87 | chvarfv 2240 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (𝐿...𝑀)) → (𝐵‘𝑘) ∈ ℝ) |
| 89 | 70, 75, 88 | syl2anc 584 |
. . . . . . . . 9
⊢ (((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) ∧ 𝑘 ∈ (𝐿...𝑗)) → (𝐵‘𝑘) ∈ ℝ) |
| 90 | | remulcl 11240 |
. . . . . . . . . 10
⊢ ((𝑘 ∈ ℝ ∧ 𝑙 ∈ ℝ) → (𝑘 · 𝑙) ∈ ℝ) |
| 91 | 90 | adantl 481 |
. . . . . . . . 9
⊢ (((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) ∧ (𝑘 ∈ ℝ ∧ 𝑙 ∈ ℝ)) → (𝑘 · 𝑙) ∈ ℝ) |
| 92 | 69, 89, 91 | seqcl 14063 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (seq𝐿( · , 𝐵)‘𝑗) ∈ ℝ) |
| 93 | | simp3 1139 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 𝜑) |
| 94 | | fzofzp1 13803 |
. . . . . . . . . 10
⊢ (𝑗 ∈ (𝐿..^𝑀) → (𝑗 + 1) ∈ (𝐿...𝑀)) |
| 95 | 94 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝑗 + 1) ∈ (𝐿...𝑀)) |
| 96 | | nfv 1914 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖(𝑗 + 1) ∈ (𝐿...𝑀) |
| 97 | 33, 96 | nfan 1899 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) |
| 98 | | nfcv 2905 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑖(𝑗 + 1) |
| 99 | 38, 98 | nffv 6916 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖(𝐵‘(𝑗 + 1)) |
| 100 | 99 | nfel1 2922 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖(𝐵‘(𝑗 + 1)) ∈ ℝ |
| 101 | 97, 100 | nfim 1896 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
| 102 | | eleq1 2829 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑗 + 1) → (𝑖 ∈ (𝐿...𝑀) ↔ (𝑗 + 1) ∈ (𝐿...𝑀))) |
| 103 | 102 | anbi2d 630 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 1) → ((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) ↔ (𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)))) |
| 104 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑗 + 1) → (𝐵‘𝑖) = (𝐵‘(𝑗 + 1))) |
| 105 | 104 | eleq1d 2826 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 1) → ((𝐵‘𝑖) ∈ ℝ ↔ (𝐵‘(𝑗 + 1)) ∈ ℝ)) |
| 106 | 103, 105 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 + 1) → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ∈ ℝ) ↔ ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ∈ ℝ))) |
| 107 | 101, 106,
87 | vtoclg1f 3570 |
. . . . . . . . . 10
⊢ ((𝑗 + 1) ∈ (𝐿...𝑀) → ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ∈ ℝ)) |
| 108 | 107 | anabsi7 671 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
| 109 | 93, 95, 108 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝐵‘(𝑗 + 1)) ∈ ℝ) |
| 110 | | pm3.35 803 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1))) → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) |
| 111 | 110 | ancoms 458 |
. . . . . . . . . . 11
⊢ (((𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) |
| 112 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((0 ≤
(𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1) → 0 ≤ (𝐴‘𝑗)) |
| 113 | 111, 112 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (𝐴‘𝑗)) |
| 114 | 113 | 3adant1 1131 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (𝐴‘𝑗)) |
| 115 | 51 | fveq1i 6907 |
. . . . . . . . 9
⊢ (𝐴‘𝑗) = (seq𝐿( · , 𝐵)‘𝑗) |
| 116 | 114, 115 | breqtrdi 5184 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (seq𝐿( · , 𝐵)‘𝑗)) |
| 117 | | simp1 1137 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 𝑗 ∈ (𝐿..^𝑀)) |
| 118 | 94 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐿..^𝑀)) → (𝑗 + 1) ∈ (𝐿...𝑀)) |
| 119 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐿..^𝑀)) → 𝜑) |
| 120 | 119, 118 | jca 511 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐿..^𝑀)) → (𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀))) |
| 121 | 36, 37, 99 | nfbr 5190 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖0 ≤
(𝐵‘(𝑗 + 1)) |
| 122 | 97, 121 | nfim 1896 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘(𝑗 + 1))) |
| 123 | 104 | breq2d 5155 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 1) → (0 ≤ (𝐵‘𝑖) ↔ 0 ≤ (𝐵‘(𝑗 + 1)))) |
| 124 | 103, 123 | imbi12d 344 |
. . . . . . . . . . 11
⊢ (𝑖 = (𝑗 + 1) → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘𝑖)) ↔ ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘(𝑗 + 1))))) |
| 125 | 122, 124,
48 | vtoclg1f 3570 |
. . . . . . . . . 10
⊢ ((𝑗 + 1) ∈ (𝐿...𝑀) → ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → 0 ≤ (𝐵‘(𝑗 + 1)))) |
| 126 | 118, 120,
125 | sylc 65 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝐿..^𝑀)) → 0 ≤ (𝐵‘(𝑗 + 1))) |
| 127 | 93, 117, 126 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (𝐵‘(𝑗 + 1))) |
| 128 | 92, 109, 116, 127 | mulge0d 11840 |
. . . . . . 7
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1)))) |
| 129 | | seqp1 14057 |
. . . . . . . 8
⊢ (𝑗 ∈
(ℤ≥‘𝐿) → (seq𝐿( · , 𝐵)‘(𝑗 + 1)) = ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1)))) |
| 130 | 69, 129 | syl 17 |
. . . . . . 7
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (seq𝐿( · , 𝐵)‘(𝑗 + 1)) = ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1)))) |
| 131 | 128, 130 | breqtrrd 5171 |
. . . . . 6
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (seq𝐿( · , 𝐵)‘(𝑗 + 1))) |
| 132 | 51 | fveq1i 6907 |
. . . . . 6
⊢ (𝐴‘(𝑗 + 1)) = (seq𝐿( · , 𝐵)‘(𝑗 + 1)) |
| 133 | 131, 132 | breqtrrdi 5185 |
. . . . 5
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 0 ≤ (𝐴‘(𝑗 + 1))) |
| 134 | 92, 109 | remulcld 11291 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1))) ∈ ℝ) |
| 135 | | 1red 11262 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → 1 ∈ ℝ) |
| 136 | 93, 95 | jca 511 |
. . . . . . . . . . 11
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀))) |
| 137 | 99, 37, 57 | nfbr 5190 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑖(𝐵‘(𝑗 + 1)) ≤ 1 |
| 138 | 97, 137 | nfim 1896 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑖((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ≤ 1) |
| 139 | 104 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (𝑖 = (𝑗 + 1) → ((𝐵‘𝑖) ≤ 1 ↔ (𝐵‘(𝑗 + 1)) ≤ 1)) |
| 140 | 103, 139 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (𝑖 = (𝑗 + 1) → (((𝜑 ∧ 𝑖 ∈ (𝐿...𝑀)) → (𝐵‘𝑖) ≤ 1) ↔ ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ≤ 1))) |
| 141 | 138, 140,
62 | vtoclg1f 3570 |
. . . . . . . . . . 11
⊢ ((𝑗 + 1) ∈ (𝐿...𝑀) → ((𝜑 ∧ (𝑗 + 1) ∈ (𝐿...𝑀)) → (𝐵‘(𝑗 + 1)) ≤ 1)) |
| 142 | 95, 136, 141 | sylc 65 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝐵‘(𝑗 + 1)) ≤ 1) |
| 143 | 109, 135,
92, 116, 142 | lemul2ad 12208 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1))) ≤ ((seq𝐿( · , 𝐵)‘𝑗) · 1)) |
| 144 | 92 | recnd 11289 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (seq𝐿( · , 𝐵)‘𝑗) ∈ ℂ) |
| 145 | 144 | mulridd 11278 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → ((seq𝐿( · , 𝐵)‘𝑗) · 1) = (seq𝐿( · , 𝐵)‘𝑗)) |
| 146 | 143, 145 | breqtrd 5169 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1))) ≤ (seq𝐿( · , 𝐵)‘𝑗)) |
| 147 | | simp2 1138 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1))) |
| 148 | 110 | simprd 495 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1))) → (𝐴‘𝑗) ≤ 1) |
| 149 | 93, 147, 148 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝐴‘𝑗) ≤ 1) |
| 150 | 115, 149 | eqbrtrrid 5179 |
. . . . . . . 8
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (seq𝐿( · , 𝐵)‘𝑗) ≤ 1) |
| 151 | 134, 92, 135, 146, 150 | letrd 11418 |
. . . . . . 7
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → ((seq𝐿( · , 𝐵)‘𝑗) · (𝐵‘(𝑗 + 1))) ≤ 1) |
| 152 | 130, 151 | eqbrtrd 5165 |
. . . . . 6
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (seq𝐿( · , 𝐵)‘(𝑗 + 1)) ≤ 1) |
| 153 | 132, 152 | eqbrtrid 5178 |
. . . . 5
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (𝐴‘(𝑗 + 1)) ≤ 1) |
| 154 | 133, 153 | jca 511 |
. . . 4
⊢ ((𝑗 ∈ (𝐿..^𝑀) ∧ (𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) ∧ 𝜑) → (0 ≤ (𝐴‘(𝑗 + 1)) ∧ (𝐴‘(𝑗 + 1)) ≤ 1)) |
| 155 | 154 | 3exp 1120 |
. . 3
⊢ (𝑗 ∈ (𝐿..^𝑀) → ((𝜑 → (0 ≤ (𝐴‘𝑗) ∧ (𝐴‘𝑗) ≤ 1)) → (𝜑 → (0 ≤ (𝐴‘(𝑗 + 1)) ∧ (𝐴‘(𝑗 + 1)) ≤ 1)))) |
| 156 | 6, 11, 16, 21, 67, 155 | fzind2 13824 |
. 2
⊢ (𝐾 ∈ (𝐿...𝑀) → (𝜑 → (0 ≤ (𝐴‘𝐾) ∧ (𝐴‘𝐾) ≤ 1))) |
| 157 | 1, 156 | mpcom 38 |
1
⊢ (𝜑 → (0 ≤ (𝐴‘𝐾) ∧ (𝐴‘𝐾) ≤ 1)) |