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 41189
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 12787 . . . . . 6 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
2 pire 24617 . . . . . . . . . . . 12 π ∈ ℝ
32renegcli 10670 . . . . . . . . . . 11 -π ∈ ℝ
43a1i 11 . . . . . . . . . 10 (𝜑 → -π ∈ ℝ)
5 fourierdlem74.xre . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
64, 5readdcld 10393 . . . . . . . . 9 (𝜑 → (-π + 𝑋) ∈ ℝ)
72a1i 11 . . . . . . . . . 10 (𝜑 → π ∈ ℝ)
87, 5readdcld 10393 . . . . . . . . 9 (𝜑 → (π + 𝑋) ∈ ℝ)
96, 8iccssred 40524 . . . . . . . 8 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
109adantr 474 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
11 fourierdlem74.p . . . . . . . . 9 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
12 fourierdlem74.m . . . . . . . . 9 (𝜑𝑀 ∈ ℕ)
13 fourierdlem74.v . . . . . . . . 9 (𝜑𝑉 ∈ (𝑃𝑀))
1411, 12, 13fourierdlem15 41131 . . . . . . . 8 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
1514ffvelrnda 6613 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
1610, 15sseldd 3828 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ℝ)
171, 16sylan2 586 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
1817adantr 474 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) ∈ ℝ)
195ad2antrr 717 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℝ)
2011fourierdlem2 41118 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
2112, 20syl 17 . . . . . . . . 9 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
2213, 21mpbid 224 . . . . . . . 8 (𝜑 → (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
2322simprrd 790 . . . . . . 7 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
2423r19.21bi 3141 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
2524adantr 474 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
26 eqcom 2832 . . . . . . 7 ((𝑉‘(𝑖 + 1)) = 𝑋𝑋 = (𝑉‘(𝑖 + 1)))
2726biimpi 208 . . . . . 6 ((𝑉‘(𝑖 + 1)) = 𝑋𝑋 = (𝑉‘(𝑖 + 1)))
2827adantl 475 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 = (𝑉‘(𝑖 + 1)))
2925, 28breqtrrd 4903 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) < 𝑋)
30 fourierdlem74.f . . . . . 6 (𝜑𝐹:ℝ⟶ℝ)
31 ioossre 12530 . . . . . . 7 ((𝑉𝑖)(,)𝑋) ⊆ ℝ
3231a1i 11 . . . . . 6 (𝜑 → ((𝑉𝑖)(,)𝑋) ⊆ ℝ)
3330, 32fssresd 6312 . . . . 5 (𝜑 → (𝐹 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
3433ad2antrr 717 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐹 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
35 limcresi 24055 . . . . . . . 8 ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋)
36 fourierdlem74.w . . . . . . . 8 (𝜑𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
3735, 36sseldi 3825 . . . . . . 7 (𝜑𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
3837adantr 474 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
39 mnfxr 10421 . . . . . . . . . 10 -∞ ∈ ℝ*
4039a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ*)
4117rexrd 10413 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ*)
4217mnfltd 12251 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < (𝑉𝑖))
4340, 41, 42xrltled 12276 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑉𝑖))
44 iooss1 12505 . . . . . . . . 9 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑉𝑖)) → ((𝑉𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
4540, 43, 44syl2anc 579 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
4645resabs1d 5668 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) = (𝐹 ↾ ((𝑉𝑖)(,)𝑋)))
4746oveq1d 6925 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
4838, 47eleqtrd 2908 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
4948adantr 474 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑊 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
50 eqid 2825 . . . 4 (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋)))
51 ax-resscn 10316 . . . . . . . . . 10 ℝ ⊆ ℂ
5251a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℂ)
5330, 52fssd 6296 . . . . . . . . 9 (𝜑𝐹:ℝ⟶ℂ)
54 ssid 3848 . . . . . . . . . 10 ℝ ⊆ ℝ
5554a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℝ)
56 eqid 2825 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5756tgioo2 22983 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
5856, 57dvres 24081 . . . . . . . . 9 (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑉𝑖)(,)𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))))
5952, 53, 55, 32, 58syl22anc 872 . . . . . . . 8 (𝜑 → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))))
60 fourierdlem74.g . . . . . . . . . . 11 𝐺 = (ℝ D 𝐹)
6160eqcomi 2834 . . . . . . . . . 10 (ℝ D 𝐹) = 𝐺
62 ioontr 40531 . . . . . . . . . 10 ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋)
6361, 62reseq12i 5631 . . . . . . . . 9 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋))
6463a1i 11 . . . . . . . 8 (𝜑 → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6559, 64eqtrd 2861 . . . . . . 7 (𝜑 → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6665dmeqd 5562 . . . . . 6 (𝜑 → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6766ad2antrr 717 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
68 fourierdlem74.gcn . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
6968adantr 474 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
70 oveq2 6918 . . . . . . . . . 10 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) = ((𝑉𝑖)(,)𝑋))
7170reseq2d 5633 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) = 𝑋 → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
7271, 70feq12d 6270 . . . . . . . 8 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ))
7372adantl 475 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ))
7469, 73mpbid 224 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
75 fdm 6290 . . . . . 6 ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ → dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋))
7674, 75syl 17 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋))
7767, 76eqtrd 2861 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((𝑉𝑖)(,)𝑋))
78 limcresi 24055 . . . . . . . 8 ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋)
7945resabs1d 5668 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
8079oveq1d 6925 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
8178, 80syl5sseq 3878 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
82 fourierdlem74.e . . . . . . . 8 (𝜑𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋))
8382adantr 474 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋))
8481, 83sseldd 3828 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
8559, 64eqtr2d 2862 . . . . . . . 8 (𝜑 → (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))))
8685oveq1d 6925 . . . . . . 7 (𝜑 → ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8786adantr 474 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8884, 87eleqtrd 2908 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8988adantr 474 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
90 eqid 2825 . . . 4 (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
91 oveq2 6918 . . . . . . 7 (𝑥 = 𝑠 → (𝑋 + 𝑥) = (𝑋 + 𝑠))
9291fveq2d 6441 . . . . . 6 (𝑥 = 𝑠 → ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
9392oveq1d 6925 . . . . 5 (𝑥 = 𝑠 → (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊) = (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
9493cbvmptv 4975 . . . 4 (𝑥 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊)) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
95 id 22 . . . . 5 (𝑥 = 𝑠𝑥 = 𝑠)
9695cbvmptv 4975 . . . 4 (𝑥 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ 𝑥) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ 𝑠)
9718, 19, 29, 34, 49, 50, 77, 89, 90, 94, 96fourierdlem60 41175 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim 0))
98 fourierdlem74.a . . . . 5 𝐴 = if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
99 iftrue 4314 . . . . 5 ((𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = 𝐸)
10098, 99syl5eq 2873 . . . 4 ((𝑉‘(𝑖 + 1)) = 𝑋𝐴 = 𝐸)
101100adantl 475 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = 𝐸)
102 fourierdlem74.h . . . . . . 7 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
103102reseq1i 5629 . . . . . 6 (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
104103a1i 11 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
105 ioossicc 12554 . . . . . . . 8 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
1063rexri 10422 . . . . . . . . . 10 -π ∈ ℝ*
107106a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ*)
1082rexri 10422 . . . . . . . . . 10 π ∈ ℝ*
109108a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → π ∈ ℝ*)
1103a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → -π ∈ ℝ)
1112a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → π ∈ ℝ)
1125adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
11316, 112resubcld 10789 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
1144recnd 10392 . . . . . . . . . . . . . . . 16 (𝜑 → -π ∈ ℂ)
1155recnd 10392 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℂ)
116114, 115pncand 10721 . . . . . . . . . . . . . . 15 (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
117116eqcomd 2831 . . . . . . . . . . . . . 14 (𝜑 → -π = ((-π + 𝑋) − 𝑋))
118117adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → -π = ((-π + 𝑋) − 𝑋))
1196adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ∈ ℝ)
1208adantr 474 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑀)) → (π + 𝑋) ∈ ℝ)
121 elicc2 12533 . . . . . . . . . . . . . . . . 17 (((-π + 𝑋) ∈ ℝ ∧ (π + 𝑋) ∈ ℝ) → ((𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋))))
122119, 120, 121syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋))))
12315, 122mpbid 224 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋)))
124123simp2d 1177 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ≤ (𝑉𝑖))
125119, 16, 112, 124lesub1dd 10975 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((-π + 𝑋) − 𝑋) ≤ ((𝑉𝑖) − 𝑋))
126118, 125eqbrtrd 4897 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → -π ≤ ((𝑉𝑖) − 𝑋))
127123simp3d 1178 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ≤ (π + 𝑋))
12816, 120, 112, 127lesub1dd 10975 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ≤ ((π + 𝑋) − 𝑋))
129111recnd 10392 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → π ∈ ℂ)
130115adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℂ)
131129, 130pncand 10721 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((π + 𝑋) − 𝑋) = π)
132128, 131breqtrd 4901 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ≤ π)
133110, 111, 113, 126, 132eliccd 40523 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ (-π[,]π))
134 fourierdlem74.q . . . . . . . . . . 11 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
135133, 134fmptd 6638 . . . . . . . . . 10 (𝜑𝑄:(0...𝑀)⟶(-π[,]π))
136135adantr 474 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
137 simpr 479 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
138107, 109, 136, 137fourierdlem8 41124 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
139105, 138syl5ss 3838 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
140139resmptd 5693 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
141140adantr 474 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
1421adantl 475 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
1431, 113sylan2 586 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
144134fvmpt2 6543 . . . . . . . . 9 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
145142, 143, 144syl2anc 579 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
146145adantr 474 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
147 fveq2 6437 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑉𝑖) = (𝑉𝑗))
148147oveq1d 6925 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑗) − 𝑋))
149148cbvmptv 4975 . . . . . . . . . . . 12 (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
150134, 149eqtri 2849 . . . . . . . . . . 11 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
151150a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋)))
152 fveq2 6437 . . . . . . . . . . . 12 (𝑗 = (𝑖 + 1) → (𝑉𝑗) = (𝑉‘(𝑖 + 1)))
153152oveq1d 6925 . . . . . . . . . . 11 (𝑗 = (𝑖 + 1) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
154153adantl 475 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
155 fzofzp1 12867 . . . . . . . . . . 11 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
156155adantl 475 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
15722simpld 490 . . . . . . . . . . . . . 14 (𝜑𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)))
158 elmapi 8149 . . . . . . . . . . . . . 14 (𝑉 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
159157, 158syl 17 . . . . . . . . . . . . 13 (𝜑𝑉:(0...𝑀)⟶ℝ)
160159adantr 474 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
161160, 156ffvelrnd 6614 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
1625adantr 474 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
163161, 162resubcld 10789 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
164151, 154, 156, 163fvmptd 6539 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
165164adantr 474 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
166 oveq1 6917 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋𝑋))
167166adantl 475 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋𝑋))
168115ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
169168subidd 10708 . . . . . . . . 9 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋𝑋) = 0)
1701, 169sylanl2 671 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋𝑋) = 0)
171165, 167, 1703eqtrd 2865 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = 0)
172146, 171oveq12d 6928 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑉𝑖) − 𝑋)(,)0))
173 simplr 785 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
174 fourierdlem74.o . . . . . . . . . . . . 13 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
17512adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑀 ∈ ℕ)
1764, 7, 5, 11, 174, 12, 13, 134fourierdlem14 41130 . . . . . . . . . . . . . 14 (𝜑𝑄 ∈ (𝑂𝑀))
177176adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑄 ∈ (𝑂𝑀))
178 simpr 479 . . . . . . . . . . . . . 14 ((𝜑𝑠 = 0) → 𝑠 = 0)
179 fourierdlem74.x . . . . . . . . . . . . . . . . . 18 (𝜑𝑋 ∈ ran 𝑉)
180 ffn 6282 . . . . . . . . . . . . . . . . . . 19 (𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)) → 𝑉 Fn (0...𝑀))
181 fvelrnb 6494 . . . . . . . . . . . . . . . . . . 19 (𝑉 Fn (0...𝑀) → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋))
18214, 180, 1813syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋))
183179, 182mpbid 224 . . . . . . . . . . . . . . . . 17 (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋)
184 simpr 479 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
185134fvmpt2 6543 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ (-π[,]π)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
186184, 133, 185syl2anc 579 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
187186adantr 474 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
188 oveq1 6917 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉𝑖) = 𝑋 → ((𝑉𝑖) − 𝑋) = (𝑋𝑋))
189188adantl 475 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → ((𝑉𝑖) − 𝑋) = (𝑋𝑋))
190115subidd 10708 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑋𝑋) = 0)
191190ad2antrr 717 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑋𝑋) = 0)
192187, 189, 1913eqtrd 2865 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑄𝑖) = 0)
193192ex 403 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) = 𝑋 → (𝑄𝑖) = 0))
194193reximdva 3225 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋 → ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0))
195183, 194mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0)
196113, 134fmptd 6638 . . . . . . . . . . . . . . . . 17 (𝜑𝑄:(0...𝑀)⟶ℝ)
197 ffn 6282 . . . . . . . . . . . . . . . . 17 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
198 fvelrnb 6494 . . . . . . . . . . . . . . . . 17 (𝑄 Fn (0...𝑀) → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0))
199196, 197, 1983syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0))
200195, 199mpbird 249 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ran 𝑄)
201200adantr 474 . . . . . . . . . . . . . 14 ((𝜑𝑠 = 0) → 0 ∈ ran 𝑄)
202178, 201eqeltrd 2906 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑠 ∈ ran 𝑄)
203174, 175, 177, 202fourierdlem12 41128 . . . . . . . . . . . 12 (((𝜑𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
204203an32s 642 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
205204adantlr 706 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
206173, 205pm2.65da 851 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
207206adantlr 706 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
208207iffalsed 4319 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
209 elioore 12500 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
210209adantl 475 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
211 0red 10367 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
212 elioo3g 12499 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ℝ*) ∧ ((𝑄𝑖) < 𝑠𝑠 < (𝑄‘(𝑖 + 1)))))
213212biimpi 208 . . . . . . . . . . . . . 14 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ℝ*) ∧ ((𝑄𝑖) < 𝑠𝑠 < (𝑄‘(𝑖 + 1)))))
214213simprrd 790 . . . . . . . . . . . . 13 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 < (𝑄‘(𝑖 + 1)))
215214adantl 475 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
216171adantr 474 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) = 0)
217215, 216breqtrd 4901 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
218210, 211, 217ltnsymd 10512 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
219218iffalsed 4319 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
220219oveq2d 6926 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
221220oveq1d 6925 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
22241ad2antrr 717 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
2235rexrd 10413 . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ*)
224223ad3antrrr 721 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
225162ad2antrr 717 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
226225, 210readdcld 10393 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
227115adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
228 iccssre 12550 . . . . . . . . . . . . . . . . . . 19 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
2293, 2, 228mp2an 683 . . . . . . . . . . . . . . . . . 18 (-π[,]π) ⊆ ℝ
230229, 51sstri 3836 . . . . . . . . . . . . . . . . 17 (-π[,]π) ⊆ ℂ
231186, 133eqeltrd 2906 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) ∈ (-π[,]π))
2321, 231sylan2 586 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ (-π[,]π))
233230, 232sseldi 3825 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
234227, 233addcomd 10564 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄𝑖)) = ((𝑄𝑖) + 𝑋))
235145oveq1d 6925 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑋) = (((𝑉𝑖) − 𝑋) + 𝑋))
23617recnd 10392 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℂ)
237236, 227npcand 10724 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑉𝑖) − 𝑋) + 𝑋) = (𝑉𝑖))
238234, 235, 2373eqtrrd 2866 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
239238adantr 474 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
240145, 143eqeltrd 2906 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
241240adantr 474 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
242209adantl 475 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
2435ad2antrr 717 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
244213simprld 788 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑄𝑖) < 𝑠)
245244adantl 475 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
246241, 242, 243, 245ltadd2dd 10522 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
247239, 246eqbrtrd 4897 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
248247adantlr 706 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
249 ltaddneg 10577 . . . . . . . . . . . . 13 ((𝑠 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
250210, 225, 249syl2anc 579 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
251217, 250mpbid 224 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < 𝑋)
252222, 224, 226, 248, 251eliood 40517 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋))
253 fvres 6456 . . . . . . . . . . 11 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋) → ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
254253eqcomd 2831 . . . . . . . . . 10 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
255252, 254syl 17 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
256255oveq1d 6925 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝑊) = (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
257256oveq1d 6925 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠) = ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
258208, 221, 2573eqtrd 2865 . . . . . 6 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
259172, 258mpteq12dva 4957 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
260104, 141, 2593eqtrd 2865 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
261260, 171oveq12d 6928 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim 0))
26297, 101, 2613eltr4d 2921 . 2 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
263 eqid 2825 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
264 eqid 2825 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠)
265 eqid 2825 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
26630adantr 474 . . . . . . . . . 10 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℝ)
2675adantr 474 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
268209adantl 475 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
269267, 268readdcld 10393 . . . . . . . . . 10 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
270266, 269ffvelrnd 6614 . . . . . . . . 9 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
271270recnd 10392 . . . . . . . 8 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
272271adantlr 706 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
2732723adantl3 1213 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
274 fourierdlem74.y . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ)
275274recnd 10392 . . . . . . . . 9 (𝜑𝑌 ∈ ℂ)
276 limccl 24045 . . . . . . . . . 10 ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ ℂ
277276, 36sseldi 3825 . . . . . . . . 9 (𝜑𝑊 ∈ ℂ)
278275, 277ifcld 4353 . . . . . . . 8 (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
279278adantr 474 . . . . . . 7 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
2802793ad2antl1 1240 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
281273, 280subcld 10720 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
282209recnd 10392 . . . . . . 7 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℂ)
283282adantl 475 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
284 velsn 4415 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
285206, 284sylnibr 321 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
2862853adantl3 1213 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
287283, 286eldifd 3809 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
288 eqid 2825 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
289 eqid 2825 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊)
290 eqid 2825 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
291277ad2antrr 717 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑊 ∈ ℂ)
29230adantr 474 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℝ)
293 ioossre 12530 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
294293a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
29541adantr 474 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
296161rexrd 10413 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
297296adantr 474 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
298269adantlr 706 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
299196adantr 474 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
300299, 156ffvelrnd 6614 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
301300adantr 474 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
302214adantl 475 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
303242, 301, 243, 302ltadd2dd 10522 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
304164oveq2d 6926 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
305161recnd 10392 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
306227, 305pncan3d 10723 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
307304, 306eqtrd 2861 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
308307adantr 474 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
309303, 308breqtrd 4901 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
310295, 297, 298, 247, 309eliood 40517 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
311 ioossre 12530 . . . . . . . . . . . 12 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
312311a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
313242, 302ltned 10499 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
314 fourierdlem74.r . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
315307eqcomd 2831 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
316315oveq2d 6926 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
317314, 316eleqtrd 2908 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
318300recnd 10392 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
319292, 162, 294, 288, 310, 312, 313, 317, 318fourierdlem53 41168 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
320 ioosscn 40513 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
321320a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
322277adantr 474 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ℂ)
323289, 321, 322, 318constlimc 40649 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) lim (𝑄‘(𝑖 + 1))))
324288, 289, 290, 272, 291, 319, 323sublimc 40677 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑅𝑊) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
325324adantr 474 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅𝑊) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
326 iftrue 4314 . . . . . . . . . 10 ((𝑉‘(𝑖 + 1)) < 𝑋 → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑊)
327326oveq2d 6926 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) < 𝑋 → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅𝑊))
328327adantl 475 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅𝑊))
329209adantl 475 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
330 0red 10367 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
331300ad2antrr 717 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
332214adantl 475 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
333164adantr 474 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
334161adantr 474 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
3355ad2antrr 717 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
336 simpr 479 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) < 𝑋)
337334, 335, 336ltled 10511 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ≤ 𝑋)
338334, 335suble0d 10950 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0 ↔ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
339337, 338mpbird 249 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0)
340333, 339eqbrtrd 4897 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) ≤ 0)
341340adantr 474 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ≤ 0)
342329, 331, 330, 332, 341ltletrd 10523 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
343329, 330, 342ltnsymd 10512 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
344343iffalsed 4319 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
345344oveq2d 6926 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
346345mpteq2dva 4969 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)))
347346oveq1d 6925 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
348325, 328, 3473eltr4d 2921 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
3493483adantl3 1213 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
350 simpl1 1246 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝜑)
351 simpl2 1248 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑖 ∈ (0..^𝑀))
3525ad2antrr 717 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
3533523adantl3 1213 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
354161adantr 474 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
3553543adantl3 1213 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
356 neqne 3007 . . . . . . . . . . 11 (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
357356necomd 3054 . . . . . . . . . 10 (¬ (𝑉‘(𝑖 + 1)) = 𝑋𝑋 ≠ (𝑉‘(𝑖 + 1)))
358357adantr 474 . . . . . . . . 9 ((¬ (𝑉‘(𝑖 + 1)) = 𝑋 ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
3593583ad2antl3 1242 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
360 simpr 479 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
361353, 355, 359, 360lttri5d 40309 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
362 eqid 2825 . . . . . . . 8 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊))
363272adantlr 706 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
364278ad3antrrr 721 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
365319adantr 474 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
366 eqid 2825 . . . . . . . . . . 11 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌)
367275adantr 474 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ℂ)
368366, 321, 367, 318constlimc 40649 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
369368adantr 474 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑌 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
3705ad2antrr 717 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ∈ ℝ)
371161adantr 474 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
372 simpr 479 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 < (𝑉‘(𝑖 + 1)))
373370, 371, 372ltnsymd 10512 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
374373iffalsed 4319 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑌)
375 0red 10367 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
376240ad2antrr 717 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
377209adantl 475 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
378190eqcomd 2831 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 = (𝑋𝑋))
379378ad2antrr 717 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 = (𝑋𝑋))
38017adantr 474 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉𝑖) ∈ ℝ)
38141ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) ∈ ℝ*)
382296ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
383162ad2antrr 717 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ℝ)
384 simpr 479 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ¬ 𝑋 ≤ (𝑉𝑖))
38517adantr 474 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) ∈ ℝ)
3865ad2antrr 717 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ℝ)
387385, 386ltnled 10510 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ((𝑉𝑖) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑉𝑖)))
388384, 387mpbird 249 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) < 𝑋)
389388adantlr 706 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) < 𝑋)
390 simplr 785 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 < (𝑉‘(𝑖 + 1)))
391381, 382, 383, 389, 390eliood 40517 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
39211, 12, 13, 179fourierdlem12 41128 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
393392ad2antrr 717 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ¬ 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
394391, 393condan 852 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ≤ (𝑉𝑖))
395370, 380, 370, 394lesub1dd 10975 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑋𝑋) ≤ ((𝑉𝑖) − 𝑋))
396379, 395eqbrtrd 4897 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ ((𝑉𝑖) − 𝑋))
397145eqcomd 2831 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) = (𝑄𝑖))
398397adantr 474 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑉𝑖) − 𝑋) = (𝑄𝑖))
399396, 398breqtrd 4901 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ (𝑄𝑖))
400399adantr 474 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ≤ (𝑄𝑖))
401244adantl 475 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
402375, 376, 377, 400, 401lelttrd 10521 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
403402iftrued 4316 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
404403mpteq2dva 4969 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌))
405404oveq1d 6925 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
406369, 374, 4053eltr4d 2921 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim (𝑄‘(𝑖 + 1))))
407288, 362, 263, 363, 364, 365, 406sublimc 40677 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
408350, 351, 361, 407syl21anc 871 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
409349, 408pm2.61dan 847 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
410321, 264, 318idlimc 40651 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim (𝑄‘(𝑖 + 1))))
4114103adant3 1166 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim (𝑄‘(𝑖 + 1))))
4121643adant3 1166 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
4133053adant3 1166 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
4142273adant3 1166 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
4153563ad2ant3 1169 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
416413, 414, 415subne0d 10729 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≠ 0)
417412, 416eqnetrd 3066 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ≠ 0)
4182063adantl3 1213 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
419418neqned 3006 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
420263, 264, 265, 281, 287, 409, 411, 417, 419divlimc 40681 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim (𝑄‘(𝑖 + 1))))
421 iffalse 4317 . . . . . 6 (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
42298, 421syl5eq 2873 . . . . 5 (¬ (𝑉‘(𝑖 + 1)) = 𝑋𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
4234223ad2ant3 1169 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
424 ioossre 12530 . . . . . . . . . . . . 13 (-∞(,)𝑋) ⊆ ℝ
425424a1i 11 . . . . . . . . . . . 12 (𝜑 → (-∞(,)𝑋) ⊆ ℝ)
42630, 425fssresd 6312 . . . . . . . . . . 11 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)):(-∞(,)𝑋)⟶ℝ)
427424, 52syl5ss 3838 . . . . . . . . . . 11 (𝜑 → (-∞(,)𝑋) ⊆ ℂ)
42839a1i 11 . . . . . . . . . . . 12 (𝜑 → -∞ ∈ ℝ*)
4295mnfltd 12251 . . . . . . . . . . . 12 (𝜑 → -∞ < 𝑋)
43056, 428, 5, 429lptioo2cn 40670 . . . . . . . . . . 11 (𝜑𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘(-∞(,)𝑋)))
431426, 427, 430, 36limcrecl 40654 . . . . . . . . . 10 (𝜑𝑊 ∈ ℝ)
43230, 5, 274, 431, 102fourierdlem9 41125 . . . . . . . . 9 (𝜑𝐻:(-π[,]π)⟶ℝ)
433432adantr 474 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐻:(-π[,]π)⟶ℝ)
434433, 139feqresmpt 6501 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)))
435139sselda 3827 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (-π[,]π))
436 0cnd 10356 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℂ)
437278ad2antrr 717 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
438272, 437subcld 10720 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
439282adantl 475 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
440206neqned 3006 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
441438, 439, 440divcld 11134 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℂ)
442436, 441ifcld 4353 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ)
443102fvmpt2 6543 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
444435, 442, 443syl2anc 579 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
445206iffalsed 4319 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
446444, 445eqtrd 2861 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
447446mpteq2dva 4969 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
448434, 447eqtrd 2861 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
4494483adant3 1166 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
450449oveq1d 6925 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim (𝑄‘(𝑖 + 1))))
451420, 423, 4503eltr4d 2921 . . 3 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
4524513expa 1151 . 2 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
453262, 452pm2.61dan 847 1 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  w3a 1111   = wceq 1656  wcel 2164  wne 2999  wral 3117  wrex 3118  {crab 3121  wss 3798  ifcif 4308  {csn 4399   class class class wbr 4875  cmpt 4954  dom cdm 5346  ran crn 5347  cres 5348   Fn wfn 6122  wf 6123  cfv 6127  (class class class)co 6910  𝑚 cmap 8127  cc 10257  cr 10258  0cc0 10259  1c1 10260   + caddc 10262  -∞cmnf 10396  *cxr 10397   < clt 10398  cle 10399  cmin 10592  -cneg 10593   / cdiv 11016  cn 11357  (,)cioo 12470  [,]cicc 12473  ...cfz 12626  ..^cfzo 12767  πcpi 15176  TopOpenctopn 16442  topGenctg 16458  fldccnfld 20113  intcnt 21199   lim climc 24032   D cdv 24033
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-rep 4996  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214  ax-inf2 8822  ax-cnex 10315  ax-resscn 10316  ax-1cn 10317  ax-icn 10318  ax-addcl 10319  ax-addrcl 10320  ax-mulcl 10321  ax-mulrcl 10322  ax-mulcom 10323  ax-addass 10324  ax-mulass 10325  ax-distr 10326  ax-i2m1 10327  ax-1ne0 10328  ax-1rid 10329  ax-rnegex 10330  ax-rrecex 10331  ax-cnre 10332  ax-pre-lttri 10333  ax-pre-lttrn 10334  ax-pre-ltadd 10335  ax-pre-mulgt0 10336  ax-pre-sup 10337  ax-addf 10338  ax-mulf 10339
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-fal 1670  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-nel 3103  df-ral 3122  df-rex 3123  df-reu 3124  df-rmo 3125  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-int 4700  df-iun 4744  df-iin 4745  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-se 5306  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-isom 6136  df-riota 6871  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-of 7162  df-om 7332  df-1st 7433  df-2nd 7434  df-supp 7565  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-2o 7832  df-oadd 7835  df-er 8014  df-map 8129  df-pm 8130  df-ixp 8182  df-en 8229  df-dom 8230  df-sdom 8231  df-fin 8232  df-fsupp 8551  df-fi 8592  df-sup 8623  df-inf 8624  df-oi 8691  df-card 9085  df-cda 9312  df-pnf 10400  df-mnf 10401  df-xr 10402  df-ltxr 10403  df-le 10404  df-sub 10594  df-neg 10595  df-div 11017  df-nn 11358  df-2 11421  df-3 11422  df-4 11423  df-5 11424  df-6 11425  df-7 11426  df-8 11427  df-9 11428  df-n0 11626  df-z 11712  df-dec 11829  df-uz 11976  df-q 12079  df-rp 12120  df-xneg 12239  df-xadd 12240  df-xmul 12241  df-ioo 12474  df-ioc 12475  df-ico 12476  df-icc 12477  df-fz 12627  df-fzo 12768  df-fl 12895  df-seq 13103  df-exp 13162  df-fac 13361  df-bc 13390  df-hash 13418  df-shft 14191  df-cj 14223  df-re 14224  df-im 14225  df-sqrt 14359  df-abs 14360  df-limsup 14586  df-clim 14603  df-rlim 14604  df-sum 14801  df-ef 15177  df-sin 15179  df-cos 15180  df-pi 15182  df-struct 16231  df-ndx 16232  df-slot 16233  df-base 16235  df-sets 16236  df-ress 16237  df-plusg 16325  df-mulr 16326  df-starv 16327  df-sca 16328  df-vsca 16329  df-ip 16330  df-tset 16331  df-ple 16332  df-ds 16334  df-unif 16335  df-hom 16336  df-cco 16337  df-rest 16443  df-topn 16444  df-0g 16462  df-gsum 16463  df-topgen 16464  df-pt 16465  df-prds 16468  df-xrs 16522  df-qtop 16527  df-imas 16528  df-xps 16530  df-mre 16606  df-mrc 16607  df-acs 16609  df-mgm 17602  df-sgrp 17644  df-mnd 17655  df-submnd 17696  df-mulg 17902  df-cntz 18107  df-cmn 18555  df-psmet 20105  df-xmet 20106  df-met 20107  df-bl 20108  df-mopn 20109  df-fbas 20110  df-fg 20111  df-cnfld 20114  df-top 21076  df-topon 21093  df-topsp 21115  df-bases 21128  df-cld 21201  df-ntr 21202  df-cls 21203  df-nei 21280  df-lp 21318  df-perf 21319  df-cn 21409  df-cnp 21410  df-haus 21497  df-cmp 21568  df-tx 21743  df-hmeo 21936  df-fil 22027  df-fm 22119  df-flim 22120  df-flf 22121  df-xms 22502  df-ms 22503  df-tms 22504  df-cncf 23058  df-limc 24036  df-dv 24037
This theorem is referenced by:  fourierdlem88  41203  fourierdlem103  41218  fourierdlem104  41219
  Copyright terms: Public domain W3C validator