| Step | Hyp | Ref
| Expression |
| 1 | | fourierdlem50.u |
. . 3
⊢ 𝑈 = (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 2 | | fourierdlem50.m |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 3 | | fourierdlem50.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 4 | | fourierdlem50.b |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 5 | | fourierdlem50.altb |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 < 𝐵) |
| 6 | 3, 4, 5 | ltled 11409 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≤ 𝐵) |
| 7 | | fourierdlem50.p |
. . . . . . . . . . . . 13
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝‘𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
| 8 | | fourierdlem50.v |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑉 ∈ (𝑃‘𝑀)) |
| 9 | 7, 2, 8 | fourierdlem15 46137 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋))) |
| 10 | | pire 26500 |
. . . . . . . . . . . . . . . 16
⊢ π
∈ ℝ |
| 11 | 10 | renegcli 11570 |
. . . . . . . . . . . . . . 15
⊢ -π
∈ ℝ |
| 12 | 11 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → -π ∈
ℝ) |
| 13 | | fourierdlem50.xre |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 14 | 12, 13 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (-π + 𝑋) ∈ ℝ) |
| 15 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → π ∈
ℝ) |
| 16 | 15, 13 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (π + 𝑋) ∈ ℝ) |
| 17 | 14, 16 | iccssred 13474 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ) |
| 18 | 9, 17 | fssd 6753 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑉:(0...𝑀)⟶ℝ) |
| 19 | 18 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑉‘𝑖) ∈ ℝ) |
| 20 | 13 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ) |
| 21 | 19, 20 | resubcld 11691 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑉‘𝑖) − 𝑋) ∈ ℝ) |
| 22 | | fourierdlem50.q |
. . . . . . . . 9
⊢ 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋)) |
| 23 | 21, 22 | fmptd 7134 |
. . . . . . . 8
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
| 24 | 22 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))) |
| 25 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 0 → (𝑉‘𝑖) = (𝑉‘0)) |
| 26 | 25 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑖 = 0 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘0) − 𝑋)) |
| 27 | 26 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = 0) → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘0) − 𝑋)) |
| 28 | | nnssnn0 12529 |
. . . . . . . . . . . . . . 15
⊢ ℕ
⊆ ℕ0 |
| 29 | 28 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ℕ ⊆
ℕ0) |
| 30 | | nn0uz 12920 |
. . . . . . . . . . . . . 14
⊢
ℕ0 = (ℤ≥‘0) |
| 31 | 29, 30 | sseqtrdi 4024 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ℕ ⊆
(ℤ≥‘0)) |
| 32 | 31, 2 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑀 ∈
(ℤ≥‘0)) |
| 33 | | eluzfz1 13571 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈
(ℤ≥‘0) → 0 ∈ (0...𝑀)) |
| 34 | 32, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ∈ (0...𝑀)) |
| 35 | 18, 34 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑉‘0) ∈ ℝ) |
| 36 | 35, 13 | resubcld 11691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑉‘0) − 𝑋) ∈ ℝ) |
| 37 | 24, 27, 34, 36 | fvmptd 7023 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄‘0) = ((𝑉‘0) − 𝑋)) |
| 38 | 7 | fourierdlem2 46124 |
. . . . . . . . . . . . . . . 16
⊢ (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))) |
| 39 | 2, 38 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑉 ∈ (𝑃‘𝑀) ↔ (𝑉 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))))) |
| 40 | 8, 39 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑉 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))))) |
| 41 | 40 | simprd 495 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1)))) |
| 42 | 41 | simpld 494 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑉‘0) = (-π + 𝑋) ∧ (𝑉‘𝑀) = (π + 𝑋))) |
| 43 | 42 | simpld 494 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑉‘0) = (-π + 𝑋)) |
| 44 | 43 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑉‘0) − 𝑋) = ((-π + 𝑋) − 𝑋)) |
| 45 | 12 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → -π ∈
ℂ) |
| 46 | 13 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℂ) |
| 47 | 45, 46 | pncand 11621 |
. . . . . . . . . 10
⊢ (𝜑 → ((-π + 𝑋) − 𝑋) = -π) |
| 48 | 37, 44, 47 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘0) = -π) |
| 49 | 12 | rexrd 11311 |
. . . . . . . . . 10
⊢ (𝜑 → -π ∈
ℝ*) |
| 50 | 15 | rexrd 11311 |
. . . . . . . . . 10
⊢ (𝜑 → π ∈
ℝ*) |
| 51 | | fourierdlem50.ab |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴[,]𝐵) ⊆ (-π[,]π)) |
| 52 | 3 | leidd 11829 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 𝐴) |
| 53 | 3, 4, 3, 52, 6 | eliccd 45517 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (𝐴[,]𝐵)) |
| 54 | 51, 53 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ (-π[,]π)) |
| 55 | | iccgelb 13443 |
. . . . . . . . . 10
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐴 ∈ (-π[,]π)) →
-π ≤ 𝐴) |
| 56 | 49, 50, 54, 55 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → -π ≤ 𝐴) |
| 57 | 48, 56 | eqbrtrd 5165 |
. . . . . . . 8
⊢ (𝜑 → (𝑄‘0) ≤ 𝐴) |
| 58 | 4 | leidd 11829 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ≤ 𝐵) |
| 59 | 3, 4, 4, 6, 58 | eliccd 45517 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ (𝐴[,]𝐵)) |
| 60 | 51, 59 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ (-π[,]π)) |
| 61 | | iccleub 13442 |
. . . . . . . . . 10
⊢ ((-π
∈ ℝ* ∧ π ∈ ℝ* ∧ 𝐵 ∈ (-π[,]π)) →
𝐵 ≤
π) |
| 62 | 49, 50, 60, 61 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ≤ π) |
| 63 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑖 = 𝑀 → (𝑉‘𝑖) = (𝑉‘𝑀)) |
| 64 | 63 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝑖 = 𝑀 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑀) − 𝑋)) |
| 65 | 64 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 = 𝑀) → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑀) − 𝑋)) |
| 66 | | eluzfz2 13572 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈
(ℤ≥‘0) → 𝑀 ∈ (0...𝑀)) |
| 67 | 32, 66 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ (0...𝑀)) |
| 68 | 18, 67 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑉‘𝑀) ∈ ℝ) |
| 69 | 68, 13 | resubcld 11691 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑉‘𝑀) − 𝑋) ∈ ℝ) |
| 70 | 24, 65, 67, 69 | fvmptd 7023 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑄‘𝑀) = ((𝑉‘𝑀) − 𝑋)) |
| 71 | 42 | simprd 495 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑉‘𝑀) = (π + 𝑋)) |
| 72 | 71 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑉‘𝑀) − 𝑋) = ((π + 𝑋) − 𝑋)) |
| 73 | 15 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → π ∈
ℂ) |
| 74 | 73, 46 | pncand 11621 |
. . . . . . . . . 10
⊢ (𝜑 → ((π + 𝑋) − 𝑋) = π) |
| 75 | 70, 72, 74 | 3eqtrrd 2782 |
. . . . . . . . 9
⊢ (𝜑 → π = (𝑄‘𝑀)) |
| 76 | 62, 75 | breqtrd 5169 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ≤ (𝑄‘𝑀)) |
| 77 | | fourierdlem50.j |
. . . . . . . 8
⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) |
| 78 | | fourierdlem50.t |
. . . . . . . 8
⊢ 𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) |
| 79 | | prfi 9363 |
. . . . . . . . . . . 12
⊢ {𝐴, 𝐵} ∈ Fin |
| 80 | 79 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐴, 𝐵} ∈ Fin) |
| 81 | | fzfid 14014 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0...𝑀) ∈ Fin) |
| 82 | 22 | rnmptfi 45176 |
. . . . . . . . . . . . 13
⊢
((0...𝑀) ∈ Fin
→ ran 𝑄 ∈
Fin) |
| 83 | 81, 82 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran 𝑄 ∈ Fin) |
| 84 | | infi 9302 |
. . . . . . . . . . . 12
⊢ (ran
𝑄 ∈ Fin → (ran
𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) |
| 85 | 83, 84 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) |
| 86 | | unfi 9211 |
. . . . . . . . . . 11
⊢ (({𝐴, 𝐵} ∈ Fin ∧ (ran 𝑄 ∩ (𝐴(,)𝐵)) ∈ Fin) → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin) |
| 87 | 80, 85, 86 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ∈ Fin) |
| 88 | 78, 87 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ Fin) |
| 89 | 3, 4 | jca 511 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ)) |
| 90 | | prssg 4819 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ)) |
| 91 | 3, 4, 90 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ↔ {𝐴, 𝐵} ⊆ ℝ)) |
| 92 | 89, 91 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → {𝐴, 𝐵} ⊆ ℝ) |
| 93 | | inss2 4238 |
. . . . . . . . . . . . 13
⊢ (ran
𝑄 ∩ (𝐴(,)𝐵)) ⊆ (𝐴(,)𝐵) |
| 94 | | ioossre 13448 |
. . . . . . . . . . . . 13
⊢ (𝐴(,)𝐵) ⊆ ℝ |
| 95 | 93, 94 | sstri 3993 |
. . . . . . . . . . . 12
⊢ (ran
𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ |
| 96 | 95 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (ran 𝑄 ∩ (𝐴(,)𝐵)) ⊆ ℝ) |
| 97 | 92, 96 | unssd 4192 |
. . . . . . . . . 10
⊢ (𝜑 → ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) ⊆ ℝ) |
| 98 | 78, 97 | eqsstrid 4022 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ⊆ ℝ) |
| 99 | | fourierdlem50.s |
. . . . . . . . 9
⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝑇)) |
| 100 | | fourierdlem50.n |
. . . . . . . . 9
⊢ 𝑁 = ((♯‘𝑇) − 1) |
| 101 | 88, 98, 99, 100 | fourierdlem36 46158 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝑇)) |
| 102 | | eqid 2737 |
. . . . . . . 8
⊢
sup({𝑥 ∈
(0..^𝑀) ∣ (𝑄‘𝑥) ≤ (𝑆‘𝐽)}, ℝ, < ) = sup({𝑥 ∈ (0..^𝑀) ∣ (𝑄‘𝑥) ≤ (𝑆‘𝐽)}, ℝ, < ) |
| 103 | 2, 3, 4, 6, 23, 57, 76, 77, 78, 101, 102 | fourierdlem20 46142 |
. . . . . . 7
⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 104 | | fourierdlem50.ch |
. . . . . . . . . . . . 13
⊢ (𝜒 ↔ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))))) |
| 105 | 104 | biimpi 216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))))) |
| 106 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝜑) |
| 107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝜑) |
| 108 | | simplr 769 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0..^𝑀)) |
| 109 | 105, 108 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → 𝑘 ∈ (0..^𝑀)) |
| 110 | 107, 109 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝜑 ∧ 𝑘 ∈ (0..^𝑀))) |
| 111 | | simp-4r 784 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0..^𝑀)) |
| 112 | 105, 111 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → 𝑖 ∈ (0..^𝑀)) |
| 113 | | elfzofz 13715 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ (0..^𝑀) → 𝑘 ∈ (0...𝑀)) |
| 114 | 113 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 ∈ (0...𝑀)) |
| 115 | 105, 114 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → 𝑘 ∈ (0...𝑀)) |
| 116 | 107, 18 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → 𝑉:(0...𝑀)⟶ℝ) |
| 117 | 116, 115 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝑉‘𝑘) ∈ ℝ) |
| 118 | 107, 13 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → 𝑋 ∈ ℝ) |
| 119 | 117, 118 | resubcld 11691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → ((𝑉‘𝑘) − 𝑋) ∈ ℝ) |
| 120 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = 𝑘 → (𝑉‘𝑖) = (𝑉‘𝑘)) |
| 121 | 120 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 = 𝑘 → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘𝑘) − 𝑋)) |
| 122 | 121, 22 | fvmptg 7014 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 ∈ (0...𝑀) ∧ ((𝑉‘𝑘) − 𝑋) ∈ ℝ) → (𝑄‘𝑘) = ((𝑉‘𝑘) − 𝑋)) |
| 123 | 115, 119,
122 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑄‘𝑘) = ((𝑉‘𝑘) − 𝑋)) |
| 124 | 123, 119 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑄‘𝑘) ∈ ℝ) |
| 125 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
| 126 | | fzofzp1 13803 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀)) |
| 127 | 126 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀)) |
| 128 | 125, 127 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
| 129 | 107, 112,
128 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑄‘(𝑖 + 1)) ∈ ℝ) |
| 130 | | isof1o 7343 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) → 𝑆:(0...𝑁)–1-1-onto→𝑇) |
| 131 | 101, 130 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝑇) |
| 132 | | f1of 6848 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑆:(0...𝑁)–1-1-onto→𝑇 → 𝑆:(0...𝑁)⟶𝑇) |
| 133 | 131, 132 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝑆:(0...𝑁)⟶𝑇) |
| 134 | | fzofzp1 13803 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁)) |
| 135 | 77, 134 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁)) |
| 136 | 133, 135 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ 𝑇) |
| 137 | 98, 136 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
| 138 | 107, 137 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
| 139 | | elfzofz 13715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁)) |
| 140 | 77, 139 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐽 ∈ (0...𝑁)) |
| 141 | 133, 140 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑆‘𝐽) ∈ 𝑇) |
| 142 | 98, 141 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ) |
| 143 | 107, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝑆‘𝐽) ∈ ℝ) |
| 144 | 105 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) |
| 145 | 124 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → (𝑄‘𝑘) ∈
ℝ*) |
| 146 | 23 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
| 147 | | fzofzp1 13803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑘 ∈ (0..^𝑀) → (𝑘 + 1) ∈ (0...𝑀)) |
| 148 | 147 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → (𝑘 + 1) ∈ (0...𝑀)) |
| 149 | 146, 148 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈ ℝ) |
| 150 | 149 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) ∈
ℝ*) |
| 151 | 110, 150 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → (𝑄‘(𝑘 + 1)) ∈
ℝ*) |
| 152 | 143 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → (𝑆‘𝐽) ∈
ℝ*) |
| 153 | 138 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → (𝑆‘(𝐽 + 1)) ∈
ℝ*) |
| 154 | | elfzoelz 13699 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ) |
| 155 | 154 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℝ) |
| 156 | 155 | ltp1d 12198 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 < (𝐽 + 1)) |
| 157 | 77, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝐽 < (𝐽 + 1)) |
| 158 | | isoeq5 7341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑇 = ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))) → (𝑆 Isom < , < ((0...𝑁), 𝑇) ↔ 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))))) |
| 159 | 78, 158 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑆 Isom < , < ((0...𝑁), 𝑇) ↔ 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))) |
| 160 | 101, 159 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵))))) |
| 161 | | isorel 7346 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑆 Isom < , < ((0...𝑁), ({𝐴, 𝐵} ∪ (ran 𝑄 ∩ (𝐴(,)𝐵)))) ∧ (𝐽 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))) |
| 162 | 160, 140,
135, 161 | syl12anc 837 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (𝐽 < (𝐽 + 1) ↔ (𝑆‘𝐽) < (𝑆‘(𝐽 + 1)))) |
| 163 | 157, 162 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))) |
| 164 | 107, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → (𝑆‘𝐽) < (𝑆‘(𝐽 + 1))) |
| 165 | 145, 151,
152, 153, 164 | ioossioobi 45530 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1))))) |
| 166 | 144, 165 | mpbid 232 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → ((𝑄‘𝑘) ≤ (𝑆‘𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1)))) |
| 167 | 166 | simpld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝑄‘𝑘) ≤ (𝑆‘𝐽)) |
| 168 | 124, 143,
138, 167, 164 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑄‘𝑘) < (𝑆‘(𝐽 + 1))) |
| 169 | | elfzofz 13715 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀)) |
| 170 | 169 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0...𝑀)) |
| 171 | 170 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑖 ∈ (0...𝑀)) |
| 172 | 105, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → 𝑖 ∈ (0...𝑀)) |
| 173 | 107, 172,
21 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜒 → ((𝑉‘𝑖) − 𝑋) ∈ ℝ) |
| 174 | 22 | fvmpt2 7027 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑖 ∈ (0...𝑀) ∧ ((𝑉‘𝑖) − 𝑋) ∈ ℝ) → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋)) |
| 175 | 172, 173,
174 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (𝑄‘𝑖) = ((𝑉‘𝑖) − 𝑋)) |
| 176 | 175, 173 | eqeltrd 2841 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → (𝑄‘𝑖) ∈ ℝ) |
| 177 | | simpllr 776 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 178 | 105, 177 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 179 | 176, 129,
143, 138, 164, 178 | fourierdlem10 46132 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → ((𝑄‘𝑖) ≤ (𝑆‘𝐽) ∧ (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1)))) |
| 180 | 179 | simprd 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑖 + 1))) |
| 181 | 124, 138,
129, 168, 180 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑄‘𝑘) < (𝑄‘(𝑖 + 1))) |
| 182 | 124, 129,
118, 181 | ltadd2dd 11420 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑋 + (𝑄‘𝑘)) < (𝑋 + (𝑄‘(𝑖 + 1)))) |
| 183 | 123 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑋 + (𝑄‘𝑘)) = (𝑋 + ((𝑉‘𝑘) − 𝑋))) |
| 184 | 107, 46 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → 𝑋 ∈ ℂ) |
| 185 | 117 | recnd 11289 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑉‘𝑘) ∈ ℂ) |
| 186 | 184, 185 | pncan3d 11623 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑋 + ((𝑉‘𝑘) − 𝑋)) = (𝑉‘𝑘)) |
| 187 | 183, 186 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑉‘𝑘) = (𝑋 + (𝑄‘𝑘))) |
| 188 | 112, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝑖 + 1) ∈ (0...𝑀)) |
| 189 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ) |
| 190 | 189, 127 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ) |
| 191 | 107, 112,
190 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℝ) |
| 192 | 191, 118 | resubcld 11691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜒 → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) |
| 193 | 188, 192 | jca 511 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)) |
| 194 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = (𝑖 + 1) → (𝑘 ∈ (0...𝑀) ↔ (𝑖 + 1) ∈ (0...𝑀))) |
| 195 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = (𝑖 + 1) → (𝑉‘𝑘) = (𝑉‘(𝑖 + 1))) |
| 196 | 195 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = (𝑖 + 1) → ((𝑉‘𝑘) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋)) |
| 197 | 196 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = (𝑖 + 1) → (((𝑉‘𝑘) − 𝑋) ∈ ℝ ↔ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)) |
| 198 | 194, 197 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = (𝑖 + 1) → ((𝑘 ∈ (0...𝑀) ∧ ((𝑉‘𝑘) − 𝑋) ∈ ℝ) ↔ ((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ))) |
| 199 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 = (𝑖 + 1) → (𝑄‘𝑘) = (𝑄‘(𝑖 + 1))) |
| 200 | 199, 196 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = (𝑖 + 1) → ((𝑄‘𝑘) = ((𝑉‘𝑘) − 𝑋) ↔ (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))) |
| 201 | 198, 200 | imbi12d 344 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = (𝑖 + 1) → (((𝑘 ∈ (0...𝑀) ∧ ((𝑉‘𝑘) − 𝑋) ∈ ℝ) → (𝑄‘𝑘) = ((𝑉‘𝑘) − 𝑋)) ↔ (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)))) |
| 202 | 201, 122 | vtoclg 3554 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑖 + 1) ∈ (0...𝑀) → (((𝑖 + 1) ∈ (0...𝑀) ∧ ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))) |
| 203 | 188, 193,
202 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋)) |
| 204 | 203 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋))) |
| 205 | 191 | recnd 11289 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑉‘(𝑖 + 1)) ∈ ℂ) |
| 206 | 184, 205 | pncan3d 11623 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1))) |
| 207 | 204, 206 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1)))) |
| 208 | 182, 187,
207 | 3brtr4d 5175 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑉‘𝑘) < (𝑉‘(𝑖 + 1))) |
| 209 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑖 → (𝑙 ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀))) |
| 210 | 209 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑖 → (((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)))) |
| 211 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑖 → (𝑙 + 1) = (𝑖 + 1)) |
| 212 | 211 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑖 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑖 + 1))) |
| 213 | 212 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑖 → ((𝑉‘𝑘) < (𝑉‘(𝑙 + 1)) ↔ (𝑉‘𝑘) < (𝑉‘(𝑖 + 1)))) |
| 214 | 210, 213 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑖 → ((((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘𝑘) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑘) < (𝑉‘(𝑖 + 1))))) |
| 215 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑖 → (𝑉‘𝑙) = (𝑉‘𝑖)) |
| 216 | 215 | breq2d 5155 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑖 → ((𝑉‘𝑘) ≤ (𝑉‘𝑙) ↔ (𝑉‘𝑘) ≤ (𝑉‘𝑖))) |
| 217 | 214, 216 | imbi12d 344 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑖 → (((((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉‘𝑘) ≤ (𝑉‘𝑙)) ↔ ((((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉‘𝑘) ≤ (𝑉‘𝑖)))) |
| 218 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = 𝑘 → (ℎ ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀))) |
| 219 | 218 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = 𝑘 → ((𝜑 ∧ ℎ ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑘 ∈ (0..^𝑀)))) |
| 220 | 219 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = 𝑘 → (((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)))) |
| 221 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = 𝑘 → (𝑉‘ℎ) = (𝑉‘𝑘)) |
| 222 | 221 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = 𝑘 → ((𝑉‘ℎ) < (𝑉‘(𝑙 + 1)) ↔ (𝑉‘𝑘) < (𝑉‘(𝑙 + 1)))) |
| 223 | 220, 222 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = 𝑘 → ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘𝑘) < (𝑉‘(𝑙 + 1))))) |
| 224 | 221 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = 𝑘 → ((𝑉‘ℎ) ≤ (𝑉‘𝑙) ↔ (𝑉‘𝑘) ≤ (𝑉‘𝑙))) |
| 225 | 223, 224 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = 𝑘 → (((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) → (𝑉‘ℎ) ≤ (𝑉‘𝑙)) ↔ ((((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉‘𝑘) ≤ (𝑉‘𝑙)))) |
| 226 | | elfzoelz 13699 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ ∈ (0..^𝑀) → ℎ ∈ ℤ) |
| 227 | 226 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) → ℎ ∈ ℤ) |
| 228 | | elfzoelz 13699 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℤ) |
| 229 | 228 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ ℤ) |
| 230 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ∧ ¬ ℎ < (𝑙 + 1)) → (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) |
| 231 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ) |
| 232 | | fzofzp1 13803 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ (0...𝑀)) |
| 233 | 232 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → (𝑙 + 1) ∈ (0...𝑀)) |
| 234 | 231, 233 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ 𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ) |
| 235 | 234 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) → (𝑉‘(𝑙 + 1)) ∈ ℝ) |
| 236 | 235 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ ℎ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ∈ ℝ) |
| 237 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ℎ ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ) |
| 238 | | elfzofz 13715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℎ ∈ (0..^𝑀) → ℎ ∈ (0...𝑀)) |
| 239 | 238 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝜑 ∧ ℎ ∈ (0..^𝑀)) → ℎ ∈ (0...𝑀)) |
| 240 | 237, 239 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝜑 ∧ ℎ ∈ (0..^𝑀)) → (𝑉‘ℎ) ∈ ℝ) |
| 241 | 240 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ ℎ < (𝑙 + 1)) → (𝑉‘ℎ) ∈ ℝ) |
| 242 | 228 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 ∈ (0..^𝑀) → 𝑙 ∈ ℝ) |
| 243 | | peano2re 11434 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑙 ∈ ℝ → (𝑙 + 1) ∈
ℝ) |
| 244 | 242, 243 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℝ) |
| 245 | 244 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ ℎ < (𝑙 + 1)) → (𝑙 + 1) ∈ ℝ) |
| 246 | 226 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℎ ∈ (0..^𝑀) → ℎ ∈ ℝ) |
| 247 | 246 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ ℎ < (𝑙 + 1)) → ℎ ∈ ℝ) |
| 248 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ ℎ < (𝑙 + 1)) → ¬ ℎ < (𝑙 + 1)) |
| 249 | 245, 247,
248 | nltled 11411 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ ℎ < (𝑙 + 1)) → (𝑙 + 1) ≤ ℎ) |
| 250 | 228 | peano2zd 12725 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑙 ∈ (0..^𝑀) → (𝑙 + 1) ∈ ℤ) |
| 251 | 250 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ℎ) → (𝑙 + 1) ∈ ℤ) |
| 252 | 226 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ℎ) → ℎ ∈ ℤ) |
| 253 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ℎ) → (𝑙 + 1) ≤ ℎ) |
| 254 | | eluz2 12884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ℎ ∈
(ℤ≥‘(𝑙 + 1)) ↔ ((𝑙 + 1) ∈ ℤ ∧ ℎ ∈ ℤ ∧ (𝑙 + 1) ≤ ℎ)) |
| 255 | 251, 252,
253, 254 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ℎ) → ℎ ∈ (ℤ≥‘(𝑙 + 1))) |
| 256 | 255 | adantlll 718 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ℎ) → ℎ ∈ (ℤ≥‘(𝑙 + 1))) |
| 257 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝜑) |
| 258 | | 0zd 12625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 0 ∈ ℤ) |
| 259 | | elfzoel2 13698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (ℎ ∈ (0..^𝑀) → 𝑀 ∈ ℤ) |
| 260 | 259 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑀 ∈ ℤ) |
| 261 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 ∈ ((𝑙 + 1)...ℎ) → 𝑖 ∈ ℤ) |
| 262 | 261 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑖 ∈ ℤ) |
| 263 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 0 ∈ ℝ) |
| 264 | 261 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑖 ∈ ((𝑙 + 1)...ℎ) → 𝑖 ∈ ℝ) |
| 265 | 264 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑖 ∈ ℝ) |
| 266 | 242 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑙 ∈ ℝ) |
| 267 | | elfzole1 13707 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑙 ∈ (0..^𝑀) → 0 ≤ 𝑙) |
| 268 | 267 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 0 ≤ 𝑙) |
| 269 | 266, 243 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → (𝑙 + 1) ∈ ℝ) |
| 270 | 266 | ltp1d 12198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑙 < (𝑙 + 1)) |
| 271 | | elfzle1 13567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑖 ∈ ((𝑙 + 1)...ℎ) → (𝑙 + 1) ≤ 𝑖) |
| 272 | 271 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → (𝑙 + 1) ≤ 𝑖) |
| 273 | 266, 269,
265, 270, 272 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑙 < 𝑖) |
| 274 | 263, 266,
265, 268, 273 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 0 < 𝑖) |
| 275 | 263, 265,
274 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 0 ≤ 𝑖) |
| 276 | 275 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 0 ≤ 𝑖) |
| 277 | 264 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑖 ∈ ℝ) |
| 278 | 259 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (ℎ ∈ (0..^𝑀) → 𝑀 ∈ ℝ) |
| 279 | 278 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑀 ∈ ℝ) |
| 280 | 246 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → ℎ ∈ ℝ) |
| 281 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (𝑖 ∈ ((𝑙 + 1)...ℎ) → 𝑖 ≤ ℎ) |
| 282 | 281 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑖 ≤ ℎ) |
| 283 | | elfzolt2 13708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℎ ∈ (0..^𝑀) → ℎ < 𝑀) |
| 284 | 283 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → ℎ < 𝑀) |
| 285 | 277, 280,
279, 282, 284 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑖 < 𝑀) |
| 286 | 277, 279,
285 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑖 ≤ 𝑀) |
| 287 | 286 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑖 ≤ 𝑀) |
| 288 | 258, 260,
262, 276, 287 | elfzd 13555 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑖 ∈ (0...𝑀)) |
| 289 | 288 | adantlll 718 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → 𝑖 ∈ (0...𝑀)) |
| 290 | 257, 289,
19 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → (𝑉‘𝑖) ∈ ℝ) |
| 291 | 290 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ℎ) ∧ 𝑖 ∈ ((𝑙 + 1)...ℎ)) → (𝑉‘𝑖) ∈ ℝ) |
| 292 | | simplll 775 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝜑) |
| 293 | | 0zd 12625 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 0 ∈
ℤ) |
| 294 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑖 ∈ ((𝑙 + 1)...(ℎ − 1)) → 𝑖 ∈ ℤ) |
| 295 | 294 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑖 ∈ ℤ) |
| 296 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 0 ∈
ℝ) |
| 297 | 295 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑖 ∈ ℝ) |
| 298 | 242 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑙 ∈ ℝ) |
| 299 | 267 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 0 ≤ 𝑙) |
| 300 | 298, 243 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → (𝑙 + 1) ∈ ℝ) |
| 301 | 298 | ltp1d 12198 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑙 < (𝑙 + 1)) |
| 302 | | elfzle1 13567 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (𝑖 ∈ ((𝑙 + 1)...(ℎ − 1)) → (𝑙 + 1) ≤ 𝑖) |
| 303 | 302 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → (𝑙 + 1) ≤ 𝑖) |
| 304 | 298, 300,
297, 301, 303 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑙 < 𝑖) |
| 305 | 296, 298,
297, 299, 304 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 0 < 𝑖) |
| 306 | 296, 297,
305 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 0 ≤ 𝑖) |
| 307 | | eluz2 12884 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑖 ∈
(ℤ≥‘0) ↔ (0 ∈ ℤ ∧ 𝑖 ∈ ℤ ∧ 0 ≤
𝑖)) |
| 308 | 293, 295,
306, 307 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑖 ∈
(ℤ≥‘0)) |
| 309 | 308 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑖 ∈
(ℤ≥‘0)) |
| 310 | | elfzoel2 13698 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℤ) |
| 311 | 310 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑀 ∈ ℤ) |
| 312 | 294 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑖 ∈ ((𝑙 + 1)...(ℎ − 1)) → 𝑖 ∈ ℝ) |
| 313 | 312 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑖 ∈ ℝ) |
| 314 | | peano2rem 11576 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℎ ∈ ℝ → (ℎ − 1) ∈
ℝ) |
| 315 | 246, 314 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (ℎ ∈ (0..^𝑀) → (ℎ − 1) ∈ ℝ) |
| 316 | 315 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → (ℎ − 1) ∈ ℝ) |
| 317 | 278 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑀 ∈ ℝ) |
| 318 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝑖 ∈ ((𝑙 + 1)...(ℎ − 1)) → 𝑖 ≤ (ℎ − 1)) |
| 319 | 318 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑖 ≤ (ℎ − 1)) |
| 320 | 246 | ltm1d 12200 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (ℎ ∈ (0..^𝑀) → (ℎ − 1) < ℎ) |
| 321 | 315, 246,
278, 320, 283 | lttrd 11422 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (ℎ ∈ (0..^𝑀) → (ℎ − 1) < 𝑀) |
| 322 | 321 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → (ℎ − 1) < 𝑀) |
| 323 | 313, 316,
317, 319, 322 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑖 < 𝑀) |
| 324 | 323 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑖 < 𝑀) |
| 325 | 324 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑖 < 𝑀) |
| 326 | | elfzo2 13702 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑖 ∈ (0..^𝑀) ↔ (𝑖 ∈ (ℤ≥‘0)
∧ 𝑀 ∈ ℤ
∧ 𝑖 < 𝑀)) |
| 327 | 309, 311,
325, 326 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → 𝑖 ∈ (0..^𝑀)) |
| 328 | 169, 19 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ∈ ℝ) |
| 329 | 41 | simprd 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉‘𝑖) < (𝑉‘(𝑖 + 1))) |
| 330 | 329 | r19.21bi 3251 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) < (𝑉‘(𝑖 + 1))) |
| 331 | 328, 190,
330 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑉‘𝑖) ≤ (𝑉‘(𝑖 + 1))) |
| 332 | 292, 327,
331 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → (𝑉‘𝑖) ≤ (𝑉‘(𝑖 + 1))) |
| 333 | 332 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ℎ) ∧ 𝑖 ∈ ((𝑙 + 1)...(ℎ − 1))) → (𝑉‘𝑖) ≤ (𝑉‘(𝑖 + 1))) |
| 334 | 256, 291,
333 | monoord 14073 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑙 + 1) ≤ ℎ) → (𝑉‘(𝑙 + 1)) ≤ (𝑉‘ℎ)) |
| 335 | 249, 334 | syldan 591 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ ℎ < (𝑙 + 1)) → (𝑉‘(𝑙 + 1)) ≤ (𝑉‘ℎ)) |
| 336 | 236, 241,
335 | lensymd 11412 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ ¬ ℎ < (𝑙 + 1)) → ¬ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) |
| 337 | 336 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ∧ ¬ ℎ < (𝑙 + 1)) → ¬ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) |
| 338 | 230, 337 | condan 818 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) → ℎ < (𝑙 + 1)) |
| 339 | | zleltp1 12668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℎ ∈ ℤ ∧ 𝑙 ∈ ℤ) → (ℎ ≤ 𝑙 ↔ ℎ < (𝑙 + 1))) |
| 340 | 227, 229,
339 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) → (ℎ ≤ 𝑙 ↔ ℎ < (𝑙 + 1))) |
| 341 | 338, 340 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) → ℎ ≤ 𝑙) |
| 342 | | eluz2 12884 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 ∈
(ℤ≥‘ℎ) ↔ (ℎ ∈ ℤ ∧ 𝑙 ∈ ℤ ∧ ℎ ≤ 𝑙)) |
| 343 | 227, 229,
341, 342 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) → 𝑙 ∈ (ℤ≥‘ℎ)) |
| 344 | 18 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑉:(0...𝑀)⟶ℝ) |
| 345 | | 0zd 12625 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...𝑙)) → 0 ∈ ℤ) |
| 346 | 259 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑀 ∈ ℤ) |
| 347 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑖 ∈ (ℎ...𝑙) → 𝑖 ∈ ℤ) |
| 348 | 347 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑖 ∈ ℤ) |
| 349 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 0 ∈ ℝ) |
| 350 | 246 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → ℎ ∈ ℝ) |
| 351 | 347 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (ℎ...𝑙) → 𝑖 ∈ ℝ) |
| 352 | 351 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑖 ∈ ℝ) |
| 353 | | elfzole1 13707 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ ∈ (0..^𝑀) → 0 ≤ ℎ) |
| 354 | 353 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 0 ≤ ℎ) |
| 355 | | elfzle1 13567 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (ℎ...𝑙) → ℎ ≤ 𝑖) |
| 356 | 355 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → ℎ ≤ 𝑖) |
| 357 | 349, 350,
352, 354, 356 | letrd 11418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 0 ≤ 𝑖) |
| 358 | 357 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...𝑙)) → 0 ≤ 𝑖) |
| 359 | 351 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑖 ∈ ℝ) |
| 360 | 310 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑙 ∈ (0..^𝑀) → 𝑀 ∈ ℝ) |
| 361 | 360 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑀 ∈ ℝ) |
| 362 | 242 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑙 ∈ ℝ) |
| 363 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑖 ∈ (ℎ...𝑙) → 𝑖 ≤ 𝑙) |
| 364 | 363 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑖 ≤ 𝑙) |
| 365 | | elfzolt2 13708 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑙 ∈ (0..^𝑀) → 𝑙 < 𝑀) |
| 366 | 365 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑙 < 𝑀) |
| 367 | 359, 362,
361, 364, 366 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑖 < 𝑀) |
| 368 | 359, 361,
367 | ltled 11409 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑖 ≤ 𝑀) |
| 369 | 368 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑖 ≤ 𝑀) |
| 370 | 345, 346,
348, 358, 369 | elfzd 13555 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((ℎ ∈ (0..^𝑀) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑖 ∈ (0...𝑀)) |
| 371 | 370 | adantlll 718 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...𝑙)) → 𝑖 ∈ (0...𝑀)) |
| 372 | 344, 371 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...𝑙)) → (𝑉‘𝑖) ∈ ℝ) |
| 373 | 372 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (ℎ...𝑙)) → (𝑉‘𝑖) ∈ ℝ) |
| 374 | | simp-4l 783 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝜑) |
| 375 | | 0zd 12625 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 0 ∈
ℤ) |
| 376 | | elfzelz 13564 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ (ℎ...(𝑙 − 1)) → 𝑖 ∈ ℤ) |
| 377 | 376 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 ∈ ℤ) |
| 378 | | 0red 11264 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 0 ∈
ℝ) |
| 379 | 246 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → ℎ ∈ ℝ) |
| 380 | 377 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 ∈ ℝ) |
| 381 | 353 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 0 ≤ ℎ) |
| 382 | | elfzle1 13567 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (ℎ...(𝑙 − 1)) → ℎ ≤ 𝑖) |
| 383 | 382 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → ℎ ≤ 𝑖) |
| 384 | 378, 379,
380, 381, 383 | letrd 11418 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 0 ≤ 𝑖) |
| 385 | 375, 377,
384, 307 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 ∈
(ℤ≥‘0)) |
| 386 | 385 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 ∈
(ℤ≥‘0)) |
| 387 | 386 | ad4ant14 752 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 ∈
(ℤ≥‘0)) |
| 388 | 310 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑀 ∈ ℤ) |
| 389 | 376 | zred 12722 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑖 ∈ (ℎ...(𝑙 − 1)) → 𝑖 ∈ ℝ) |
| 390 | 389 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 ∈ ℝ) |
| 391 | 242 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑙 ∈ ℝ) |
| 392 | 360 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑀 ∈ ℝ) |
| 393 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑖 ∈ (ℎ...(𝑙 − 1)) → 𝑖 ≤ (𝑙 − 1)) |
| 394 | 393 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 ≤ (𝑙 − 1)) |
| 395 | | zltlem1 12670 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑖 ∈ ℤ ∧ 𝑙 ∈ ℤ) → (𝑖 < 𝑙 ↔ 𝑖 ≤ (𝑙 − 1))) |
| 396 | 376, 228,
395 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → (𝑖 < 𝑙 ↔ 𝑖 ≤ (𝑙 − 1))) |
| 397 | 394, 396 | mpbird 257 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 < 𝑙) |
| 398 | 365 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑙 < 𝑀) |
| 399 | 390, 391,
392, 397, 398 | lttrd 11422 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑙 ∈ (0..^𝑀) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 < 𝑀) |
| 400 | 399 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 < 𝑀) |
| 401 | 400 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 < 𝑀) |
| 402 | 387, 388,
401, 326 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → 𝑖 ∈ (0..^𝑀)) |
| 403 | 374, 402,
331 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ∧ 𝑖 ∈ (ℎ...(𝑙 − 1))) → (𝑉‘𝑖) ≤ (𝑉‘(𝑖 + 1))) |
| 404 | 343, 373,
403 | monoord 14073 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) → (𝑉‘ℎ) ≤ (𝑉‘𝑙)) |
| 405 | 225, 404 | chvarvv 1998 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘𝑘) < (𝑉‘(𝑙 + 1))) → (𝑉‘𝑘) ≤ (𝑉‘𝑙)) |
| 406 | 217, 405 | chvarvv 1998 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘𝑘) < (𝑉‘(𝑖 + 1))) → (𝑉‘𝑘) ≤ (𝑉‘𝑖)) |
| 407 | 110, 112,
208, 406 | syl21anc 838 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (𝑉‘𝑘) ≤ (𝑉‘𝑖)) |
| 408 | 107, 112 | jca 511 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝜑 ∧ 𝑖 ∈ (0..^𝑀))) |
| 409 | 110, 149 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑄‘(𝑘 + 1)) ∈ ℝ) |
| 410 | 179 | simpld 494 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝑄‘𝑖) ≤ (𝑆‘𝐽)) |
| 411 | 176, 143,
138, 410, 164 | lelttrd 11419 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑄‘𝑖) < (𝑆‘(𝐽 + 1))) |
| 412 | 166 | simprd 495 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑆‘(𝐽 + 1)) ≤ (𝑄‘(𝑘 + 1))) |
| 413 | 176, 138,
409, 411, 412 | ltletrd 11421 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑄‘𝑖) < (𝑄‘(𝑘 + 1))) |
| 414 | 176, 409,
118, 413 | ltadd2dd 11420 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑋 + (𝑄‘𝑖)) < (𝑋 + (𝑄‘(𝑘 + 1)))) |
| 415 | 175 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑋 + (𝑄‘𝑖)) = (𝑋 + ((𝑉‘𝑖) − 𝑋))) |
| 416 | 107, 172,
19 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝑉‘𝑖) ∈ ℝ) |
| 417 | 416 | recnd 11289 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑉‘𝑖) ∈ ℂ) |
| 418 | 184, 417 | pncan3d 11623 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑋 + ((𝑉‘𝑖) − 𝑋)) = (𝑉‘𝑖)) |
| 419 | 415, 418 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑉‘𝑖) = (𝑋 + (𝑄‘𝑖))) |
| 420 | 22 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉‘𝑖) − 𝑋))) |
| 421 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑖 = (𝑘 + 1) → (𝑉‘𝑖) = (𝑉‘(𝑘 + 1))) |
| 422 | 421 | oveq1d 7446 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑖 = (𝑘 + 1) → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋)) |
| 423 | 422 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) ∧ 𝑖 = (𝑘 + 1)) → ((𝑉‘𝑖) − 𝑋) = ((𝑉‘(𝑘 + 1)) − 𝑋)) |
| 424 | 18 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ) |
| 425 | 424, 148 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → (𝑉‘(𝑘 + 1)) ∈ ℝ) |
| 426 | 13 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ) |
| 427 | 425, 426 | resubcld 11691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → ((𝑉‘(𝑘 + 1)) − 𝑋) ∈ ℝ) |
| 428 | 420, 423,
148, 427 | fvmptd 7023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑘 ∈ (0..^𝑀)) → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋)) |
| 429 | 107, 109,
428 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑄‘(𝑘 + 1)) = ((𝑉‘(𝑘 + 1)) − 𝑋)) |
| 430 | 429 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑋 + (𝑄‘(𝑘 + 1))) = (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋))) |
| 431 | 110, 425 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℝ) |
| 432 | 431 | recnd 11289 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜒 → (𝑉‘(𝑘 + 1)) ∈ ℂ) |
| 433 | 184, 432 | pncan3d 11623 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜒 → (𝑋 + ((𝑉‘(𝑘 + 1)) − 𝑋)) = (𝑉‘(𝑘 + 1))) |
| 434 | 430, 433 | eqtr2d 2778 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜒 → (𝑉‘(𝑘 + 1)) = (𝑋 + (𝑄‘(𝑘 + 1)))) |
| 435 | 414, 419,
434 | 3brtr4d 5175 |
. . . . . . . . . . . . . . . 16
⊢ (𝜒 → (𝑉‘𝑖) < (𝑉‘(𝑘 + 1))) |
| 436 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑘 → (𝑙 ∈ (0..^𝑀) ↔ 𝑘 ∈ (0..^𝑀))) |
| 437 | 436 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑘 → (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)))) |
| 438 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑙 = 𝑘 → (𝑙 + 1) = (𝑘 + 1)) |
| 439 | 438 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑙 = 𝑘 → (𝑉‘(𝑙 + 1)) = (𝑉‘(𝑘 + 1))) |
| 440 | 439 | breq2d 5155 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑘 → ((𝑉‘𝑖) < (𝑉‘(𝑙 + 1)) ↔ (𝑉‘𝑖) < (𝑉‘(𝑘 + 1)))) |
| 441 | 437, 440 | anbi12d 632 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑘 → ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < (𝑉‘(𝑘 + 1))))) |
| 442 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑙 = 𝑘 → (𝑉‘𝑙) = (𝑉‘𝑘)) |
| 443 | 442 | breq2d 5155 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑙 = 𝑘 → ((𝑉‘𝑖) ≤ (𝑉‘𝑙) ↔ (𝑉‘𝑖) ≤ (𝑉‘𝑘))) |
| 444 | 441, 443 | imbi12d 344 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑙 = 𝑘 → (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉‘𝑖) ≤ (𝑉‘𝑙)) ↔ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉‘𝑖) ≤ (𝑉‘𝑘)))) |
| 445 | | eleq1w 2824 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ = 𝑖 → (ℎ ∈ (0..^𝑀) ↔ 𝑖 ∈ (0..^𝑀))) |
| 446 | 445 | anbi2d 630 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = 𝑖 → ((𝜑 ∧ ℎ ∈ (0..^𝑀)) ↔ (𝜑 ∧ 𝑖 ∈ (0..^𝑀)))) |
| 447 | 446 | anbi1d 631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = 𝑖 → (((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ↔ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)))) |
| 448 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ = 𝑖 → (𝑉‘ℎ) = (𝑉‘𝑖)) |
| 449 | 448 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = 𝑖 → ((𝑉‘ℎ) < (𝑉‘(𝑙 + 1)) ↔ (𝑉‘𝑖) < (𝑉‘(𝑙 + 1)))) |
| 450 | 447, 449 | anbi12d 632 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = 𝑖 → ((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) ↔ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < (𝑉‘(𝑙 + 1))))) |
| 451 | 448 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ = 𝑖 → ((𝑉‘ℎ) ≤ (𝑉‘𝑙) ↔ (𝑉‘𝑖) ≤ (𝑉‘𝑙))) |
| 452 | 450, 451 | imbi12d 344 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ = 𝑖 → (((((𝜑 ∧ ℎ ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘ℎ) < (𝑉‘(𝑙 + 1))) → (𝑉‘ℎ) ≤ (𝑉‘𝑙)) ↔ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉‘𝑖) ≤ (𝑉‘𝑙)))) |
| 453 | 452, 404 | chvarvv 1998 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑙 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < (𝑉‘(𝑙 + 1))) → (𝑉‘𝑖) ≤ (𝑉‘𝑙)) |
| 454 | 444, 453 | chvarvv 1998 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑘 ∈ (0..^𝑀)) ∧ (𝑉‘𝑖) < (𝑉‘(𝑘 + 1))) → (𝑉‘𝑖) ≤ (𝑉‘𝑘)) |
| 455 | 408, 109,
435, 454 | syl21anc 838 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → (𝑉‘𝑖) ≤ (𝑉‘𝑘)) |
| 456 | 117, 416 | letri3d 11403 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → ((𝑉‘𝑘) = (𝑉‘𝑖) ↔ ((𝑉‘𝑘) ≤ (𝑉‘𝑖) ∧ (𝑉‘𝑖) ≤ (𝑉‘𝑘)))) |
| 457 | 407, 455,
456 | mpbir2and 713 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → (𝑉‘𝑘) = (𝑉‘𝑖)) |
| 458 | 7, 2, 8 | fourierdlem34 46156 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑉:(0...𝑀)–1-1→ℝ) |
| 459 | 107, 458 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜒 → 𝑉:(0...𝑀)–1-1→ℝ) |
| 460 | | f1fveq 7282 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉:(0...𝑀)–1-1→ℝ ∧ (𝑘 ∈ (0...𝑀) ∧ 𝑖 ∈ (0...𝑀))) → ((𝑉‘𝑘) = (𝑉‘𝑖) ↔ 𝑘 = 𝑖)) |
| 461 | 459, 115,
172, 460 | syl12anc 837 |
. . . . . . . . . . . . . 14
⊢ (𝜒 → ((𝑉‘𝑘) = (𝑉‘𝑖) ↔ 𝑘 = 𝑖)) |
| 462 | 457, 461 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜒 → 𝑘 = 𝑖) |
| 463 | 104, 462 | sylbir 235 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) → 𝑘 = 𝑖) |
| 464 | 463 | ex 412 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))) → 𝑘 = 𝑖)) |
| 465 | | simpl 482 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 466 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑖 → (𝑄‘𝑘) = (𝑄‘𝑖)) |
| 467 | | oveq1 7438 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑖 → (𝑘 + 1) = (𝑖 + 1)) |
| 468 | 467 | fveq2d 6910 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = 𝑖 → (𝑄‘(𝑘 + 1)) = (𝑄‘(𝑖 + 1))) |
| 469 | 466, 468 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑖 → ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))) = ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 470 | 469 | eqcomd 2743 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑖 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) |
| 471 | 470 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) |
| 472 | 465, 471 | sseqtrd 4020 |
. . . . . . . . . . . . 13
⊢ ((((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑘 = 𝑖) → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) |
| 473 | 472 | ex 412 |
. . . . . . . . . . . 12
⊢ (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑘 = 𝑖 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))))) |
| 474 | 473 | ad2antlr 727 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (𝑘 = 𝑖 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))))) |
| 475 | 464, 474 | impbid 212 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑘 ∈ (0..^𝑀)) → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)) |
| 476 | 475 | ralrimiva 3146 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)) |
| 477 | 476 | ex 412 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∀𝑘 ∈ (0..^𝑀)(((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))) |
| 478 | 477 | reximdva 3168 |
. . . . . . 7
⊢ (𝜑 → (∃𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖))) |
| 479 | 103, 478 | mpd 15 |
. . . . . 6
⊢ (𝜑 → ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)) |
| 480 | | reu6 3732 |
. . . . . 6
⊢
(∃!𝑘 ∈
(0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ ∃𝑖 ∈ (0..^𝑀)∀𝑘 ∈ (0..^𝑀)(((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))) ↔ 𝑘 = 𝑖)) |
| 481 | 479, 480 | sylibr 234 |
. . . . 5
⊢ (𝜑 → ∃!𝑘 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) |
| 482 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (𝑄‘𝑖) = (𝑄‘𝑘)) |
| 483 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (𝑖 + 1) = (𝑘 + 1)) |
| 484 | 483 | fveq2d 6910 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑘 + 1))) |
| 485 | 482, 484 | oveq12d 7449 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) |
| 486 | 485 | sseq2d 4016 |
. . . . . 6
⊢ (𝑖 = 𝑘 → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1))))) |
| 487 | 486 | cbvreuvw 3404 |
. . . . 5
⊢
(∃!𝑖 ∈
(0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ∃!𝑘 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑘)(,)(𝑄‘(𝑘 + 1)))) |
| 488 | 481, 487 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∃!𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) |
| 489 | | riotacl 7405 |
. . . 4
⊢
(∃!𝑖 ∈
(0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀)) |
| 490 | 488, 489 | syl 17 |
. . 3
⊢ (𝜑 → (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (0..^𝑀)) |
| 491 | 1, 490 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝑈 ∈ (0..^𝑀)) |
| 492 | 1 | eqcomi 2746 |
. . . 4
⊢
(℩𝑖
∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈 |
| 493 | 492 | a1i 11 |
. . 3
⊢ (𝜑 → (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈) |
| 494 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑖 = 𝑈 → (𝑄‘𝑖) = (𝑄‘𝑈)) |
| 495 | | oveq1 7438 |
. . . . . . . 8
⊢ (𝑖 = 𝑈 → (𝑖 + 1) = (𝑈 + 1)) |
| 496 | 495 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑖 = 𝑈 → (𝑄‘(𝑖 + 1)) = (𝑄‘(𝑈 + 1))) |
| 497 | 494, 496 | oveq12d 7449 |
. . . . . 6
⊢ (𝑖 = 𝑈 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) = ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1)))) |
| 498 | 497 | sseq2d 4016 |
. . . . 5
⊢ (𝑖 = 𝑈 → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1))))) |
| 499 | 498 | riota2 7413 |
. . . 4
⊢ ((𝑈 ∈ (0..^𝑀) ∧ ∃!𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈)) |
| 500 | 491, 488,
499 | syl2anc 584 |
. . 3
⊢ (𝜑 → (((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1))) ↔ (℩𝑖 ∈ (0..^𝑀)((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = 𝑈)) |
| 501 | 493, 500 | mpbird 257 |
. 2
⊢ (𝜑 → ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1)))) |
| 502 | 491, 501 | jca 511 |
1
⊢ (𝜑 → (𝑈 ∈ (0..^𝑀) ∧ ((𝑆‘𝐽)(,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑄‘𝑈)(,)(𝑄‘(𝑈 + 1))))) |