Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fourierdlem63 Structured version   Visualization version   GIF version

Theorem fourierdlem63 46125
Description: The upper bound of intervals in the moved partition are mapped to points that are not greater than the corresponding upper bounds in the original partition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem63.t 𝑇 = (𝐵𝐴)
fourierdlem63.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem63.m (𝜑𝑀 ∈ ℕ)
fourierdlem63.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem63.c (𝜑𝐶 ∈ ℝ)
fourierdlem63.d (𝜑𝐷 ∈ ℝ)
fourierdlem63.cltd (𝜑𝐶 < 𝐷)
fourierdlem63.o 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐶 ∧ (𝑝𝑚) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem63.h 𝐻 = ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
fourierdlem63.n 𝑁 = ((♯‘𝐻) − 1)
fourierdlem63.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
fourierdlem63.e 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
fourierdlem63.k (𝜑𝐾 ∈ (0...𝑀))
fourierdlem63.j (𝜑𝐽 ∈ (0..^𝑁))
fourierdlem63.y (𝜑𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))))
fourierdlem63.eyltqk (𝜑 → (𝐸𝑌) < (𝑄𝐾))
fourierdlem63.x 𝑋 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌))
Assertion
Ref Expression
fourierdlem63 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄𝐾))
Distinct variable groups:   𝐴,𝑖,𝑚,𝑝   𝑥,𝐴,𝑖   𝐵,𝑖,𝑚,𝑝   𝑥,𝐵   𝐶,𝑖,𝑚,𝑝   𝑥,𝐶   𝐷,𝑖,𝑚,𝑝   𝑥,𝐷   𝑘,𝐸,𝑥   𝑓,𝐻   𝑥,𝐻   𝑘,𝐽,𝑥   𝑘,𝐾,𝑥   𝑖,𝑀,𝑚,𝑝   𝑓,𝑁   𝑖,𝑁,𝑚,𝑝   𝑥,𝑁   𝑄,𝑖,𝑘,𝑥   𝑄,𝑝   𝑆,𝑓   𝑆,𝑖,𝑘,𝑥   𝑆,𝑝   𝑇,𝑖,𝑘,𝑥   𝑘,𝑌,𝑥   𝜑,𝑓   𝜑,𝑖,𝑘,𝑥
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝐴(𝑓,𝑘)   𝐵(𝑓,𝑘)   𝐶(𝑓,𝑘)   𝐷(𝑓,𝑘)   𝑃(𝑥,𝑓,𝑖,𝑘,𝑚,𝑝)   𝑄(𝑓,𝑚)   𝑆(𝑚)   𝑇(𝑓,𝑚,𝑝)   𝐸(𝑓,𝑖,𝑚,𝑝)   𝐻(𝑖,𝑘,𝑚,𝑝)   𝐽(𝑓,𝑖,𝑚,𝑝)   𝐾(𝑓,𝑖,𝑚,𝑝)   𝑀(𝑥,𝑓,𝑘)   𝑁(𝑘)   𝑂(𝑥,𝑓,𝑖,𝑘,𝑚,𝑝)   𝑋(𝑥,𝑓,𝑖,𝑘,𝑚,𝑝)   𝑌(𝑓,𝑖,𝑚,𝑝)

Proof of Theorem fourierdlem63
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem63.e . . . . 5 𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)))
21a1i 11 . . . 4 (𝜑𝐸 = (𝑥 ∈ ℝ ↦ (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇))))
3 id 22 . . . . . 6 (𝑥 = (𝑆‘(𝐽 + 1)) → 𝑥 = (𝑆‘(𝐽 + 1)))
4 oveq2 7439 . . . . . . . . 9 (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
54oveq1d 7446 . . . . . . . 8 (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
65fveq2d 6911 . . . . . . 7 (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
76oveq1d 7446 . . . . . 6 (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
83, 7oveq12d 7449 . . . . 5 (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
98adantl 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...𝑁), 𝐻))
2110, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20fourierdlem54 46116 . . . . . . . . . 10 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2221simpld 494 . . . . . . . . 9 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
2322simprd 495 . . . . . . . 8 (𝜑𝑆 ∈ (𝑂𝑁))
2422simpld 494 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
2517fourierdlem2 46065 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
2624, 25syl 17 . . . . . . . 8 (𝜑 → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
2723, 26mpbid 232 . . . . . . 7 (𝜑 → (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
2827simpld 494 . . . . . 6 (𝜑𝑆 ∈ (ℝ ↑m (0...𝑁)))
29 elmapi 8888 . . . . . 6 (𝑆 ∈ (ℝ ↑m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3028, 29syl 17 . . . . 5 (𝜑𝑆:(0...𝑁)⟶ℝ)
31 fourierdlem63.j . . . . . 6 (𝜑𝐽 ∈ (0..^𝑁))
32 fzofzp1 13800 . . . . . 6 (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
3331, 32syl 17 . . . . 5 (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
3430, 33ffvelcdmd 7105 . . . 4 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
3511, 12, 13fourierdlem11 46074 . . . . . . . . . . 11 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
3635simp2d 1142 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
3736, 34resubcld 11689 . . . . . . . . 9 (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
3835simp1d 1141 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
3936, 38resubcld 11689 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
4010, 39eqeltrid 2843 . . . . . . . . 9 (𝜑𝑇 ∈ ℝ)
4135simp3d 1143 . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
4238, 36posdifd 11848 . . . . . . . . . . . 12 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
4341, 42mpbid 232 . . . . . . . . . . 11 (𝜑 → 0 < (𝐵𝐴))
4443, 10breqtrrdi 5190 . . . . . . . . . 10 (𝜑 → 0 < 𝑇)
4544gt0ne0d 11825 . . . . . . . . 9 (𝜑𝑇 ≠ 0)
4637, 40, 45redivcld 12093 . . . . . . . 8 (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
4746flcld 13835 . . . . . . 7 (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
4847zred 12720 . . . . . 6 (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
4948, 40remulcld 11289 . . . . 5 (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
5034, 49readdcld 11288 . . . 4 (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
512, 9, 34, 50fvmptd 7023 . . 3 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
5251, 50eqeltrd 2839 . 2 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
5311fourierdlem2 46065 . . . . . . 7 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
5412, 53syl 17 . . . . . 6 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
5513, 54mpbid 232 . . . . 5 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
5655simpld 494 . . . 4 (𝜑𝑄 ∈ (ℝ ↑m (0...𝑀)))
57 elmapi 8888 . . . 4 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
5856, 57syl 17 . . 3 (𝜑𝑄:(0...𝑀)⟶ℝ)
59 fourierdlem63.k . . 3 (𝜑𝐾 ∈ (0...𝑀))
6058, 59ffvelcdmd 7105 . 2 (𝜑 → (𝑄𝐾) ∈ ℝ)
6114adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ)
6215adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ)
6338rexrd 11309 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ*)
64 iocssre 13464 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
6563, 36, 64syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
6638, 36, 41, 10, 1fourierdlem4 46067 . . . . . . . . . . . 12 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
67 fourierdlem63.y . . . . . . . . . . . . . 14 (𝜑𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))))
68 elfzofz 13712 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
6931, 68syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ (0...𝑁))
7030, 69ffvelcdmd 7105 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆𝐽) ∈ ℝ)
7134rexrd 11309 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ*)
72 elico2 13448 . . . . . . . . . . . . . . 15 (((𝑆𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ*) → (𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1)))))
7370, 71, 72syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1)))))
7467, 73mpbid 232 . . . . . . . . . . . . 13 (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1))))
7574simp1d 1141 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ)
7666, 75ffvelcdmd 7105 . . . . . . . . . . 11 (𝜑 → (𝐸𝑌) ∈ (𝐴(,]𝐵))
7765, 76sseldd 3996 . . . . . . . . . 10 (𝜑 → (𝐸𝑌) ∈ ℝ)
7877, 75resubcld 11689 . . . . . . . . 9 (𝜑 → ((𝐸𝑌) − 𝑌) ∈ ℝ)
7960, 78resubcld 11689 . . . . . . . 8 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ℝ)
8079adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ℝ)
81 icossicc 13473 . . . . . . . . . . . . . 14 ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆𝐽)[,](𝑆‘(𝐽 + 1)))
8214rexrd 11309 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℝ*)
8315rexrd 11309 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ ℝ*)
8417, 24, 23fourierdlem15 46078 . . . . . . . . . . . . . . 15 (𝜑𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
8582, 83, 84, 31fourierdlem8 46071 . . . . . . . . . . . . . 14 (𝜑 → ((𝑆𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
8681, 85sstrid 4007 . . . . . . . . . . . . 13 (𝜑 → ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
8786, 67sseldd 3996 . . . . . . . . . . . 12 (𝜑𝑌 ∈ (𝐶[,]𝐷))
88 elicc2 13449 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷)))
8914, 15, 88syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷)))
9087, 89mpbid 232 . . . . . . . . . . 11 (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷))
9190simp2d 1142 . . . . . . . . . 10 (𝜑𝐶𝑌)
9260, 77resubcld 11689 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐾) − (𝐸𝑌)) ∈ ℝ)
93 fourierdlem63.eyltqk . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝑌) < (𝑄𝐾))
9477, 60posdifd 11848 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸𝑌) < (𝑄𝐾) ↔ 0 < ((𝑄𝐾) − (𝐸𝑌))))
9593, 94mpbid 232 . . . . . . . . . . . . 13 (𝜑 → 0 < ((𝑄𝐾) − (𝐸𝑌)))
9692, 95elrpd 13072 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝐾) − (𝐸𝑌)) ∈ ℝ+)
9775, 96ltaddrpd 13108 . . . . . . . . . . 11 (𝜑𝑌 < (𝑌 + ((𝑄𝐾) − (𝐸𝑌))))
9860recnd 11287 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝐾) ∈ ℂ)
9977recnd 11287 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑌) ∈ ℂ)
10075recnd 11287 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ ℂ)
10198, 99, 100subsub3d 11648 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) = (((𝑄𝐾) + 𝑌) − (𝐸𝑌)))
10298, 100addcomd 11461 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐾) + 𝑌) = (𝑌 + (𝑄𝐾)))
103102oveq1d 7446 . . . . . . . . . . . 12 (𝜑 → (((𝑄𝐾) + 𝑌) − (𝐸𝑌)) = ((𝑌 + (𝑄𝐾)) − (𝐸𝑌)))
104100, 98, 99addsubassd 11638 . . . . . . . . . . . 12 (𝜑 → ((𝑌 + (𝑄𝐾)) − (𝐸𝑌)) = (𝑌 + ((𝑄𝐾) − (𝐸𝑌))))
105101, 103, 1043eqtrrd 2780 . . . . . . . . . . 11 (𝜑 → (𝑌 + ((𝑄𝐾) − (𝐸𝑌))) = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10697, 105breqtrd 5174 . . . . . . . . . 10 (𝜑𝑌 < ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10714, 75, 79, 91, 106lelttrd 11417 . . . . . . . . 9 (𝜑𝐶 < ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10814, 79, 107ltled 11407 . . . . . . . 8 (𝜑𝐶 ≤ ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
109108adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
11034adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
11160adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) ∈ ℝ)
11252, 34resubcld 11689 . . . . . . . . . . . 12 (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
113112adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
114111, 113resubcld 11689 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ)
11574simp3d 1143 . . . . . . . . . . . . . 14 (𝜑𝑌 < (𝑆‘(𝐽 + 1)))
11675, 34, 115ltled 11407 . . . . . . . . . . . . 13 (𝜑𝑌 ≤ (𝑆‘(𝐽 + 1)))
11738, 36, 41, 10, 1, 75, 34, 116fourierdlem7 46070 . . . . . . . . . . . 12 (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸𝑌) − 𝑌))
118112, 78, 60, 117lesub2dd 11878 . . . . . . . . . . 11 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
119118adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
12098adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) ∈ ℂ)
12152recnd 11287 . . . . . . . . . . . . . 14 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
122121adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
123110recnd 11287 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ)
124120, 122, 123subsubd 11646 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))))
12598, 121subcld 11618 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ)
12634recnd 11287 . . . . . . . . . . . . . 14 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
127125, 126addcomd 11461 . . . . . . . . . . . . 13 (𝜑 → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
128127adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
129124, 128eqtrd 2775 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
130 simpr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
13152adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
132111, 131sublt0d 11887 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))))
133130, 132mpbird 257 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0)
134111, 131resubcld 11689 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
135 ltaddneg 11475 . . . . . . . . . . . . 13 ((((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
136134, 110, 135syl2anc 584 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
137133, 136mpbid 232 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))
138129, 137eqbrtrd 5170 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1)))
13980, 114, 110, 119, 138lelttrd 11417 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1)))
14084, 33ffvelcdmd 7105 . . . . . . . . . . . 12 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
141 elicc2 13449 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
14214, 15, 141syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
143140, 142mpbid 232 . . . . . . . . . . 11 (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))
144143simp3d 1143 . . . . . . . . . 10 (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
145144adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
14680, 110, 62, 139, 145ltletrd 11419 . . . . . . . 8 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) < 𝐷)
14780, 62, 146ltled 11407 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ 𝐷)
14861, 62, 80, 109, 147eliccd 45457 . . . . . 6 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ (𝐶[,]𝐷))
149 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌𝑥 = 𝑌)
150 oveq2 7439 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑌 → (𝐵𝑥) = (𝐵𝑌))
151150oveq1d 7446 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑌) / 𝑇))
152151fveq2d 6911 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑌) / 𝑇)))
153152oveq1d 7446 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇))
154149, 153oveq12d 7449 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
155154adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
15636, 75resubcld 11689 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵𝑌) ∈ ℝ)
157156, 40, 45redivcld 12093 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵𝑌) / 𝑇) ∈ ℝ)
158157flcld 13835 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℤ)
159158zred 12720 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℝ)
160159, 40remulcld 11289 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) ∈ ℝ)
16175, 160readdcld 11288 . . . . . . . . . . . . 13 (𝜑 → (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) ∈ ℝ)
1622, 155, 75, 161fvmptd 7023 . . . . . . . . . . . 12 (𝜑 → (𝐸𝑌) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
163162oveq1d 7446 . . . . . . . . . . 11 (𝜑 → ((𝐸𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌))
164163oveq1d 7446 . . . . . . . . . 10 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇))
165160recnd 11287 . . . . . . . . . . . 12 (𝜑 → ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) ∈ ℂ)
166100, 165pncan2d 11620 . . . . . . . . . . 11 (𝜑 → ((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇))
167166oveq1d 7446 . . . . . . . . . 10 (𝜑 → (((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) / 𝑇))
168159recnd 11287 . . . . . . . . . . 11 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℂ)
16940recnd 11287 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
170168, 169, 45divcan4d 12047 . . . . . . . . . 10 (𝜑 → (((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵𝑌) / 𝑇)))
171164, 167, 1703eqtrd 2779 . . . . . . . . 9 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵𝑌) / 𝑇)))
172171, 158eqeltrd 2839 . . . . . . . 8 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) ∈ ℤ)
17378recnd 11287 . . . . . . . . . . . 12 (𝜑 → ((𝐸𝑌) − 𝑌) ∈ ℂ)
174173, 169, 45divcan1d 12042 . . . . . . . . . . 11 (𝜑 → ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸𝑌) − 𝑌))
175174oveq2d 7447 . . . . . . . . . 10 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((𝐸𝑌) − 𝑌)))
17698, 173npcand 11622 . . . . . . . . . 10 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((𝐸𝑌) − 𝑌)) = (𝑄𝐾))
177175, 176eqtrd 2775 . . . . . . . . 9 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄𝐾))
178 ffun 6740 . . . . . . . . . . 11 (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
17958, 178syl 17 . . . . . . . . . 10 (𝜑 → Fun 𝑄)
18058fdmd 6747 . . . . . . . . . . 11 (𝜑 → dom 𝑄 = (0...𝑀))
18159, 180eleqtrrd 2842 . . . . . . . . . 10 (𝜑𝐾 ∈ dom 𝑄)
182 fvelrn 7096 . . . . . . . . . 10 ((Fun 𝑄𝐾 ∈ dom 𝑄) → (𝑄𝐾) ∈ ran 𝑄)
183179, 181, 182syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑄𝐾) ∈ ran 𝑄)
184177, 183eqeltrd 2839 . . . . . . . 8 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)
185 oveq1 7438 . . . . . . . . . . 11 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇))
186185oveq2d 7447 . . . . . . . . . 10 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)))
187186eleq1d 2824 . . . . . . . . 9 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → ((((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄))
188187rspcev 3622 . . . . . . . 8 (((((𝐸𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
189172, 184, 188syl2anc 584 . . . . . . 7 (𝜑 → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
190189adantr 480 . . . . . 6 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
191 oveq1 7438 . . . . . . . . 9 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)))
192191eleq1d 2824 . . . . . . . 8 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
193192rexbidv 3177 . . . . . . 7 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
194193elrab 3695 . . . . . 6 (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
195148, 190, 194sylanbrc 583 . . . . 5 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
196 elun2 4193 . . . . 5 (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
197195, 196syl 17 . . . 4 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
198 fourierdlem63.x . . . 4 𝑋 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌))
199197, 198, 183eltr4g 2856 . . 3 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋𝐻)
200 elfzelz 13561 . . . . . . . . 9 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
201200ad2antlr 727 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ)
202 elfzoelz 13696 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
20331, 202syl 17 . . . . . . . . . 10 (𝜑𝐽 ∈ ℤ)
204203ad2antrr 726 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 ∈ ℤ)
205 simpr 484 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → (𝑆𝐽) < (𝑆𝑗))
20621simprd 495 . . . . . . . . . . . . 13 (𝜑𝑆 Isom < , < ((0...𝑁), 𝐻))
207206ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
20869ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝐽 ∈ (0...𝑁))
209 simplr 769 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝑗 ∈ (0...𝑁))
210 isorel 7346 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆𝐽) < (𝑆𝑗)))
211207, 208, 209, 210syl12anc 837 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → (𝐽 < 𝑗 ↔ (𝑆𝐽) < (𝑆𝑗)))
212205, 211mpbird 257 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝐽 < 𝑗)
213212adantrr 717 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 < 𝑗)
214 simpr 484 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
215206ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
216 simplr 769 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 ∈ (0...𝑁))
21733ad2antrr 726 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝐽 + 1) ∈ (0...𝑁))
218 isorel 7346 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
219215, 216, 217, 218syl12anc 837 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝑗 < (𝐽 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
220214, 219mpbird 257 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 < (𝐽 + 1))
221220adantrl 716 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1))
222 btwnnz 12692 . . . . . . . . 9 ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
223204, 213, 221, 222syl3anc 1370 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → ¬ 𝑗 ∈ ℤ)
224201, 223pm2.65da 817 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑁)) → ¬ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
225224adantlr 715 . . . . . 6 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
22670ad2antrr 726 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) ∈ ℝ)
22775ad2antrr 726 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → 𝑌 ∈ ℝ)
22830ffvelcdmda 7104 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑆𝑗) ∈ ℝ)
229228adantr 480 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) ∈ ℝ)
23074simp2d 1142 . . . . . . . . . 10 (𝜑 → (𝑆𝐽) ≤ 𝑌)
231230ad2antrr 726 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) ≤ 𝑌)
232106, 198breqtrrdi 5190 . . . . . . . . . . . 12 (𝜑𝑌 < 𝑋)
233232adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑌 < 𝑋)
234 eqcom 2742 . . . . . . . . . . . . 13 (𝑋 = (𝑆𝑗) ↔ (𝑆𝑗) = 𝑋)
235234biimpri 228 . . . . . . . . . . . 12 ((𝑆𝑗) = 𝑋𝑋 = (𝑆𝑗))
236235adantl 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑋 = (𝑆𝑗))
237233, 236breqtrd 5174 . . . . . . . . . 10 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑌 < (𝑆𝑗))
238237adantlr 715 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → 𝑌 < (𝑆𝑗))
239226, 227, 229, 231, 238lelttrd 11417 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) < (𝑆𝑗))
240239adantllr 719 . . . . . . 7 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) < (𝑆𝑗))
241 simpr 484 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) = 𝑋)
242198, 139eqbrtrid 5183 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1)))
243242adantr 480 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1)))
244241, 243eqbrtrd 5170 . . . . . . . 8 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
245244adantlr 715 . . . . . . 7 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
246240, 245jca 511 . . . . . 6 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
247225, 246mtand 816 . . . . 5 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆𝑗) = 𝑋)
248247nrexdv 3147 . . . 4 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
249 isof1o 7343 . . . . . . . . 9 (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto𝐻)
250206, 249syl 17 . . . . . . . 8 (𝜑𝑆:(0...𝑁)–1-1-onto𝐻)
251 f1ofo 6856 . . . . . . . 8 (𝑆:(0...𝑁)–1-1-onto𝐻𝑆:(0...𝑁)–onto𝐻)
252250, 251syl 17 . . . . . . 7 (𝜑𝑆:(0...𝑁)–onto𝐻)
253 foelrn 7127 . . . . . . 7 ((𝑆:(0...𝑁)–onto𝐻𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗))
254252, 253sylan 580 . . . . . 6 ((𝜑𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗))
255234rexbii 3092 . . . . . 6 (∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
256254, 255sylib 218 . . . . 5 ((𝜑𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
257256adantlr 715 . . . 4 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
258248, 257mtand 816 . . 3 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ 𝑋𝐻)
259199, 258pm2.65da 817 . 2 (𝜑 → ¬ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
26052, 60, 259nltled 11409 1 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄𝐾))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1537  wcel 2106  wral 3059  wrex 3068  {crab 3433  cun 3961  wss 3963  {cpr 4633   class class class wbr 5148  cmpt 5231  dom cdm 5689  ran crn 5690  cio 6514  Fun wfun 6557  wf 6559  ontowfo 6561  1-1-ontowf1o 6562  cfv 6563   Isom wiso 6564  (class class class)co 7431  m cmap 8865  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156   · cmul 11158  *cxr 11292   < clt 11293  cle 11294  cmin 11490   / cdiv 11918  cn 12264  cz 12611  (,]cioc 13385  [,)cico 13386  [,]cicc 13387  ...cfz 13544  ..^cfzo 13691  cfl 13827  chash 14366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-oadd 8509  df-er 8744  df-map 8867  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fi 9449  df-sup 9480  df-inf 9481  df-oi 9548  df-dju 9939  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-xnn0 12598  df-z 12612  df-uz 12877  df-q 12989  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-ioo 13388  df-ioc 13389  df-ico 13390  df-icc 13391  df-fz 13545  df-fzo 13692  df-fl 13829  df-seq 14040  df-exp 14100  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-rest 17469  df-topgen 17490  df-psmet 21374  df-xmet 21375  df-met 21376  df-bl 21377  df-mopn 21378  df-top 22916  df-topon 22933  df-bases 22969  df-cld 23043  df-ntr 23044  df-cls 23045  df-nei 23122  df-lp 23160  df-cmp 23411
This theorem is referenced by:  fourierdlem79  46141
  Copyright terms: Public domain W3C validator