Step | Hyp | Ref
| Expression |
1 | | fourierdlem63.e |
. . . . 5
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))) |
3 | | id 22 |
. . . . . 6
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → 𝑥 = (𝑆‘(𝐽 + 1))) |
4 | | oveq2 7221 |
. . . . . . . . 9
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1)))) |
5 | 4 | oveq1d 7228 |
. . . . . . . 8
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) |
6 | 5 | fveq2d 6721 |
. . . . . . 7
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))) |
7 | 6 | oveq1d 7228 |
. . . . . 6
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) |
8 | 3, 7 | oveq12d 7231 |
. . . . 5
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))) |
9 | 8 | adantl 485 |
. . . 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 43376 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻))) |
22 | 21 | simpld 498 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁))) |
23 | 22 | simprd 499 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁)) |
24 | 22 | simpld 498 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
25 | 17 | fourierdlem2 43325 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑m
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑m
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) |
27 | 23, 26 | mpbid 235 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∈ (ℝ ↑m
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) |
28 | 27 | simpld 498 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (ℝ ↑m
(0...𝑁))) |
29 | | elmapi 8530 |
. . . . . 6
⊢ (𝑆 ∈ (ℝ
↑m (0...𝑁))
→ 𝑆:(0...𝑁)⟶ℝ) |
30 | 28, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ) |
31 | | fourierdlem63.j |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) |
32 | | fzofzp1 13339 |
. . . . . 6
⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁)) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁)) |
34 | 30, 33 | ffvelrnd 6905 |
. . . 4
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
35 | 11, 12, 13 | fourierdlem11 43334 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) |
36 | 35 | simp2d 1145 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
37 | 36, 34 | resubcld 11260 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ) |
38 | 35 | simp1d 1144 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
39 | 36, 38 | resubcld 11260 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
40 | 10, 39 | eqeltrid 2842 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ ℝ) |
41 | 35 | simp3d 1146 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) |
42 | 38, 36 | posdifd 11419 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
43 | 41, 42 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
44 | 43, 10 | breqtrrdi 5095 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝑇) |
45 | 44 | gt0ne0d 11396 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ≠ 0) |
46 | 37, 40, 45 | redivcld 11660 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ) |
47 | 46 | flcld 13373 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ) |
48 | 47 | zred 12282 |
. . . . . 6
⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ) |
49 | 48, 40 | remulcld 10863 |
. . . . 5
⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ) |
50 | 34, 49 | readdcld 10862 |
. . . 4
⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ) |
51 | 2, 9, 34, 50 | fvmptd 6825 |
. . 3
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))) |
52 | 51, 50 | eqeltrd 2838 |
. 2
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ) |
53 | 11 | fourierdlem2 43325 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
54 | 12, 53 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
55 | 13, 54 | mpbid 235 |
. . . . 5
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑m
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
56 | 55 | simpld 498 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑m
(0...𝑀))) |
57 | | elmapi 8530 |
. . . 4
⊢ (𝑄 ∈ (ℝ
↑m (0...𝑀))
→ 𝑄:(0...𝑀)⟶ℝ) |
58 | 56, 57 | syl 17 |
. . 3
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
59 | | fourierdlem63.k |
. . 3
⊢ (𝜑 → 𝐾 ∈ (0...𝑀)) |
60 | 58, 59 | ffvelrnd 6905 |
. 2
⊢ (𝜑 → (𝑄‘𝐾) ∈ ℝ) |
61 | 14 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ) |
62 | 15 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ) |
63 | 38 | rexrd 10883 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
64 | | iocssre 13015 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴(,]𝐵) ⊆
ℝ) |
65 | 63, 36, 64 | syl2anc 587 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ) |
66 | 38, 36, 41, 10, 1 | fourierdlem4 43327 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵)) |
67 | | fourierdlem63.y |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1)))) |
68 | | elfzofz 13258 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁)) |
69 | 31, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽 ∈ (0...𝑁)) |
70 | 30, 69 | ffvelrnd 6905 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ) |
71 | 34 | rexrd 10883 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈
ℝ*) |
72 | | elico2 12999 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆‘𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ*) →
(𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1))))) |
73 | 70, 71, 72 | syl2anc 587 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1))))) |
74 | 67, 73 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))) |
75 | 74 | simp1d 1144 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ ℝ) |
76 | 66, 75 | ffvelrnd 6905 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸‘𝑌) ∈ (𝐴(,]𝐵)) |
77 | 65, 76 | sseldd 3902 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸‘𝑌) ∈ ℝ) |
78 | 77, 75 | resubcld 11260 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℝ) |
79 | 60, 78 | resubcld 11260 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ) |
80 | 79 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ) |
81 | | icossicc 13024 |
. . . . . . . . . . . . . 14
⊢ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) |
82 | 14 | rexrd 10883 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
83 | 15 | rexrd 10883 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
84 | 17, 24, 23 | fourierdlem15 43338 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷)) |
85 | 82, 83, 84, 31 | fourierdlem8 43331 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷)) |
86 | 81, 85 | sstrid 3912 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷)) |
87 | 86, 67 | sseldd 3902 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ (𝐶[,]𝐷)) |
88 | | elicc2 13000 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))) |
89 | 14, 15, 88 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))) |
90 | 87, 89 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)) |
91 | 90 | simp2d 1145 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ≤ 𝑌) |
92 | 60, 77 | resubcld 11260 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ) |
93 | | fourierdlem63.eyltqk |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾)) |
94 | 77, 60 | posdifd 11419 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸‘𝑌) < (𝑄‘𝐾) ↔ 0 < ((𝑄‘𝐾) − (𝐸‘𝑌)))) |
95 | 93, 94 | mpbid 235 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((𝑄‘𝐾) − (𝐸‘𝑌))) |
96 | 92, 95 | elrpd 12625 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈
ℝ+) |
97 | 75, 96 | ltaddrpd 12661 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 < (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌)))) |
98 | 60 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄‘𝐾) ∈ ℂ) |
99 | 77 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸‘𝑌) ∈ ℂ) |
100 | 75 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ ℂ) |
101 | 98, 99, 100 | subsub3d 11219 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) = (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌))) |
102 | 98, 100 | addcomd 11034 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘𝐾) + 𝑌) = (𝑌 + (𝑄‘𝐾))) |
103 | 102 | oveq1d 7228 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)) = ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌))) |
104 | 100, 98, 99 | addsubassd 11209 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)) = (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌)))) |
105 | 101, 103,
104 | 3eqtrrd 2782 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))) = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
106 | 97, 105 | breqtrd 5079 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
107 | 14, 75, 79, 91, 106 | lelttrd 10990 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
108 | 14, 79, 107 | ltled 10980 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
109 | 108 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
110 | 34 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
111 | 60 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℝ) |
112 | 52, 34 | resubcld 11260 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ) |
113 | 112 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ) |
114 | 111, 113 | resubcld 11260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ) |
115 | 74 | simp3d 1146 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 < (𝑆‘(𝐽 + 1))) |
116 | 75, 34, 115 | ltled 10980 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ≤ (𝑆‘(𝐽 + 1))) |
117 | 38, 36, 41, 10, 1, 75, 34, 116 | fourierdlem7 43330 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸‘𝑌) − 𝑌)) |
118 | 112, 78, 60, 117 | lesub2dd 11449 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))))) |
119 | 118 | adantr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))))) |
120 | 98 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℂ) |
121 | 52 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ) |
122 | 121 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ) |
123 | 110 | recnd 10861 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ) |
124 | 120, 122,
123 | subsubd 11217 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1)))) |
125 | 98, 121 | subcld 11189 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ) |
126 | 34 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ) |
127 | 125, 126 | addcomd 11034 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))))) |
128 | 127 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))))) |
129 | 124, 128 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))))) |
130 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) |
131 | 52 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ) |
132 | 111, 131 | sublt0d 11458 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))) |
133 | 130, 132 | mpbird 260 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0) |
134 | 111, 131 | resubcld 11260 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ) |
135 | | ltaddneg 11047 |
. . . . . . . . . . . . 13
⊢ ((((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))) |
136 | 134, 110,
135 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))) |
137 | 133, 136 | mpbid 235 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))) |
138 | 129, 137 | eqbrtrd 5075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1))) |
139 | 80, 114, 110, 119, 138 | lelttrd 10990 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1))) |
140 | 84, 33 | ffvelrnd 6905 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷)) |
141 | | elicc2 13000 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))) |
142 | 14, 15, 141 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))) |
143 | 140, 142 | mpbid 235 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)) |
144 | 143 | simp3d 1146 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷) |
145 | 144 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷) |
146 | 80, 110, 62, 139, 145 | ltletrd 10992 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < 𝐷) |
147 | 80, 62, 146 | ltled 10980 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ 𝐷) |
148 | 61, 62, 80, 109, 147 | eliccd 42717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷)) |
149 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌) |
150 | | oveq2 7221 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑌 → (𝐵 − 𝑥) = (𝐵 − 𝑌)) |
151 | 150 | oveq1d 7228 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑌 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑌) / 𝑇)) |
152 | 151 | fveq2d 6721 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑌 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑌) / 𝑇))) |
153 | 152 | oveq1d 7228 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) |
154 | 149, 153 | oveq12d 7231 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))) |
155 | 154 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))) |
156 | 36, 75 | resubcld 11260 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐵 − 𝑌) ∈ ℝ) |
157 | 156, 40, 45 | redivcld 11660 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐵 − 𝑌) / 𝑇) ∈ ℝ) |
158 | 157 | flcld 13373 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℤ) |
159 | 158 | zred 12282 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℝ) |
160 | 159, 40 | remulcld 10863 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℝ) |
161 | 75, 160 | readdcld 10862 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) ∈ ℝ) |
162 | 2, 155, 75, 161 | fvmptd 6825 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸‘𝑌) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))) |
163 | 162 | oveq1d 7228 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌)) |
164 | 163 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇)) |
165 | 160 | recnd 10861 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℂ) |
166 | 100, 165 | pncan2d 11191 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) |
167 | 166 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇)) |
168 | 159 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℂ) |
169 | 40 | recnd 10861 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℂ) |
170 | 168, 169,
45 | divcan4d 11614 |
. . . . . . . . . 10
⊢ (𝜑 → (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇))) |
171 | 164, 167,
170 | 3eqtrd 2781 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇))) |
172 | 171, 158 | eqeltrd 2838 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ) |
173 | 78 | recnd 10861 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℂ) |
174 | 173, 169,
45 | divcan1d 11609 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸‘𝑌) − 𝑌)) |
175 | 174 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌))) |
176 | 98, 173 | npcand 11193 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)) = (𝑄‘𝐾)) |
177 | 175, 176 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄‘𝐾)) |
178 | | ffun 6548 |
. . . . . . . . . . 11
⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄) |
179 | 58, 178 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝑄) |
180 | 58 | fdmd 6556 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑄 = (0...𝑀)) |
181 | 59, 180 | eleqtrrd 2841 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ dom 𝑄) |
182 | | fvelrn 6897 |
. . . . . . . . . 10
⊢ ((Fun
𝑄 ∧ 𝐾 ∈ dom 𝑄) → (𝑄‘𝐾) ∈ ran 𝑄) |
183 | 179, 181,
182 | syl2anc 587 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘𝐾) ∈ ran 𝑄) |
184 | 177, 183 | eqeltrd 2838 |
. . . . . . . 8
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) |
185 | | oveq1 7220 |
. . . . . . . . . . 11
⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) |
186 | 185 | oveq2d 7229 |
. . . . . . . . . 10
⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇))) |
187 | 186 | eleq1d 2822 |
. . . . . . . . 9
⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → ((((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)) |
188 | 187 | rspcev 3537 |
. . . . . . . 8
⊢
(((((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄) |
189 | 172, 184,
188 | syl2anc 587 |
. . . . . . 7
⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄) |
190 | 189 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄) |
191 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇))) |
192 | 191 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
193 | 192 | rexbidv 3216 |
. . . . . . 7
⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
194 | 193 | elrab 3602 |
. . . . . 6
⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
195 | 148, 190,
194 | sylanbrc 586 |
. . . . 5
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) |
196 | | elun2 4091 |
. . . . 5
⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
197 | 195, 196 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
198 | | fourierdlem63.x |
. . . 4
⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) |
199 | 197, 198,
18 | 3eltr4g 2855 |
. . 3
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 ∈ 𝐻) |
200 | | elfzelz 13112 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ) |
201 | 200 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ) |
202 | | elfzoelz 13243 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ) |
203 | 31, 202 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℤ) |
204 | 203 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 ∈ ℤ) |
205 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
206 | 21 | simprd 499 |
. . . . . . . . . . . . 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 7135 |
. . . . . . . . . . . 12
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗))) |
211 | 207, 208,
209, 210 | syl12anc 837 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗))) |
212 | 205, 211 | mpbird 260 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 < 𝑗) |
213 | 212 | adantrr 717 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 < 𝑗) |
214 | | simpr 488 |
. . . . . . . . . . 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 7135 |
. . . . . . . . . . . 12
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
219 | 215, 216,
217, 218 | syl12anc 837 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
220 | 214, 219 | mpbird 260 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 < (𝐽 + 1)) |
221 | 220 | adantrl 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1)) |
222 | | btwnnz 12253 |
. . . . . . . . 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 | ffvelrnda 6904 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑆‘𝑗) ∈ ℝ) |
229 | 228 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) ∈ ℝ) |
230 | 74 | simp2d 1145 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆‘𝐽) ≤ 𝑌) |
231 | 230 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ≤ 𝑌) |
232 | 106, 198 | breqtrrdi 5095 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 < 𝑋) |
233 | 232 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < 𝑋) |
234 | | eqcom 2744 |
. . . . . . . . . . . . 13
⊢ (𝑋 = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = 𝑋) |
235 | 234 | biimpri 231 |
. . . . . . . . . . . 12
⊢ ((𝑆‘𝑗) = 𝑋 → 𝑋 = (𝑆‘𝑗)) |
236 | 235 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 = (𝑆‘𝑗)) |
237 | 233, 236 | breqtrd 5079 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗)) |
238 | 237 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗)) |
239 | 226, 227,
229, 231, 238 | lelttrd 10990 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
240 | 239 | adantllr 719 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
241 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) = 𝑋) |
242 | 198, 139 | eqbrtrid 5088 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1))) |
243 | 242 | adantr 484 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1))) |
244 | 241, 243 | eqbrtrd 5075 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
245 | 244 | adantlr 715 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
246 | 240, 245 | jca 515 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
247 | 225, 246 | mtand 816 |
. . . . 5
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆‘𝑗) = 𝑋) |
248 | 247 | nrexdv 3189 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋) |
249 | | isof1o 7132 |
. . . . . . . . 9
⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto→𝐻) |
250 | 206, 249 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻) |
251 | | f1ofo 6668 |
. . . . . . . 8
⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)–onto→𝐻) |
252 | 250, 251 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻) |
253 | | foelrn 6925 |
. . . . . . 7
⊢ ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗)) |
254 | 252, 253 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗)) |
255 | 234 | rexbii 3170 |
. . . . . 6
⊢
(∃𝑗 ∈
(0...𝑁)𝑋 = (𝑆‘𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋) |
256 | 254, 255 | sylib 221 |
. . . . 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 10982 |
1
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾)) |