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 46184
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 6910 . . . . . . 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 46175 . . . . . . . . . 10 (𝜑 → ((𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)) ∧ 𝑆 Isom < , < ((0...𝑁), 𝐻)))
2221simpld 494 . . . . . . . . 9 (𝜑 → (𝑁 ∈ ℕ ∧ 𝑆 ∈ (𝑂𝑁)))
2322simprd 495 . . . . . . . 8 (𝜑𝑆 ∈ (𝑂𝑁))
2422simpld 494 . . . . . . . . 9 (𝜑𝑁 ∈ ℕ)
2517fourierdlem2 46124 . . . . . . . . 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 8889 . . . . . 6 (𝑆 ∈ (ℝ ↑m (0...𝑁)) → 𝑆:(0...𝑁)⟶ℝ)
3028, 29syl 17 . . . . 5 (𝜑𝑆:(0...𝑁)⟶ℝ)
31 fourierdlem63.j . . . . . 6 (𝜑𝐽 ∈ (0..^𝑁))
32 fzofzp1 13803 . . . . . 6 (𝐽 ∈ (0..^𝑁) → (𝐽 + 1) ∈ (0...𝑁))
3331, 32syl 17 . . . . 5 (𝜑 → (𝐽 + 1) ∈ (0...𝑁))
3430, 33ffvelcdmd 7105 . . . 4 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ)
3511, 12, 13fourierdlem11 46133 . . . . . . . . . . 11 (𝜑 → (𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 < 𝐵))
3635simp2d 1144 . . . . . . . . . 10 (𝜑𝐵 ∈ ℝ)
3736, 34resubcld 11691 . . . . . . . . 9 (𝜑 → (𝐵 − (𝑆‘(𝐽 + 1))) ∈ ℝ)
3835simp1d 1143 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
3936, 38resubcld 11691 . . . . . . . . . 10 (𝜑 → (𝐵𝐴) ∈ ℝ)
4010, 39eqeltrid 2845 . . . . . . . . 9 (𝜑𝑇 ∈ ℝ)
4135simp3d 1145 . . . . . . . . . . . 12 (𝜑𝐴 < 𝐵)
4238, 36posdifd 11850 . . . . . . . . . . . 12 (𝜑 → (𝐴 < 𝐵 ↔ 0 < (𝐵𝐴)))
4341, 42mpbid 232 . . . . . . . . . . 11 (𝜑 → 0 < (𝐵𝐴))
4443, 10breqtrrdi 5185 . . . . . . . . . 10 (𝜑 → 0 < 𝑇)
4544gt0ne0d 11827 . . . . . . . . 9 (𝜑𝑇 ≠ 0)
4637, 40, 45redivcld 12095 . . . . . . . 8 (𝜑 → ((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇) ∈ ℝ)
4746flcld 13838 . . . . . . 7 (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℤ)
4847zred 12722 . . . . . 6 (𝜑 → (⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) ∈ ℝ)
4948, 40remulcld 11291 . . . . 5 (𝜑 → ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇) ∈ ℝ)
5034, 49readdcld 11290 . . . 4 (𝜑 → ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)) ∈ ℝ)
512, 9, 34, 50fvmptd 7023 . . 3 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((⌊‘((𝐵 − (𝑆‘(𝐽 + 1))) / 𝑇)) · 𝑇)))
5251, 50eqeltrd 2841 . 2 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
5311fourierdlem2 46124 . . . . . . 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 8889 . . . 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 11311 . . . . . . . . . . . 12 (𝜑𝐴 ∈ ℝ*)
64 iocssre 13467 . . . . . . . . . . . 12 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ) → (𝐴(,]𝐵) ⊆ ℝ)
6563, 36, 64syl2anc 584 . . . . . . . . . . 11 (𝜑 → (𝐴(,]𝐵) ⊆ ℝ)
6638, 36, 41, 10, 1fourierdlem4 46126 . . . . . . . . . . . 12 (𝜑𝐸:ℝ⟶(𝐴(,]𝐵))
67 fourierdlem63.y . . . . . . . . . . . . . 14 (𝜑𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))))
68 elfzofz 13715 . . . . . . . . . . . . . . . . 17 (𝐽 ∈ (0..^𝑁) → 𝐽 ∈ (0...𝑁))
6931, 68syl 17 . . . . . . . . . . . . . . . 16 (𝜑𝐽 ∈ (0...𝑁))
7030, 69ffvelcdmd 7105 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆𝐽) ∈ ℝ)
7134rexrd 11311 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℝ*)
72 elico2 13451 . . . . . . . . . . . . . . 15 (((𝑆𝐽) ∈ ℝ ∧ (𝑆‘(𝐽 + 1)) ∈ ℝ*) → (𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1)))))
7370, 71, 72syl2anc 584 . . . . . . . . . . . . . 14 (𝜑 → (𝑌 ∈ ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ↔ (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1)))))
7467, 73mpbid 232 . . . . . . . . . . . . 13 (𝜑 → (𝑌 ∈ ℝ ∧ (𝑆𝐽) ≤ 𝑌𝑌 < (𝑆‘(𝐽 + 1))))
7574simp1d 1143 . . . . . . . . . . . 12 (𝜑𝑌 ∈ ℝ)
7666, 75ffvelcdmd 7105 . . . . . . . . . . 11 (𝜑 → (𝐸𝑌) ∈ (𝐴(,]𝐵))
7765, 76sseldd 3984 . . . . . . . . . 10 (𝜑 → (𝐸𝑌) ∈ ℝ)
7877, 75resubcld 11691 . . . . . . . . 9 (𝜑 → ((𝐸𝑌) − 𝑌) ∈ ℝ)
7960, 78resubcld 11691 . . . . . . . 8 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ℝ)
8079adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ℝ)
81 icossicc 13476 . . . . . . . . . . . . . 14 ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ ((𝑆𝐽)[,](𝑆‘(𝐽 + 1)))
8214rexrd 11311 . . . . . . . . . . . . . . 15 (𝜑𝐶 ∈ ℝ*)
8315rexrd 11311 . . . . . . . . . . . . . . 15 (𝜑𝐷 ∈ ℝ*)
8417, 24, 23fourierdlem15 46137 . . . . . . . . . . . . . . 15 (𝜑𝑆:(0...𝑁)⟶(𝐶[,]𝐷))
8582, 83, 84, 31fourierdlem8 46130 . . . . . . . . . . . . . 14 (𝜑 → ((𝑆𝐽)[,](𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
8681, 85sstrid 3995 . . . . . . . . . . . . 13 (𝜑 → ((𝑆𝐽)[,)(𝑆‘(𝐽 + 1))) ⊆ (𝐶[,]𝐷))
8786, 67sseldd 3984 . . . . . . . . . . . 12 (𝜑𝑌 ∈ (𝐶[,]𝐷))
88 elicc2 13452 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷)))
8914, 15, 88syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝑌 ∈ (𝐶[,]𝐷) ↔ (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷)))
9087, 89mpbid 232 . . . . . . . . . . 11 (𝜑 → (𝑌 ∈ ℝ ∧ 𝐶𝑌𝑌𝐷))
9190simp2d 1144 . . . . . . . . . 10 (𝜑𝐶𝑌)
9260, 77resubcld 11691 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐾) − (𝐸𝑌)) ∈ ℝ)
93 fourierdlem63.eyltqk . . . . . . . . . . . . . 14 (𝜑 → (𝐸𝑌) < (𝑄𝐾))
9477, 60posdifd 11850 . . . . . . . . . . . . . 14 (𝜑 → ((𝐸𝑌) < (𝑄𝐾) ↔ 0 < ((𝑄𝐾) − (𝐸𝑌))))
9593, 94mpbid 232 . . . . . . . . . . . . 13 (𝜑 → 0 < ((𝑄𝐾) − (𝐸𝑌)))
9692, 95elrpd 13074 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝐾) − (𝐸𝑌)) ∈ ℝ+)
9775, 96ltaddrpd 13110 . . . . . . . . . . 11 (𝜑𝑌 < (𝑌 + ((𝑄𝐾) − (𝐸𝑌))))
9860recnd 11289 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝐾) ∈ ℂ)
9977recnd 11289 . . . . . . . . . . . . 13 (𝜑 → (𝐸𝑌) ∈ ℂ)
10075recnd 11289 . . . . . . . . . . . . 13 (𝜑𝑌 ∈ ℂ)
10198, 99, 100subsub3d 11650 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) = (((𝑄𝐾) + 𝑌) − (𝐸𝑌)))
10298, 100addcomd 11463 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝐾) + 𝑌) = (𝑌 + (𝑄𝐾)))
103102oveq1d 7446 . . . . . . . . . . . 12 (𝜑 → (((𝑄𝐾) + 𝑌) − (𝐸𝑌)) = ((𝑌 + (𝑄𝐾)) − (𝐸𝑌)))
104100, 98, 99addsubassd 11640 . . . . . . . . . . . 12 (𝜑 → ((𝑌 + (𝑄𝐾)) − (𝐸𝑌)) = (𝑌 + ((𝑄𝐾) − (𝐸𝑌))))
105101, 103, 1043eqtrrd 2782 . . . . . . . . . . 11 (𝜑 → (𝑌 + ((𝑄𝐾) − (𝐸𝑌))) = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10697, 105breqtrd 5169 . . . . . . . . . 10 (𝜑𝑌 < ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10714, 75, 79, 91, 106lelttrd 11419 . . . . . . . . 9 (𝜑𝐶 < ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
10814, 79, 107ltled 11409 . . . . . . . 8 (𝜑𝐶 ≤ ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
109108adantr 480 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝐶 ≤ ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)))
11034adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℝ)
11160adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) ∈ ℝ)
11252, 34resubcld 11691 . . . . . . . . . . . 12 (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
113112adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ∈ ℝ)
114111, 113resubcld 11691 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) ∈ ℝ)
11574simp3d 1145 . . . . . . . . . . . . . 14 (𝜑𝑌 < (𝑆‘(𝐽 + 1)))
11675, 34, 115ltled 11409 . . . . . . . . . . . . 13 (𝜑𝑌 ≤ (𝑆‘(𝐽 + 1)))
11738, 36, 41, 10, 1, 75, 34, 116fourierdlem7 46129 . . . . . . . . . . . 12 (𝜑 → ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1))) ≤ ((𝐸𝑌) − 𝑌))
118112, 78, 60, 117lesub2dd 11880 . . . . . . . . . . 11 (𝜑 → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
119118adantr 480 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))))
12098adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) ∈ ℂ)
12152recnd 11289 . . . . . . . . . . . . . 14 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
122121adantr 480 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℂ)
123110recnd 11289 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ∈ ℂ)
124120, 122, 123subsubd 11648 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))))
12598, 121subcld 11620 . . . . . . . . . . . . . 14 (𝜑 → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℂ)
12634recnd 11289 . . . . . . . . . . . . . 14 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ ℂ)
127125, 126addcomd 11463 . . . . . . . . . . . . 13 (𝜑 → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
128127adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) + (𝑆‘(𝐽 + 1))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
129124, 128eqtrd 2777 . . . . . . . . . . 11 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) = ((𝑆‘(𝐽 + 1)) + ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1))))))
130 simpr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1))))
13152adantr 480 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝐸‘(𝑆‘(𝐽 + 1))) ∈ ℝ)
132111, 131sublt0d 11889 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0 ↔ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))))
133130, 132mpbird 257 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) < 0)
134111, 131resubcld 11691 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − (𝐸‘(𝑆‘(𝐽 + 1)))) ∈ ℝ)
135 ltaddneg 11477 . . . . . . . . . . . . 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 5165 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸‘(𝑆‘(𝐽 + 1))) − (𝑆‘(𝐽 + 1)))) < (𝑆‘(𝐽 + 1)))
13980, 114, 110, 119, 138lelttrd 11419 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) < (𝑆‘(𝐽 + 1)))
14084, 33ffvelcdmd 7105 . . . . . . . . . . . 12 (𝜑 → (𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷))
141 elicc2 13452 . . . . . . . . . . . . 13 ((𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ) → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
14214, 15, 141syl2anc 584 . . . . . . . . . . . 12 (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ (𝐶[,]𝐷) ↔ ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷)))
143140, 142mpbid 232 . . . . . . . . . . 11 (𝜑 → ((𝑆‘(𝐽 + 1)) ∈ ℝ ∧ 𝐶 ≤ (𝑆‘(𝐽 + 1)) ∧ (𝑆‘(𝐽 + 1)) ≤ 𝐷))
144143simp3d 1145 . . . . . . . . . 10 (𝜑 → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
145144adantr 480 . . . . . . . . 9 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → (𝑆‘(𝐽 + 1)) ≤ 𝐷)
14680, 110, 62, 139, 145ltletrd 11421 . . . . . . . 8 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) < 𝐷)
14780, 62, 146ltled 11409 . . . . . . 7 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ≤ 𝐷)
14861, 62, 80, 109, 147eliccd 45517 . . . . . 6 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ (𝐶[,]𝐷))
149 id 22 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌𝑥 = 𝑌)
150 oveq2 7439 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑌 → (𝐵𝑥) = (𝐵𝑌))
151150oveq1d 7446 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑌 → ((𝐵𝑥) / 𝑇) = ((𝐵𝑌) / 𝑇))
152151fveq2d 6910 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑌 → (⌊‘((𝐵𝑥) / 𝑇)) = (⌊‘((𝐵𝑌) / 𝑇)))
153152oveq1d 7446 . . . . . . . . . . . . . . 15 (𝑥 = 𝑌 → ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇) = ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇))
154149, 153oveq12d 7449 . . . . . . . . . . . . . 14 (𝑥 = 𝑌 → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
155154adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑥 = 𝑌) → (𝑥 + ((⌊‘((𝐵𝑥) / 𝑇)) · 𝑇)) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
15636, 75resubcld 11691 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵𝑌) ∈ ℝ)
157156, 40, 45redivcld 12095 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵𝑌) / 𝑇) ∈ ℝ)
158157flcld 13838 . . . . . . . . . . . . . . . 16 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℤ)
159158zred 12722 . . . . . . . . . . . . . . 15 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℝ)
160159, 40remulcld 11291 . . . . . . . . . . . . . 14 (𝜑 → ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) ∈ ℝ)
16175, 160readdcld 11290 . . . . . . . . . . . . 13 (𝜑 → (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) ∈ ℝ)
1622, 155, 75, 161fvmptd 7023 . . . . . . . . . . . 12 (𝜑 → (𝐸𝑌) = (𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)))
163162oveq1d 7446 . . . . . . . . . . 11 (𝜑 → ((𝐸𝑌) − 𝑌) = ((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌))
164163oveq1d 7446 . . . . . . . . . 10 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) = (((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇))
165160recnd 11289 . . . . . . . . . . . 12 (𝜑 → ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) ∈ ℂ)
166100, 165pncan2d 11622 . . . . . . . . . . 11 (𝜑 → ((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) = ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇))
167166oveq1d 7446 . . . . . . . . . 10 (𝜑 → (((𝑌 + ((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇)) − 𝑌) / 𝑇) = (((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) / 𝑇))
168159recnd 11289 . . . . . . . . . . 11 (𝜑 → (⌊‘((𝐵𝑌) / 𝑇)) ∈ ℂ)
16940recnd 11289 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
170168, 169, 45divcan4d 12049 . . . . . . . . . 10 (𝜑 → (((⌊‘((𝐵𝑌) / 𝑇)) · 𝑇) / 𝑇) = (⌊‘((𝐵𝑌) / 𝑇)))
171164, 167, 1703eqtrd 2781 . . . . . . . . 9 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) = (⌊‘((𝐵𝑌) / 𝑇)))
172171, 158eqeltrd 2841 . . . . . . . 8 (𝜑 → (((𝐸𝑌) − 𝑌) / 𝑇) ∈ ℤ)
17378recnd 11289 . . . . . . . . . . . 12 (𝜑 → ((𝐸𝑌) − 𝑌) ∈ ℂ)
174173, 169, 45divcan1d 12044 . . . . . . . . . . 11 (𝜑 → ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇) = ((𝐸𝑌) − 𝑌))
175174oveq2d 7447 . . . . . . . . . 10 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((𝐸𝑌) − 𝑌)))
17698, 173npcand 11624 . . . . . . . . . 10 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((𝐸𝑌) − 𝑌)) = (𝑄𝐾))
177175, 176eqtrd 2777 . . . . . . . . 9 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) = (𝑄𝐾))
178 ffun 6739 . . . . . . . . . . 11 (𝑄:(0...𝑀)⟶ℝ → Fun 𝑄)
17958, 178syl 17 . . . . . . . . . 10 (𝜑 → Fun 𝑄)
18058fdmd 6746 . . . . . . . . . . 11 (𝜑 → dom 𝑄 = (0...𝑀))
18159, 180eleqtrrd 2844 . . . . . . . . . 10 (𝜑𝐾 ∈ dom 𝑄)
182 fvelrn 7096 . . . . . . . . . 10 ((Fun 𝑄𝐾 ∈ dom 𝑄) → (𝑄𝐾) ∈ ran 𝑄)
183179, 181, 182syl2anc 584 . . . . . . . . 9 (𝜑 → (𝑄𝐾) ∈ ran 𝑄)
184177, 183eqeltrd 2841 . . . . . . . 8 (𝜑 → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄)
185 oveq1 7438 . . . . . . . . . . 11 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → (𝑘 · 𝑇) = ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇))
186185oveq2d 7447 . . . . . . . . . 10 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)))
187186eleq1d 2826 . . . . . . . . 9 (𝑘 = (((𝐸𝑌) − 𝑌) / 𝑇) → ((((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄))
188187rspcev 3622 . . . . . . . 8 (((((𝐸𝑌) − 𝑌) / 𝑇) ∈ ℤ ∧ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + ((((𝐸𝑌) − 𝑌) / 𝑇) · 𝑇)) ∈ ran 𝑄) → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
189172, 184, 188syl2anc 584 . . . . . . 7 (𝜑 → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
190189adantr 480 . . . . . 6 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄)
191 oveq1 7438 . . . . . . . . 9 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → (𝑥 + (𝑘 · 𝑇)) = (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)))
192191eleq1d 2826 . . . . . . . 8 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → ((𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
193192rexbidv 3179 . . . . . . 7 (𝑥 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) → (∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄 ↔ ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
194193elrab 3692 . . . . . 6 (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} ↔ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ (𝐶[,]𝐷) ∧ ∃𝑘 ∈ ℤ (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) + (𝑘 · 𝑇)) ∈ ran 𝑄))
195148, 190, 194sylanbrc 583 . . . . 5 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄})
196 elun2 4183 . . . . 5 (((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄} → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
197195, 196syl 17 . . . 4 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ((𝑄𝐾) − ((𝐸𝑌) − 𝑌)) ∈ ({𝐶, 𝐷} ∪ {𝑥 ∈ (𝐶[,]𝐷) ∣ ∃𝑘 ∈ ℤ (𝑥 + (𝑘 · 𝑇)) ∈ ran 𝑄}))
198 fourierdlem63.x . . . 4 𝑋 = ((𝑄𝐾) − ((𝐸𝑌) − 𝑌))
199197, 198, 183eltr4g 2858 . . 3 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋𝐻)
200 elfzelz 13564 . . . . . . . . 9 (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ)
201200ad2antlr 727 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1)))) → 𝑗 ∈ ℤ)
202 elfzoelz 13699 . . . . . . . . . . 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 12694 . . . . . . . . 9 ((𝐽 ∈ ℤ ∧ 𝐽 < 𝑗𝑗 < (𝐽 + 1)) → ¬ 𝑗 ∈ ℤ)
223204, 213, 221, 222syl3anc 1373 . . . . . . . 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 1144 . . . . . . . . . 10 (𝜑 → (𝑆𝐽) ≤ 𝑌)
231230ad2antrr 726 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) ≤ 𝑌)
232106, 198breqtrrdi 5185 . . . . . . . . . . . 12 (𝜑𝑌 < 𝑋)
233232adantr 480 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑌 < 𝑋)
234 eqcom 2744 . . . . . . . . . . . . 13 (𝑋 = (𝑆𝑗) ↔ (𝑆𝑗) = 𝑋)
235234biimpri 228 . . . . . . . . . . . 12 ((𝑆𝑗) = 𝑋𝑋 = (𝑆𝑗))
236235adantl 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑋 = (𝑆𝑗))
237233, 236breqtrd 5169 . . . . . . . . . 10 ((𝜑 ∧ (𝑆𝑗) = 𝑋) → 𝑌 < (𝑆𝑗))
238237adantlr 715 . . . . . . . . 9 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → 𝑌 < (𝑆𝑗))
239226, 227, 229, 231, 238lelttrd 11419 . . . . . . . 8 (((𝜑𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) < (𝑆𝑗))
240239adantllr 719 . . . . . . 7 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝐽) < (𝑆𝑗))
241 simpr 484 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) = 𝑋)
242198, 139eqbrtrid 5178 . . . . . . . . . 10 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → 𝑋 < (𝑆‘(𝐽 + 1)))
243242adantr 480 . . . . . . . . 9 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → 𝑋 < (𝑆‘(𝐽 + 1)))
244241, 243eqbrtrd 5165 . . . . . . . 8 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
245244adantlr 715 . . . . . . 7 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → (𝑆𝑗) < (𝑆‘(𝐽 + 1)))
246240, 245jca 511 . . . . . 6 ((((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) ∧ (𝑆𝑗) = 𝑋) → ((𝑆𝐽) < (𝑆𝑗) ∧ (𝑆𝑗) < (𝑆‘(𝐽 + 1))))
247225, 246mtand 816 . . . . 5 (((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) ∧ 𝑗 ∈ (0...𝑁)) → ¬ (𝑆𝑗) = 𝑋)
248247nrexdv 3149 . . . 4 ((𝜑 ∧ (𝑄𝐾) < (𝐸‘(𝑆‘(𝐽 + 1)))) → ¬ ∃𝑗 ∈ (0...𝑁)(𝑆𝑗) = 𝑋)
249 isof1o 7343 . . . . . . . . 9 (𝑆 Isom < , < ((0...𝑁), 𝐻) → 𝑆:(0...𝑁)–1-1-onto𝐻)
250206, 249syl 17 . . . . . . . 8 (𝜑𝑆:(0...𝑁)–1-1-onto𝐻)
251 f1ofo 6855 . . . . . . . 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 3094 . . . . . 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 11411 1 (𝜑 → (𝐸‘(𝑆‘(𝐽 + 1))) ≤ (𝑄𝐾))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wral 3061  wrex 3070  {crab 3436  cun 3949  wss 3951  {cpr 4628   class class class wbr 5143  cmpt 5225  dom cdm 5685  ran crn 5686  cio 6512  Fun wfun 6555  wf 6557  ontowfo 6559  1-1-ontowf1o 6560  cfv 6561   Isom wiso 6562  (class class class)co 7431  m cmap 8866  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  *cxr 11294   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  cn 12266  cz 12613  (,]cioc 13388  [,)cico 13389  [,]cicc 13390  ...cfz 13547  ..^cfzo 13694  cfl 13830  chash 14369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-oadd 8510  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-xnn0 12600  df-z 12614  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ioo 13391  df-ioc 13392  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-rest 17467  df-topgen 17488  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-top 22900  df-topon 22917  df-bases 22953  df-cld 23027  df-ntr 23028  df-cls 23029  df-nei 23106  df-lp 23144  df-cmp 23395
This theorem is referenced by:  fourierdlem79  46200
  Copyright terms: Public domain W3C validator