Step | Hyp | Ref
| Expression |
1 | | fourierdlem63.e |
. . . . 5
⊢ 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇))) |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝜑 → 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)))) |
3 | | id 22 |
. . . . . 6
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → 𝑥 = (𝑆‘(𝐽 + 1))) |
4 | | oveq2 6658 |
. . . . . . . . 9
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵 − 𝑥) = (𝐵 − (𝑆‘(𝐽 + 1)))) |
5 | 4 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) |
6 | 5 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))) |
7 | 6 | oveq1d 6665 |
. . . . . 6
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) |
8 | 3, 7 | oveq12d 6668 |
. . . . 5
⊢ (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))) |
9 | 8 | adantl 482 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 = (𝑆‘(𝐽 + 1))) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))) |
10 | | fourierdlem63.t |
. . . . . . . . . . 11
⊢ 𝑇 = (𝐵 − 𝐴) |
11 | | fourierdlem63.p |
. . . . . . . . . . 11
⊢ 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚
(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
⊢ 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚
(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 40377 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻))) |
22 | 21 | simpld 475 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂‘𝑁))) |
23 | 22 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → 𝑆 ∈ (𝑂‘𝑁)) |
24 | 22 | simpld 475 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℕ) |
25 | 17 | fourierdlem2 40326 |
. . . . . . . . 9
⊢ (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) |
26 | 24, 25 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝑆 ∈ (𝑂‘𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))))) |
27 | 23, 26 | mpbid 222 |
. . . . . . 7
⊢ (𝜑 → (𝑆 ∈ (ℝ ↑𝑚
(0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆‘𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆‘𝑖) < (𝑆‘(𝑖 + 1))))) |
28 | 27 | simpld 475 |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ (ℝ ↑𝑚
(0...𝑁))) |
29 | | elmapi 7879 |
. . . . . 6
⊢ (𝑆 ∈ (ℝ
↑𝑚 (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ) |
30 | 28, 29 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆:(0...𝑁)⟶ℝ) |
31 | | fourierdlem63.j |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ (0..^𝑁)) |
32 | | fzofzp1 12565 |
. . . . . 6
⊢ (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁)) |
33 | 31, 32 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝐽 + 1) ∈ (0...𝑁)) |
34 | 30, 33 | ffvelrnd 6360 |
. . . 4
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
35 | 11, 12, 13 | fourierdlem11 40335 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵)) |
36 | 35 | simp2d 1074 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) |
37 | 36, 34 | resubcld 10458 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ) |
38 | 35 | simp1d 1073 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
39 | 36, 38 | resubcld 10458 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 − 𝐴) ∈ ℝ) |
40 | 10, 39 | syl5eqel 2705 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ∈ ℝ) |
41 | 35 | simp3d 1075 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 < 𝐵) |
42 | 38, 36 | posdifd 10614 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵 − 𝐴))) |
43 | 41, 42 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 < (𝐵 − 𝐴)) |
44 | 43, 10 | syl6breqr 4695 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < 𝑇) |
45 | 44 | gt0ne0d 10592 |
. . . . . . . . 9
⊢ (𝜑 → 𝑇 ≠ 0) |
46 | 37, 40, 45 | redivcld 10853 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ) |
47 | 46 | flcld 12599 |
. . . . . . 7
⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ) |
48 | 47 | zred 11482 |
. . . . . 6
⊢ (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ) |
49 | 48, 40 | remulcld 10070 |
. . . . 5
⊢ (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ) |
50 | 34, 49 | readdcld 10069 |
. . . 4
⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ) |
51 | 2, 9, 34, 50 | fvmptd 6288 |
. . 3
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))) |
52 | 51, 50 | eqeltrd 2701 |
. 2
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ) |
53 | 11 | fourierdlem2 40326 |
. . . . . . 7
⊢ (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
54 | 12, 53 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))) |
55 | 13, 54 | mpbid 222 |
. . . . 5
⊢ (𝜑 → (𝑄 ∈ (ℝ ↑𝑚
(0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))) |
56 | 55 | simpld 475 |
. . . 4
⊢ (𝜑 → 𝑄 ∈ (ℝ ↑𝑚
(0...𝑀))) |
57 | | elmapi 7879 |
. . . 4
⊢ (𝑄 ∈ (ℝ
↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ) |
58 | 56, 57 | syl 17 |
. . 3
⊢ (𝜑 → 𝑄:(0...𝑀)⟶ℝ) |
59 | | fourierdlem63.k |
. . 3
⊢ (𝜑 → 𝐾 ∈ (0...𝑀)) |
60 | 58, 59 | ffvelrnd 6360 |
. 2
⊢ (𝜑 → (𝑄‘𝐾) ∈ ℝ) |
61 | 14 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ) |
62 | 15 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ) |
63 | 38 | rexrd 10089 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
64 | | iocssre 12253 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ ℝ*
∧ 𝐵 ∈ ℝ)
→ (𝐴(,]𝐵) ⊆
ℝ) |
65 | 63, 36, 64 | syl2anc 693 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴(,]𝐵) ⊆ ℝ) |
66 | 38, 36, 41, 10, 1 | fourierdlem4 40328 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸:ℝ⟶(𝐴(,]𝐵)) |
67 | | fourierdlem63.y |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1)))) |
68 | | elfzofz 12485 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁)) |
69 | 31, 68 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐽 ∈ (0...𝑁)) |
70 | 30, 69 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆‘𝐽) ∈ ℝ) |
71 | 34 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈
ℝ*) |
72 | | elico2 12237 |
. . . . . . . . . . . . . . 15
⊢ (((𝑆‘𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ*) →
(𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1))))) |
73 | 70, 71, 72 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌 ∈ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1))))) |
74 | 67, 73 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆‘𝐽) ≤ 𝑌 ∧ 𝑌 < (𝑆‘(𝐽 + 1)))) |
75 | 74 | simp1d 1073 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ ℝ) |
76 | 66, 75 | ffvelrnd 6360 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐸‘𝑌) ∈ (𝐴(,]𝐵)) |
77 | 65, 76 | sseldd 3604 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐸‘𝑌) ∈ ℝ) |
78 | 77, 75 | resubcld 10458 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℝ) |
79 | 60, 78 | resubcld 10458 |
. . . . . . . 8
⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ) |
80 | 79 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ℝ) |
81 | | icossicc 12260 |
. . . . . . . . . . . . . 14
⊢ ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) |
82 | 14 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈
ℝ*) |
83 | 15 | rexrd 10089 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐷 ∈
ℝ*) |
84 | 17, 24, 23 | fourierdlem15 40339 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆:(0...𝑁)⟶(𝐶[,]𝐷)) |
85 | 82, 83, 84, 31 | fourierdlem8 40332 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑆‘𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷)) |
86 | 81, 85 | syl5ss 3614 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑆‘𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷)) |
87 | 86, 67 | sseldd 3604 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ (𝐶[,]𝐷)) |
88 | | elicc2 12238 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))) |
89 | 14, 15, 88 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷))) |
90 | 87, 89 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶 ≤ 𝑌 ∧ 𝑌 ≤ 𝐷)) |
91 | 90 | simp2d 1074 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ≤ 𝑌) |
92 | 60, 77 | resubcld 10458 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈ ℝ) |
93 | | fourierdlem63.eyltqk |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸‘𝑌) < (𝑄‘𝐾)) |
94 | 77, 60 | posdifd 10614 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐸‘𝑌) < (𝑄‘𝐾) ↔ 0 < ((𝑄‘𝐾) − (𝐸‘𝑌)))) |
95 | 93, 94 | mpbid 222 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 < ((𝑄‘𝐾) − (𝐸‘𝑌))) |
96 | 92, 95 | elrpd 11869 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘𝑌)) ∈
ℝ+) |
97 | 75, 96 | ltaddrpd 11905 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑌 < (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌)))) |
98 | 60 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑄‘𝐾) ∈ ℂ) |
99 | 77 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸‘𝑌) ∈ ℂ) |
100 | 75 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ∈ ℂ) |
101 | 98, 99, 100 | subsub3d 10422 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) = (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌))) |
102 | 98, 100 | addcomd 10238 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑄‘𝐾) + 𝑌) = (𝑌 + (𝑄‘𝐾))) |
103 | 102 | oveq1d 6665 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝑄‘𝐾) + 𝑌) − (𝐸‘𝑌)) = ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌))) |
104 | 100, 98, 99 | addsubassd 10412 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑌 + (𝑄‘𝐾)) − (𝐸‘𝑌)) = (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌)))) |
105 | 101, 103,
104 | 3eqtrrd 2661 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑌 + ((𝑄‘𝐾) − (𝐸‘𝑌))) = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
106 | 97, 105 | breqtrd 4679 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑌 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
107 | 14, 75, 79, 91, 106 | lelttrd 10195 |
. . . . . . . . 9
⊢ (𝜑 → 𝐶 < ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
108 | 14, 79, 107 | ltled 10185 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
109 | 108 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌))) |
110 | 34 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ) |
111 | 60 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℝ) |
112 | 52, 34 | resubcld 10458 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ) |
113 | 112 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ) |
114 | 111, 113 | resubcld 10458 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ) |
115 | 74 | simp3d 1075 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 < (𝑆‘(𝐽 + 1))) |
116 | 75, 34, 115 | ltled 10185 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑌 ≤ (𝑆‘(𝐽 + 1))) |
117 | 38, 36, 41, 10, 1, 75, 34, 116 | fourierdlem7 40331 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸‘𝑌) − 𝑌)) |
118 | 112, 78, 60, 117 | lesub2dd 10644 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))))) |
119 | 118 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))))) |
120 | 98 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) ∈ ℂ) |
121 | 52 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ) |
122 | 121 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ) |
123 | 110 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ) |
124 | 120, 122,
123 | subsubd 10420 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1)))) |
125 | 98, 121 | subcld 10392 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ) |
126 | 34 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ) |
127 | 125, 126 | addcomd 10238 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))))) |
128 | 127 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))))) |
129 | 124, 128 | eqtrd 2656 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))))) |
130 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) |
131 | 52 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ) |
132 | 111, 131 | sublt0d 10653 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))) |
133 | 130, 132 | mpbird 247 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0) |
134 | 111, 131 | resubcld 10458 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ) |
135 | | ltaddneg 10251 |
. . . . . . . . . . . . 13
⊢ ((((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))) |
136 | 134, 110,
135 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))) |
137 | 133, 136 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑆‘(𝐽 + 1)) + ((𝑄‘𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))) |
138 | 129, 137 | eqbrtrd 4675 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1))) |
139 | 80, 114, 110, 119, 138 | lelttrd 10195 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1))) |
140 | 84, 33 | ffvelrnd 6360 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷)) |
141 | | elicc2 12238 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))) |
142 | 14, 15, 141 | syl2anc 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))) |
143 | 140, 142 | mpbid 222 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)) |
144 | 143 | simp3d 1075 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷) |
145 | 144 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷) |
146 | 80, 110, 62, 139, 145 | ltletrd 10197 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) < 𝐷) |
147 | 80, 62, 146 | ltled 10185 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ≤ 𝐷) |
148 | 61, 62, 80, 109, 147 | eliccd 39726 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷)) |
149 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → 𝑥 = 𝑌) |
150 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑌 → (𝐵 − 𝑥) = (𝐵 − 𝑌)) |
151 | 150 | oveq1d 6665 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑌 → ((𝐵 − 𝑥) / 𝑇) = ((𝐵 − 𝑌) / 𝑇)) |
152 | 151 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑌 → (⌊‘((𝐵 − 𝑥) / 𝑇)) = (⌊‘((𝐵 − 𝑌) / 𝑇))) |
153 | 152 | oveq1d 6665 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑌 → ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) |
154 | 149, 153 | oveq12d 6668 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))) |
155 | 154 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵 − 𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))) |
156 | 36, 75 | resubcld 10458 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐵 − 𝑌) ∈ ℝ) |
157 | 156, 40, 45 | redivcld 10853 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐵 − 𝑌) / 𝑇) ∈ ℝ) |
158 | 157 | flcld 12599 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℤ) |
159 | 158 | zred 11482 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℝ) |
160 | 159, 40 | remulcld 10070 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℝ) |
161 | 75, 160 | readdcld 10069 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) ∈ ℝ) |
162 | 2, 155, 75, 161 | fvmptd 6288 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸‘𝑌) = (𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇))) |
163 | 162 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌)) |
164 | 163 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇)) |
165 | 160 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) ∈ ℂ) |
166 | 100, 165 | pncan2d 10394 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) |
167 | 166 | oveq1d 6665 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑌 + ((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇)) |
168 | 159 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → (⌊‘((𝐵 − 𝑌) / 𝑇)) ∈ ℂ) |
169 | 40 | recnd 10068 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑇 ∈ ℂ) |
170 | 168, 169,
45 | divcan4d 10807 |
. . . . . . . . . 10
⊢ (𝜑 → (((⌊‘((𝐵 − 𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇))) |
171 | 164, 167,
170 | 3eqtrd 2660 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵 − 𝑌) / 𝑇))) |
172 | 171, 158 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ) |
173 | 78 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸‘𝑌) − 𝑌) ∈ ℂ) |
174 | 173, 169,
45 | divcan1d 10802 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸‘𝑌) − 𝑌)) |
175 | 174 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌))) |
176 | 98, 173 | npcand 10396 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((𝐸‘𝑌) − 𝑌)) = (𝑄‘𝐾)) |
177 | 175, 176 | eqtrd 2656 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄‘𝐾)) |
178 | | ffun 6048 |
. . . . . . . . . . 11
⊢ (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄) |
179 | 58, 178 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → Fun 𝑄) |
180 | | fdm 6051 |
. . . . . . . . . . . 12
⊢ (𝑄:(0...𝑀)⟶ℝ → dom 𝑄 = (0...𝑀)) |
181 | 58, 180 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑄 = (0...𝑀)) |
182 | 59, 181 | eleqtrrd 2704 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾 ∈ dom 𝑄) |
183 | | fvelrn 6352 |
. . . . . . . . . 10
⊢ ((Fun
𝑄 ∧ 𝐾 ∈ dom 𝑄) → (𝑄‘𝐾) ∈ ran 𝑄) |
184 | 179, 182,
183 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (𝑄‘𝐾) ∈ ran 𝑄) |
185 | 177, 184 | eqeltrd 2701 |
. . . . . . . 8
⊢ (𝜑 → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) |
186 | | oveq1 6657 |
. . . . . . . . . . 11
⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) |
187 | 186 | oveq2d 6666 |
. . . . . . . . . 10
⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇))) |
188 | 187 | eleq1d 2686 |
. . . . . . . . 9
⊢ (𝑘 = (((𝐸‘𝑌) − 𝑌) / 𝑇) → ((((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)) |
189 | 188 | rspcev 3309 |
. . . . . . . 8
⊢
(((((𝐸‘𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + ((((𝐸‘𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄) |
190 | 172, 185,
189 | syl2anc 693 |
. . . . . . 7
⊢ (𝜑 → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄) |
191 | 190 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄) |
192 | | oveq1 6657 |
. . . . . . . . 9
⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇))) |
193 | 192 | eleq1d 2686 |
. . . . . . . 8
⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
194 | 193 | rexbidv 3052 |
. . . . . . 7
⊢ (𝑥 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
195 | 194 | elrab 3363 |
. . . . . 6
⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)) |
196 | 148, 191,
195 | sylanbrc 698 |
. . . . 5
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}) |
197 | | elun2 3781 |
. . . . 5
⊢ (((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
198 | 196, 197 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})) |
199 | | fourierdlem63.x |
. . . 4
⊢ 𝑋 = ((𝑄‘𝐾) − ((𝐸‘𝑌) − 𝑌)) |
200 | 198, 199,
18 | 3eltr4g 2718 |
. . 3
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 ∈ 𝐻) |
201 | | elfzelz 12342 |
. . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ) |
202 | 201 | ad2antlr 763 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ) |
203 | | elfzoelz 12470 |
. . . . . . . . . . 11
⊢ (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ) |
204 | 31, 203 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐽 ∈ ℤ) |
205 | 204 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 ∈ ℤ) |
206 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
207 | 21 | simprd 479 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑆 Isom < , < ((0...𝑁), 𝐻)) |
208 | 207 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝐻)) |
209 | 69 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 ∈ (0...𝑁)) |
210 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝑗 ∈ (0...𝑁)) |
211 | | isorel 6576 |
. . . . . . . . . . . 12
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗))) |
212 | 208, 209,
210, 211 | syl12anc 1324 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → (𝐽 < 𝑗 ↔ (𝑆‘𝐽) < (𝑆‘𝑗))) |
213 | 206, 212 | mpbird 247 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝐽) < (𝑆‘𝑗)) → 𝐽 < 𝑗) |
214 | 213 | adantrr 753 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 < 𝑗) |
215 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
216 | 207 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑆 Isom < , < ((0...𝑁), 𝐻)) |
217 | | simplr 792 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 ∈ (0...𝑁)) |
218 | 33 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝐽 + 1) ∈ (0...𝑁)) |
219 | | isorel 6576 |
. . . . . . . . . . . 12
⊢ ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
220 | 216, 217,
218, 219 | syl12anc 1324 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → (𝑗 < (𝐽 + 1) ↔ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
221 | 215, 220 | mpbird 247 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 < (𝐽 + 1)) |
222 | 221 | adantrl 752 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1)) |
223 | | btwnnz 11453 |
. . . . . . . . 9
⊢ ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗 ∧ 𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ) |
224 | 205, 214,
222, 223 | syl3anc 1326 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) → ¬ 𝑗 ∈ ℤ) |
225 | 202, 224 | pm2.65da 600 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
226 | 225 | adantlr 751 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
227 | 70 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ∈ ℝ) |
228 | 75 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 ∈ ℝ) |
229 | 30 | ffvelrnda 6359 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑆‘𝑗) ∈ ℝ) |
230 | 229 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) ∈ ℝ) |
231 | 74 | simp2d 1074 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑆‘𝐽) ≤ 𝑌) |
232 | 231 | ad2antrr 762 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) ≤ 𝑌) |
233 | 106, 199 | syl6breqr 4695 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 < 𝑋) |
234 | 233 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < 𝑋) |
235 | | eqcom 2629 |
. . . . . . . . . . . . 13
⊢ (𝑋 = (𝑆‘𝑗) ↔ (𝑆‘𝑗) = 𝑋) |
236 | 235 | biimpri 218 |
. . . . . . . . . . . 12
⊢ ((𝑆‘𝑗) = 𝑋 → 𝑋 = (𝑆‘𝑗)) |
237 | 236 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 = (𝑆‘𝑗)) |
238 | 234, 237 | breqtrd 4679 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗)) |
239 | 238 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → 𝑌 < (𝑆‘𝑗)) |
240 | 227, 228,
230, 232, 239 | lelttrd 10195 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
241 | 240 | adantllr 755 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝐽) < (𝑆‘𝑗)) |
242 | | simpr 477 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) = 𝑋) |
243 | 199, 139 | syl5eqbr 4688 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1))) |
244 | 243 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1))) |
245 | 242, 244 | eqbrtrd 4675 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
246 | 245 | adantlr 751 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → (𝑆‘𝑗) < (𝑆‘(𝐽 + 1))) |
247 | 241, 246 | jca 554 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆‘𝑗) = 𝑋) → ((𝑆‘𝐽) < (𝑆‘𝑗) ∧ (𝑆‘𝑗) < (𝑆‘(𝐽 + 1)))) |
248 | 226, 247 | mtand 691 |
. . . . 5
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆‘𝑗) = 𝑋) |
249 | 248 | nrexdv 3001 |
. . . 4
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋) |
250 | | isof1o 6573 |
. . . . . . . . 9
⊢ (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto→𝐻) |
251 | 207, 250 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑆:(0...𝑁)–1-1-onto→𝐻) |
252 | | f1ofo 6144 |
. . . . . . . 8
⊢ (𝑆:(0...𝑁)–1-1-onto→𝐻 → 𝑆:(0...𝑁)–onto→𝐻) |
253 | 251, 252 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑆:(0...𝑁)–onto→𝐻) |
254 | | foelrn 6378 |
. . . . . . 7
⊢ ((𝑆:(0...𝑁)–onto→𝐻 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗)) |
255 | 253, 254 | sylan 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆‘𝑗)) |
256 | 235 | rexbii 3041 |
. . . . . 6
⊢
(∃𝑗 ∈
(0...𝑁)𝑋 = (𝑆‘𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋) |
257 | 255, 256 | sylib 208 |
. . . . 5
⊢ ((𝜑 ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋) |
258 | 257 | adantlr 751 |
. . . 4
⊢ (((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑋 ∈ 𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆‘𝑗) = 𝑋) |
259 | 249, 258 | mtand 691 |
. . 3
⊢ ((𝜑 ∧ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ 𝑋 ∈ 𝐻) |
260 | 200, 259 | pm2.65da 600 |
. 2
⊢ (𝜑 → ¬ (𝑄‘𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) |
261 | 52, 60, 260 | nltled 10187 |
1
⊢ (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄‘𝐾)) |