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 40858
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 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem63.m (𝜑𝑀 ∈ ℕ)
fourierdlem63.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem63.c (𝜑𝐶 ∈ ℝ)
fourierdlem63.d (𝜑𝐷 ∈ ℝ)
fourierdlem63.cltd (𝜑𝐶 < 𝐷)
fourierdlem63.o 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (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 6809 . . . . . . . . 9 (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
54oveq1d 6816 . . . . . . . 8 (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
65fveq2d 6344 . . . . . . 7 (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
76oveq1d 6816 . . . . . 6 (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
83, 7oveq12d 6819 . . . . 5 (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
98adantl 473 . . . 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...𝑁), 𝐻))
2110, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20fourierdlem54 40849 . . . . . . . . . 10 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2221simpld 477 . . . . . . . . 9 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
2322simprd 482 . . . . . . . 8 (𝜑𝑆 ∈ (𝑂𝑁))
2422simpld 477 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
2517fourierdlem2 40798 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
2624, 25syl 17 . . . . . . . 8 (𝜑 → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
2723, 26mpbid 222 . . . . . . 7 (𝜑 → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
2827simpld 477 . . . . . 6 (𝜑𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)))
29 elmapi 8033 . . . . . 6 (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3028, 29syl 17 . . . . 5 (𝜑𝑆:(0...𝑁)⟶ℝ)
31 fourierdlem63.j . . . . . 6 (𝜑𝐽 ∈ (0..^𝑁))
32 fzofzp1 12730 . . . . . 6 (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
3331, 32syl 17 . . . . 5 (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
3430, 33ffvelrnd 6511 . . . 4 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
3511, 12, 13fourierdlem11 40807 . . . . . . . . . . 11 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
3635simp2d 1135 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
3736, 34resubcld 10621 . . . . . . . . 9 (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
3835simp1d 1134 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
3936, 38resubcld 10621 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
4010, 39syl5eqel 2831 . . . . . . . . 9 (𝜑𝑇 ∈ ℝ)
4135simp3d 1136 . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
4238, 36posdifd 10777 . . . . . . . . . . . 12 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
4341, 42mpbid 222 . . . . . . . . . . 11 (𝜑 → 0 < (𝐵𝐴))
4443, 10syl6breqr 4834 . . . . . . . . . 10 (𝜑 → 0 < 𝑇)
4544gt0ne0d 10755 . . . . . . . . 9 (𝜑𝑇 ≠ 0)
4637, 40, 45redivcld 11016 . . . . . . . 8 (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
4746flcld 12764 . . . . . . 7 (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
4847zred 11645 . . . . . 6 (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
4948, 40remulcld 10233 . . . . 5 (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
5034, 49readdcld 10232 . . . 4 (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
512, 9, 34, 50fvmptd 6438 . . 3 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
5251, 50eqeltrd 2827 . 2 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
5311fourierdlem2 40798 . . . . . . 7 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
5412, 53syl 17 . . . . . 6 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
5513, 54mpbid 222 . . . . 5 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
5655simpld 477 . . . 4 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
57 elmapi 8033 . . . 4 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
5856, 57syl 17 . . 3 (𝜑𝑄:(0...𝑀)⟶ℝ)
59 fourierdlem63.k . . 3 (𝜑𝐾 ∈ (0...𝑀))
6058, 59ffvelrnd 6511 . 2 (𝜑 → (𝑄𝐾) ∈ ℝ)
6114adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ)
6215adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ)
6338rexrd 10252 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ*)
64 iocssre 12417 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
6563, 36, 64syl2anc 696 . . . . . . . . . . 11 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
6638, 36, 41, 10, 1fourierdlem4 40800 . . . . . . . . . . . 12 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
67 fourierdlem63.y . . . . . . . . . . . . . 14 (𝜑𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))))
68 elfzofz 12650 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
6931, 68syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ (0...𝑁))
7030, 69ffvelrnd 6511 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆𝐽) ∈ ℝ)
7134rexrd 10252 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ*)
72 elico2 12401 . . . . . . . . . . . . . . 15 (((𝑆𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ*) → (𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1)))))
7370, 71, 72syl2anc 696 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1)))))
7467, 73mpbid 222 . . . . . . . . . . . . 13 (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1))))
7574simp1d 1134 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ)
7666, 75ffvelrnd 6511 . . . . . . . . . . 11 (𝜑 → (𝐸𝑌) ∈ (𝐴(,]𝐵))
7765, 76sseldd 3733 . . . . . . . . . 10 (𝜑 → (𝐸𝑌) ∈ ℝ)
7877, 75resubcld 10621 . . . . . . . . 9 (𝜑 → ((𝐸𝑌) − 𝑌) ∈ ℝ)
7960, 78resubcld 10621 . . . . . . . 8 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ℝ)
8079adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ℝ)
81 icossicc 12424 . . . . . . . . . . . . . 14 ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆𝐽)[,](𝑆‘(𝐽 + 1)))
8214rexrd 10252 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℝ*)
8315rexrd 10252 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ ℝ*)
8417, 24, 23fourierdlem15 40811 . . . . . . . . . . . . . . 15 (𝜑𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
8582, 83, 84, 31fourierdlem8 40804 . . . . . . . . . . . . . 14 (𝜑 → ((𝑆𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
8681, 85syl5ss 3743 . . . . . . . . . . . . 13 (𝜑 → ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
8786, 67sseldd 3733 . . . . . . . . . . . 12 (𝜑𝑌 ∈ (𝐶[,]𝐷))
88 elicc2 12402 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷)))
8914, 15, 88syl2anc 696 . . . . . . . . . . . 12 (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷)))
9087, 89mpbid 222 . . . . . . . . . . 11 (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷))
9190simp2d 1135 . . . . . . . . . 10 (𝜑𝐶𝑌)
9260, 77resubcld 10621 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐾) − (𝐸𝑌)) ∈ ℝ)
93 fourierdlem63.eyltqk . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝑌) < (𝑄𝐾))
9477, 60posdifd 10777 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸𝑌) < (𝑄𝐾) ↔ 0 < ((𝑄𝐾) − (𝐸𝑌))))
9593, 94mpbid 222 . . . . . . . . . . . . 13 (𝜑 → 0 < ((𝑄𝐾) − (𝐸𝑌)))
9692, 95elrpd 12033 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝐾) − (𝐸𝑌)) ∈ ℝ+)
9775, 96ltaddrpd 12069 . . . . . . . . . . 11 (𝜑𝑌 < (𝑌 + ((𝑄𝐾) − (𝐸𝑌))))
9860recnd 10231 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝐾) ∈ ℂ)
9977recnd 10231 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑌) ∈ ℂ)
10075recnd 10231 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ ℂ)
10198, 99, 100subsub3d 10585 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) = (((𝑄𝐾) + 𝑌) − (𝐸𝑌)))
10298, 100addcomd 10401 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐾) + 𝑌) = (𝑌 + (𝑄𝐾)))
103102oveq1d 6816 . . . . . . . . . . . 12 (𝜑 → (((𝑄𝐾) + 𝑌) − (𝐸𝑌)) = ((𝑌 + (𝑄𝐾)) − (𝐸𝑌)))
104100, 98, 99addsubassd 10575 . . . . . . . . . . . 12 (𝜑 → ((𝑌 + (𝑄𝐾)) − (𝐸𝑌)) = (𝑌 + ((𝑄𝐾) − (𝐸𝑌))))
105101, 103, 1043eqtrrd 2787 . . . . . . . . . . 11 (𝜑 → (𝑌 + ((𝑄𝐾) − (𝐸𝑌))) = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10697, 105breqtrd 4818 . . . . . . . . . 10 (𝜑𝑌 < ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10714, 75, 79, 91, 106lelttrd 10358 . . . . . . . . 9 (𝜑𝐶 < ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10814, 79, 107ltled 10348 . . . . . . . 8 (𝜑𝐶 ≤ ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
109108adantr 472 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
11034adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
11160adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) ∈ ℝ)
11252, 34resubcld 10621 . . . . . . . . . . . 12 (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
113112adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
114111, 113resubcld 10621 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ)
11574simp3d 1136 . . . . . . . . . . . . . 14 (𝜑𝑌 < (𝑆‘(𝐽 + 1)))
11675, 34, 115ltled 10348 . . . . . . . . . . . . 13 (𝜑𝑌 ≤ (𝑆‘(𝐽 + 1)))
11738, 36, 41, 10, 1, 75, 34, 116fourierdlem7 40803 . . . . . . . . . . . 12 (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸𝑌) − 𝑌))
118112, 78, 60, 117lesub2dd 10807 . . . . . . . . . . 11 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
119118adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
12098adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) ∈ ℂ)
12152recnd 10231 . . . . . . . . . . . . . 14 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
122121adantr 472 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
123110recnd 10231 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ)
124120, 122, 123subsubd 10583 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))))
12598, 121subcld 10555 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ)
12634recnd 10231 . . . . . . . . . . . . . 14 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
127125, 126addcomd 10401 . . . . . . . . . . . . 13 (𝜑 → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
128127adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
129124, 128eqtrd 2782 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
130 simpr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
13152adantr 472 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
132111, 131sublt0d 10816 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))))
133130, 132mpbird 247 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0)
134111, 131resubcld 10621 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
135 ltaddneg 10414 . . . . . . . . . . . . 13 ((((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
136134, 110, 135syl2anc 696 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
137133, 136mpbid 222 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))
138129, 137eqbrtrd 4814 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1)))
13980, 114, 110, 119, 138lelttrd 10358 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1)))
14084, 33ffvelrnd 6511 . . . . . . . . . . . 12 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
141 elicc2 12402 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
14214, 15, 141syl2anc 696 . . . . . . . . . . . 12 (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
143140, 142mpbid 222 . . . . . . . . . . 11 (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))
144143simp3d 1136 . . . . . . . . . 10 (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
145144adantr 472 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
14680, 110, 62, 139, 145ltletrd 10360 . . . . . . . 8 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) < 𝐷)
14780, 62, 146ltled 10348 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ 𝐷)
14861, 62, 80, 109, 147eliccd 40198 . . . . . 6 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ (𝐶[,]𝐷))
149 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌𝑥 = 𝑌)
150 oveq2 6809 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑌 → (𝐵𝑥) = (𝐵𝑌))
151150oveq1d 6816 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑌) / 𝑇))
152151fveq2d 6344 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑌) / 𝑇)))
153152oveq1d 6816 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇))
154149, 153oveq12d 6819 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
155154adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
15636, 75resubcld 10621 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵𝑌) ∈ ℝ)
157156, 40, 45redivcld 11016 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵𝑌) / 𝑇) ∈ ℝ)
158157flcld 12764 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℤ)
159158zred 11645 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℝ)
160159, 40remulcld 10233 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) ∈ ℝ)
16175, 160readdcld 10232 . . . . . . . . . . . . 13 (𝜑 → (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) ∈ ℝ)
1622, 155, 75, 161fvmptd 6438 . . . . . . . . . . . 12 (𝜑 → (𝐸𝑌) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
163162oveq1d 6816 . . . . . . . . . . 11 (𝜑 → ((𝐸𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌))
164163oveq1d 6816 . . . . . . . . . 10 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇))
165160recnd 10231 . . . . . . . . . . . 12 (𝜑 → ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) ∈ ℂ)
166100, 165pncan2d 10557 . . . . . . . . . . 11 (𝜑 → ((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇))
167166oveq1d 6816 . . . . . . . . . 10 (𝜑 → (((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) / 𝑇))
168159recnd 10231 . . . . . . . . . . 11 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℂ)
16940recnd 10231 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
170168, 169, 45divcan4d 10970 . . . . . . . . . 10 (𝜑 → (((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵𝑌) / 𝑇)))
171164, 167, 1703eqtrd 2786 . . . . . . . . 9 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵𝑌) / 𝑇)))
172171, 158eqeltrd 2827 . . . . . . . 8 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) ∈ ℤ)
17378recnd 10231 . . . . . . . . . . . 12 (𝜑 → ((𝐸𝑌) − 𝑌) ∈ ℂ)
174173, 169, 45divcan1d 10965 . . . . . . . . . . 11 (𝜑 → ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸𝑌) − 𝑌))
175174oveq2d 6817 . . . . . . . . . 10 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((𝐸𝑌) − 𝑌)))
17698, 173npcand 10559 . . . . . . . . . 10 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((𝐸𝑌) − 𝑌)) = (𝑄𝐾))
177175, 176eqtrd 2782 . . . . . . . . 9 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄𝐾))
178 ffun 6197 . . . . . . . . . . 11 (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
17958, 178syl 17 . . . . . . . . . 10 (𝜑 → Fun 𝑄)
180 fdm 6200 . . . . . . . . . . . 12 (𝑄:(0...𝑀)⟶ℝ → dom 𝑄 = (0...𝑀))
18158, 180syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝑄 = (0...𝑀))
18259, 181eleqtrrd 2830 . . . . . . . . . 10 (𝜑𝐾 ∈ dom 𝑄)
183 fvelrn 6503 . . . . . . . . . 10 ((Fun 𝑄𝐾 ∈ dom 𝑄) → (𝑄𝐾) ∈ ran 𝑄)
184179, 182, 183syl2anc 696 . . . . . . . . 9 (𝜑 → (𝑄𝐾) ∈ ran 𝑄)
185177, 184eqeltrd 2827 . . . . . . . 8 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)
186 oveq1 6808 . . . . . . . . . . 11 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇))
187186oveq2d 6817 . . . . . . . . . 10 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)))
188187eleq1d 2812 . . . . . . . . 9 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → ((((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄))
189188rspcev 3437 . . . . . . . 8 (((((𝐸𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
190172, 185, 189syl2anc 696 . . . . . . 7 (𝜑 → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
191190adantr 472 . . . . . 6 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
192 oveq1 6808 . . . . . . . . 9 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)))
193192eleq1d 2812 . . . . . . . 8 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
194193rexbidv 3178 . . . . . . 7 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
195194elrab 3492 . . . . . 6 (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
196148, 191, 195sylanbrc 701 . . . . 5 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
197 elun2 3912 . . . . 5 (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
198196, 197syl 17 . . . 4 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
199 fourierdlem63.x . . . 4 𝑋 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌))
200198, 199, 183eltr4g 2844 . . 3 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋𝐻)
201 elfzelz 12506 . . . . . . . . 9 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
202201ad2antlr 765 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ)
203 elfzoelz 12635 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
20431, 203syl 17 . . . . . . . . . 10 (𝜑𝐽 ∈ ℤ)
205204ad2antrr 764 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 ∈ ℤ)
206 simpr 479 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → (𝑆𝐽) < (𝑆𝑗))
20721simprd 482 . . . . . . . . . . . . 13 (𝜑𝑆 Isom < , < ((0...𝑁), 𝐻))
208207ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
20969ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝐽 ∈ (0...𝑁))
210 simplr 809 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝑗 ∈ (0...𝑁))
211 isorel 6727 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆𝐽) < (𝑆𝑗)))
212208, 209, 210, 211syl12anc 1461 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → (𝐽 < 𝑗 ↔ (𝑆𝐽) < (𝑆𝑗)))
213206, 212mpbird 247 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝐽 < 𝑗)
214213adantrr 755 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 < 𝑗)
215 simpr 479 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
216207ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
217 simplr 809 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 ∈ (0...𝑁))
21833ad2antrr 764 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝐽 + 1) ∈ (0...𝑁))
219 isorel 6727 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
220216, 217, 218, 219syl12anc 1461 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝑗 < (𝐽 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
221215, 220mpbird 247 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 < (𝐽 + 1))
222221adantrl 754 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1))
223 btwnnz 11616 . . . . . . . . 9 ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
224205, 214, 222, 223syl3anc 1463 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → ¬ 𝑗 ∈ ℤ)
225202, 224pm2.65da 601 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑁)) → ¬ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
226225adantlr 753 . . . . . 6 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
22770ad2antrr 764 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) ∈ ℝ)
22875ad2antrr 764 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → 𝑌 ∈ ℝ)
22930ffvelrnda 6510 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑆𝑗) ∈ ℝ)
230229adantr 472 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) ∈ ℝ)
23174simp2d 1135 . . . . . . . . . 10 (𝜑 → (𝑆𝐽) ≤ 𝑌)
232231ad2antrr 764 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) ≤ 𝑌)
233106, 199syl6breqr 4834 . . . . . . . . . . . 12 (𝜑𝑌 < 𝑋)
234233adantr 472 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑌 < 𝑋)
235 eqcom 2755 . . . . . . . . . . . . 13 (𝑋 = (𝑆𝑗) ↔ (𝑆𝑗) = 𝑋)
236235biimpri 218 . . . . . . . . . . . 12 ((𝑆𝑗) = 𝑋𝑋 = (𝑆𝑗))
237236adantl 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑋 = (𝑆𝑗))
238234, 237breqtrd 4818 . . . . . . . . . 10 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑌 < (𝑆𝑗))
239238adantlr 753 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → 𝑌 < (𝑆𝑗))
240227, 228, 230, 232, 239lelttrd 10358 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) < (𝑆𝑗))
241240adantllr 757 . . . . . . 7 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) < (𝑆𝑗))
242 simpr 479 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) = 𝑋)
243199, 139syl5eqbr 4827 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1)))
244243adantr 472 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1)))
245242, 244eqbrtrd 4814 . . . . . . . 8 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
246245adantlr 753 . . . . . . 7 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
247241, 246jca 555 . . . . . 6 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
248226, 247mtand 694 . . . . 5 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆𝑗) = 𝑋)
249248nrexdv 3127 . . . 4 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
250 isof1o 6724 . . . . . . . . 9 (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto𝐻)
251207, 250syl 17 . . . . . . . 8 (𝜑𝑆:(0...𝑁)–1-1-onto𝐻)
252 f1ofo 6293 . . . . . . . 8 (𝑆:(0...𝑁)–1-1-onto𝐻𝑆:(0...𝑁)–onto𝐻)
253251, 252syl 17 . . . . . . 7 (𝜑𝑆:(0...𝑁)–onto𝐻)
254 foelrn 6529 . . . . . . 7 ((𝑆:(0...𝑁)–onto𝐻𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗))
255253, 254sylan 489 . . . . . 6 ((𝜑𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗))
256235rexbii 3167 . . . . . 6 (∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
257255, 256sylib 208 . . . . 5 ((𝜑𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
258257adantlr 753 . . . 4 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
259249, 258mtand 694 . . 3 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ 𝑋𝐻)
260200, 259pm2.65da 601 . 2 (𝜑 → ¬ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
26152, 60, 260nltled 10350 1 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄𝐾))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1620  wcel 2127  wral 3038  wrex 3039  {crab 3042  cun 3701  wss 3703  {cpr 4311   class class class wbr 4792  cmpt 4869  dom cdm 5254  ran crn 5255  cio 5998  Fun wfun 6031  wf 6033  ontowfo 6035  1-1-ontowf1o 6036  cfv 6037   Isom wiso 6038  (class class class)co 6801  𝑚 cmap 8011  cc 10097  cr 10098  0cc0 10099  1c1 10100   + caddc 10102   · cmul 10104  *cxr 10236   < clt 10237  cle 10238  cmin 10429   / cdiv 10847  cn 11183  cz 11540  (,]cioc 12340  [,)cico 12341  [,]cicc 12342  ...cfz 12490  ..^cfzo 12630  cfl 12756  chash 13282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-rep 4911  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-inf2 8699  ax-cnex 10155  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-mulcom 10163  ax-addass 10164  ax-mulass 10165  ax-distr 10166  ax-i2m1 10167  ax-1ne0 10168  ax-1rid 10169  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172  ax-pre-lttri 10173  ax-pre-lttrn 10174  ax-pre-ltadd 10175  ax-pre-mulgt0 10176  ax-pre-sup 10177
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-reu 3045  df-rmo 3046  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-int 4616  df-iun 4662  df-iin 4663  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-se 5214  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-isom 6046  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-om 7219  df-1st 7321  df-2nd 7322  df-wrecs 7564  df-recs 7625  df-rdg 7663  df-1o 7717  df-oadd 7721  df-er 7899  df-map 8013  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-fi 8470  df-sup 8501  df-inf 8502  df-oi 8568  df-card 8926  df-cda 9153  df-pnf 10239  df-mnf 10240  df-xr 10241  df-ltxr 10242  df-le 10243  df-sub 10431  df-neg 10432  df-div 10848  df-nn 11184  df-2 11242  df-3 11243  df-n0 11456  df-xnn0 11527  df-z 11541  df-uz 11851  df-q 11953  df-rp 11997  df-xneg 12110  df-xadd 12111  df-xmul 12112  df-ioo 12343  df-ioc 12344  df-ico 12345  df-icc 12346  df-fz 12491  df-fzo 12631  df-fl 12758  df-seq 12967  df-exp 13026  df-hash 13283  df-cj 14009  df-re 14010  df-im 14011  df-sqrt 14145  df-abs 14146  df-rest 16256  df-topgen 16277  df-psmet 19911  df-xmet 19912  df-met 19913  df-bl 19914  df-mopn 19915  df-top 20872  df-topon 20889  df-bases 20923  df-cld 20996  df-ntr 20997  df-cls 20998  df-nei 21075  df-lp 21113  df-cmp 21363
This theorem is referenced by:  fourierdlem79  40874
  Copyright terms: Public domain W3C validator