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 41864
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 6982 . . . . . . . . 9 (𝑥 = (𝑆‘(𝐽 + 1)) → (𝐵𝑥) = (𝐵 − (𝑆‘(𝐽 + 1))))
54oveq1d 6989 . . . . . . . 8 (𝑥 = (𝑆‘(𝐽 + 1)) → ((𝐵𝑥) / 𝑇) = ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇))
65fveq2d 6501 . . . . . . 7 (𝑥 = (𝑆‘(𝐽 + 1)) → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)))
76oveq1d 6989 . . . . . 6 (𝑥 = (𝑆‘(𝐽 + 1)) → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇))
83, 7oveq12d 6992 . . . . 5 (𝑥 = (𝑆‘(𝐽 + 1)) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
98adantl 474 . . . 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 41855 . . . . . . . . . 10 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2221simpld 487 . . . . . . . . 9 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
2322simprd 488 . . . . . . . 8 (𝜑𝑆 ∈ (𝑂𝑁))
2422simpld 487 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
2517fourierdlem2 41804 . . . . . . . . 9 (𝑁 ∈ ℕ → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
2624, 25syl 17 . . . . . . . 8 (𝜑 → (𝑆 ∈ (𝑂𝑁) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
2723, 26mpbid 224 . . . . . . 7 (𝜑 → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) ∧ (((𝑆‘0) = 𝐶 ∧ (𝑆𝑁) = 𝐷) ∧ ∀𝑖 ∈ (0..^𝑁)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
2827simpld 487 . . . . . 6 (𝜑𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)))
29 elmapi 8224 . . . . . 6 (𝑆 ∈ (ℝ ↑𝑚 (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3028, 29syl 17 . . . . 5 (𝜑𝑆:(0...𝑁)⟶ℝ)
31 fourierdlem63.j . . . . . 6 (𝜑𝐽 ∈ (0..^𝑁))
32 fzofzp1 12946 . . . . . 6 (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
3331, 32syl 17 . . . . 5 (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
3430, 33ffvelrnd 6675 . . . 4 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
3511, 12, 13fourierdlem11 41813 . . . . . . . . . . 11 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
3635simp2d 1123 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
3736, 34resubcld 10865 . . . . . . . . 9 (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
3835simp1d 1122 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
3936, 38resubcld 10865 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
4010, 39syl5eqel 2867 . . . . . . . . 9 (𝜑𝑇 ∈ ℝ)
4135simp3d 1124 . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
4238, 36posdifd 11024 . . . . . . . . . . . 12 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
4341, 42mpbid 224 . . . . . . . . . . 11 (𝜑 → 0 < (𝐵𝐴))
4443, 10syl6breqr 4969 . . . . . . . . . 10 (𝜑 → 0 < 𝑇)
4544gt0ne0d 11001 . . . . . . . . 9 (𝜑𝑇 ≠ 0)
4637, 40, 45redivcld 11265 . . . . . . . 8 (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
4746flcld 12980 . . . . . . 7 (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
4847zred 11897 . . . . . 6 (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
4948, 40remulcld 10466 . . . . 5 (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
5034, 49readdcld 10465 . . . 4 (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
512, 9, 34, 50fvmptd 6599 . . 3 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
5251, 50eqeltrd 2863 . 2 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
5311fourierdlem2 41804 . . . . . . 7 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
5412, 53syl 17 . . . . . 6 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
5513, 54mpbid 224 . . . . 5 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
5655simpld 487 . . . 4 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
57 elmapi 8224 . . . 4 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
5856, 57syl 17 . . 3 (𝜑𝑄:(0...𝑀)⟶ℝ)
59 fourierdlem63.k . . 3 (𝜑𝐾 ∈ (0...𝑀))
6058, 59ffvelrnd 6675 . 2 (𝜑 → (𝑄𝐾) ∈ ℝ)
6114adantr 473 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ∈ ℝ)
6215adantr 473 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐷 ∈ ℝ)
6338rexrd 10486 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ*)
64 iocssre 12629 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
6563, 36, 64syl2anc 576 . . . . . . . . . . 11 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
6638, 36, 41, 10, 1fourierdlem4 41806 . . . . . . . . . . . 12 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
67 fourierdlem63.y . . . . . . . . . . . . . 14 (𝜑𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))))
68 elfzofz 12866 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
6931, 68syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ (0...𝑁))
7030, 69ffvelrnd 6675 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆𝐽) ∈ ℝ)
7134rexrd 10486 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ*)
72 elico2 12613 . . . . . . . . . . . . . . 15 (((𝑆𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ*) → (𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1)))))
7370, 71, 72syl2anc 576 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1)))))
7467, 73mpbid 224 . . . . . . . . . . . . 13 (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1))))
7574simp1d 1122 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ)
7666, 75ffvelrnd 6675 . . . . . . . . . . 11 (𝜑 → (𝐸𝑌) ∈ (𝐴(,]𝐵))
7765, 76sseldd 3858 . . . . . . . . . 10 (𝜑 → (𝐸𝑌) ∈ ℝ)
7877, 75resubcld 10865 . . . . . . . . 9 (𝜑 → ((𝐸𝑌) − 𝑌) ∈ ℝ)
7960, 78resubcld 10865 . . . . . . . 8 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ℝ)
8079adantr 473 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ℝ)
81 icossicc 12637 . . . . . . . . . . . . . 14 ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆𝐽)[,](𝑆‘(𝐽 + 1)))
8214rexrd 10486 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℝ*)
8315rexrd 10486 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ ℝ*)
8417, 24, 23fourierdlem15 41817 . . . . . . . . . . . . . . 15 (𝜑𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
8582, 83, 84, 31fourierdlem8 41810 . . . . . . . . . . . . . 14 (𝜑 → ((𝑆𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
8681, 85syl5ss 3868 . . . . . . . . . . . . 13 (𝜑 → ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
8786, 67sseldd 3858 . . . . . . . . . . . 12 (𝜑𝑌 ∈ (𝐶[,]𝐷))
88 elicc2 12614 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷)))
8914, 15, 88syl2anc 576 . . . . . . . . . . . 12 (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷)))
9087, 89mpbid 224 . . . . . . . . . . 11 (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷))
9190simp2d 1123 . . . . . . . . . 10 (𝜑𝐶𝑌)
9260, 77resubcld 10865 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐾) − (𝐸𝑌)) ∈ ℝ)
93 fourierdlem63.eyltqk . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝑌) < (𝑄𝐾))
9477, 60posdifd 11024 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸𝑌) < (𝑄𝐾) ↔ 0 < ((𝑄𝐾) − (𝐸𝑌))))
9593, 94mpbid 224 . . . . . . . . . . . . 13 (𝜑 → 0 < ((𝑄𝐾) − (𝐸𝑌)))
9692, 95elrpd 12242 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝐾) − (𝐸𝑌)) ∈ ℝ+)
9775, 96ltaddrpd 12278 . . . . . . . . . . 11 (𝜑𝑌 < (𝑌 + ((𝑄𝐾) − (𝐸𝑌))))
9860recnd 10464 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝐾) ∈ ℂ)
9977recnd 10464 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑌) ∈ ℂ)
10075recnd 10464 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ ℂ)
10198, 99, 100subsub3d 10824 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) = (((𝑄𝐾) + 𝑌) − (𝐸𝑌)))
10298, 100addcomd 10638 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐾) + 𝑌) = (𝑌 + (𝑄𝐾)))
103102oveq1d 6989 . . . . . . . . . . . 12 (𝜑 → (((𝑄𝐾) + 𝑌) − (𝐸𝑌)) = ((𝑌 + (𝑄𝐾)) − (𝐸𝑌)))
104100, 98, 99addsubassd 10814 . . . . . . . . . . . 12 (𝜑 → ((𝑌 + (𝑄𝐾)) − (𝐸𝑌)) = (𝑌 + ((𝑄𝐾) − (𝐸𝑌))))
105101, 103, 1043eqtrrd 2816 . . . . . . . . . . 11 (𝜑 → (𝑌 + ((𝑄𝐾) − (𝐸𝑌))) = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10697, 105breqtrd 4953 . . . . . . . . . 10 (𝜑𝑌 < ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10714, 75, 79, 91, 106lelttrd 10594 . . . . . . . . 9 (𝜑𝐶 < ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10814, 79, 107ltled 10584 . . . . . . . 8 (𝜑𝐶 ≤ ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
109108adantr 473 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
11034adantr 473 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
11160adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) ∈ ℝ)
11252, 34resubcld 10865 . . . . . . . . . . . 12 (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
113112adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
114111, 113resubcld 10865 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ)
11574simp3d 1124 . . . . . . . . . . . . . 14 (𝜑𝑌 < (𝑆‘(𝐽 + 1)))
11675, 34, 115ltled 10584 . . . . . . . . . . . . 13 (𝜑𝑌 ≤ (𝑆‘(𝐽 + 1)))
11738, 36, 41, 10, 1, 75, 34, 116fourierdlem7 41809 . . . . . . . . . . . 12 (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸𝑌) − 𝑌))
118112, 78, 60, 117lesub2dd 11054 . . . . . . . . . . 11 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
119118adantr 473 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
12098adantr 473 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) ∈ ℂ)
12152recnd 10464 . . . . . . . . . . . . . 14 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
122121adantr 473 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
123110recnd 10464 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ)
124120, 122, 123subsubd 10822 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))))
12598, 121subcld 10794 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ)
12634recnd 10464 . . . . . . . . . . . . . 14 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
127125, 126addcomd 10638 . . . . . . . . . . . . 13 (𝜑 → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
128127adantr 473 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
129124, 128eqtrd 2811 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
130 simpr 477 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
13152adantr 473 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
132111, 131sublt0d 11063 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))))
133130, 132mpbird 249 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0)
134111, 131resubcld 10865 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
135 ltaddneg 10651 . . . . . . . . . . . . 13 ((((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
136134, 110, 135syl2anc 576 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1))))
137133, 136mpbid 224 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))) < (𝑆‘(𝐽 + 1)))
138129, 137eqbrtrd 4949 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1)))
13980, 114, 110, 119, 138lelttrd 10594 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1)))
14084, 33ffvelrnd 6675 . . . . . . . . . . . 12 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
141 elicc2 12614 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
14214, 15, 141syl2anc 576 . . . . . . . . . . . 12 (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
143140, 142mpbid 224 . . . . . . . . . . 11 (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))
144143simp3d 1124 . . . . . . . . . 10 (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
145144adantr 473 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
14680, 110, 62, 139, 145ltletrd 10596 . . . . . . . 8 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) < 𝐷)
14780, 62, 146ltled 10584 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ 𝐷)
14861, 62, 80, 109, 147eliccd 41189 . . . . . 6 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ (𝐶[,]𝐷))
149 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌𝑥 = 𝑌)
150 oveq2 6982 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑌 → (𝐵𝑥) = (𝐵𝑌))
151150oveq1d 6989 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑌) / 𝑇))
152151fveq2d 6501 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑌) / 𝑇)))
153152oveq1d 6989 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇))
154149, 153oveq12d 6992 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
155154adantl 474 . . . . . . . . . . . . 13 ((𝜑𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
15636, 75resubcld 10865 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵𝑌) ∈ ℝ)
157156, 40, 45redivcld 11265 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵𝑌) / 𝑇) ∈ ℝ)
158157flcld 12980 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℤ)
159158zred 11897 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℝ)
160159, 40remulcld 10466 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) ∈ ℝ)
16175, 160readdcld 10465 . . . . . . . . . . . . 13 (𝜑 → (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) ∈ ℝ)
1622, 155, 75, 161fvmptd 6599 . . . . . . . . . . . 12 (𝜑 → (𝐸𝑌) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
163162oveq1d 6989 . . . . . . . . . . 11 (𝜑 → ((𝐸𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌))
164163oveq1d 6989 . . . . . . . . . 10 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇))
165160recnd 10464 . . . . . . . . . . . 12 (𝜑 → ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) ∈ ℂ)
166100, 165pncan2d 10796 . . . . . . . . . . 11 (𝜑 → ((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇))
167166oveq1d 6989 . . . . . . . . . 10 (𝜑 → (((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) / 𝑇))
168159recnd 10464 . . . . . . . . . . 11 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℂ)
16940recnd 10464 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
170168, 169, 45divcan4d 11219 . . . . . . . . . 10 (𝜑 → (((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵𝑌) / 𝑇)))
171164, 167, 1703eqtrd 2815 . . . . . . . . 9 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵𝑌) / 𝑇)))
172171, 158eqeltrd 2863 . . . . . . . 8 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) ∈ ℤ)
17378recnd 10464 . . . . . . . . . . . 12 (𝜑 → ((𝐸𝑌) − 𝑌) ∈ ℂ)
174173, 169, 45divcan1d 11214 . . . . . . . . . . 11 (𝜑 → ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸𝑌) − 𝑌))
175174oveq2d 6990 . . . . . . . . . 10 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((𝐸𝑌) − 𝑌)))
17698, 173npcand 10798 . . . . . . . . . 10 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((𝐸𝑌) − 𝑌)) = (𝑄𝐾))
177175, 176eqtrd 2811 . . . . . . . . 9 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄𝐾))
178 ffun 6345 . . . . . . . . . . 11 (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
17958, 178syl 17 . . . . . . . . . 10 (𝜑 → Fun 𝑄)
18058fdmd 6351 . . . . . . . . . . 11 (𝜑 → dom 𝑄 = (0...𝑀))
18159, 180eleqtrrd 2866 . . . . . . . . . 10 (𝜑𝐾 ∈ dom 𝑄)
182 fvelrn 6667 . . . . . . . . . 10 ((Fun 𝑄𝐾 ∈ dom 𝑄) → (𝑄𝐾) ∈ ran 𝑄)
183179, 181, 182syl2anc 576 . . . . . . . . 9 (𝜑 → (𝑄𝐾) ∈ ran 𝑄)
184177, 183eqeltrd 2863 . . . . . . . 8 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)
185 oveq1 6981 . . . . . . . . . . 11 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇))
186185oveq2d 6990 . . . . . . . . . 10 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)))
187186eleq1d 2847 . . . . . . . . 9 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → ((((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄))
188187rspcev 3532 . . . . . . . 8 (((((𝐸𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
189172, 184, 188syl2anc 576 . . . . . . 7 (𝜑 → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
190189adantr 473 . . . . . 6 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
191 oveq1 6981 . . . . . . . . 9 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)))
192191eleq1d 2847 . . . . . . . 8 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
193192rexbidv 3239 . . . . . . 7 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
194193elrab 3592 . . . . . 6 (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
195148, 190, 194sylanbrc 575 . . . . 5 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
196 elun2 4041 . . . . 5 (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
197195, 196syl 17 . . . 4 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
198 fourierdlem63.x . . . 4 𝑋 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌))
199197, 198, 183eltr4g 2880 . . 3 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋𝐻)
200 elfzelz 12721 . . . . . . . . 9 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
201200ad2antlr 714 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ)
202 elfzoelz 12851 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ ℤ)
20331, 202syl 17 . . . . . . . . . 10 (𝜑𝐽 ∈ ℤ)
204203ad2antrr 713 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 ∈ ℤ)
205 simpr 477 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → (𝑆𝐽) < (𝑆𝑗))
20621simprd 488 . . . . . . . . . . . . 13 (𝜑𝑆 Isom < , < ((0...𝑁), 𝐻))
207206ad2antrr 713 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
20869ad2antrr 713 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝐽 ∈ (0...𝑁))
209 simplr 756 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝑗 ∈ (0...𝑁))
210 isorel 6900 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝐽 ∈ (0...𝑁) ∧ 𝑗 ∈ (0...𝑁))) → (𝐽 < 𝑗 ↔ (𝑆𝐽) < (𝑆𝑗)))
211207, 208, 209, 210syl12anc 824 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → (𝐽 < 𝑗 ↔ (𝑆𝐽) < (𝑆𝑗)))
212205, 211mpbird 249 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝐽) < (𝑆𝑗)) → 𝐽 < 𝑗)
213212adantrr 704 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝐽 < 𝑗)
214 simpr 477 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
215206ad2antrr 713 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑆 Isom < , < ((0...𝑁), 𝐻))
216 simplr 756 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 ∈ (0...𝑁))
21733ad2antrr 713 . . . . . . . . . . . 12 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝐽 + 1) ∈ (0...𝑁))
218 isorel 6900 . . . . . . . . . . . 12 ((𝑆 Isom < , < ((0...𝑁), 𝐻) ∧ (𝑗 ∈ (0...𝑁) ∧ (𝐽 + 1) ∈ (0...𝑁))) → (𝑗 < (𝐽 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
219215, 216, 217, 218syl12anc 824 . . . . . . . . . . 11 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → (𝑗 < (𝐽 + 1) ↔ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
220214, 219mpbird 249 . . . . . . . . . 10 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))) → 𝑗 < (𝐽 + 1))
221220adantrl 703 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 < (𝐽 + 1))
222 btwnnz 11868 . . . . . . . . 9 ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
223204, 213, 221, 222syl3anc 1351 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → ¬ 𝑗 ∈ ℤ)
224201, 223pm2.65da 804 . . . . . . 7 ((𝜑𝑗 ∈ (0...𝑁)) → ¬ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
225224adantlr 702 . . . . . 6 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
22670ad2antrr 713 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) ∈ ℝ)
22775ad2antrr 713 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → 𝑌 ∈ ℝ)
22830ffvelrnda 6674 . . . . . . . . . 10 ((𝜑𝑗 ∈ (0...𝑁)) → (𝑆𝑗) ∈ ℝ)
229228adantr 473 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) ∈ ℝ)
23074simp2d 1123 . . . . . . . . . 10 (𝜑 → (𝑆𝐽) ≤ 𝑌)
231230ad2antrr 713 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) ≤ 𝑌)
232106, 198syl6breqr 4969 . . . . . . . . . . . 12 (𝜑𝑌 < 𝑋)
233232adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑌 < 𝑋)
234 eqcom 2782 . . . . . . . . . . . . 13 (𝑋 = (𝑆𝑗) ↔ (𝑆𝑗) = 𝑋)
235234biimpri 220 . . . . . . . . . . . 12 ((𝑆𝑗) = 𝑋𝑋 = (𝑆𝑗))
236235adantl 474 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑋 = (𝑆𝑗))
237233, 236breqtrd 4953 . . . . . . . . . 10 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑌 < (𝑆𝑗))
238237adantlr 702 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → 𝑌 < (𝑆𝑗))
239226, 227, 229, 231, 238lelttrd 10594 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) < (𝑆𝑗))
240239adantllr 706 . . . . . . 7 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) < (𝑆𝑗))
241 simpr 477 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) = 𝑋)
242198, 139syl5eqbr 4962 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1)))
243242adantr 473 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1)))
244241, 243eqbrtrd 4949 . . . . . . . 8 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
245244adantlr 702 . . . . . . 7 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
246240, 245jca 504 . . . . . 6 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
247225, 246mtand 803 . . . . 5 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆𝑗) = 𝑋)
248247nrexdv 3212 . . . 4 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
249 isof1o 6897 . . . . . . . . 9 (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto𝐻)
250206, 249syl 17 . . . . . . . 8 (𝜑𝑆:(0...𝑁)–1-1-onto𝐻)
251 f1ofo 6449 . . . . . . . 8 (𝑆:(0...𝑁)–1-1-onto𝐻𝑆:(0...𝑁)–onto𝐻)
252250, 251syl 17 . . . . . . 7 (𝜑𝑆:(0...𝑁)–onto𝐻)
253 foelrn 6693 . . . . . . 7 ((𝑆:(0...𝑁)–onto𝐻𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗))
254252, 253sylan 572 . . . . . 6 ((𝜑𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗))
255234rexbii 3191 . . . . . 6 (∃𝑗 ∈ (0...𝑁)𝑋 = (𝑆𝑗) ↔ ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
256254, 255sylib 210 . . . . 5 ((𝜑𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
257256adantlr 702 . . . 4 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑋𝐻) → ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
258248, 257mtand 803 . . 3 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ 𝑋𝐻)
259199, 258pm2.65da 804 . 2 (𝜑 → ¬ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
26052, 60, 259nltled 10586 1 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄𝐾))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2048  wral 3085  wrex 3086  {crab 3089  cun 3826  wss 3828  {cpr 4441   class class class wbr 4927  cmpt 5006  dom cdm 5404  ran crn 5405  cio 6148  Fun wfun 6180  wf 6182  ontowfo 6184  1-1-ontowf1o 6185  cfv 6186   Isom wiso 6187  (class class class)co 6974  𝑚 cmap 8202  cc 10329  cr 10330  0cc0 10331  1c1 10332   + caddc 10334   · cmul 10336  *cxr 10469   < clt 10470  cle 10471  cmin 10666   / cdiv 11094  cn 11435  cz 11790  (,]cioc 12552  [,)cico 12553  [,]cicc 12554  ...cfz 12705  ..^cfzo 12846  cfl 12972  chash 13502
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2747  ax-rep 5047  ax-sep 5058  ax-nul 5065  ax-pow 5117  ax-pr 5184  ax-un 7277  ax-inf2 8894  ax-cnex 10387  ax-resscn 10388  ax-1cn 10389  ax-icn 10390  ax-addcl 10391  ax-addrcl 10392  ax-mulcl 10393  ax-mulrcl 10394  ax-mulcom 10395  ax-addass 10396  ax-mulass 10397  ax-distr 10398  ax-i2m1 10399  ax-1ne0 10400  ax-1rid 10401  ax-rnegex 10402  ax-rrecex 10403  ax-cnre 10404  ax-pre-lttri 10405  ax-pre-lttrn 10406  ax-pre-ltadd 10407  ax-pre-mulgt0 10408  ax-pre-sup 10409
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2756  df-cleq 2768  df-clel 2843  df-nfc 2915  df-ne 2965  df-nel 3071  df-ral 3090  df-rex 3091  df-reu 3092  df-rmo 3093  df-rab 3094  df-v 3414  df-sbc 3681  df-csb 3786  df-dif 3831  df-un 3833  df-in 3835  df-ss 3842  df-pss 3844  df-nul 4178  df-if 4349  df-pw 4422  df-sn 4440  df-pr 4442  df-tp 4444  df-op 4446  df-uni 4711  df-int 4748  df-iun 4792  df-iin 4793  df-br 4928  df-opab 4990  df-mpt 5007  df-tr 5029  df-id 5309  df-eprel 5314  df-po 5323  df-so 5324  df-fr 5363  df-se 5364  df-we 5365  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-pred 5984  df-ord 6030  df-on 6031  df-lim 6032  df-suc 6033  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-isom 6195  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-om 7395  df-1st 7498  df-2nd 7499  df-wrecs 7747  df-recs 7809  df-rdg 7847  df-1o 7901  df-oadd 7905  df-er 8085  df-map 8204  df-en 8303  df-dom 8304  df-sdom 8305  df-fin 8306  df-fi 8666  df-sup 8697  df-inf 8698  df-oi 8765  df-dju 9120  df-card 9158  df-pnf 10472  df-mnf 10473  df-xr 10474  df-ltxr 10475  df-le 10476  df-sub 10668  df-neg 10669  df-div 11095  df-nn 11436  df-2 11500  df-3 11501  df-n0 11705  df-xnn0 11777  df-z 11791  df-uz 12056  df-q 12160  df-rp 12202  df-xneg 12321  df-xadd 12322  df-xmul 12323  df-ioo 12555  df-ioc 12556  df-ico 12557  df-icc 12558  df-fz 12706  df-fzo 12847  df-fl 12974  df-seq 13182  df-exp 13242  df-hash 13503  df-cj 14313  df-re 14314  df-im 14315  df-sqrt 14449  df-abs 14450  df-rest 16546  df-topgen 16567  df-psmet 20233  df-xmet 20234  df-met 20235  df-bl 20236  df-mopn 20237  df-top 21200  df-topon 21217  df-bases 21252  df-cld 21325  df-ntr 21326  df-cls 21327  df-nei 21404  df-lp 21442  df-cmp 21693
This theorem is referenced by:  fourierdlem79  41880
  Copyright terms: Public domain W3C validator