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

Theorem fourierdlem74 40900
Description: Given a piecewise smooth function 𝐹, the derived function 𝐻 has a limit at the upper bound of each interval of the partition 𝑄. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem74.xre (𝜑𝑋 ∈ ℝ)
fourierdlem74.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem74.f (𝜑𝐹:ℝ⟶ℝ)
fourierdlem74.x (𝜑𝑋 ∈ ran 𝑉)
fourierdlem74.y (𝜑𝑌 ∈ ℝ)
fourierdlem74.w (𝜑𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
fourierdlem74.h 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
fourierdlem74.m (𝜑𝑀 ∈ ℕ)
fourierdlem74.v (𝜑𝑉 ∈ (𝑃𝑀))
fourierdlem74.r ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
fourierdlem74.q 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
fourierdlem74.o 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem74.g 𝐺 = (ℝ D 𝐹)
fourierdlem74.gcn ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
fourierdlem74.e (𝜑𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋))
fourierdlem74.a 𝐴 = if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
Assertion
Ref Expression
fourierdlem74 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
Distinct variable groups:   𝐸,𝑠   𝐹,𝑠   𝐻,𝑠   𝑖,𝑀,𝑚,𝑝   𝑀,𝑠,𝑖   𝑄,𝑖,𝑝   𝑄,𝑠   𝑅,𝑠   𝑖,𝑉,𝑝   𝑉,𝑠   𝑊,𝑠   𝑖,𝑋,𝑚,𝑝   𝑋,𝑠   𝑌,𝑠   𝜑,𝑖,𝑠
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝐴(𝑖,𝑚,𝑠,𝑝)   𝑃(𝑖,𝑚,𝑠,𝑝)   𝑄(𝑚)   𝑅(𝑖,𝑚,𝑝)   𝐸(𝑖,𝑚,𝑝)   𝐹(𝑖,𝑚,𝑝)   𝐺(𝑖,𝑚,𝑠,𝑝)   𝐻(𝑖,𝑚,𝑝)   𝑂(𝑖,𝑚,𝑠,𝑝)   𝑉(𝑚)   𝑊(𝑖,𝑚,𝑝)   𝑌(𝑖,𝑚,𝑝)

Proof of Theorem fourierdlem74
Dummy variables 𝑥 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elfzofz 12679 . . . . . 6 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
2 pire 24409 . . . . . . . . . . . 12 π ∈ ℝ
32renegcli 10534 . . . . . . . . . . 11 -π ∈ ℝ
43a1i 11 . . . . . . . . . 10 (𝜑 → -π ∈ ℝ)
5 fourierdlem74.xre . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
64, 5readdcld 10261 . . . . . . . . 9 (𝜑 → (-π + 𝑋) ∈ ℝ)
72a1i 11 . . . . . . . . . 10 (𝜑 → π ∈ ℝ)
87, 5readdcld 10261 . . . . . . . . 9 (𝜑 → (π + 𝑋) ∈ ℝ)
96, 8iccssred 40230 . . . . . . . 8 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
109adantr 472 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
11 fourierdlem74.p . . . . . . . . 9 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
12 fourierdlem74.m . . . . . . . . 9 (𝜑𝑀 ∈ ℕ)
13 fourierdlem74.v . . . . . . . . 9 (𝜑𝑉 ∈ (𝑃𝑀))
1411, 12, 13fourierdlem15 40842 . . . . . . . 8 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
1514ffvelrnda 6522 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
1610, 15sseldd 3745 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ℝ)
171, 16sylan2 492 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
1817adantr 472 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) ∈ ℝ)
195ad2antrr 764 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℝ)
2011fourierdlem2 40829 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
2112, 20syl 17 . . . . . . . . 9 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
2213, 21mpbid 222 . . . . . . . 8 (𝜑 → (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
2322simprrd 814 . . . . . . 7 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
2423r19.21bi 3070 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
2524adantr 472 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
26 eqcom 2767 . . . . . . 7 ((𝑉‘(𝑖 + 1)) = 𝑋𝑋 = (𝑉‘(𝑖 + 1)))
2726biimpi 206 . . . . . 6 ((𝑉‘(𝑖 + 1)) = 𝑋𝑋 = (𝑉‘(𝑖 + 1)))
2827adantl 473 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 = (𝑉‘(𝑖 + 1)))
2925, 28breqtrrd 4832 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) < 𝑋)
30 fourierdlem74.f . . . . . 6 (𝜑𝐹:ℝ⟶ℝ)
31 ioossre 12428 . . . . . . 7 ((𝑉𝑖)(,)𝑋) ⊆ ℝ
3231a1i 11 . . . . . 6 (𝜑 → ((𝑉𝑖)(,)𝑋) ⊆ ℝ)
3330, 32fssresd 6232 . . . . 5 (𝜑 → (𝐹 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
3433ad2antrr 764 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐹 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
35 limcresi 23848 . . . . . . . 8 ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋)
36 fourierdlem74.w . . . . . . . 8 (𝜑𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
3735, 36sseldi 3742 . . . . . . 7 (𝜑𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
3837adantr 472 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
39 mnfxr 10288 . . . . . . . . . 10 -∞ ∈ ℝ*
4039a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ*)
4117rexrd 10281 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ*)
4217mnfltd 12151 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < (𝑉𝑖))
4340, 41, 42xrltled 39985 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑉𝑖))
44 iooss1 12403 . . . . . . . . 9 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑉𝑖)) → ((𝑉𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
4540, 43, 44syl2anc 696 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
4645resabs1d 5586 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) = (𝐹 ↾ ((𝑉𝑖)(,)𝑋)))
4746oveq1d 6828 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
4838, 47eleqtrd 2841 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
4948adantr 472 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑊 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
50 eqid 2760 . . . 4 (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋)))
51 ax-resscn 10185 . . . . . . . . . 10 ℝ ⊆ ℂ
5251a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℂ)
5330, 52fssd 6218 . . . . . . . . 9 (𝜑𝐹:ℝ⟶ℂ)
54 ssid 3765 . . . . . . . . . 10 ℝ ⊆ ℝ
5554a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℝ)
56 eqid 2760 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5756tgioo2 22807 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
5856, 57dvres 23874 . . . . . . . . 9 (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑉𝑖)(,)𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))))
5952, 53, 55, 32, 58syl22anc 1478 . . . . . . . 8 (𝜑 → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))))
60 fourierdlem74.g . . . . . . . . . . 11 𝐺 = (ℝ D 𝐹)
6160eqcomi 2769 . . . . . . . . . 10 (ℝ D 𝐹) = 𝐺
62 ioontr 40239 . . . . . . . . . 10 ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋)
6361, 62reseq12i 5549 . . . . . . . . 9 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋))
6463a1i 11 . . . . . . . 8 (𝜑 → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6559, 64eqtrd 2794 . . . . . . 7 (𝜑 → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6665dmeqd 5481 . . . . . 6 (𝜑 → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6766ad2antrr 764 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
68 fourierdlem74.gcn . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
6968adantr 472 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
70 oveq2 6821 . . . . . . . . . 10 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) = ((𝑉𝑖)(,)𝑋))
7170reseq2d 5551 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) = 𝑋 → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
7271, 70feq12d 6194 . . . . . . . 8 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ))
7372adantl 473 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ))
7469, 73mpbid 222 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
75 fdm 6212 . . . . . 6 ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ → dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋))
7674, 75syl 17 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋))
7767, 76eqtrd 2794 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((𝑉𝑖)(,)𝑋))
78 limcresi 23848 . . . . . . . 8 ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋)
7945resabs1d 5586 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
8079oveq1d 6828 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
8178, 80syl5sseq 3794 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
82 fourierdlem74.e . . . . . . . 8 (𝜑𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋))
8382adantr 472 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋))
8481, 83sseldd 3745 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
8559, 64eqtr2d 2795 . . . . . . . 8 (𝜑 → (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))))
8685oveq1d 6828 . . . . . . 7 (𝜑 → ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8786adantr 472 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8884, 87eleqtrd 2841 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8988adantr 472 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
90 eqid 2760 . . . 4 (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
91 oveq2 6821 . . . . . . 7 (𝑥 = 𝑠 → (𝑋 + 𝑥) = (𝑋 + 𝑠))
9291fveq2d 6356 . . . . . 6 (𝑥 = 𝑠 → ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
9392oveq1d 6828 . . . . 5 (𝑥 = 𝑠 → (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊) = (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
9493cbvmptv 4902 . . . 4 (𝑥 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊)) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
95 id 22 . . . . 5 (𝑥 = 𝑠𝑥 = 𝑠)
9695cbvmptv 4902 . . . 4 (𝑥 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ 𝑥) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ 𝑠)
9718, 19, 29, 34, 49, 50, 77, 89, 90, 94, 96fourierdlem60 40886 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim 0))
98 fourierdlem74.a . . . . 5 𝐴 = if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
99 iftrue 4236 . . . . 5 ((𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = 𝐸)
10098, 99syl5eq 2806 . . . 4 ((𝑉‘(𝑖 + 1)) = 𝑋𝐴 = 𝐸)
101100adantl 473 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = 𝐸)
102 fourierdlem74.h . . . . . . 7 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
103102reseq1i 5547 . . . . . 6 (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
104103a1i 11 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
105 ioossicc 12452 . . . . . . . 8 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
1063rexri 10289 . . . . . . . . . 10 -π ∈ ℝ*
107106a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ*)
1082rexri 10289 . . . . . . . . . 10 π ∈ ℝ*
109108a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → π ∈ ℝ*)
1103a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → -π ∈ ℝ)
1112a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → π ∈ ℝ)
1125adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
11316, 112resubcld 10650 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
1144recnd 10260 . . . . . . . . . . . . . . . 16 (𝜑 → -π ∈ ℂ)
1155recnd 10260 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℂ)
116114, 115pncand 10585 . . . . . . . . . . . . . . 15 (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
117116eqcomd 2766 . . . . . . . . . . . . . 14 (𝜑 → -π = ((-π + 𝑋) − 𝑋))
118117adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → -π = ((-π + 𝑋) − 𝑋))
1196adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ∈ ℝ)
1208adantr 472 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑀)) → (π + 𝑋) ∈ ℝ)
121 elicc2 12431 . . . . . . . . . . . . . . . . 17 (((-π + 𝑋) ∈ ℝ ∧ (π + 𝑋) ∈ ℝ) → ((𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋))))
122119, 120, 121syl2anc 696 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋))))
12315, 122mpbid 222 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋)))
124123simp2d 1138 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ≤ (𝑉𝑖))
125119, 16, 112, 124lesub1dd 10835 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((-π + 𝑋) − 𝑋) ≤ ((𝑉𝑖) − 𝑋))
126118, 125eqbrtrd 4826 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → -π ≤ ((𝑉𝑖) − 𝑋))
127123simp3d 1139 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ≤ (π + 𝑋))
12816, 120, 112, 127lesub1dd 10835 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ≤ ((π + 𝑋) − 𝑋))
129111recnd 10260 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → π ∈ ℂ)
130115adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℂ)
131129, 130pncand 10585 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((π + 𝑋) − 𝑋) = π)
132128, 131breqtrd 4830 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ≤ π)
133110, 111, 113, 126, 132eliccd 40229 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ (-π[,]π))
134 fourierdlem74.q . . . . . . . . . . 11 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
135133, 134fmptd 6548 . . . . . . . . . 10 (𝜑𝑄:(0...𝑀)⟶(-π[,]π))
136135adantr 472 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
137 simpr 479 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
138107, 109, 136, 137fourierdlem8 40835 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
139105, 138syl5ss 3755 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
140139resmptd 5610 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
141140adantr 472 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
1421adantl 473 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
1431, 113sylan2 492 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
144134fvmpt2 6453 . . . . . . . . 9 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
145142, 143, 144syl2anc 696 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
146145adantr 472 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
147 fveq2 6352 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑉𝑖) = (𝑉𝑗))
148147oveq1d 6828 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑗) − 𝑋))
149148cbvmptv 4902 . . . . . . . . . . . 12 (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
150134, 149eqtri 2782 . . . . . . . . . . 11 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
151150a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋)))
152 fveq2 6352 . . . . . . . . . . . 12 (𝑗 = (𝑖 + 1) → (𝑉𝑗) = (𝑉‘(𝑖 + 1)))
153152oveq1d 6828 . . . . . . . . . . 11 (𝑗 = (𝑖 + 1) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
154153adantl 473 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
155 fzofzp1 12759 . . . . . . . . . . 11 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
156155adantl 473 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
15722simpld 477 . . . . . . . . . . . . . 14 (𝜑𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)))
158 elmapi 8045 . . . . . . . . . . . . . 14 (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
159157, 158syl 17 . . . . . . . . . . . . 13 (𝜑𝑉:(0...𝑀)⟶ℝ)
160159adantr 472 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
161160, 156ffvelrnd 6523 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
1625adantr 472 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
163161, 162resubcld 10650 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
164151, 154, 156, 163fvmptd 6450 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
165164adantr 472 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
166 oveq1 6820 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋𝑋))
167166adantl 473 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋𝑋))
168115ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
169168subidd 10572 . . . . . . . . 9 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋𝑋) = 0)
1701, 169sylanl2 686 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋𝑋) = 0)
171165, 167, 1703eqtrd 2798 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = 0)
172146, 171oveq12d 6831 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑉𝑖) − 𝑋)(,)0))
173 simplr 809 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
174 fourierdlem74.o . . . . . . . . . . . . 13 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
17512adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑀 ∈ ℕ)
1764, 7, 5, 11, 174, 12, 13, 134fourierdlem14 40841 . . . . . . . . . . . . . 14 (𝜑𝑄 ∈ (𝑂𝑀))
177176adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑄 ∈ (𝑂𝑀))
178 simpr 479 . . . . . . . . . . . . . 14 ((𝜑𝑠 = 0) → 𝑠 = 0)
179 fourierdlem74.x . . . . . . . . . . . . . . . . . 18 (𝜑𝑋 ∈ ran 𝑉)
180 ffn 6206 . . . . . . . . . . . . . . . . . . 19 (𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)) → 𝑉 Fn (0...𝑀))
181 fvelrnb 6405 . . . . . . . . . . . . . . . . . . 19 (𝑉 Fn (0...𝑀) → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋))
18214, 180, 1813syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋))
183179, 182mpbid 222 . . . . . . . . . . . . . . . . 17 (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋)
184 simpr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
185134fvmpt2 6453 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ (-π[,]π)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
186184, 133, 185syl2anc 696 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
187186adantr 472 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
188 oveq1 6820 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉𝑖) = 𝑋 → ((𝑉𝑖) − 𝑋) = (𝑋𝑋))
189188adantl 473 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → ((𝑉𝑖) − 𝑋) = (𝑋𝑋))
190115subidd 10572 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑋𝑋) = 0)
191190ad2antrr 764 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑋𝑋) = 0)
192187, 189, 1913eqtrd 2798 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑄𝑖) = 0)
193192ex 449 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) = 𝑋 → (𝑄𝑖) = 0))
194193reximdva 3155 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋 → ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0))
195183, 194mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0)
196113, 134fmptd 6548 . . . . . . . . . . . . . . . . 17 (𝜑𝑄:(0...𝑀)⟶ℝ)
197 ffn 6206 . . . . . . . . . . . . . . . . 17 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
198 fvelrnb 6405 . . . . . . . . . . . . . . . . 17 (𝑄 Fn (0...𝑀) → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0))
199196, 197, 1983syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0))
200195, 199mpbird 247 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ran 𝑄)
201200adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑠 = 0) → 0 ∈ ran 𝑄)
202178, 201eqeltrd 2839 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑠 ∈ ran 𝑄)
203174, 175, 177, 202fourierdlem12 40839 . . . . . . . . . . . 12 (((𝜑𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
204203an32s 881 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
205204adantlr 753 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
206173, 205pm2.65da 601 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
207206adantlr 753 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
208207iffalsed 4241 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
209 elioore 12398 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
210209adantl 473 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
211 0red 10233 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
212 elioo3g 12397 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ℝ*) ∧ ((𝑄𝑖) < 𝑠𝑠 < (𝑄‘(𝑖 + 1)))))
213212biimpi 206 . . . . . . . . . . . . . 14 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ℝ*) ∧ ((𝑄𝑖) < 𝑠𝑠 < (𝑄‘(𝑖 + 1)))))
214213simprrd 814 . . . . . . . . . . . . 13 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 < (𝑄‘(𝑖 + 1)))
215214adantl 473 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
216171adantr 472 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) = 0)
217215, 216breqtrd 4830 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
218210, 211, 217ltnsymd 10378 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
219218iffalsed 4241 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
220219oveq2d 6829 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
221220oveq1d 6828 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
22241ad2antrr 764 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
2235rexrd 10281 . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ*)
224223ad3antrrr 768 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
225162ad2antrr 764 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
226225, 210readdcld 10261 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
227115adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
228 iccssre 12448 . . . . . . . . . . . . . . . . . . 19 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
2293, 2, 228mp2an 710 . . . . . . . . . . . . . . . . . 18 (-π[,]π) ⊆ ℝ
230229, 51sstri 3753 . . . . . . . . . . . . . . . . 17 (-π[,]π) ⊆ ℂ
231186, 133eqeltrd 2839 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) ∈ (-π[,]π))
2321, 231sylan2 492 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ (-π[,]π))
233230, 232sseldi 3742 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
234227, 233addcomd 10430 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄𝑖)) = ((𝑄𝑖) + 𝑋))
235145oveq1d 6828 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑋) = (((𝑉𝑖) − 𝑋) + 𝑋))
23617recnd 10260 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℂ)
237236, 227npcand 10588 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑉𝑖) − 𝑋) + 𝑋) = (𝑉𝑖))
238234, 235, 2373eqtrrd 2799 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
239238adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
240145, 143eqeltrd 2839 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
241240adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
242209adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
2435ad2antrr 764 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
244213simprld 812 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑄𝑖) < 𝑠)
245244adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
246241, 242, 243, 245ltadd2dd 10388 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
247239, 246eqbrtrd 4826 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
248247adantlr 753 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
249 ltaddneg 10443 . . . . . . . . . . . . 13 ((𝑠 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
250210, 225, 249syl2anc 696 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
251217, 250mpbid 222 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < 𝑋)
252222, 224, 226, 248, 251eliood 40223 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋))
253 fvres 6368 . . . . . . . . . . 11 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋) → ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
254253eqcomd 2766 . . . . . . . . . 10 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
255252, 254syl 17 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
256255oveq1d 6828 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝑊) = (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
257256oveq1d 6828 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠) = ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
258208, 221, 2573eqtrd 2798 . . . . . 6 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
259172, 258mpteq12dva 4884 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
260104, 141, 2593eqtrd 2798 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
261260, 171oveq12d 6831 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim 0))
26297, 101, 2613eltr4d 2854 . 2 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
263 eqid 2760 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
264 eqid 2760 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠)
265 eqid 2760 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
26630adantr 472 . . . . . . . . . 10 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℝ)
2675adantr 472 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
268209adantl 473 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
269267, 268readdcld 10261 . . . . . . . . . 10 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
270266, 269ffvelrnd 6523 . . . . . . . . 9 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
271270recnd 10260 . . . . . . . 8 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
272271adantlr 753 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
2732723adantl3 1174 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
274 fourierdlem74.y . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ)
275274recnd 10260 . . . . . . . . 9 (𝜑𝑌 ∈ ℂ)
276 limccl 23838 . . . . . . . . . 10 ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ ℂ
277276, 36sseldi 3742 . . . . . . . . 9 (𝜑𝑊 ∈ ℂ)
278275, 277ifcld 4275 . . . . . . . 8 (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
279278adantr 472 . . . . . . 7 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
2802793ad2antl1 1201 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
281273, 280subcld 10584 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
282209recnd 10260 . . . . . . 7 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℂ)
283282adantl 473 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
284 velsn 4337 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
285206, 284sylnibr 318 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
2862853adantl3 1174 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
287283, 286eldifd 3726 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
288 eqid 2760 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
289 eqid 2760 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊)
290 eqid 2760 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
291277ad2antrr 764 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑊 ∈ ℂ)
29230adantr 472 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℝ)
293 ioossre 12428 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
294293a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
29541adantr 472 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
296161rexrd 10281 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
297296adantr 472 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
298269adantlr 753 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
299196adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
300299, 156ffvelrnd 6523 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
301300adantr 472 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
302214adantl 473 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
303242, 301, 243, 302ltadd2dd 10388 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
304164oveq2d 6829 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
305161recnd 10260 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
306227, 305pncan3d 10587 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
307304, 306eqtrd 2794 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
308307adantr 472 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
309303, 308breqtrd 4830 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
310295, 297, 298, 247, 309eliood 40223 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
311 ioossre 12428 . . . . . . . . . . . 12 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
312311a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
313242, 302ltned 10365 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
314 fourierdlem74.r . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
315307eqcomd 2766 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
316315oveq2d 6829 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
317314, 316eleqtrd 2841 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
318300recnd 10260 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
319292, 162, 294, 288, 310, 312, 313, 317, 318fourierdlem53 40879 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
320 ioosscn 40219 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
321320a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
322277adantr 472 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ℂ)
323289, 321, 322, 318constlimc 40359 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) lim (𝑄‘(𝑖 + 1))))
324288, 289, 290, 272, 291, 319, 323sublimc 40387 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑅𝑊) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
325324adantr 472 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅𝑊) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
326 iftrue 4236 . . . . . . . . . 10 ((𝑉‘(𝑖 + 1)) < 𝑋 → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑊)
327326oveq2d 6829 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) < 𝑋 → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅𝑊))
328327adantl 473 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅𝑊))
329209adantl 473 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
330 0red 10233 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
331300ad2antrr 764 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
332214adantl 473 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
333164adantr 472 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
334161adantr 472 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
3355ad2antrr 764 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
336 simpr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) < 𝑋)
337334, 335, 336ltled 10377 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ≤ 𝑋)
338334, 335suble0d 10810 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0 ↔ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
339337, 338mpbird 247 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0)
340333, 339eqbrtrd 4826 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) ≤ 0)
341340adantr 472 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ≤ 0)
342329, 331, 330, 332, 341ltletrd 10389 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
343329, 330, 342ltnsymd 10378 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
344343iffalsed 4241 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
345344oveq2d 6829 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
346345mpteq2dva 4896 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)))
347346oveq1d 6828 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
348325, 328, 3473eltr4d 2854 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
3493483adantl3 1174 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
350 simpl1 1228 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝜑)
351 simpl2 1230 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑖 ∈ (0..^𝑀))
3525ad2antrr 764 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
3533523adantl3 1174 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
354161adantr 472 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
3553543adantl3 1174 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
356 neqne 2940 . . . . . . . . . . 11 (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
357356necomd 2987 . . . . . . . . . 10 (¬ (𝑉‘(𝑖 + 1)) = 𝑋𝑋 ≠ (𝑉‘(𝑖 + 1)))
358357adantr 472 . . . . . . . . 9 ((¬ (𝑉‘(𝑖 + 1)) = 𝑋 ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
3593583ad2antl3 1203 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
360 simpr 479 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
361353, 355, 359, 360lttri5d 40012 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
362 eqid 2760 . . . . . . . 8 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊))
363272adantlr 753 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
364278ad3antrrr 768 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
365319adantr 472 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
366 eqid 2760 . . . . . . . . . . 11 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌)
367275adantr 472 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ℂ)
368366, 321, 367, 318constlimc 40359 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
369368adantr 472 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑌 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
3705ad2antrr 764 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ∈ ℝ)
371161adantr 472 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
372 simpr 479 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 < (𝑉‘(𝑖 + 1)))
373370, 371, 372ltnsymd 10378 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
374373iffalsed 4241 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑌)
375 0red 10233 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
376240ad2antrr 764 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
377209adantl 473 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
378190eqcomd 2766 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 = (𝑋𝑋))
379378ad2antrr 764 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 = (𝑋𝑋))
38017adantr 472 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉𝑖) ∈ ℝ)
38141ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) ∈ ℝ*)
382296ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
383162ad2antrr 764 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ℝ)
384 simpr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ¬ 𝑋 ≤ (𝑉𝑖))
38517adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) ∈ ℝ)
3865ad2antrr 764 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ℝ)
387385, 386ltnled 10376 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ((𝑉𝑖) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑉𝑖)))
388384, 387mpbird 247 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) < 𝑋)
389388adantlr 753 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) < 𝑋)
390 simplr 809 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 < (𝑉‘(𝑖 + 1)))
391381, 382, 383, 389, 390eliood 40223 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
39211, 12, 13, 179fourierdlem12 40839 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
393392ad2antrr 764 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ¬ 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
394391, 393condan 870 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ≤ (𝑉𝑖))
395370, 380, 370, 394lesub1dd 10835 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑋𝑋) ≤ ((𝑉𝑖) − 𝑋))
396379, 395eqbrtrd 4826 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ ((𝑉𝑖) − 𝑋))
397145eqcomd 2766 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) = (𝑄𝑖))
398397adantr 472 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑉𝑖) − 𝑋) = (𝑄𝑖))
399396, 398breqtrd 4830 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ (𝑄𝑖))
400399adantr 472 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ≤ (𝑄𝑖))
401244adantl 473 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
402375, 376, 377, 400, 401lelttrd 10387 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
403402iftrued 4238 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
404403mpteq2dva 4896 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌))
405404oveq1d 6828 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
406369, 374, 4053eltr4d 2854 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim (𝑄‘(𝑖 + 1))))
407288, 362, 263, 363, 364, 365, 406sublimc 40387 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
408350, 351, 361, 407syl21anc 1476 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
409349, 408pm2.61dan 867 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
410321, 264, 318idlimc 40361 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim (𝑄‘(𝑖 + 1))))
4114103adant3 1127 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim (𝑄‘(𝑖 + 1))))
4121643adant3 1127 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
4133053adant3 1127 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
4142273adant3 1127 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
4153563ad2ant3 1130 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
416413, 414, 415subne0d 10593 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≠ 0)
417412, 416eqnetrd 2999 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ≠ 0)
4182063adantl3 1174 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
419418neqned 2939 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
420263, 264, 265, 281, 287, 409, 411, 417, 419divlimc 40391 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim (𝑄‘(𝑖 + 1))))
421 iffalse 4239 . . . . . 6 (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
42298, 421syl5eq 2806 . . . . 5 (¬ (𝑉‘(𝑖 + 1)) = 𝑋𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
4234223ad2ant3 1130 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
424 ioossre 12428 . . . . . . . . . . . . 13 (-∞(,)𝑋) ⊆ ℝ
425424a1i 11 . . . . . . . . . . . 12 (𝜑 → (-∞(,)𝑋) ⊆ ℝ)
42630, 425fssresd 6232 . . . . . . . . . . 11 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)):(-∞(,)𝑋)⟶ℝ)
427424, 52syl5ss 3755 . . . . . . . . . . 11 (𝜑 → (-∞(,)𝑋) ⊆ ℂ)
42839a1i 11 . . . . . . . . . . . 12 (𝜑 → -∞ ∈ ℝ*)
4295mnfltd 12151 . . . . . . . . . . . 12 (𝜑 → -∞ < 𝑋)
43056, 428, 5, 429lptioo2cn 40380 . . . . . . . . . . 11 (𝜑𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘(-∞(,)𝑋)))
431426, 427, 430, 36limcrecl 40364 . . . . . . . . . 10 (𝜑𝑊 ∈ ℝ)
43230, 5, 274, 431, 102fourierdlem9 40836 . . . . . . . . 9 (𝜑𝐻:(-π[,]π)⟶ℝ)
433432adantr 472 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐻:(-π[,]π)⟶ℝ)
434433, 139feqresmpt 6412 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)))
435139sselda 3744 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (-π[,]π))
436 0cnd 10225 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℂ)
437278ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
438272, 437subcld 10584 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
439282adantl 473 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
440206neqned 2939 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
441438, 439, 440divcld 10993 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℂ)
442436, 441ifcld 4275 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ)
443102fvmpt2 6453 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
444435, 442, 443syl2anc 696 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
445206iffalsed 4241 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
446444, 445eqtrd 2794 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
447446mpteq2dva 4896 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
448434, 447eqtrd 2794 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
4494483adant3 1127 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
450449oveq1d 6828 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim (𝑄‘(𝑖 + 1))))
451420, 423, 4503eltr4d 2854 . . 3 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
4524513expa 1112 . 2 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
453262, 452pm2.61dan 867 1 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383  w3a 1072   = wceq 1632  wcel 2139  wne 2932  wral 3050  wrex 3051  {crab 3054  wss 3715  ifcif 4230  {csn 4321   class class class wbr 4804  cmpt 4881  dom cdm 5266  ran crn 5267  cres 5268   Fn wfn 6044  wf 6045  cfv 6049  (class class class)co 6813  𝑚 cmap 8023  cc 10126  cr 10127  0cc0 10128  1c1 10129   + caddc 10131  -∞cmnf 10264  *cxr 10265   < clt 10266  cle 10267  cmin 10458  -cneg 10459   / cdiv 10876  cn 11212  (,)cioo 12368  [,]cicc 12371  ...cfz 12519  ..^cfzo 12659  πcpi 14996  TopOpenctopn 16284  topGenctg 16300  fldccnfld 19948  intcnt 21023   lim climc 23825   D cdv 23826
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206  ax-addf 10207  ax-mulf 10208
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-iin 4675  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-of 7062  df-om 7231  df-1st 7333  df-2nd 7334  df-supp 7464  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-er 7911  df-map 8025  df-pm 8026  df-ixp 8075  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-fsupp 8441  df-fi 8482  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-4 11273  df-5 11274  df-6 11275  df-7 11276  df-8 11277  df-9 11278  df-n0 11485  df-z 11570  df-dec 11686  df-uz 11880  df-q 11982  df-rp 12026  df-xneg 12139  df-xadd 12140  df-xmul 12141  df-ioo 12372  df-ioc 12373  df-ico 12374  df-icc 12375  df-fz 12520  df-fzo 12660  df-fl 12787  df-seq 12996  df-exp 13055  df-fac 13255  df-bc 13284  df-hash 13312  df-shft 14006  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-limsup 14401  df-clim 14418  df-rlim 14419  df-sum 14616  df-ef 14997  df-sin 14999  df-cos 15000  df-pi 15002  df-struct 16061  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-mulr 16157  df-starv 16158  df-sca 16159  df-vsca 16160  df-ip 16161  df-tset 16162  df-ple 16163  df-ds 16166  df-unif 16167  df-hom 16168  df-cco 16169  df-rest 16285  df-topn 16286  df-0g 16304  df-gsum 16305  df-topgen 16306  df-pt 16307  df-prds 16310  df-xrs 16364  df-qtop 16369  df-imas 16370  df-xps 16372  df-mre 16448  df-mrc 16449  df-acs 16451  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17950  df-cmn 18395  df-psmet 19940  df-xmet 19941  df-met 19942  df-bl 19943  df-mopn 19944  df-fbas 19945  df-fg 19946  df-cnfld 19949  df-top 20901  df-topon 20918  df-topsp 20939  df-bases 20952  df-cld 21025  df-ntr 21026  df-cls 21027  df-nei 21104  df-lp 21142  df-perf 21143  df-cn 21233  df-cnp 21234  df-haus 21321  df-cmp 21392  df-tx 21567  df-hmeo 21760  df-fil 21851  df-fm 21943  df-flim 21944  df-flf 21945  df-xms 22326  df-ms 22327  df-tms 22328  df-cncf 22882  df-limc 23829  df-dv 23830
This theorem is referenced by:  fourierdlem88  40914  fourierdlem103  40929  fourierdlem104  40930
  Copyright terms: Public domain W3C validator