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 44400
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 7365 . . . . . . . . 9 (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
54oveq1d 7372 . . . . . . . 8 (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
65fveq2d 6846 . . . . . . 7 (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
76oveq1d 7372 . . . . . 6 (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
83, 7oveq12d 7375 . . . . 5 (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
98adantl 482 . . . 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 44391 . . . . . . . . . 10 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2221simpld 495 . . . . . . . . 9 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
2322simprd 496 . . . . . . . 8 (𝜑𝑆 ∈ (𝑂𝑁))
2422simpld 495 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
2517fourierdlem2 44340 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
2624, 25syl 17 . . . . . . . 8 (𝜑 → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
2723, 26mpbid 231 . . . . . . 7 (𝜑 → (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
2827simpld 495 . . . . . 6 (𝜑𝑆 ∈ (ℝ ↑m (0...𝑁)))
29 elmapi 8787 . . . . . 6 (𝑆 ∈ (ℝ ↑m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3028, 29syl 17 . . . . 5 (𝜑𝑆:(0...𝑁)⟶ℝ)
31 fourierdlem63.j . . . . . 6 (𝜑𝐽 ∈ (0..^𝑁))
32 fzofzp1 13669 . . . . . 6 (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
3331, 32syl 17 . . . . 5 (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
3430, 33ffvelcdmd 7036 . . . 4 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
3511, 12, 13fourierdlem11 44349 . . . . . . . . . . 11 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
3635simp2d 1143 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
3736, 34resubcld 11583 . . . . . . . . 9 (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
3835simp1d 1142 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
3936, 38resubcld 11583 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
4010, 39eqeltrid 2842 . . . . . . . . 9 (𝜑𝑇 ∈ ℝ)
4135simp3d 1144 . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
4238, 36posdifd 11742 . . . . . . . . . . . 12 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
4341, 42mpbid 231 . . . . . . . . . . 11 (𝜑 → 0 < (𝐵𝐴))
4443, 10breqtrrdi 5147 . . . . . . . . . 10 (𝜑 → 0 < 𝑇)
4544gt0ne0d 11719 . . . . . . . . 9 (𝜑𝑇 ≠ 0)
4637, 40, 45redivcld 11983 . . . . . . . 8 (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
4746flcld 13703 . . . . . . 7 (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
4847zred 12607 . . . . . 6 (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
4948, 40remulcld 11185 . . . . 5 (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
5034, 49readdcld 11184 . . . 4 (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
512, 9, 34, 50fvmptd 6955 . . 3 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
5251, 50eqeltrd 2838 . 2 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
5311fourierdlem2 44340 . . . . . . 7 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
5412, 53syl 17 . . . . . 6 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
5513, 54mpbid 231 . . . . 5 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
5655simpld 495 . . . 4 (𝜑𝑄 ∈ (ℝ ↑m (0...𝑀)))
57 elmapi 8787 . . . 4 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
5856, 57syl 17 . . 3 (𝜑𝑄:(0...𝑀)⟶ℝ)
59 fourierdlem63.k . . 3 (𝜑𝐾 ∈ (0...𝑀))
6058, 59ffvelcdmd 7036 . 2 (𝜑 → (𝑄𝐾) ∈ ℝ)
6114adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ)
6215adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ)
6338rexrd 11205 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ*)
64 iocssre 13344 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
6563, 36, 64syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
6638, 36, 41, 10, 1fourierdlem4 44342 . . . . . . . . . . . 12 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
67 fourierdlem63.y . . . . . . . . . . . . . 14 (𝜑𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))))
68 elfzofz 13588 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
6931, 68syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ (0...𝑁))
7030, 69ffvelcdmd 7036 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆𝐽) ∈ ℝ)
7134rexrd 11205 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ*)
72 elico2 13328 . . . . . . . . . . . . . . 15 (((𝑆𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ*) → (𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1)))))
7370, 71, 72syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1)))))
7467, 73mpbid 231 . . . . . . . . . . . . 13 (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1))))
7574simp1d 1142 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ)
7666, 75ffvelcdmd 7036 . . . . . . . . . . 11 (𝜑 → (𝐸𝑌) ∈ (𝐴(,]𝐵))
7765, 76sseldd 3945 . . . . . . . . . 10 (𝜑 → (𝐸𝑌) ∈ ℝ)
7877, 75resubcld 11583 . . . . . . . . 9 (𝜑 → ((𝐸𝑌) − 𝑌) ∈ ℝ)
7960, 78resubcld 11583 . . . . . . . 8 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ℝ)
8079adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ℝ)
81 icossicc 13353 . . . . . . . . . . . . . 14 ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆𝐽)[,](𝑆‘(𝐽 + 1)))
8214rexrd 11205 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℝ*)
8315rexrd 11205 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ ℝ*)
8417, 24, 23fourierdlem15 44353 . . . . . . . . . . . . . . 15 (𝜑𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
8582, 83, 84, 31fourierdlem8 44346 . . . . . . . . . . . . . 14 (𝜑 → ((𝑆𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
8681, 85sstrid 3955 . . . . . . . . . . . . 13 (𝜑 → ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
8786, 67sseldd 3945 . . . . . . . . . . . 12 (𝜑𝑌 ∈ (𝐶[,]𝐷))
88 elicc2 13329 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷)))
8914, 15, 88syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷)))
9087, 89mpbid 231 . . . . . . . . . . 11 (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷))
9190simp2d 1143 . . . . . . . . . 10 (𝜑𝐶𝑌)
9260, 77resubcld 11583 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐾) − (𝐸𝑌)) ∈ ℝ)
93 fourierdlem63.eyltqk . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝑌) < (𝑄𝐾))
9477, 60posdifd 11742 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸𝑌) < (𝑄𝐾) ↔ 0 < ((𝑄𝐾) − (𝐸𝑌))))
9593, 94mpbid 231 . . . . . . . . . . . . 13 (𝜑 → 0 < ((𝑄𝐾) − (𝐸𝑌)))
9692, 95elrpd 12954 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝐾) − (𝐸𝑌)) ∈ ℝ+)
9775, 96ltaddrpd 12990 . . . . . . . . . . 11 (𝜑𝑌 < (𝑌 + ((𝑄𝐾) − (𝐸𝑌))))
9860recnd 11183 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝐾) ∈ ℂ)
9977recnd 11183 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑌) ∈ ℂ)
10075recnd 11183 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ ℂ)
10198, 99, 100subsub3d 11542 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) = (((𝑄𝐾) + 𝑌) − (𝐸𝑌)))
10298, 100addcomd 11357 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐾) + 𝑌) = (𝑌 + (𝑄𝐾)))
103102oveq1d 7372 . . . . . . . . . . . 12 (𝜑 → (((𝑄𝐾) + 𝑌) − (𝐸𝑌)) = ((𝑌 + (𝑄𝐾)) − (𝐸𝑌)))
104100, 98, 99addsubassd 11532 . . . . . . . . . . . 12 (𝜑 → ((𝑌 + (𝑄𝐾)) − (𝐸𝑌)) = (𝑌 + ((𝑄𝐾) − (𝐸𝑌))))
105101, 103, 1043eqtrrd 2781 . . . . . . . . . . 11 (𝜑 → (𝑌 + ((𝑄𝐾) − (𝐸𝑌))) = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10697, 105breqtrd 5131 . . . . . . . . . 10 (𝜑𝑌 < ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10714, 75, 79, 91, 106lelttrd 11313 . . . . . . . . 9 (𝜑𝐶 < ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10814, 79, 107ltled 11303 . . . . . . . 8 (𝜑𝐶 ≤ ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
109108adantr 481 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
11034adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
11160adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) ∈ ℝ)
11252, 34resubcld 11583 . . . . . . . . . . . 12 (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
113112adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
114111, 113resubcld 11583 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ)
11574simp3d 1144 . . . . . . . . . . . . . 14 (𝜑𝑌 < (𝑆‘(𝐽 + 1)))
11675, 34, 115ltled 11303 . . . . . . . . . . . . 13 (𝜑𝑌 ≤ (𝑆‘(𝐽 + 1)))
11738, 36, 41, 10, 1, 75, 34, 116fourierdlem7 44345 . . . . . . . . . . . 12 (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸𝑌) − 𝑌))
118112, 78, 60, 117lesub2dd 11772 . . . . . . . . . . 11 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
119118adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
12098adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) ∈ ℂ)
12152recnd 11183 . . . . . . . . . . . . . 14 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
122121adantr 481 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
123110recnd 11183 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ)
124120, 122, 123subsubd 11540 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))))
12598, 121subcld 11512 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ)
12634recnd 11183 . . . . . . . . . . . . . 14 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
127125, 126addcomd 11357 . . . . . . . . . . . . 13 (𝜑 → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
128127adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
129124, 128eqtrd 2776 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
130 simpr 485 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
13152adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
132111, 131sublt0d 11781 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))))
133130, 132mpbird 256 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0)
134111, 131resubcld 11583 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
135 ltaddneg 11370 . . . . . . . . . . . . 13 ((((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
136134, 110, 135syl2anc 584 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
137133, 136mpbid 231 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))
138129, 137eqbrtrd 5127 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1)))
13980, 114, 110, 119, 138lelttrd 11313 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1)))
14084, 33ffvelcdmd 7036 . . . . . . . . . . . 12 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
141 elicc2 13329 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
14214, 15, 141syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
143140, 142mpbid 231 . . . . . . . . . . 11 (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))
144143simp3d 1144 . . . . . . . . . 10 (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
145144adantr 481 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
14680, 110, 62, 139, 145ltletrd 11315 . . . . . . . 8 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) < 𝐷)
14780, 62, 146ltled 11303 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ 𝐷)
14861, 62, 80, 109, 147eliccd 43732 . . . . . 6 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ (𝐶[,]𝐷))
149 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌𝑥 = 𝑌)
150 oveq2 7365 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑌 → (𝐵𝑥) = (𝐵𝑌))
151150oveq1d 7372 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑌) / 𝑇))
152151fveq2d 6846 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑌) / 𝑇)))
153152oveq1d 7372 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇))
154149, 153oveq12d 7375 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
155154adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
15636, 75resubcld 11583 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵𝑌) ∈ ℝ)
157156, 40, 45redivcld 11983 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵𝑌) / 𝑇) ∈ ℝ)
158157flcld 13703 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℤ)
159158zred 12607 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℝ)
160159, 40remulcld 11185 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) ∈ ℝ)
16175, 160readdcld 11184 . . . . . . . . . . . . 13 (𝜑 → (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) ∈ ℝ)
1622, 155, 75, 161fvmptd 6955 . . . . . . . . . . . 12 (𝜑 → (𝐸𝑌) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
163162oveq1d 7372 . . . . . . . . . . 11 (𝜑 → ((𝐸𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌))
164163oveq1d 7372 . . . . . . . . . 10 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇))
165160recnd 11183 . . . . . . . . . . . 12 (𝜑 → ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) ∈ ℂ)
166100, 165pncan2d 11514 . . . . . . . . . . 11 (𝜑 → ((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇))
167166oveq1d 7372 . . . . . . . . . 10 (𝜑 → (((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) / 𝑇))
168159recnd 11183 . . . . . . . . . . 11 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℂ)
16940recnd 11183 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
170168, 169, 45divcan4d 11937 . . . . . . . . . 10 (𝜑 → (((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵𝑌) / 𝑇)))
171164, 167, 1703eqtrd 2780 . . . . . . . . 9 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵𝑌) / 𝑇)))
172171, 158eqeltrd 2838 . . . . . . . 8 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) ∈ ℤ)
17378recnd 11183 . . . . . . . . . . . 12 (𝜑 → ((𝐸𝑌) − 𝑌) ∈ ℂ)
174173, 169, 45divcan1d 11932 . . . . . . . . . . 11 (𝜑 → ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸𝑌) − 𝑌))
175174oveq2d 7373 . . . . . . . . . 10 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((𝐸𝑌) − 𝑌)))
17698, 173npcand 11516 . . . . . . . . . 10 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((𝐸𝑌) − 𝑌)) = (𝑄𝐾))
177175, 176eqtrd 2776 . . . . . . . . 9 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄𝐾))
178 ffun 6671 . . . . . . . . . . 11 (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
17958, 178syl 17 . . . . . . . . . 10 (𝜑 → Fun 𝑄)
18058fdmd 6679 . . . . . . . . . . 11 (𝜑 → dom 𝑄 = (0...𝑀))
18159, 180eleqtrrd 2841 . . . . . . . . . 10 (𝜑𝐾 ∈ dom 𝑄)
182 fvelrn 7027 . . . . . . . . . 10 ((Fun 𝑄𝐾 ∈ dom 𝑄) → (𝑄𝐾) ∈ ran 𝑄)
183179, 181, 182syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑄𝐾) ∈ ran 𝑄)
184177, 183eqeltrd 2838 . . . . . . . 8 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)
185 oveq1 7364 . . . . . . . . . . 11 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇))
186185oveq2d 7373 . . . . . . . . . 10 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)))
187186eleq1d 2822 . . . . . . . . 9 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → ((((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄))
188187rspcev 3581 . . . . . . . 8 (((((𝐸𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
189172, 184, 188syl2anc 584 . . . . . . 7 (𝜑 → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
190189adantr 481 . . . . . 6 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
191 oveq1 7364 . . . . . . . . 9 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)))
192191eleq1d 2822 . . . . . . . 8 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
193192rexbidv 3175 . . . . . . 7 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
194193elrab 3645 . . . . . 6 (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
195148, 190, 194sylanbrc 583 . . . . 5 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
196 elun2 4137 . . . . 5 (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
197195, 196syl 17 . . . 4 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
198 fourierdlem63.x . . . 4 𝑋 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌))
199197, 198, 183eltr4g 2855 . . 3 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋𝐻)
200 elfzelz 13441 . . . . . . . . 9 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
201200ad2antlr 725 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ)
202 elfzoelz 13572 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
20331, 202syl 17 . . . . . . . . . 10 (𝜑𝐽 ∈ ℤ)
204203ad2antrr 724 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 ∈ ℤ)
205 simpr 485 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → (𝑆𝐽) < (𝑆𝑗))
20621simprd 496 . . . . . . . . . . . . 13 (𝜑𝑆 Isom < , < ((0...𝑁), 𝐻))
207206ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
20869ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝐽 ∈ (0...𝑁))
209 simplr 767 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝑗 ∈ (0...𝑁))
210 isorel 7271 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆𝐽) < (𝑆𝑗)))
211207, 208, 209, 210syl12anc 835 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → (𝐽 < 𝑗 ↔ (𝑆𝐽) < (𝑆𝑗)))
212205, 211mpbird 256 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝐽 < 𝑗)
213212adantrr 715 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 < 𝑗)
214 simpr 485 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
215206ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
216 simplr 767 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 ∈ (0...𝑁))
21733ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝐽 + 1) ∈ (0...𝑁))
218 isorel 7271 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
219215, 216, 217, 218syl12anc 835 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝑗 < (𝐽 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
220214, 219mpbird 256 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 < (𝐽 + 1))
221220adantrl 714 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1))
222 btwnnz 12579 . . . . . . . . 9 ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
223204, 213, 221, 222syl3anc 1371 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → ¬ 𝑗 ∈ ℤ)
224201, 223pm2.65da 815 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑁)) → ¬ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
225224adantlr 713 . . . . . 6 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
22670ad2antrr 724 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) ∈ ℝ)
22775ad2antrr 724 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → 𝑌 ∈ ℝ)
22830ffvelcdmda 7035 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑆𝑗) ∈ ℝ)
229228adantr 481 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) ∈ ℝ)
23074simp2d 1143 . . . . . . . . . 10 (𝜑 → (𝑆𝐽) ≤ 𝑌)
231230ad2antrr 724 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) ≤ 𝑌)
232106, 198breqtrrdi 5147 . . . . . . . . . . . 12 (𝜑𝑌 < 𝑋)
233232adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑌 < 𝑋)
234 eqcom 2743 . . . . . . . . . . . . 13 (𝑋 = (𝑆𝑗) ↔ (𝑆𝑗) = 𝑋)
235234biimpri 227 . . . . . . . . . . . 12 ((𝑆𝑗) = 𝑋𝑋 = (𝑆𝑗))
236235adantl 482 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑋 = (𝑆𝑗))
237233, 236breqtrd 5131 . . . . . . . . . 10 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑌 < (𝑆𝑗))
238237adantlr 713 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → 𝑌 < (𝑆𝑗))
239226, 227, 229, 231, 238lelttrd 11313 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) < (𝑆𝑗))
240239adantllr 717 . . . . . . 7 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) < (𝑆𝑗))
241 simpr 485 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) = 𝑋)
242198, 139eqbrtrid 5140 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1)))
243242adantr 481 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1)))
244241, 243eqbrtrd 5127 . . . . . . . 8 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
245244adantlr 713 . . . . . . 7 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
246240, 245jca 512 . . . . . 6 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
247225, 246mtand 814 . . . . 5 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆𝑗) = 𝑋)
248247nrexdv 3146 . . . 4 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
249 isof1o 7268 . . . . . . . . 9 (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto𝐻)
250206, 249syl 17 . . . . . . . 8 (𝜑𝑆:(0...𝑁)–1-1-onto𝐻)
251 f1ofo 6791 . . . . . . . 8 (𝑆:(0...𝑁)–1-1-onto𝐻𝑆:(0...𝑁)–onto𝐻)
252250, 251syl 17 . . . . . . 7 (𝜑𝑆:(0...𝑁)–onto𝐻)
253 foelrn 7056 . . . . . . 7 ((𝑆:(0...𝑁)–onto𝐻𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗))
254252, 253sylan 580 . . . . . 6 ((𝜑𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗))
255234rexbii 3097 . . . . . 6 (∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
256254, 255sylib 217 . . . . 5 ((𝜑𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
257256adantlr 713 . . . 4 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
258248, 257mtand 814 . . 3 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ 𝑋𝐻)
259199, 258pm2.65da 815 . 2 (𝜑 → ¬ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
26052, 60, 259nltled 11305 1 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄𝐾))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wral 3064  wrex 3073  {crab 3407  cun 3908  wss 3910  {cpr 4588   class class class wbr 5105  cmpt 5188  dom cdm 5633  ran crn 5634  cio 6446  Fun wfun 6490  wf 6492  ontowfo 6494  1-1-ontowf1o 6495  cfv 6496   Isom wiso 6497  (class class class)co 7357  m cmap 8765  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  *cxr 11188   < clt 11189  cle 11190  cmin 11385   / cdiv 11812  cn 12153  cz 12499  (,]cioc 13265  [,)cico 13266  [,]cicc 13267  ...cfz 13424  ..^cfzo 13567  cfl 13695  chash 14230
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ioo 13268  df-ioc 13269  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-rest 17304  df-topgen 17325  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-top 22243  df-topon 22260  df-bases 22296  df-cld 22370  df-ntr 22371  df-cls 22372  df-nei 22449  df-lp 22487  df-cmp 22738
This theorem is referenced by:  fourierdlem79  44416
  Copyright terms: Public domain W3C validator