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 46135
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 13711 . . . . . 6 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
2 pire 26514 . . . . . . . . . . . 12 π ∈ ℝ
32renegcli 11567 . . . . . . . . . . 11 -π ∈ ℝ
43a1i 11 . . . . . . . . . 10 (𝜑 → -π ∈ ℝ)
5 fourierdlem74.xre . . . . . . . . . 10 (𝜑𝑋 ∈ ℝ)
64, 5readdcld 11287 . . . . . . . . 9 (𝜑 → (-π + 𝑋) ∈ ℝ)
72a1i 11 . . . . . . . . . 10 (𝜑 → π ∈ ℝ)
87, 5readdcld 11287 . . . . . . . . 9 (𝜑 → (π + 𝑋) ∈ ℝ)
96, 8iccssred 13470 . . . . . . . 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 46077 . . . . . . . 8 (𝜑𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)))
1514ffvelcdmda 7103 . . . . . . 7 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)))
1610, 15sseldd 3995 . . . . . 6 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ∈ ℝ)
171, 16sylan2 593 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ)
1817adantr 480 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) ∈ ℝ)
195ad2antrr 726 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℝ)
2011fourierdlem2 46064 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
2112, 20syl 17 . . . . . . . . 9 (𝜑 → (𝑉 ∈ (𝑃𝑀) ↔ (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1))))))
2213, 21mpbid 232 . . . . . . . 8 (𝜑 → (𝑉 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑉‘0) = (-π + 𝑋) ∧ (𝑉𝑀) = (π + 𝑋)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))))
2322simprrd 774 . . . . . . 7 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑉𝑖) < (𝑉‘(𝑖 + 1)))
2423r19.21bi 3248 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
2524adantr 480 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) < (𝑉‘(𝑖 + 1)))
26 eqcom 2741 . . . . . . 7 ((𝑉‘(𝑖 + 1)) = 𝑋𝑋 = (𝑉‘(𝑖 + 1)))
2726biimpi 216 . . . . . 6 ((𝑉‘(𝑖 + 1)) = 𝑋𝑋 = (𝑉‘(𝑖 + 1)))
2827adantl 481 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 = (𝑉‘(𝑖 + 1)))
2925, 28breqtrrd 5175 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉𝑖) < 𝑋)
30 fourierdlem74.f . . . . . 6 (𝜑𝐹:ℝ⟶ℝ)
31 ioossre 13444 . . . . . . 7 ((𝑉𝑖)(,)𝑋) ⊆ ℝ
3231a1i 11 . . . . . 6 (𝜑 → ((𝑉𝑖)(,)𝑋) ⊆ ℝ)
3330, 32fssresd 6775 . . . . 5 (𝜑 → (𝐹 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
3433ad2antrr 726 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐹 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
35 limcresi 25934 . . . . . . . 8 ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋)
36 fourierdlem74.w . . . . . . . 8 (𝜑𝑊 ∈ ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋))
3735, 36sselid 3992 . . . . . . 7 (𝜑𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
3837adantr 480 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
39 mnfxr 11315 . . . . . . . . . 10 -∞ ∈ ℝ*
4039a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ∈ ℝ*)
4117rexrd 11308 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℝ*)
4217mnfltd 13163 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ < (𝑉𝑖))
4340, 41, 42xrltled 13188 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -∞ ≤ (𝑉𝑖))
44 iooss1 13418 . . . . . . . . 9 ((-∞ ∈ ℝ* ∧ -∞ ≤ (𝑉𝑖)) → ((𝑉𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
4540, 43, 44syl2anc 584 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖)(,)𝑋) ⊆ (-∞(,)𝑋))
4645resabs1d 6027 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) = (𝐹 ↾ ((𝑉𝑖)(,)𝑋)))
4746oveq1d 7445 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐹 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
4838, 47eleqtrd 2840 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
4948adantr 480 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑊 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
50 eqid 2734 . . . 4 (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋)))
51 ax-resscn 11209 . . . . . . . . . 10 ℝ ⊆ ℂ
5251a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℂ)
5330, 52fssd 6753 . . . . . . . . 9 (𝜑𝐹:ℝ⟶ℂ)
54 ssid 4017 . . . . . . . . . 10 ℝ ⊆ ℝ
5554a1i 11 . . . . . . . . 9 (𝜑 → ℝ ⊆ ℝ)
56 eqid 2734 . . . . . . . . . 10 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
5756tgioo2 24838 . . . . . . . . . 10 (topGen‘ran (,)) = ((TopOpen‘ℂfld) ↾t ℝ)
5856, 57dvres 25960 . . . . . . . . 9 (((ℝ ⊆ ℂ ∧ 𝐹:ℝ⟶ℂ) ∧ (ℝ ⊆ ℝ ∧ ((𝑉𝑖)(,)𝑋) ⊆ ℝ)) → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))))
5952, 53, 55, 32, 58syl22anc 839 . . . . . . . 8 (𝜑 → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))))
60 fourierdlem74.g . . . . . . . . . . 11 𝐺 = (ℝ D 𝐹)
6160eqcomi 2743 . . . . . . . . . 10 (ℝ D 𝐹) = 𝐺
62 ioontr 45463 . . . . . . . . . 10 ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋)
6361, 62reseq12i 5997 . . . . . . . . 9 ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋))
6463a1i 11 . . . . . . . 8 (𝜑 → ((ℝ D 𝐹) ↾ ((int‘(topGen‘ran (,)))‘((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6559, 64eqtrd 2774 . . . . . . 7 (𝜑 → (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6665dmeqd 5918 . . . . . 6 (𝜑 → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
6766ad2antrr 726 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
68 fourierdlem74.gcn . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
6968adantr 480 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ)
70 oveq2 7438 . . . . . . . . . 10 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) = ((𝑉𝑖)(,)𝑋))
7170reseq2d 5999 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) = 𝑋 → (𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
7271, 70feq12d 6724 . . . . . . . 8 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ))
7372adantl 481 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐺 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))):((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))⟶ℝ ↔ (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ))
7469, 73mpbid 232 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ)
75 fdm 6745 . . . . . 6 ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)):((𝑉𝑖)(,)𝑋)⟶ℝ → dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋))
7674, 75syl 17 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = ((𝑉𝑖)(,)𝑋))
7767, 76eqtrd 2774 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → dom (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) = ((𝑉𝑖)(,)𝑋))
78 limcresi 25934 . . . . . . . 8 ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋)
7945resabs1d 6027 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) = (𝐺 ↾ ((𝑉𝑖)(,)𝑋)))
8079oveq1d 7445 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝐺 ↾ (-∞(,)𝑋)) ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
8178, 80sseqtrid 4047 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
82 fourierdlem74.e . . . . . . . 8 (𝜑𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋))
8382adantr 480 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ (-∞(,)𝑋)) lim 𝑋))
8481, 83sseldd 3995 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋))
8559, 64eqtr2d 2775 . . . . . . . 8 (𝜑 → (𝐺 ↾ ((𝑉𝑖)(,)𝑋)) = (ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))))
8685oveq1d 7445 . . . . . . 7 (𝜑 → ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8786adantr 480 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐺 ↾ ((𝑉𝑖)(,)𝑋)) lim 𝑋) = ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8884, 87eleqtrd 2840 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
8988adantr 480 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((ℝ D (𝐹 ↾ ((𝑉𝑖)(,)𝑋))) lim 𝑋))
90 eqid 2734 . . . 4 (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
91 oveq2 7438 . . . . . . 7 (𝑥 = 𝑠 → (𝑋 + 𝑥) = (𝑋 + 𝑠))
9291fveq2d 6910 . . . . . 6 (𝑥 = 𝑠 → ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
9392oveq1d 7445 . . . . 5 (𝑥 = 𝑠 → (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊) = (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
9493cbvmptv 5260 . . . 4 (𝑥 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑥)) − 𝑊)) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
95 id 22 . . . . 5 (𝑥 = 𝑠𝑥 = 𝑠)
9695cbvmptv 5260 . . . 4 (𝑥 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ 𝑥) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ 𝑠)
9718, 19, 29, 34, 49, 50, 77, 89, 90, 94, 96fourierdlem60 46121 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐸 ∈ ((𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim 0))
98 fourierdlem74.a . . . . 5 𝐴 = if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
99 iftrue 4536 . . . . 5 ((𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = 𝐸)
10098, 99eqtrid 2786 . . . 4 ((𝑉‘(𝑖 + 1)) = 𝑋𝐴 = 𝐸)
101100adantl 481 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = 𝐸)
102 fourierdlem74.h . . . . . . 7 𝐻 = (𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
103102reseq1i 5995 . . . . . 6 (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
104103a1i 11 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑠 ∈ (-π[,]π) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))))
105 ioossicc 13469 . . . . . . . 8 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
1063rexri 11316 . . . . . . . . . 10 -π ∈ ℝ*
107106a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → -π ∈ ℝ*)
1082rexri 11316 . . . . . . . . . 10 π ∈ ℝ*
109108a1i 11 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → π ∈ ℝ*)
1103a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → -π ∈ ℝ)
1112a1i 11 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → π ∈ ℝ)
1125adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℝ)
11316, 112resubcld 11688 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
1144recnd 11286 . . . . . . . . . . . . . . . 16 (𝜑 → -π ∈ ℂ)
1155recnd 11286 . . . . . . . . . . . . . . . 16 (𝜑𝑋 ∈ ℂ)
116114, 115pncand 11618 . . . . . . . . . . . . . . 15 (𝜑 → ((-π + 𝑋) − 𝑋) = -π)
117116eqcomd 2740 . . . . . . . . . . . . . 14 (𝜑 → -π = ((-π + 𝑋) − 𝑋))
118117adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → -π = ((-π + 𝑋) − 𝑋))
1196adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ∈ ℝ)
1208adantr 480 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0...𝑀)) → (π + 𝑋) ∈ ℝ)
121 elicc2 13448 . . . . . . . . . . . . . . . . 17 (((-π + 𝑋) ∈ ℝ ∧ (π + 𝑋) ∈ ℝ) → ((𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋))))
122119, 120, 121syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) ∈ ((-π + 𝑋)[,](π + 𝑋)) ↔ ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋))))
12315, 122mpbid 232 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) ∈ ℝ ∧ (-π + 𝑋) ≤ (𝑉𝑖) ∧ (𝑉𝑖) ≤ (π + 𝑋)))
124123simp2d 1142 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (-π + 𝑋) ≤ (𝑉𝑖))
125119, 16, 112, 124lesub1dd 11876 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((-π + 𝑋) − 𝑋) ≤ ((𝑉𝑖) − 𝑋))
126118, 125eqbrtrd 5169 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → -π ≤ ((𝑉𝑖) − 𝑋))
127123simp3d 1143 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑉𝑖) ≤ (π + 𝑋))
12816, 120, 112, 127lesub1dd 11876 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ≤ ((π + 𝑋) − 𝑋))
129111recnd 11286 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → π ∈ ℂ)
130115adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑋 ∈ ℂ)
131129, 130pncand 11618 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → ((π + 𝑋) − 𝑋) = π)
132128, 131breqtrd 5173 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ≤ π)
133110, 111, 113, 126, 132eliccd 45456 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) − 𝑋) ∈ (-π[,]π))
134 fourierdlem74.q . . . . . . . . . . 11 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋))
135133, 134fmptd 7133 . . . . . . . . . 10 (𝜑𝑄:(0...𝑀)⟶(-π[,]π))
136135adantr 480 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(-π[,]π))
137 simpr 484 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
138107, 109, 136, 137fourierdlem8 46070 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
139105, 138sstrid 4006 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ (-π[,]π))
140139resmptd 6059 . . . . . 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 593 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) ∈ ℝ)
144134fvmpt2 7026 . . . . . . . . 9 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ ℝ) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
145142, 143, 144syl2anc 584 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
146145adantr 480 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
147 fveq2 6906 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 → (𝑉𝑖) = (𝑉𝑗))
148147oveq1d 7445 . . . . . . . . . . . . 13 (𝑖 = 𝑗 → ((𝑉𝑖) − 𝑋) = ((𝑉𝑗) − 𝑋))
149148cbvmptv 5260 . . . . . . . . . . . 12 (𝑖 ∈ (0...𝑀) ↦ ((𝑉𝑖) − 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
150134, 149eqtri 2762 . . . . . . . . . . 11 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋))
151150a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((𝑉𝑗) − 𝑋)))
152 fveq2 6906 . . . . . . . . . . . 12 (𝑗 = (𝑖 + 1) → (𝑉𝑗) = (𝑉‘(𝑖 + 1)))
153152oveq1d 7445 . . . . . . . . . . 11 (𝑗 = (𝑖 + 1) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
154153adantl 481 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑉𝑗) − 𝑋) = ((𝑉‘(𝑖 + 1)) − 𝑋))
155 fzofzp1 13799 . . . . . . . . . . 11 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
156155adantl 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
15722simpld 494 . . . . . . . . . . . . . 14 (𝜑𝑉 ∈ (ℝ ↑m (0...𝑀)))
158 elmapi 8887 . . . . . . . . . . . . . 14 (𝑉 ∈ (ℝ ↑m (0...𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
159157, 158syl 17 . . . . . . . . . . . . 13 (𝜑𝑉:(0...𝑀)⟶ℝ)
160159adantr 480 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑉:(0...𝑀)⟶ℝ)
161160, 156ffvelcdmd 7104 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
1625adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℝ)
163161, 162resubcld 11688 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉‘(𝑖 + 1)) − 𝑋) ∈ ℝ)
164151, 154, 156, 163fvmptd 7022 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
165164adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
166 oveq1 7437 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) = 𝑋 → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋𝑋))
167166adantl 481 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) = (𝑋𝑋))
168115ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
169168subidd 11605 . . . . . . . . 9 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋𝑋) = 0)
1701, 169sylanl2 681 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑋𝑋) = 0)
171165, 167, 1703eqtrd 2778 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = 0)
172146, 171oveq12d 7448 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) = (((𝑉𝑖) − 𝑋)(,)0))
173 simplr 769 . . . . . . . . . 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 46076 . . . . . . . . . . . . . 14 (𝜑𝑄 ∈ (𝑂𝑀))
177176adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑄 ∈ (𝑂𝑀))
178 simpr 484 . . . . . . . . . . . . . 14 ((𝜑𝑠 = 0) → 𝑠 = 0)
179 fourierdlem74.x . . . . . . . . . . . . . . . . . 18 (𝜑𝑋 ∈ ran 𝑉)
180 ffn 6736 . . . . . . . . . . . . . . . . . . 19 (𝑉:(0...𝑀)⟶((-π + 𝑋)[,](π + 𝑋)) → 𝑉 Fn (0...𝑀))
181 fvelrnb 6968 . . . . . . . . . . . . . . . . . . 19 (𝑉 Fn (0...𝑀) → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋))
18214, 180, 1813syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑋 ∈ ran 𝑉 ↔ ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋))
183179, 182mpbid 232 . . . . . . . . . . . . . . . . 17 (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋)
184 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑖 ∈ (0...𝑀))
185134fvmpt2 7026 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑀) ∧ ((𝑉𝑖) − 𝑋) ∈ (-π[,]π)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
186184, 133, 185syl2anc 584 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
187186adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑄𝑖) = ((𝑉𝑖) − 𝑋))
188 oveq1 7437 . . . . . . . . . . . . . . . . . . . . 21 ((𝑉𝑖) = 𝑋 → ((𝑉𝑖) − 𝑋) = (𝑋𝑋))
189188adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → ((𝑉𝑖) − 𝑋) = (𝑋𝑋))
190115subidd 11605 . . . . . . . . . . . . . . . . . . . . 21 (𝜑 → (𝑋𝑋) = 0)
191190ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑋𝑋) = 0)
192187, 189, 1913eqtrd 2778 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑖 ∈ (0...𝑀)) ∧ (𝑉𝑖) = 𝑋) → (𝑄𝑖) = 0)
193192ex 412 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑉𝑖) = 𝑋 → (𝑄𝑖) = 0))
194193reximdva 3165 . . . . . . . . . . . . . . . . 17 (𝜑 → (∃𝑖 ∈ (0...𝑀)(𝑉𝑖) = 𝑋 → ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0))
195183, 194mpd 15 . . . . . . . . . . . . . . . 16 (𝜑 → ∃𝑖 ∈ (0...𝑀)(𝑄𝑖) = 0)
196113, 134fmptd 7133 . . . . . . . . . . . . . . . . 17 (𝜑𝑄:(0...𝑀)⟶ℝ)
197 ffn 6736 . . . . . . . . . . . . . . . . 17 (𝑄:(0...𝑀)⟶ℝ → 𝑄 Fn (0...𝑀))
198 fvelrnb 6968 . . . . . . . . . . . . . . . . 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 2838 . . . . . . . . . . . . 13 ((𝜑𝑠 = 0) → 𝑠 ∈ ran 𝑄)
203174, 175, 177, 202fourierdlem12 46074 . . . . . . . . . . . 12 (((𝜑𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
204203an32s 652 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
205204adantlr 715 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∧ 𝑠 = 0) → ¬ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
206173, 205pm2.65da 817 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
207206adantlr 715 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
208207iffalsed 4541 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
209 elioore 13413 . . . . . . . . . . . 12 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℝ)
210209adantl 481 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
211 0red 11261 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
212 elioo3g 13412 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ℝ*) ∧ ((𝑄𝑖) < 𝑠𝑠 < (𝑄‘(𝑖 + 1)))))
213212biimpi 216 . . . . . . . . . . . . . 14 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (((𝑄𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*𝑠 ∈ ℝ*) ∧ ((𝑄𝑖) < 𝑠𝑠 < (𝑄‘(𝑖 + 1)))))
214213simprrd 774 . . . . . . . . . . . . 13 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 < (𝑄‘(𝑖 + 1)))
215214adantl 481 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
216171adantr 480 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) = 0)
217215, 216breqtrd 5173 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
218210, 211, 217ltnsymd 11407 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
219218iffalsed 4541 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
220219oveq2d 7446 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
221220oveq1d 7445 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) = (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
22241ad2antrr 726 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
2235rexrd 11308 . . . . . . . . . . . 12 (𝜑𝑋 ∈ ℝ*)
224223ad3antrrr 730 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ*)
225162ad2antrr 726 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
226225, 210readdcld 11287 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
227115adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑋 ∈ ℂ)
228 iccssre 13465 . . . . . . . . . . . . . . . . . . 19 ((-π ∈ ℝ ∧ π ∈ ℝ) → (-π[,]π) ⊆ ℝ)
2293, 2, 228mp2an 692 . . . . . . . . . . . . . . . . . 18 (-π[,]π) ⊆ ℝ
230229, 51sstri 4004 . . . . . . . . . . . . . . . . 17 (-π[,]π) ⊆ ℂ
231186, 133eqeltrd 2838 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) ∈ (-π[,]π))
2321, 231sylan2 593 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ (-π[,]π))
233230, 232sselid 3992 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
234227, 233addcomd 11460 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄𝑖)) = ((𝑄𝑖) + 𝑋))
235145oveq1d 7445 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑋) = (((𝑉𝑖) − 𝑋) + 𝑋))
23617recnd 11286 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) ∈ ℂ)
237236, 227npcand 11621 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑉𝑖) − 𝑋) + 𝑋) = (𝑉𝑖))
238234, 235, 2373eqtrrd 2779 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
239238adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) = (𝑋 + (𝑄𝑖)))
240145, 143eqeltrd 2838 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
241240adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
242209adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
2435ad2antrr 726 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
244213simprld 772 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑄𝑖) < 𝑠)
245244adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
246241, 242, 243, 245ltadd2dd 11417 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄𝑖)) < (𝑋 + 𝑠))
247239, 246eqbrtrd 5169 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
248247adantlr 715 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) < (𝑋 + 𝑠))
249 ltaddneg 11474 . . . . . . . . . . . . 13 ((𝑠 ∈ ℝ ∧ 𝑋 ∈ ℝ) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
250210, 225, 249syl2anc 584 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
251217, 250mpbid 232 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < 𝑋)
252222, 224, 226, 248, 251eliood 45450 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋))
253 fvres 6925 . . . . . . . . . . 11 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋) → ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) = (𝐹‘(𝑋 + 𝑠)))
254253eqcomd 2740 . . . . . . . . . 10 ((𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)𝑋) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
255252, 254syl 17 . . . . . . . . 9 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) = ((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)))
256255oveq1d 7445 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − 𝑊) = (((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊))
257256oveq1d 7445 . . . . . . 7 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − 𝑊) / 𝑠) = ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
258208, 221, 2573eqtrd 2778 . . . . . 6 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠))
259172, 258mpteq12dva 5236 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
260104, 141, 2593eqtrd 2778 . . . 4 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)))
261260, 171oveq12d 7448 . . 3 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ (((𝑉𝑖) − 𝑋)(,)0) ↦ ((((𝐹 ↾ ((𝑉𝑖)(,)𝑋))‘(𝑋 + 𝑠)) − 𝑊) / 𝑠)) lim 0))
26297, 101, 2613eltr4d 2853 . 2 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
263 eqid 2734 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)))
264 eqid 2734 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠)
265 eqid 2734 . . . . 5 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
26630adantr 480 . . . . . . . . . 10 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℝ)
2675adantr 480 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑋 ∈ ℝ)
268209adantl 481 . . . . . . . . . . 11 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
269267, 268readdcld 11287 . . . . . . . . . 10 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
270266, 269ffvelcdmd 7104 . . . . . . . . 9 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℝ)
271270recnd 11286 . . . . . . . 8 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
272271adantlr 715 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
2732723adantl3 1167 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
274 fourierdlem74.y . . . . . . . . . 10 (𝜑𝑌 ∈ ℝ)
275274recnd 11286 . . . . . . . . 9 (𝜑𝑌 ∈ ℂ)
276 limccl 25924 . . . . . . . . . 10 ((𝐹 ↾ (-∞(,)𝑋)) lim 𝑋) ⊆ ℂ
277276, 36sselid 3992 . . . . . . . . 9 (𝜑𝑊 ∈ ℂ)
278275, 277ifcld 4576 . . . . . . . 8 (𝜑 → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
279278adantr 480 . . . . . . 7 ((𝜑𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
2802793ad2antl1 1184 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
281273, 280subcld 11617 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
282209recnd 11286 . . . . . . 7 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑠 ∈ ℂ)
283282adantl 481 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
284 velsn 4646 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
285206, 284sylnibr 329 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
2862853adantl3 1167 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 ∈ {0})
287283, 286eldifd 3973 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (ℂ ∖ {0}))
288 eqid 2734 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠)))
289 eqid 2734 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊)
290 eqid 2734 . . . . . . . . . 10 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
291277ad2antrr 726 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑊 ∈ ℂ)
29230adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℝ)
293 ioossre 13444 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
294293a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
29541adantr 480 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉𝑖) ∈ ℝ*)
296161rexrd 11308 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
297296adantr 480 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
298269adantlr 715 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ℝ)
299196adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
300299, 156ffvelcdmd 7104 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
301300adantr 480 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
302214adantl 481 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < (𝑄‘(𝑖 + 1)))
303242, 301, 243, 302ltadd2dd 11417 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑋 + (𝑄‘(𝑖 + 1))))
304164oveq2d 7446 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)))
305161recnd 11286 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
306227, 305pncan3d 11620 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + ((𝑉‘(𝑖 + 1)) − 𝑋)) = (𝑉‘(𝑖 + 1)))
307304, 306eqtrd 2774 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
308307adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + (𝑄‘(𝑖 + 1))) = (𝑉‘(𝑖 + 1)))
309303, 308breqtrd 5173 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) < (𝑉‘(𝑖 + 1)))
310295, 297, 298, 247, 309eliood 45450 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑋 + 𝑠) ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
311 ioossre 13444 . . . . . . . . . . . 12 ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ
312311a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))) ⊆ ℝ)
313242, 302ltned 11394 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ (𝑄‘(𝑖 + 1)))
314 fourierdlem74.r . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))))
315307eqcomd 2740 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑉‘(𝑖 + 1)) = (𝑋 + (𝑄‘(𝑖 + 1))))
316315oveq2d 7446 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑉‘(𝑖 + 1))) = ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
317314, 316eleqtrd 2840 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1)))) lim (𝑋 + (𝑄‘(𝑖 + 1)))))
318300recnd 11286 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
319292, 162, 294, 288, 310, 312, 313, 317, 318fourierdlem53 46114 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
320 ioosscn 13445 . . . . . . . . . . . 12 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
321320a1i 11 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
322277adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ℂ)
323289, 321, 322, 318constlimc 45579 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑊 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑊) lim (𝑄‘(𝑖 + 1))))
324288, 289, 290, 272, 291, 319, 323sublimc 45607 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑅𝑊) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
325324adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅𝑊) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
326 iftrue 4536 . . . . . . . . . 10 ((𝑉‘(𝑖 + 1)) < 𝑋 → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑊)
327326oveq2d 7446 . . . . . . . . 9 ((𝑉‘(𝑖 + 1)) < 𝑋 → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅𝑊))
328327adantl 481 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) = (𝑅𝑊))
329209adantl 481 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
330 0red 11261 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
331300ad2antrr 726 . . . . . . . . . . . . . 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 726 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
336 simpr 484 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) < 𝑋)
337334, 335, 336ltled 11406 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ≤ 𝑋)
338334, 335suble0d 11851 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0 ↔ (𝑉‘(𝑖 + 1)) ≤ 𝑋))
339337, 338mpbird 257 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≤ 0)
340333, 339eqbrtrd 5169 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑄‘(𝑖 + 1)) ≤ 0)
341340adantr 480 . . . . . . . . . . . . . 14 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ≤ 0)
342329, 331, 330, 332, 341ltletrd 11418 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 < 0)
343329, 330, 342ltnsymd 11407 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 0 < 𝑠)
344343iffalsed 4541 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑊)
345344oveq2d 7446 . . . . . . . . . 10 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) = ((𝐹‘(𝑋 + 𝑠)) − 𝑊))
346345mpteq2dva 5247 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)))
347346oveq1d 7445 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − 𝑊)) lim (𝑄‘(𝑖 + 1))))
348325, 328, 3473eltr4d 2853 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
3493483adantl3 1167 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
350 simpl1 1190 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝜑)
351 simpl2 1191 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑖 ∈ (0..^𝑀))
3525ad2antrr 726 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
3533523adantl3 1167 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ∈ ℝ)
354161adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
3553543adantl3 1167 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
356 neqne 2945 . . . . . . . . . . 11 (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
357356necomd 2993 . . . . . . . . . 10 (¬ (𝑉‘(𝑖 + 1)) = 𝑋𝑋 ≠ (𝑉‘(𝑖 + 1)))
358357adantr 480 . . . . . . . . 9 ((¬ (𝑉‘(𝑖 + 1)) = 𝑋 ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
3593583ad2antl3 1186 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 ≠ (𝑉‘(𝑖 + 1)))
360 simpr 484 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
361353, 355, 359, 360lttri5d 45249 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → 𝑋 < (𝑉‘(𝑖 + 1)))
362 eqid 2734 . . . . . . . 8 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊))
363272adantlr 715 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑋 + 𝑠)) ∈ ℂ)
364278ad3antrrr 730 . . . . . . . 8 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
365319adantr 480 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑅 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘(𝑋 + 𝑠))) lim (𝑄‘(𝑖 + 1))))
366 eqid 2734 . . . . . . . . . . 11 (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌)
367275adantr 480 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ℂ)
368366, 321, 367, 318constlimc 45579 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑌 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
369368adantr 480 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑌 ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
3705ad2antrr 726 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ∈ ℝ)
371161adantr 480 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉‘(𝑖 + 1)) ∈ ℝ)
372 simpr 484 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 < (𝑉‘(𝑖 + 1)))
373370, 371, 372ltnsymd 11407 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ¬ (𝑉‘(𝑖 + 1)) < 𝑋)
374373iffalsed 4541 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) = 𝑌)
375 0red 11261 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℝ)
376240ad2antrr 726 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) ∈ ℝ)
377209adantl 481 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℝ)
378190eqcomd 2740 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 = (𝑋𝑋))
379378ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 = (𝑋𝑋))
38017adantr 480 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑉𝑖) ∈ ℝ)
38141ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) ∈ ℝ*)
382296ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉‘(𝑖 + 1)) ∈ ℝ*)
383162ad2antrr 726 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ℝ)
384 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ¬ 𝑋 ≤ (𝑉𝑖))
38517adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) ∈ ℝ)
3865ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ℝ)
387385, 386ltnled 11405 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ((𝑉𝑖) < 𝑋 ↔ ¬ 𝑋 ≤ (𝑉𝑖)))
388384, 387mpbird 257 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) < 𝑋)
389388adantlr 715 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → (𝑉𝑖) < 𝑋)
390 simplr 769 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 < (𝑉‘(𝑖 + 1)))
391381, 382, 383, 389, 390eliood 45450 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
39211, 12, 13, 179fourierdlem12 46074 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → ¬ 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
393392ad2antrr 726 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ ¬ 𝑋 ≤ (𝑉𝑖)) → ¬ 𝑋 ∈ ((𝑉𝑖)(,)(𝑉‘(𝑖 + 1))))
394391, 393condan 818 . . . . . . . . . . . . . . . . 17 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 𝑋 ≤ (𝑉𝑖))
395370, 380, 370, 394lesub1dd 11876 . . . . . . . . . . . . . . . 16 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑋𝑋) ≤ ((𝑉𝑖) − 𝑋))
396379, 395eqbrtrd 5169 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ ((𝑉𝑖) − 𝑋))
397145eqcomd 2740 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑉𝑖) − 𝑋) = (𝑄𝑖))
398397adantr 480 . . . . . . . . . . . . . . 15 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑉𝑖) − 𝑋) = (𝑄𝑖))
399396, 398breqtrd 5173 . . . . . . . . . . . . . 14 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → 0 ≤ (𝑄𝑖))
400399adantr 480 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ≤ (𝑄𝑖))
401244adantl 481 . . . . . . . . . . . . 13 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄𝑖) < 𝑠)
402375, 376, 377, 400, 401lelttrd 11416 . . . . . . . . . . . 12 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 < 𝑠)
403402iftrued 4538 . . . . . . . . . . 11 ((((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) = 𝑌)
404403mpteq2dva 5247 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌))
405404oveq1d 7445 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑌) lim (𝑄‘(𝑖 + 1))))
406369, 374, 4053eltr4d 2853 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ if(0 < 𝑠, 𝑌, 𝑊)) lim (𝑄‘(𝑖 + 1))))
407288, 362, 263, 363, 364, 365, 406sublimc 45607 . . . . . . 7 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (𝑉‘(𝑖 + 1))) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
408350, 351, 361, 407syl21anc 838 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ ¬ (𝑉‘(𝑖 + 1)) < 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
409349, 408pm2.61dan 813 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊))) lim (𝑄‘(𝑖 + 1))))
410321, 264, 318idlimc 45581 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim (𝑄‘(𝑖 + 1))))
4114103adant3 1131 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ 𝑠) lim (𝑄‘(𝑖 + 1))))
4121643adant3 1131 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) = ((𝑉‘(𝑖 + 1)) − 𝑋))
4133053adant3 1131 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ∈ ℂ)
4142273adant3 1131 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝑋 ∈ ℂ)
4153563ad2ant3 1134 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑉‘(𝑖 + 1)) ≠ 𝑋)
416413, 414, 415subne0d 11626 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑉‘(𝑖 + 1)) − 𝑋) ≠ 0)
417412, 416eqnetrd 3005 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝑄‘(𝑖 + 1)) ≠ 0)
4182063adantl3 1167 . . . . . 6 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ¬ 𝑠 = 0)
419418neqned 2944 . . . . 5 (((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
420263, 264, 265, 281, 287, 409, 411, 417, 419divlimc 45611 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))) ∈ ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim (𝑄‘(𝑖 + 1))))
421 iffalse 4539 . . . . . 6 (¬ (𝑉‘(𝑖 + 1)) = 𝑋 → if((𝑉‘(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1)))) = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
42298, 421eqtrid 2786 . . . . 5 (¬ (𝑉‘(𝑖 + 1)) = 𝑋𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
4234223ad2ant3 1134 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 = ((𝑅 − if((𝑉‘(𝑖 + 1)) < 𝑋, 𝑊, 𝑌)) / (𝑄‘(𝑖 + 1))))
424 ioossre 13444 . . . . . . . . . . . . 13 (-∞(,)𝑋) ⊆ ℝ
425424a1i 11 . . . . . . . . . . . 12 (𝜑 → (-∞(,)𝑋) ⊆ ℝ)
42630, 425fssresd 6775 . . . . . . . . . . 11 (𝜑 → (𝐹 ↾ (-∞(,)𝑋)):(-∞(,)𝑋)⟶ℝ)
427424, 52sstrid 4006 . . . . . . . . . . 11 (𝜑 → (-∞(,)𝑋) ⊆ ℂ)
42839a1i 11 . . . . . . . . . . . 12 (𝜑 → -∞ ∈ ℝ*)
4295mnfltd 13163 . . . . . . . . . . . 12 (𝜑 → -∞ < 𝑋)
43056, 428, 5, 429lptioo2cn 45600 . . . . . . . . . . 11 (𝜑𝑋 ∈ ((limPt‘(TopOpen‘ℂfld))‘(-∞(,)𝑋)))
431426, 427, 430, 36limcrecl 45584 . . . . . . . . . 10 (𝜑𝑊 ∈ ℝ)
43230, 5, 274, 431, 102fourierdlem9 46071 . . . . . . . . 9 (𝜑𝐻:(-π[,]π)⟶ℝ)
433432adantr 480 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐻:(-π[,]π)⟶ℝ)
434433, 139feqresmpt 6977 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)))
435139sselda 3994 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ (-π[,]π))
436 0cnd 11251 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 0 ∈ ℂ)
437278ad2antrr 726 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(0 < 𝑠, 𝑌, 𝑊) ∈ ℂ)
438272, 437subcld 11617 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) ∈ ℂ)
439282adantl 481 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ∈ ℂ)
440206neqned 2944 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑠 ≠ 0)
441438, 439, 440divcld 12040 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠) ∈ ℂ)
442436, 441ifcld 4576 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ)
443102fvmpt2 7026 . . . . . . . . . 10 ((𝑠 ∈ (-π[,]π) ∧ if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) ∈ ℂ) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
444435, 442, 443syl2anc 584 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
445206iffalsed 4541 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → if(𝑠 = 0, 0, (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
446444, 445eqtrd 2774 . . . . . . . 8 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐻𝑠) = (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠))
447446mpteq2dva 5247 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐻𝑠)) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
448434, 447eqtrd 2774 . . . . . 6 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
4494483adant3 1131 . . . . 5 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → (𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)))
450449oveq1d 7445 . . . 4 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))) = ((𝑠 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (((𝐹‘(𝑋 + 𝑠)) − if(0 < 𝑠, 𝑌, 𝑊)) / 𝑠)) lim (𝑄‘(𝑖 + 1))))
451420, 423, 4503eltr4d 2853 . . 3 ((𝜑𝑖 ∈ (0..^𝑀) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
4524513expa 1117 . 2 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ ¬ (𝑉‘(𝑖 + 1)) = 𝑋) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
453262, 452pm2.61dan 813 1 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ((𝐻 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wral 3058  wrex 3067  {crab 3432  wss 3962  ifcif 4530  {csn 4630   class class class wbr 5147  cmpt 5230  dom cdm 5688  ran crn 5689  cres 5690   Fn wfn 6557  wf 6558  cfv 6562  (class class class)co 7430  m cmap 8864  cc 11150  cr 11151  0cc0 11152  1c1 11153   + caddc 11155  -∞cmnf 11290  *cxr 11291   < clt 11292  cle 11293  cmin 11489  -cneg 11490   / cdiv 11917  cn 12263  (,)cioo 13383  [,]cicc 13386  ...cfz 13543  ..^cfzo 13690  πcpi 16098  TopOpenctopn 17467  topGenctg 17483  fldccnfld 21381  intcnt 23040   lim climc 25911   D cdv 25912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-inf2 9678  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-int 4951  df-iun 4997  df-iin 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-se 5641  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-isom 6571  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-of 7696  df-om 7887  df-1st 8012  df-2nd 8013  df-supp 8184  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-2o 8505  df-er 8743  df-map 8866  df-pm 8867  df-ixp 8936  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-fsupp 9399  df-fi 9448  df-sup 9479  df-inf 9480  df-oi 9547  df-card 9976  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-xneg 13151  df-xadd 13152  df-xmul 13153  df-ioo 13387  df-ioc 13388  df-ico 13389  df-icc 13390  df-fz 13544  df-fzo 13691  df-fl 13828  df-seq 14039  df-exp 14099  df-fac 14309  df-bc 14338  df-hash 14366  df-shft 15102  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-limsup 15503  df-clim 15520  df-rlim 15521  df-sum 15719  df-ef 16099  df-sin 16101  df-cos 16102  df-pi 16104  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17468  df-topn 17469  df-0g 17487  df-gsum 17488  df-topgen 17489  df-pt 17490  df-prds 17493  df-xrs 17548  df-qtop 17553  df-imas 17554  df-xps 17556  df-mre 17630  df-mrc 17631  df-acs 17633  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-submnd 18809  df-mulg 19098  df-cntz 19347  df-cmn 19814  df-psmet 21373  df-xmet 21374  df-met 21375  df-bl 21376  df-mopn 21377  df-fbas 21378  df-fg 21379  df-cnfld 21382  df-top 22915  df-topon 22932  df-topsp 22954  df-bases 22968  df-cld 23042  df-ntr 23043  df-cls 23044  df-nei 23121  df-lp 23159  df-perf 23160  df-cn 23250  df-cnp 23251  df-haus 23338  df-cmp 23410  df-tx 23585  df-hmeo 23778  df-fil 23869  df-fm 23961  df-flim 23962  df-flf 23963  df-xms 24345  df-ms 24346  df-tms 24347  df-cncf 24917  df-limc 25915  df-dv 25916
This theorem is referenced by:  fourierdlem88  46149  fourierdlem103  46164  fourierdlem104  46165
  Copyright terms: Public domain W3C validator