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 45406
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 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (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 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (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 13646 . . . . . 6 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
2 pire 26312 . . . . . . . . . . . 12 π ∈ ℝ
32renegcli 11519 . . . . . . . . . . 11 -π ∈ ℝ
43a1i 11 . . . . . . . . . 10 (𝜑 → -π ∈ ℝ)
5 fourierdlem74.xre . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
64, 5readdcld 11241 . . . . . . . . 9 (𝜑 → (-π + 𝑋) ∈ ℝ)
72a1i 11 . . . . . . . . . 10 (𝜑 → π ∈ ℝ)
87, 5readdcld 11241 . . . . . . . . 9 (𝜑 → (π + 𝑋) ∈ ℝ)
96, 8iccssred 13409 . . . . . . . 8 (𝜑 → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
109adantr 480 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑀)) → ((-π + 𝑋)[,](π + 𝑋)) ⊆ ℝ)
11 fourierdlem74.p . . . . . . . . 9 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (-π + 𝑋) ∧ (𝑝𝑚) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
12 fourierdlem74.m . . . . . . . . 9 (𝜑𝑀 ∈ ℕ)
13 fourierdlem74.v . . . . . . . . 9 (𝜑𝑉 ∈ (𝑃𝑀))
1411, 12, 13fourierdlem15 45348 . . . . . . . 8 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
1514ffvelcdmda 7077 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
1610, 15sseldd 3976 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ℝ)
171, 16sylan2 592 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
1817adantr 480 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) ∈ ℝ)
195ad2antrr 723 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℝ)
2011fourierdlem2 45335 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
2112, 20syl 17 . . . . . . . . 9 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
2213, 21mpbid 231 . . . . . . . 8 (𝜑 → (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
2322simprrd 771 . . . . . . 7 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
2423r19.21bi 3240 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
2524adantr 480 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
26 eqcom 2731 . . . . . . 7 ((𝑉‘(𝑖 + 1)) = 𝑋𝑋 = (𝑉‘(𝑖 + 1)))
2726biimpi 215 . . . . . 6 ((𝑉‘(𝑖 + 1)) = 𝑋𝑋 = (𝑉‘(𝑖 + 1)))
2827adantl 481 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 = (𝑉‘(𝑖 + 1)))
2925, 28breqtrrd 5167 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) < 𝑋)
30 fourierdlem74.f . . . . . 6 (𝜑𝐹:ℝ⟶ℝ)
31 ioossre 13383 . . . . . . 7 ((𝑉𝑖)(,)𝑋) ⊆ ℝ
3231a1i 11 . . . . . 6 (𝜑 → ((𝑉𝑖)(,)𝑋) ⊆ ℝ)
3330, 32fssresd 6749 . . . . 5 (𝜑 → (𝐹 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
3433ad2antrr 723 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐹 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
35 limcresi 25738 . . . . . . . 8 ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋)
36 fourierdlem74.w . . . . . . . 8 (𝜑𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
3735, 36sselid 3973 . . . . . . 7 (𝜑𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
3837adantr 480 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
39 mnfxr 11269 . . . . . . . . . 10 -∞ ∈ ℝ*
4039a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ*)
4117rexrd 11262 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ*)
4217mnfltd 13102 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < (𝑉𝑖))
4340, 41, 42xrltled 13127 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑉𝑖))
44 iooss1 13357 . . . . . . . . 9 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑉𝑖)) → ((𝑉𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
4540, 43, 44syl2anc 583 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
4645resabs1d 6003 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) = (𝐹 ↾ ((𝑉𝑖)(,)𝑋)))
4746oveq1d 7417 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
4838, 47eleqtrd 2827 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
4948adantr 480 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑊 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
50 eqid 2724 . . . 4 (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋)))
51 ax-resscn 11164 . . . . . . . . . 10 ℝ ⊆ ℂ
5251a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℂ)
5330, 52fssd 6726 . . . . . . . . 9 (𝜑𝐹:ℝ⟶ℂ)
54 ssid 3997 . . . . . . . . . 10 ℝ ⊆ ℝ
5554a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℝ)
56 eqid 2724 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5756tgioo2 24643 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
5856, 57dvres 25764 . . . . . . . . 9 (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑉𝑖)(,)𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))))
5952, 53, 55, 32, 58syl22anc 836 . . . . . . . 8 (𝜑 → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))))
60 fourierdlem74.g . . . . . . . . . . 11 𝐺 = (ℝ D 𝐹)
6160eqcomi 2733 . . . . . . . . . 10 (ℝ D 𝐹) = 𝐺
62 ioontr 44734 . . . . . . . . . 10 ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋)
6361, 62reseq12i 5970 . . . . . . . . 9 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋))
6463a1i 11 . . . . . . . 8 (𝜑 → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6559, 64eqtrd 2764 . . . . . . 7 (𝜑 → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6665dmeqd 5896 . . . . . 6 (𝜑 → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6766ad2antrr 723 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
68 fourierdlem74.gcn . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
6968adantr 480 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
70 oveq2 7410 . . . . . . . . . 10 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) = ((𝑉𝑖)(,)𝑋))
7170reseq2d 5972 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) = 𝑋 → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
7271, 70feq12d 6696 . . . . . . . 8 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ))
7372adantl 481 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ))
7469, 73mpbid 231 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
75 fdm 6717 . . . . . 6 ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ → dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋))
7674, 75syl 17 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋))
7767, 76eqtrd 2764 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((𝑉𝑖)(,)𝑋))
78 limcresi 25738 . . . . . . . 8 ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋)
7945resabs1d 6003 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
8079oveq1d 7417 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
8178, 80sseqtrid 4027 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
82 fourierdlem74.e . . . . . . . 8 (𝜑𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋))
8382adantr 480 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋))
8481, 83sseldd 3976 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
8559, 64eqtr2d 2765 . . . . . . . 8 (𝜑 → (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))))
8685oveq1d 7417 . . . . . . 7 (𝜑 → ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8786adantr 480 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8884, 87eleqtrd 2827 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8988adantr 480 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
90 eqid 2724 . . . 4 (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
91 oveq2 7410 . . . . . . 7 (𝑥 = 𝑠 → (𝑋 + 𝑥) = (𝑋 + 𝑠))
9291fveq2d 6886 . . . . . 6 (𝑥 = 𝑠 → ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
9392oveq1d 7417 . . . . 5 (𝑥 = 𝑠 → (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊) = (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
9493cbvmptv 5252 . . . 4 (𝑥 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊)) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
95 id 22 . . . . 5 (𝑥 = 𝑠𝑥 = 𝑠)
9695cbvmptv 5252 . . . 4 (𝑥 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ 𝑥) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ 𝑠)
9718, 19, 29, 34, 49, 50, 77, 89, 90, 94, 96fourierdlem60 45392 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim 0))
98 fourierdlem74.a . . . . 5 𝐴 = if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
99 iftrue 4527 . . . . 5 ((𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = 𝐸)
10098, 99eqtrid 2776 . . . 4 ((𝑉‘(𝑖 + 1)) = 𝑋𝐴 = 𝐸)
101100adantl 481 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = 𝐸)
102 fourierdlem74.h . . . . . . 7 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
103102reseq1i 5968 . . . . . 6 (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
104103a1i 11 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
105 ioossicc 13408 . . . . . . . 8 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
1063rexri 11270 . . . . . . . . . 10 -π ∈ ℝ*
107106a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ*)
1082rexri 11270 . . . . . . . . . 10 π ∈ ℝ*
109108a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → π ∈ ℝ*)
1103a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → -π ∈ ℝ)
1112a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → π ∈ ℝ)
1125adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
11316, 112resubcld 11640 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
1144recnd 11240 . . . . . . . . . . . . . . . 16 (𝜑 → -π ∈ ℂ)
1155recnd 11240 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℂ)
116114, 115pncand 11570 . . . . . . . . . . . . . . 15 (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
117116eqcomd 2730 . . . . . . . . . . . . . 14 (𝜑 → -π = ((-π + 𝑋) − 𝑋))
118117adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → -π = ((-π + 𝑋) − 𝑋))
1196adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ∈ ℝ)
1208adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑀)) → (π + 𝑋) ∈ ℝ)
121 elicc2 13387 . . . . . . . . . . . . . . . . 17 (((-π + 𝑋) ∈ ℝ ∧ (π + 𝑋) ∈ ℝ) → ((𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋))))
122119, 120, 121syl2anc 583 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋))))
12315, 122mpbid 231 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋)))
124123simp2d 1140 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ≤ (𝑉𝑖))
125119, 16, 112, 124lesub1dd 11828 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((-π + 𝑋) − 𝑋) ≤ ((𝑉𝑖) − 𝑋))
126118, 125eqbrtrd 5161 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → -π ≤ ((𝑉𝑖) − 𝑋))
127123simp3d 1141 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ≤ (π + 𝑋))
12816, 120, 112, 127lesub1dd 11828 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ≤ ((π + 𝑋) − 𝑋))
129111recnd 11240 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → π ∈ ℂ)
130115adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℂ)
131129, 130pncand 11570 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((π + 𝑋) − 𝑋) = π)
132128, 131breqtrd 5165 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ≤ π)
133110, 111, 113, 126, 132eliccd 44727 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ (-π[,]π))
134 fourierdlem74.q . . . . . . . . . . 11 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
135133, 134fmptd 7106 . . . . . . . . . 10 (𝜑𝑄:(0...𝑀)⟶(-π[,]π))
136135adantr 480 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
137 simpr 484 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
138107, 109, 136, 137fourierdlem8 45341 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
139105, 138sstrid 3986 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
140139resmptd 6031 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
141140adantr 480 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))))
1421adantl 481 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
1431, 113sylan2 592 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
144134fvmpt2 7000 . . . . . . . . 9 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
145142, 143, 144syl2anc 583 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
146145adantr 480 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
147 fveq2 6882 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑉𝑖) = (𝑉𝑗))
148147oveq1d 7417 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑗) − 𝑋))
149148cbvmptv 5252 . . . . . . . . . . . 12 (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
150134, 149eqtri 2752 . . . . . . . . . . 11 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
151150a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋)))
152 fveq2 6882 . . . . . . . . . . . 12 (𝑗 = (𝑖 + 1) → (𝑉𝑗) = (𝑉‘(𝑖 + 1)))
153152oveq1d 7417 . . . . . . . . . . 11 (𝑗 = (𝑖 + 1) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
154153adantl 481 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
155 fzofzp1 13727 . . . . . . . . . . 11 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
156155adantl 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
15722simpld 494 . . . . . . . . . . . . . 14 (𝜑𝑉 ∈ (ℝ ↑m (0...𝑀)))
158 elmapi 8840 . . . . . . . . . . . . . 14 (𝑉 ∈ (ℝ ↑m (0...𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
159157, 158syl 17 . . . . . . . . . . . . 13 (𝜑𝑉:(0...𝑀)⟶ℝ)
160159adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
161160, 156ffvelcdmd 7078 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
1625adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
163161, 162resubcld 11640 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
164151, 154, 156, 163fvmptd 6996 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
165164adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
166 oveq1 7409 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋𝑋))
167166adantl 481 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋𝑋))
168115ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
169168subidd 11557 . . . . . . . . 9 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋𝑋) = 0)
1701, 169sylanl2 678 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋𝑋) = 0)
171165, 167, 1703eqtrd 2768 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = 0)
172146, 171oveq12d 7420 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑉𝑖) − 𝑋)(,)0))
173 simplr 766 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
174 fourierdlem74.o . . . . . . . . . . . . 13 𝑂 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = -π ∧ (𝑝𝑚) = π) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
17512adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑀 ∈ ℕ)
1764, 7, 5, 11, 174, 12, 13, 134fourierdlem14 45347 . . . . . . . . . . . . . 14 (𝜑𝑄 ∈ (𝑂𝑀))
177176adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑄 ∈ (𝑂𝑀))
178 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑠 = 0) → 𝑠 = 0)
179 fourierdlem74.x . . . . . . . . . . . . . . . . . 18 (𝜑𝑋 ∈ ran 𝑉)
180 ffn 6708 . . . . . . . . . . . . . . . . . . 19 (𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)) → 𝑉 Fn (0...𝑀))
181 fvelrnb 6943 . . . . . . . . . . . . . . . . . . 19 (𝑉 Fn (0...𝑀) → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋))
18214, 180, 1813syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋))
183179, 182mpbid 231 . . . . . . . . . . . . . . . . 17 (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋)
184 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
185134fvmpt2 7000 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ (-π[,]π)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
186184, 133, 185syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
187186adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
188 oveq1 7409 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉𝑖) = 𝑋 → ((𝑉𝑖) − 𝑋) = (𝑋𝑋))
189188adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → ((𝑉𝑖) − 𝑋) = (𝑋𝑋))
190115subidd 11557 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑋𝑋) = 0)
191190ad2antrr 723 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑋𝑋) = 0)
192187, 189, 1913eqtrd 2768 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑄𝑖) = 0)
193192ex 412 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) = 𝑋 → (𝑄𝑖) = 0))
194193reximdva 3160 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋 → ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0))
195183, 194mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0)
196113, 134fmptd 7106 . . . . . . . . . . . . . . . . 17 (𝜑𝑄:(0...𝑀)⟶ℝ)
197 ffn 6708 . . . . . . . . . . . . . . . . 17 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
198 fvelrnb 6943 . . . . . . . . . . . . . . . . 17 (𝑄 Fn (0...𝑀) → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0))
199196, 197, 1983syl 18 . . . . . . . . . . . . . . . 16 (𝜑 → (0 ∈ ran 𝑄 ↔ ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0))
200195, 199mpbird 257 . . . . . . . . . . . . . . 15 (𝜑 → 0 ∈ ran 𝑄)
201200adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑠 = 0) → 0 ∈ ran 𝑄)
202178, 201eqeltrd 2825 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑠 ∈ ran 𝑄)
203174, 175, 177, 202fourierdlem12 45345 . . . . . . . . . . . 12 (((𝜑𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
204203an32s 649 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
205204adantlr 712 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
206173, 205pm2.65da 814 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
207206adantlr 712 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
208207iffalsed 4532 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
209 elioore 13352 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
210209adantl 481 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
211 0red 11215 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
212 elioo3g 13351 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ℝ*) ∧ ((𝑄𝑖) < 𝑠𝑠 < (𝑄‘(𝑖 + 1)))))
213212biimpi 215 . . . . . . . . . . . . . 14 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ℝ*) ∧ ((𝑄𝑖) < 𝑠𝑠 < (𝑄‘(𝑖 + 1)))))
214213simprrd 771 . . . . . . . . . . . . 13 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 < (𝑄‘(𝑖 + 1)))
215214adantl 481 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
216171adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) = 0)
217215, 216breqtrd 5165 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
218210, 211, 217ltnsymd 11361 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
219218iffalsed 4532 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
220219oveq2d 7418 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
221220oveq1d 7417 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
22241ad2antrr 723 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
2235rexrd 11262 . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ*)
224223ad3antrrr 727 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
225162ad2antrr 723 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
226225, 210readdcld 11241 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
227115adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
228 iccssre 13404 . . . . . . . . . . . . . . . . . . 19 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
2293, 2, 228mp2an 689 . . . . . . . . . . . . . . . . . 18 (-π[,]π) ⊆ ℝ
230229, 51sstri 3984 . . . . . . . . . . . . . . . . 17 (-π[,]π) ⊆ ℂ
231186, 133eqeltrd 2825 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) ∈ (-π[,]π))
2321, 231sylan2 592 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ (-π[,]π))
233230, 232sselid 3973 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
234227, 233addcomd 11414 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄𝑖)) = ((𝑄𝑖) + 𝑋))
235145oveq1d 7417 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑋) = (((𝑉𝑖) − 𝑋) + 𝑋))
23617recnd 11240 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℂ)
237236, 227npcand 11573 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑉𝑖) − 𝑋) + 𝑋) = (𝑉𝑖))
238234, 235, 2373eqtrrd 2769 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
239238adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
240145, 143eqeltrd 2825 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
241240adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
242209adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
2435ad2antrr 723 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
244213simprld 769 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑄𝑖) < 𝑠)
245244adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
246241, 242, 243, 245ltadd2dd 11371 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
247239, 246eqbrtrd 5161 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
248247adantlr 712 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
249 ltaddneg 11427 . . . . . . . . . . . . 13 ((𝑠 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
250210, 225, 249syl2anc 583 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
251217, 250mpbid 231 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < 𝑋)
252222, 224, 226, 248, 251eliood 44721 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋))
253 fvres 6901 . . . . . . . . . . 11 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋) → ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
254253eqcomd 2730 . . . . . . . . . 10 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
255252, 254syl 17 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
256255oveq1d 7417 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝑊) = (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
257256oveq1d 7417 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠) = ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
258208, 221, 2573eqtrd 2768 . . . . . 6 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
259172, 258mpteq12dva 5228 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
260104, 141, 2593eqtrd 2768 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
261260, 171oveq12d 7420 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim 0))
26297, 101, 2613eltr4d 2840 . 2 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
263 eqid 2724 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
264 eqid 2724 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠)
265 eqid 2724 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
26630adantr 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℝ)
2675adantr 480 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
268209adantl 481 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
269267, 268readdcld 11241 . . . . . . . . . 10 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
270266, 269ffvelcdmd 7078 . . . . . . . . 9 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
271270recnd 11240 . . . . . . . 8 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
272271adantlr 712 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
2732723adantl3 1165 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
274 fourierdlem74.y . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ)
275274recnd 11240 . . . . . . . . 9 (𝜑𝑌 ∈ ℂ)
276 limccl 25728 . . . . . . . . . 10 ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ ℂ
277276, 36sselid 3973 . . . . . . . . 9 (𝜑𝑊 ∈ ℂ)
278275, 277ifcld 4567 . . . . . . . 8 (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
279278adantr 480 . . . . . . 7 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
2802793ad2antl1 1182 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
281273, 280subcld 11569 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
282209recnd 11240 . . . . . . 7 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℂ)
283282adantl 481 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
284 velsn 4637 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
285206, 284sylnibr 329 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
2862853adantl3 1165 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
287283, 286eldifd 3952 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
288 eqid 2724 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
289 eqid 2724 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊)
290 eqid 2724 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
291277ad2antrr 723 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑊 ∈ ℂ)
29230adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℝ)
293 ioossre 13383 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
294293a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
29541adantr 480 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
296161rexrd 11262 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
297296adantr 480 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
298269adantlr 712 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
299196adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
300299, 156ffvelcdmd 7078 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
301300adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
302214adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
303242, 301, 243, 302ltadd2dd 11371 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
304164oveq2d 7418 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
305161recnd 11240 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
306227, 305pncan3d 11572 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
307304, 306eqtrd 2764 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
308307adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
309303, 308breqtrd 5165 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
310295, 297, 298, 247, 309eliood 44721 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
311 ioossre 13383 . . . . . . . . . . . 12 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
312311a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
313242, 302ltned 11348 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
314 fourierdlem74.r . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
315307eqcomd 2730 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
316315oveq2d 7418 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
317314, 316eleqtrd 2827 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
318300recnd 11240 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
319292, 162, 294, 288, 310, 312, 313, 317, 318fourierdlem53 45385 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
320 ioosscn 13384 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
321320a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
322277adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ℂ)
323289, 321, 322, 318constlimc 44850 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) lim (𝑄‘(𝑖 + 1))))
324288, 289, 290, 272, 291, 319, 323sublimc 44878 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑅𝑊) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
325324adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅𝑊) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
326 iftrue 4527 . . . . . . . . . 10 ((𝑉‘(𝑖 + 1)) < 𝑋 → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑊)
327326oveq2d 7418 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) < 𝑋 → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅𝑊))
328327adantl 481 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅𝑊))
329209adantl 481 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
330 0red 11215 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
331300ad2antrr 723 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
332214adantl 481 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
333164adantr 480 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
334161adantr 480 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
3355ad2antrr 723 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
336 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) < 𝑋)
337334, 335, 336ltled 11360 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ≤ 𝑋)
338334, 335suble0d 11803 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0 ↔ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
339337, 338mpbird 257 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0)
340333, 339eqbrtrd 5161 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) ≤ 0)
341340adantr 480 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ≤ 0)
342329, 331, 330, 332, 341ltletrd 11372 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
343329, 330, 342ltnsymd 11361 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
344343iffalsed 4532 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
345344oveq2d 7418 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
346345mpteq2dva 5239 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)))
347346oveq1d 7417 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
348325, 328, 3473eltr4d 2840 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
3493483adantl3 1165 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
350 simpl1 1188 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝜑)
351 simpl2 1189 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑖 ∈ (0..^𝑀))
3525ad2antrr 723 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
3533523adantl3 1165 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
354161adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
3553543adantl3 1165 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
356 neqne 2940 . . . . . . . . . . 11 (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
357356necomd 2988 . . . . . . . . . 10 (¬ (𝑉‘(𝑖 + 1)) = 𝑋𝑋 ≠ (𝑉‘(𝑖 + 1)))
358357adantr 480 . . . . . . . . 9 ((¬ (𝑉‘(𝑖 + 1)) = 𝑋 ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
3593583ad2antl3 1184 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
360 simpr 484 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
361353, 355, 359, 360lttri5d 44519 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
362 eqid 2724 . . . . . . . 8 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊))
363272adantlr 712 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
364278ad3antrrr 727 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
365319adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
366 eqid 2724 . . . . . . . . . . 11 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌)
367275adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ℂ)
368366, 321, 367, 318constlimc 44850 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
369368adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑌 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
3705ad2antrr 723 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ∈ ℝ)
371161adantr 480 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
372 simpr 484 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 < (𝑉‘(𝑖 + 1)))
373370, 371, 372ltnsymd 11361 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
374373iffalsed 4532 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑌)
375 0red 11215 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
376240ad2antrr 723 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
377209adantl 481 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
378190eqcomd 2730 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 = (𝑋𝑋))
379378ad2antrr 723 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 = (𝑋𝑋))
38017adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉𝑖) ∈ ℝ)
38141ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) ∈ ℝ*)
382296ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
383162ad2antrr 723 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ℝ)
384 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ¬ 𝑋 ≤ (𝑉𝑖))
38517adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) ∈ ℝ)
3865ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ℝ)
387385, 386ltnled 11359 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ((𝑉𝑖) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑉𝑖)))
388384, 387mpbird 257 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) < 𝑋)
389388adantlr 712 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) < 𝑋)
390 simplr 766 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 < (𝑉‘(𝑖 + 1)))
391381, 382, 383, 389, 390eliood 44721 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
39211, 12, 13, 179fourierdlem12 45345 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
393392ad2antrr 723 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ¬ 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
394391, 393condan 815 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ≤ (𝑉𝑖))
395370, 380, 370, 394lesub1dd 11828 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑋𝑋) ≤ ((𝑉𝑖) − 𝑋))
396379, 395eqbrtrd 5161 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ ((𝑉𝑖) − 𝑋))
397145eqcomd 2730 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) = (𝑄𝑖))
398397adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑉𝑖) − 𝑋) = (𝑄𝑖))
399396, 398breqtrd 5165 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ (𝑄𝑖))
400399adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ≤ (𝑄𝑖))
401244adantl 481 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
402375, 376, 377, 400, 401lelttrd 11370 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
403402iftrued 4529 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
404403mpteq2dva 5239 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌))
405404oveq1d 7417 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
406369, 374, 4053eltr4d 2840 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim (𝑄‘(𝑖 + 1))))
407288, 362, 263, 363, 364, 365, 406sublimc 44878 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
408350, 351, 361, 407syl21anc 835 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
409349, 408pm2.61dan 810 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
410321, 264, 318idlimc 44852 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim (𝑄‘(𝑖 + 1))))
4114103adant3 1129 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim (𝑄‘(𝑖 + 1))))
4121643adant3 1129 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
4133053adant3 1129 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
4142273adant3 1129 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
4153563ad2ant3 1132 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
416413, 414, 415subne0d 11578 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≠ 0)
417412, 416eqnetrd 3000 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ≠ 0)
4182063adantl3 1165 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
419418neqned 2939 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
420263, 264, 265, 281, 287, 409, 411, 417, 419divlimc 44882 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim (𝑄‘(𝑖 + 1))))
421 iffalse 4530 . . . . . 6 (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
42298, 421eqtrid 2776 . . . . 5 (¬ (𝑉‘(𝑖 + 1)) = 𝑋𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
4234223ad2ant3 1132 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
424 ioossre 13383 . . . . . . . . . . . . 13 (-∞(,)𝑋) ⊆ ℝ
425424a1i 11 . . . . . . . . . . . 12 (𝜑 → (-∞(,)𝑋) ⊆ ℝ)
42630, 425fssresd 6749 . . . . . . . . . . 11 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)):(-∞(,)𝑋)⟶ℝ)
427424, 52sstrid 3986 . . . . . . . . . . 11 (𝜑 → (-∞(,)𝑋) ⊆ ℂ)
42839a1i 11 . . . . . . . . . . . 12 (𝜑 → -∞ ∈ ℝ*)
4295mnfltd 13102 . . . . . . . . . . . 12 (𝜑 → -∞ < 𝑋)
43056, 428, 5, 429lptioo2cn 44871 . . . . . . . . . . 11 (𝜑𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘(-∞(,)𝑋)))
431426, 427, 430, 36limcrecl 44855 . . . . . . . . . 10 (𝜑𝑊 ∈ ℝ)
43230, 5, 274, 431, 102fourierdlem9 45342 . . . . . . . . 9 (𝜑𝐻:(-π[,]π)⟶ℝ)
433432adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐻:(-π[,]π)⟶ℝ)
434433, 139feqresmpt 6952 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)))
435139sselda 3975 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (-π[,]π))
436 0cnd 11205 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℂ)
437278ad2antrr 723 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
438272, 437subcld 11569 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
439282adantl 481 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
440206neqned 2939 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
441438, 439, 440divcld 11988 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℂ)
442436, 441ifcld 4567 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ)
443102fvmpt2 7000 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
444435, 442, 443syl2anc 583 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
445206iffalsed 4532 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
446444, 445eqtrd 2764 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
447446mpteq2dva 5239 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
448434, 447eqtrd 2764 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
4494483adant3 1129 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
450449oveq1d 7417 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim (𝑄‘(𝑖 + 1))))
451420, 423, 4503eltr4d 2840 . . 3 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
4524513expa 1115 . 2 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
453262, 452pm2.61dan 810 1 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  w3a 1084   = wceq 1533  wcel 2098  wne 2932  wral 3053  wrex 3062  {crab 3424  wss 3941  ifcif 4521  {csn 4621   class class class wbr 5139  cmpt 5222  dom cdm 5667  ran crn 5668  cres 5669   Fn wfn 6529  wf 6530  cfv 6534  (class class class)co 7402  m cmap 8817  cc 11105  cr 11106  0cc0 11107  1c1 11108   + caddc 11110  -∞cmnf 11244  *cxr 11245   < clt 11246  cle 11247  cmin 11442  -cneg 11443   / cdiv 11869  cn 12210  (,)cioo 13322  [,]cicc 13325  ...cfz 13482  ..^cfzo 13625  πcpi 16008  TopOpenctopn 17368  topGenctg 17384  fldccnfld 21230  intcnt 22845   lim climc 25715   D cdv 25716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185  ax-addf 11186
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-nel 3039  df-ral 3054  df-rex 3063  df-rmo 3368  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-pss 3960  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-tp 4626  df-op 4628  df-uni 4901  df-int 4942  df-iun 4990  df-iin 4991  df-br 5140  df-opab 5202  df-mpt 5223  df-tr 5257  df-id 5565  df-eprel 5571  df-po 5579  df-so 5580  df-fr 5622  df-se 5623  df-we 5624  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-pred 6291  df-ord 6358  df-on 6359  df-lim 6360  df-suc 6361  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-isom 6543  df-riota 7358  df-ov 7405  df-oprab 7406  df-mpo 7407  df-of 7664  df-om 7850  df-1st 7969  df-2nd 7970  df-supp 8142  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-2o 8463  df-er 8700  df-map 8819  df-pm 8820  df-ixp 8889  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fsupp 9359  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-card 9931  df-pnf 11248  df-mnf 11249  df-xr 11250  df-ltxr 11251  df-le 11252  df-sub 11444  df-neg 11445  df-div 11870  df-nn 12211  df-2 12273  df-3 12274  df-4 12275  df-5 12276  df-6 12277  df-7 12278  df-8 12279  df-9 12280  df-n0 12471  df-z 12557  df-dec 12676  df-uz 12821  df-q 12931  df-rp 12973  df-xneg 13090  df-xadd 13091  df-xmul 13092  df-ioo 13326  df-ioc 13327  df-ico 13328  df-icc 13329  df-fz 13483  df-fzo 13626  df-fl 13755  df-seq 13965  df-exp 14026  df-fac 14232  df-bc 14261  df-hash 14289  df-shft 15012  df-cj 15044  df-re 15045  df-im 15046  df-sqrt 15180  df-abs 15181  df-limsup 15413  df-clim 15430  df-rlim 15431  df-sum 15631  df-ef 16009  df-sin 16011  df-cos 16012  df-pi 16014  df-struct 17081  df-sets 17098  df-slot 17116  df-ndx 17128  df-base 17146  df-ress 17175  df-plusg 17211  df-mulr 17212  df-starv 17213  df-sca 17214  df-vsca 17215  df-ip 17216  df-tset 17217  df-ple 17218  df-ds 17220  df-unif 17221  df-hom 17222  df-cco 17223  df-rest 17369  df-topn 17370  df-0g 17388  df-gsum 17389  df-topgen 17390  df-pt 17391  df-prds 17394  df-xrs 17449  df-qtop 17454  df-imas 17455  df-xps 17457  df-mre 17531  df-mrc 17532  df-acs 17534  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-submnd 18706  df-mulg 18988  df-cntz 19225  df-cmn 19694  df-psmet 21222  df-xmet 21223  df-met 21224  df-bl 21225  df-mopn 21226  df-fbas 21227  df-fg 21228  df-cnfld 21231  df-top 22720  df-topon 22737  df-topsp 22759  df-bases 22773  df-cld 22847  df-ntr 22848  df-cls 22849  df-nei 22926  df-lp 22964  df-perf 22965  df-cn 23055  df-cnp 23056  df-haus 23143  df-cmp 23215  df-tx 23390  df-hmeo 23583  df-fil 23674  df-fm 23766  df-flim 23767  df-flf 23768  df-xms 24150  df-ms 24151  df-tms 24152  df-cncf 24722  df-limc 25719  df-dv 25720
This theorem is referenced by:  fourierdlem88  45420  fourierdlem103  45435  fourierdlem104  45436
  Copyright terms: Public domain W3C validator