| Step | Hyp | Ref
| Expression |
| 1 | | fourierdlem63.e |
. . . . 5
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
| 2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))) |
| 3 | | id 22 |
. . . . . 6
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → 𝑥 = (𝑆‘(𝐽 + 1))) |
| 4 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1)))) |
| 5 | 4 | oveq1d 7446 |
. . . . . . . 8
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) |
| 6 | 5 | fveq2d 6910 |
. . . . . . 7
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))) |
| 7 | 6 | oveq1d 7446 |
. . . . . 6
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) |
| 8 | 3, 7 | oveq12d 7449 |
. . . . 5
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))) |
| 9 | 8 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = (𝑆‘(𝐽 + 1))) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))) |
| 10 | | fourierdlem63.t |
. . . . . . . . . . 11
⊢ 𝑇 = (𝐵 − 𝐴) |
| 11 | | fourierdlem63.p |
. . . . . . . . . . 11
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
| 12 | | fourierdlem63.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
| 13 | | fourierdlem63.q |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑄 ∈ (𝑃‘𝑀)) |
| 14 | | fourierdlem63.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 15 | | fourierdlem63.d |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℝ) |
| 16 | | fourierdlem63.cltd |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 < 𝐷) |
| 17 | | fourierdlem63.o |
. . . . . . . . . . 11
⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m
(0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝‘𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))}) |
| 18 | | fourierdlem63.h |
. . . . . . . . . . 11
⊢ 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) |
| 19 | | fourierdlem63.n |
. . . . . . . . . . 11
⊢ 𝑁 = ((♯‘𝐻) − 1) |
| 20 | | fourierdlem63.s |
. . . . . . . . . . 11
⊢ 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) |
| 21 | 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20 | fourierdlem54 46175 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻))) |
| 22 | 21 | simpld 494 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁))) |
| 23 | 22 | simprd 495 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁)) |
| 24 | 22 | simpld 494 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 25 | 17 | fourierdlem2 46124 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑m
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) |
| 26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑m
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) |
| 27 | 23, 26 | mpbid 232 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∈ (ℝ ↑m
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) |
| 28 | 27 | simpld 494 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (ℝ ↑m
(0...𝑁))) |
| 29 | | elmapi 8889 |
. . . . . 6
⊢ (𝑆 ∈ (ℝ
↑m (0...𝑁))
→ 𝑆:(0...𝑁)⟶ℝ) |
| 30 | 28, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ) |
| 31 | | fourierdlem63.j |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) |
| 32 | | fzofzp1 13803 |
. . . . . 6
⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁)) |
| 33 | 31, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁)) |
| 34 | 30, 33 | ffvelcdmd 7105 |
. . . 4
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
| 35 | 11, 12, 13 | fourierdlem11 46133 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) |
| 36 | 35 | simp2d 1144 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
| 37 | 36, 34 | resubcld 11691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ) |
| 38 | 35 | simp1d 1143 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 39 | 36, 38 | resubcld 11691 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
| 40 | 10, 39 | eqeltrid 2845 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ ℝ) |
| 41 | 35 | simp3d 1145 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) |
| 42 | 38, 36 | posdifd 11850 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
| 43 | 41, 42 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
| 44 | 43, 10 | breqtrrdi 5185 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝑇) |
| 45 | 44 | gt0ne0d 11827 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ≠ 0) |
| 46 | 37, 40, 45 | redivcld 12095 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ) |
| 47 | 46 | flcld 13838 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ) |
| 48 | 47 | zred 12722 |
. . . . . 6
⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ) |
| 49 | 48, 40 | remulcld 11291 |
. . . . 5
⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ) |
| 50 | 34, 49 | readdcld 11290 |
. . . 4
⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ) |
| 51 | 2, 9, 34, 50 | fvmptd 7023 |
. . 3
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))) |
| 52 | 51, 50 | eqeltrd 2841 |
. 2
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ) |
| 53 | 11 | fourierdlem2 46124 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
| 54 | 12, 53 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
| 55 | 13, 54 | mpbid 232 |
. . . . 5
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
| 56 | 55 | simpld 494 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) |
| 57 | | elmapi 8889 |
. . . 4
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
→ 𝑄:(0...𝑀)⟶ℝ) |
| 58 | 56, 57 | syl 17 |
. . 3
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
| 59 | | fourierdlem63.k |
. . 3
⊢ (𝜑 → 𝐾 ∈ (0...𝑀)) |
| 60 | 58, 59 | ffvelcdmd 7105 |
. 2
⊢ (𝜑 → (𝑄‘𝐾) ∈ ℝ) |
| 61 | 14 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ) |
| 62 | 15 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ) |
| 63 | 38 | rexrd 11311 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
| 64 | | iocssre 13467 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴(,]𝐵) ⊆
ℝ) |
| 65 | 63, 36, 64 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ) |
| 66 | 38, 36, 41, 10, 1 | fourierdlem4 46126 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵)) |
| 67 | | fourierdlem63.y |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1)))) |
| 68 | | elfzofz 13715 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁)) |
| 69 | 31, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽 ∈ (0...𝑁)) |
| 70 | 30, 69 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ) |
| 71 | 34 | rexrd 11311 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈
ℝ*) |
| 72 | | elico2 13451 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆‘𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ*) →
(𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1))))) |
| 73 | 70, 71, 72 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1))))) |
| 74 | 67, 73 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))) |
| 75 | 74 | simp1d 1143 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 76 | 66, 75 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸‘𝑌) ∈ (𝐴(,]𝐵)) |
| 77 | 65, 76 | sseldd 3984 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸‘𝑌) ∈ ℝ) |
| 78 | 77, 75 | resubcld 11691 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℝ) |
| 79 | 60, 78 | resubcld 11691 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ) |
| 80 | 79 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ) |
| 81 | | icossicc 13476 |
. . . . . . . . . . . . . 14
⊢ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) |
| 82 | 14 | rexrd 11311 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
| 83 | 15 | rexrd 11311 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
| 84 | 17, 24, 23 | fourierdlem15 46137 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷)) |
| 85 | 82, 83, 84, 31 | fourierdlem8 46130 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷)) |
| 86 | 81, 85 | sstrid 3995 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷)) |
| 87 | 86, 67 | sseldd 3984 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ (𝐶[,]𝐷)) |
| 88 | | elicc2 13452 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))) |
| 89 | 14, 15, 88 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))) |
| 90 | 87, 89 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)) |
| 91 | 90 | simp2d 1144 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ≤ 𝑌) |
| 92 | 60, 77 | resubcld 11691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ) |
| 93 | | fourierdlem63.eyltqk |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾)) |
| 94 | 77, 60 | posdifd 11850 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸‘𝑌) < (𝑄‘𝐾) ↔ 0 < ((𝑄‘𝐾) − (𝐸‘𝑌)))) |
| 95 | 93, 94 | mpbid 232 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((𝑄‘𝐾) − (𝐸‘𝑌))) |
| 96 | 92, 95 | elrpd 13074 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈
ℝ+) |
| 97 | 75, 96 | ltaddrpd 13110 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 < (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌)))) |
| 98 | 60 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄‘𝐾) ∈ ℂ) |
| 99 | 77 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸‘𝑌) ∈ ℂ) |
| 100 | 75 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ ℂ) |
| 101 | 98, 99, 100 | subsub3d 11650 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) = (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌))) |
| 102 | 98, 100 | addcomd 11463 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘𝐾) + 𝑌) = (𝑌 + (𝑄‘𝐾))) |
| 103 | 102 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)) = ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌))) |
| 104 | 100, 98, 99 | addsubassd 11640 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)) = (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌)))) |
| 105 | 101, 103,
104 | 3eqtrrd 2782 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))) = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
| 106 | 97, 105 | breqtrd 5169 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
| 107 | 14, 75, 79, 91, 106 | lelttrd 11419 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
| 108 | 14, 79, 107 | ltled 11409 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
| 109 | 108 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
| 110 | 34 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
| 111 | 60 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℝ) |
| 112 | 52, 34 | resubcld 11691 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ) |
| 113 | 112 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ) |
| 114 | 111, 113 | resubcld 11691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ) |
| 115 | 74 | simp3d 1145 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 < (𝑆‘(𝐽 + 1))) |
| 116 | 75, 34, 115 | ltled 11409 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ≤ (𝑆‘(𝐽 + 1))) |
| 117 | 38, 36, 41, 10, 1, 75, 34, 116 | fourierdlem7 46129 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸‘𝑌) − 𝑌)) |
| 118 | 112, 78, 60, 117 | lesub2dd 11880 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))))) |
| 119 | 118 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))))) |
| 120 | 98 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℂ) |
| 121 | 52 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ) |
| 122 | 121 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ) |
| 123 | 110 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ) |
| 124 | 120, 122,
123 | subsubd 11648 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1)))) |
| 125 | 98, 121 | subcld 11620 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ) |
| 126 | 34 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ) |
| 127 | 125, 126 | addcomd 11463 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))))) |
| 128 | 127 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))))) |
| 129 | 124, 128 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))))) |
| 130 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) |
| 131 | 52 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ) |
| 132 | 111, 131 | sublt0d 11889 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))) |
| 133 | 130, 132 | mpbird 257 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0) |
| 134 | 111, 131 | resubcld 11691 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ) |
| 135 | | ltaddneg 11477 |
. . . . . . . . . . . . 13
⊢ ((((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))) |
| 136 | 134, 110,
135 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))) |
| 137 | 133, 136 | mpbid 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))) |
| 138 | 129, 137 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1))) |
| 139 | 80, 114, 110, 119, 138 | lelttrd 11419 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1))) |
| 140 | 84, 33 | ffvelcdmd 7105 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷)) |
| 141 | | elicc2 13452 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))) |
| 142 | 14, 15, 141 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))) |
| 143 | 140, 142 | mpbid 232 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)) |
| 144 | 143 | simp3d 1145 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷) |
| 145 | 144 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷) |
| 146 | 80, 110, 62, 139, 145 | ltletrd 11421 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < 𝐷) |
| 147 | 80, 62, 146 | ltled 11409 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ 𝐷) |
| 148 | 61, 62, 80, 109, 147 | eliccd 45517 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷)) |
| 149 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌) |
| 150 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑌 → (𝐵 − 𝑥) = (𝐵 − 𝑌)) |
| 151 | 150 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑌 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑌) / 𝑇)) |
| 152 | 151 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑌 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑌) / 𝑇))) |
| 153 | 152 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) |
| 154 | 149, 153 | oveq12d 7449 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))) |
| 155 | 154 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))) |
| 156 | 36, 75 | resubcld 11691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐵 − 𝑌) ∈ ℝ) |
| 157 | 156, 40, 45 | redivcld 12095 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐵 − 𝑌) / 𝑇) ∈ ℝ) |
| 158 | 157 | flcld 13838 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℤ) |
| 159 | 158 | zred 12722 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℝ) |
| 160 | 159, 40 | remulcld 11291 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℝ) |
| 161 | 75, 160 | readdcld 11290 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) ∈ ℝ) |
| 162 | 2, 155, 75, 161 | fvmptd 7023 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸‘𝑌) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))) |
| 163 | 162 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌)) |
| 164 | 163 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇)) |
| 165 | 160 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℂ) |
| 166 | 100, 165 | pncan2d 11622 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) |
| 167 | 166 | oveq1d 7446 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇)) |
| 168 | 159 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℂ) |
| 169 | 40 | recnd 11289 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℂ) |
| 170 | 168, 169,
45 | divcan4d 12049 |
. . . . . . . . . 10
⊢ (𝜑 → (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇))) |
| 171 | 164, 167,
170 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇))) |
| 172 | 171, 158 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ) |
| 173 | 78 | recnd 11289 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℂ) |
| 174 | 173, 169,
45 | divcan1d 12044 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸‘𝑌) − 𝑌)) |
| 175 | 174 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌))) |
| 176 | 98, 173 | npcand 11624 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)) = (𝑄‘𝐾)) |
| 177 | 175, 176 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄‘𝐾)) |
| 178 | | ffun 6739 |
. . . . . . . . . . 11
⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄) |
| 179 | 58, 178 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝑄) |
| 180 | 58 | fdmd 6746 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑄 = (0...𝑀)) |
| 181 | 59, 180 | eleqtrrd 2844 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ dom 𝑄) |
| 182 | | fvelrn 7096 |
. . . . . . . . . 10
⊢ ((Fun
𝑄 ∧ 𝐾 ∈ dom 𝑄) → (𝑄‘𝐾) ∈ ran 𝑄) |
| 183 | 179, 181,
182 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘𝐾) ∈ ran 𝑄) |
| 184 | 177, 183 | eqeltrd 2841 |
. . . . . . . 8
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) |
| 185 | | oveq1 7438 |
. . . . . . . . . . 11
⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) |
| 186 | 185 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇))) |
| 187 | 186 | eleq1d 2826 |
. . . . . . . . 9
⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → ((((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)) |
| 188 | 187 | rspcev 3622 |
. . . . . . . 8
⊢
(((((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄) |
| 189 | 172, 184,
188 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄) |
| 190 | 189 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄) |
| 191 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇))) |
| 192 | 191 | eleq1d 2826 |
. . . . . . . 8
⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
| 193 | 192 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
| 194 | 193 | elrab 3692 |
. . . . . 6
⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
| 195 | 148, 190,
194 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) |
| 196 | | elun2 4183 |
. . . . 5
⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
| 197 | 195, 196 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
| 198 | | fourierdlem63.x |
. . . 4
⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) |
| 199 | 197, 198,
18 | 3eltr4g 2858 |
. . 3
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 ∈ 𝐻) |
| 200 | | elfzelz 13564 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ) |
| 201 | 200 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ) |
| 202 | | elfzoelz 13699 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ) |
| 203 | 31, 202 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℤ) |
| 204 | 203 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 ∈ ℤ) |
| 205 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
| 206 | 21 | simprd 495 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻)) |
| 207 | 206 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝐻)) |
| 208 | 69 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 ∈ (0...𝑁)) |
| 209 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑗 ∈ (0...𝑁)) |
| 210 | | isorel 7346 |
. . . . . . . . . . . 12
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗))) |
| 211 | 207, 208,
209, 210 | syl12anc 837 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗))) |
| 212 | 205, 211 | mpbird 257 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 < 𝑗) |
| 213 | 212 | adantrr 717 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 < 𝑗) |
| 214 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
| 215 | 206 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑆 Isom < , < ((0...𝑁), 𝐻)) |
| 216 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 ∈ (0...𝑁)) |
| 217 | 33 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝐽 + 1) ∈ (0...𝑁)) |
| 218 | | isorel 7346 |
. . . . . . . . . . . 12
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
| 219 | 215, 216,
217, 218 | syl12anc 837 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
| 220 | 214, 219 | mpbird 257 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 < (𝐽 + 1)) |
| 221 | 220 | adantrl 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1)) |
| 222 | | btwnnz 12694 |
. . . . . . . . 9
⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ) |
| 223 | 204, 213,
221, 222 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → ¬ 𝑗 ∈ ℤ) |
| 224 | 201, 223 | pm2.65da 817 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
| 225 | 224 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
| 226 | 70 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ∈ ℝ) |
| 227 | 75 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 ∈ ℝ) |
| 228 | 30 | ffvelcdmda 7104 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑆‘𝑗) ∈ ℝ) |
| 229 | 228 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) ∈ ℝ) |
| 230 | 74 | simp2d 1144 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆‘𝐽) ≤ 𝑌) |
| 231 | 230 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ≤ 𝑌) |
| 232 | 106, 198 | breqtrrdi 5185 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 < 𝑋) |
| 233 | 232 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < 𝑋) |
| 234 | | eqcom 2744 |
. . . . . . . . . . . . 13
⊢ (𝑋 = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = 𝑋) |
| 235 | 234 | biimpri 228 |
. . . . . . . . . . . 12
⊢ ((𝑆‘𝑗) = 𝑋 → 𝑋 = (𝑆‘𝑗)) |
| 236 | 235 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 = (𝑆‘𝑗)) |
| 237 | 233, 236 | breqtrd 5169 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗)) |
| 238 | 237 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗)) |
| 239 | 226, 227,
229, 231, 238 | lelttrd 11419 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
| 240 | 239 | adantllr 719 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
| 241 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) = 𝑋) |
| 242 | 198, 139 | eqbrtrid 5178 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1))) |
| 243 | 242 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1))) |
| 244 | 241, 243 | eqbrtrd 5165 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
| 245 | 244 | adantlr 715 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
| 246 | 240, 245 | jca 511 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
| 247 | 225, 246 | mtand 816 |
. . . . 5
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆‘𝑗) = 𝑋) |
| 248 | 247 | nrexdv 3149 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋) |
| 249 | | isof1o 7343 |
. . . . . . . . 9
⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto→𝐻) |
| 250 | 206, 249 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻) |
| 251 | | f1ofo 6855 |
. . . . . . . 8
⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)–onto→𝐻) |
| 252 | 250, 251 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻) |
| 253 | | foelrn 7127 |
. . . . . . 7
⊢ ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗)) |
| 254 | 252, 253 | sylan 580 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗)) |
| 255 | 234 | rexbii 3094 |
. . . . . 6
⊢
(∃𝑗 ∈
(0...𝑁)𝑋 = (𝑆‘𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋) |
| 256 | 254, 255 | sylib 218 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋) |
| 257 | 256 | adantlr 715 |
. . . 4
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋) |
| 258 | 248, 257 | mtand 816 |
. . 3
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ 𝑋 ∈ 𝐻) |
| 259 | 199, 258 | pm2.65da 817 |
. 2
⊢ (𝜑 → ¬ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) |
| 260 | 52, 60, 259 | nltled 11411 |
1
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾)) |