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 45491
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 13672 . . . . . 6 (𝑖 ∈ (0..^𝑀) β†’ 𝑖 ∈ (0...𝑀))
2 pire 26380 . . . . . . . . . . . 12 Ο€ ∈ ℝ
32renegcli 11543 . . . . . . . . . . 11 -Ο€ ∈ ℝ
43a1i 11 . . . . . . . . . 10 (πœ‘ β†’ -Ο€ ∈ ℝ)
5 fourierdlem74.xre . . . . . . . . . 10 (πœ‘ β†’ 𝑋 ∈ ℝ)
64, 5readdcld 11265 . . . . . . . . 9 (πœ‘ β†’ (-Ο€ + 𝑋) ∈ ℝ)
72a1i 11 . . . . . . . . . 10 (πœ‘ β†’ Ο€ ∈ ℝ)
87, 5readdcld 11265 . . . . . . . . 9 (πœ‘ β†’ (Ο€ + 𝑋) ∈ ℝ)
96, 8iccssred 13435 . . . . . . . 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 45433 . . . . . . . 8 (πœ‘ β†’ 𝑉:(0...𝑀)⟢((-Ο€ + 𝑋)[,](Ο€ + 𝑋)))
1514ffvelcdmda 7088 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ (π‘‰β€˜π‘–) ∈ ((-Ο€ + 𝑋)[,](Ο€ + 𝑋)))
1610, 15sseldd 3979 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ (π‘‰β€˜π‘–) ∈ ℝ)
171, 16sylan2 592 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜π‘–) ∈ ℝ)
1817adantr 480 . . . 4 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘‰β€˜π‘–) ∈ ℝ)
195ad2antrr 725 . . . 4 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝑋 ∈ ℝ)
2011fourierdlem2 45420 . . . . . . . . . 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 773 . . . . . . 7 (πœ‘ β†’ βˆ€π‘– ∈ (0..^𝑀)(π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1)))
2423r19.21bi 3243 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1)))
2524adantr 480 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘‰β€˜π‘–) < (π‘‰β€˜(𝑖 + 1)))
26 eqcom 2734 . . . . . . 7 ((π‘‰β€˜(𝑖 + 1)) = 𝑋 ↔ 𝑋 = (π‘‰β€˜(𝑖 + 1)))
2726biimpi 215 . . . . . 6 ((π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ 𝑋 = (π‘‰β€˜(𝑖 + 1)))
2827adantl 481 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝑋 = (π‘‰β€˜(𝑖 + 1)))
2925, 28breqtrrd 5170 . . . 4 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘‰β€˜π‘–) < 𝑋)
30 fourierdlem74.f . . . . . 6 (πœ‘ β†’ 𝐹:β„βŸΆβ„)
31 ioossre 13409 . . . . . . 7 ((π‘‰β€˜π‘–)(,)𝑋) βŠ† ℝ
3231a1i 11 . . . . . 6 (πœ‘ β†’ ((π‘‰β€˜π‘–)(,)𝑋) βŠ† ℝ)
3330, 32fssresd 6758 . . . . 5 (πœ‘ β†’ (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)):((π‘‰β€˜π‘–)(,)𝑋)βŸΆβ„)
3433ad2antrr 725 . . . 4 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)):((π‘‰β€˜π‘–)(,)𝑋)βŸΆβ„)
35 limcresi 25801 . . . . . . . 8 ((𝐹 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋) βŠ† (((𝐹 β†Ύ (-∞(,)𝑋)) β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋)
36 fourierdlem74.w . . . . . . . 8 (πœ‘ β†’ π‘Š ∈ ((𝐹 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
3735, 36sselid 3976 . . . . . . 7 (πœ‘ β†’ π‘Š ∈ (((𝐹 β†Ύ (-∞(,)𝑋)) β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋))
3837adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ π‘Š ∈ (((𝐹 β†Ύ (-∞(,)𝑋)) β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋))
39 mnfxr 11293 . . . . . . . . . 10 -∞ ∈ ℝ*
4039a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ -∞ ∈ ℝ*)
4117rexrd 11286 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜π‘–) ∈ ℝ*)
4217mnfltd 13128 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ -∞ < (π‘‰β€˜π‘–))
4340, 41, 42xrltled 13153 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ -∞ ≀ (π‘‰β€˜π‘–))
44 iooss1 13383 . . . . . . . . 9 ((-∞ ∈ ℝ* ∧ -∞ ≀ (π‘‰β€˜π‘–)) β†’ ((π‘‰β€˜π‘–)(,)𝑋) βŠ† (-∞(,)𝑋))
4540, 43, 44syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘‰β€˜π‘–)(,)𝑋) βŠ† (-∞(,)𝑋))
4645resabs1d 6010 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐹 β†Ύ (-∞(,)𝑋)) β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) = (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)))
4746oveq1d 7429 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (((𝐹 β†Ύ (-∞(,)𝑋)) β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋) = ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋))
4838, 47eleqtrd 2830 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ π‘Š ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋))
4948adantr 480 . . . 4 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ π‘Š ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋))
50 eqid 2727 . . . 4 (ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) = (ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)))
51 ax-resscn 11187 . . . . . . . . . 10 ℝ βŠ† β„‚
5251a1i 11 . . . . . . . . 9 (πœ‘ β†’ ℝ βŠ† β„‚)
5330, 52fssd 6734 . . . . . . . . 9 (πœ‘ β†’ 𝐹:β„βŸΆβ„‚)
54 ssid 4000 . . . . . . . . . 10 ℝ βŠ† ℝ
5554a1i 11 . . . . . . . . 9 (πœ‘ β†’ ℝ βŠ† ℝ)
56 eqid 2727 . . . . . . . . . 10 (TopOpenβ€˜β„‚fld) = (TopOpenβ€˜β„‚fld)
5756tgioo2 24706 . . . . . . . . . 10 (topGenβ€˜ran (,)) = ((TopOpenβ€˜β„‚fld) β†Ύt ℝ)
5856, 57dvres 25827 . . . . . . . . 9 (((ℝ βŠ† β„‚ ∧ 𝐹:β„βŸΆβ„‚) ∧ (ℝ βŠ† ℝ ∧ ((π‘‰β€˜π‘–)(,)𝑋) βŠ† ℝ)) β†’ (ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) = ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜((π‘‰β€˜π‘–)(,)𝑋))))
5952, 53, 55, 32, 58syl22anc 838 . . . . . . . 8 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) = ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜((π‘‰β€˜π‘–)(,)𝑋))))
60 fourierdlem74.g . . . . . . . . . . 11 𝐺 = (ℝ D 𝐹)
6160eqcomi 2736 . . . . . . . . . 10 (ℝ D 𝐹) = 𝐺
62 ioontr 44819 . . . . . . . . . 10 ((intβ€˜(topGenβ€˜ran (,)))β€˜((π‘‰β€˜π‘–)(,)𝑋)) = ((π‘‰β€˜π‘–)(,)𝑋)
6361, 62reseq12i 5977 . . . . . . . . 9 ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜((π‘‰β€˜π‘–)(,)𝑋))) = (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))
6463a1i 11 . . . . . . . 8 (πœ‘ β†’ ((ℝ D 𝐹) β†Ύ ((intβ€˜(topGenβ€˜ran (,)))β€˜((π‘‰β€˜π‘–)(,)𝑋))) = (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)))
6559, 64eqtrd 2767 . . . . . . 7 (πœ‘ β†’ (ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) = (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)))
6665dmeqd 5902 . . . . . 6 (πœ‘ β†’ dom (ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) = dom (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)))
6766ad2antrr 725 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ dom (ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) = dom (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)))
68 fourierdlem74.gcn . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„)
6968adantr 480 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„)
70 oveq2 7422 . . . . . . . . . 10 ((π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))) = ((π‘‰β€˜π‘–)(,)𝑋))
7170reseq2d 5979 . . . . . . . . 9 ((π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) = (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)))
7271, 70feq12d 6704 . . . . . . . 8 ((π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ ((𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„ ↔ (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)):((π‘‰β€˜π‘–)(,)𝑋)βŸΆβ„))
7372adantl 481 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ ((𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))):((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))βŸΆβ„ ↔ (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)):((π‘‰β€˜π‘–)(,)𝑋)βŸΆβ„))
7469, 73mpbid 231 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)):((π‘‰β€˜π‘–)(,)𝑋)βŸΆβ„)
75 fdm 6725 . . . . . 6 ((𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)):((π‘‰β€˜π‘–)(,)𝑋)βŸΆβ„ β†’ dom (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) = ((π‘‰β€˜π‘–)(,)𝑋))
7674, 75syl 17 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ dom (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) = ((π‘‰β€˜π‘–)(,)𝑋))
7767, 76eqtrd 2767 . . . 4 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ dom (ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) = ((π‘‰β€˜π‘–)(,)𝑋))
78 limcresi 25801 . . . . . . . 8 ((𝐺 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋) βŠ† (((𝐺 β†Ύ (-∞(,)𝑋)) β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋)
7945resabs1d 6010 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐺 β†Ύ (-∞(,)𝑋)) β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) = (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)))
8079oveq1d 7429 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (((𝐺 β†Ύ (-∞(,)𝑋)) β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋) = ((𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋))
8178, 80sseqtrid 4030 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐺 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋) βŠ† ((𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋))
82 fourierdlem74.e . . . . . . . 8 (πœ‘ β†’ 𝐸 ∈ ((𝐺 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
8382adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐸 ∈ ((𝐺 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋))
8481, 83sseldd 3979 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐸 ∈ ((𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋))
8559, 64eqtr2d 2768 . . . . . . . 8 (πœ‘ β†’ (𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) = (ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))))
8685oveq1d 7429 . . . . . . 7 (πœ‘ β†’ ((𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋) = ((ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) limβ„‚ 𝑋))
8786adantr 480 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐺 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋)) limβ„‚ 𝑋) = ((ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) limβ„‚ 𝑋))
8884, 87eleqtrd 2830 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐸 ∈ ((ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) limβ„‚ 𝑋))
8988adantr 480 . . . 4 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝐸 ∈ ((ℝ D (𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))) limβ„‚ 𝑋))
90 eqid 2727 . . . 4 (𝑠 ∈ (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0) ↦ ((((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š) / 𝑠)) = (𝑠 ∈ (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0) ↦ ((((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š) / 𝑠))
91 oveq2 7422 . . . . . . 7 (π‘₯ = 𝑠 β†’ (𝑋 + π‘₯) = (𝑋 + 𝑠))
9291fveq2d 6895 . . . . . 6 (π‘₯ = 𝑠 β†’ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + π‘₯)) = ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)))
9392oveq1d 7429 . . . . 5 (π‘₯ = 𝑠 β†’ (((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + π‘₯)) βˆ’ π‘Š) = (((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š))
9493cbvmptv 5255 . . . 4 (π‘₯ ∈ (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0) ↦ (((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + π‘₯)) βˆ’ π‘Š)) = (𝑠 ∈ (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0) ↦ (((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š))
95 id 22 . . . . 5 (π‘₯ = 𝑠 β†’ π‘₯ = 𝑠)
9695cbvmptv 5255 . . . 4 (π‘₯ ∈ (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0) ↦ π‘₯) = (𝑠 ∈ (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0) ↦ 𝑠)
9718, 19, 29, 34, 49, 50, 77, 89, 90, 94, 96fourierdlem60 45477 . . 3 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝐸 ∈ ((𝑠 ∈ (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0) ↦ ((((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š) / 𝑠)) limβ„‚ 0))
98 fourierdlem74.a . . . . 5 𝐴 = if((π‘‰β€˜(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜(𝑖 + 1))))
99 iftrue 4530 . . . . 5 ((π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ if((π‘‰β€˜(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜(𝑖 + 1)))) = 𝐸)
10098, 99eqtrid 2779 . . . 4 ((π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ 𝐴 = 𝐸)
101100adantl 481 . . 3 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝐴 = 𝐸)
102 fourierdlem74.h . . . . . . 7 𝐻 = (𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
103102reseq1i 5975 . . . . . 6 (𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = ((𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠))) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))))
104103a1i 11 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = ((𝑠 ∈ (-Ο€[,]Ο€) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠))) β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))))
105 ioossicc 13434 . . . . . . . 8 ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† ((π‘„β€˜π‘–)[,](π‘„β€˜(𝑖 + 1)))
1063rexri 11294 . . . . . . . . . 10 -Ο€ ∈ ℝ*
107106a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ -Ο€ ∈ ℝ*)
1082rexri 11294 . . . . . . . . . 10 Ο€ ∈ ℝ*
109108a1i 11 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ Ο€ ∈ ℝ*)
1103a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ -Ο€ ∈ ℝ)
1112a1i 11 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ Ο€ ∈ ℝ)
1125adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ 𝑋 ∈ ℝ)
11316, 112resubcld 11664 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) ∈ ℝ)
1144recnd 11264 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ -Ο€ ∈ β„‚)
1155recnd 11264 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑋 ∈ β„‚)
116114, 115pncand 11594 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((-Ο€ + 𝑋) βˆ’ 𝑋) = -Ο€)
117116eqcomd 2733 . . . . . . . . . . . . . 14 (πœ‘ β†’ -Ο€ = ((-Ο€ + 𝑋) βˆ’ 𝑋))
118117adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ -Ο€ = ((-Ο€ + 𝑋) βˆ’ 𝑋))
1196adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ (-Ο€ + 𝑋) ∈ ℝ)
1208adantr 480 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ (Ο€ + 𝑋) ∈ ℝ)
121 elicc2 13413 . . . . . . . . . . . . . . . . 17 (((-Ο€ + 𝑋) ∈ ℝ ∧ (Ο€ + 𝑋) ∈ ℝ) β†’ ((π‘‰β€˜π‘–) ∈ ((-Ο€ + 𝑋)[,](Ο€ + 𝑋)) ↔ ((π‘‰β€˜π‘–) ∈ ℝ ∧ (-Ο€ + 𝑋) ≀ (π‘‰β€˜π‘–) ∧ (π‘‰β€˜π‘–) ≀ (Ο€ + 𝑋))))
122119, 120, 121syl2anc 583 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ ((π‘‰β€˜π‘–) ∈ ((-Ο€ + 𝑋)[,](Ο€ + 𝑋)) ↔ ((π‘‰β€˜π‘–) ∈ ℝ ∧ (-Ο€ + 𝑋) ≀ (π‘‰β€˜π‘–) ∧ (π‘‰β€˜π‘–) ≀ (Ο€ + 𝑋))))
12315, 122mpbid 231 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ ((π‘‰β€˜π‘–) ∈ ℝ ∧ (-Ο€ + 𝑋) ≀ (π‘‰β€˜π‘–) ∧ (π‘‰β€˜π‘–) ≀ (Ο€ + 𝑋)))
124123simp2d 1141 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ (-Ο€ + 𝑋) ≀ (π‘‰β€˜π‘–))
125119, 16, 112, 124lesub1dd 11852 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ ((-Ο€ + 𝑋) βˆ’ 𝑋) ≀ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
126118, 125eqbrtrd 5164 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ -Ο€ ≀ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
127123simp3d 1142 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ (π‘‰β€˜π‘–) ≀ (Ο€ + 𝑋))
12816, 120, 112, 127lesub1dd 11852 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) ≀ ((Ο€ + 𝑋) βˆ’ 𝑋))
129111recnd 11264 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ Ο€ ∈ β„‚)
130115adantr 480 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ 𝑋 ∈ β„‚)
131129, 130pncand 11594 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ ((Ο€ + 𝑋) βˆ’ 𝑋) = Ο€)
132128, 131breqtrd 5168 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) ≀ Ο€)
133110, 111, 113, 126, 132eliccd 44812 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) ∈ (-Ο€[,]Ο€))
134 fourierdlem74.q . . . . . . . . . . 11 𝑄 = (𝑖 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
135133, 134fmptd 7118 . . . . . . . . . 10 (πœ‘ β†’ 𝑄:(0...𝑀)⟢(-Ο€[,]Ο€))
136135adantr 480 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑄:(0...𝑀)⟢(-Ο€[,]Ο€))
137 simpr 484 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑖 ∈ (0..^𝑀))
138107, 109, 136, 137fourierdlem8 45426 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘„β€˜π‘–)[,](π‘„β€˜(𝑖 + 1))) βŠ† (-Ο€[,]Ο€))
139105, 138sstrid 3989 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† (-Ο€[,]Ο€))
140139resmptd 6038 . . . . . 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 7010 . . . . . . . . 9 ((𝑖 ∈ (0...𝑀) ∧ ((π‘‰β€˜π‘–) βˆ’ 𝑋) ∈ ℝ) β†’ (π‘„β€˜π‘–) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
145142, 143, 144syl2anc 583 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜π‘–) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
146145adantr 480 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘„β€˜π‘–) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
147 fveq2 6891 . . . . . . . . . . . . . 14 (𝑖 = 𝑗 β†’ (π‘‰β€˜π‘–) = (π‘‰β€˜π‘—))
148147oveq1d 7429 . . . . . . . . . . . . 13 (𝑖 = 𝑗 β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) = ((π‘‰β€˜π‘—) βˆ’ 𝑋))
149148cbvmptv 5255 . . . . . . . . . . . 12 (𝑖 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘–) βˆ’ 𝑋)) = (𝑗 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘—) βˆ’ 𝑋))
150134, 149eqtri 2755 . . . . . . . . . . 11 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘—) βˆ’ 𝑋))
151150a1i 11 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑄 = (𝑗 ∈ (0...𝑀) ↦ ((π‘‰β€˜π‘—) βˆ’ 𝑋)))
152 fveq2 6891 . . . . . . . . . . . 12 (𝑗 = (𝑖 + 1) β†’ (π‘‰β€˜π‘—) = (π‘‰β€˜(𝑖 + 1)))
153152oveq1d 7429 . . . . . . . . . . 11 (𝑗 = (𝑖 + 1) β†’ ((π‘‰β€˜π‘—) βˆ’ 𝑋) = ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋))
154153adantl 481 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) β†’ ((π‘‰β€˜π‘—) βˆ’ 𝑋) = ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋))
155 fzofzp1 13753 . . . . . . . . . . 11 (𝑖 ∈ (0..^𝑀) β†’ (𝑖 + 1) ∈ (0...𝑀))
156155adantl 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑖 + 1) ∈ (0...𝑀))
15722simpld 494 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑉 ∈ (ℝ ↑m (0...𝑀)))
158 elmapi 8859 . . . . . . . . . . . . . 14 (𝑉 ∈ (ℝ ↑m (0...𝑀)) β†’ 𝑉:(0...𝑀)βŸΆβ„)
159157, 158syl 17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑉:(0...𝑀)βŸΆβ„)
160159adantr 480 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑉:(0...𝑀)βŸΆβ„)
161160, 156ffvelcdmd 7089 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ)
1625adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑋 ∈ ℝ)
163161, 162resubcld 11664 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋) ∈ ℝ)
164151, 154, 156, 163fvmptd 7006 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜(𝑖 + 1)) = ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋))
165164adantr 480 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘„β€˜(𝑖 + 1)) = ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋))
166 oveq1 7421 . . . . . . . . 9 ((π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋) = (𝑋 βˆ’ 𝑋))
167166adantl 481 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋) = (𝑋 βˆ’ 𝑋))
168115ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝑋 ∈ β„‚)
169168subidd 11581 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (𝑋 βˆ’ 𝑋) = 0)
1701, 169sylanl2 680 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (𝑋 βˆ’ 𝑋) = 0)
171165, 167, 1703eqtrd 2771 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘„β€˜(𝑖 + 1)) = 0)
172146, 171oveq12d 7432 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) = (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0))
173 simplr 768 . . . . . . . . . 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 45432 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑄 ∈ (π‘‚β€˜π‘€))
177176adantr 480 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 = 0) β†’ 𝑄 ∈ (π‘‚β€˜π‘€))
178 simpr 484 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑠 = 0) β†’ 𝑠 = 0)
179 fourierdlem74.x . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝑋 ∈ ran 𝑉)
180 ffn 6716 . . . . . . . . . . . . . . . . . . 19 (𝑉:(0...𝑀)⟢((-Ο€ + 𝑋)[,](Ο€ + 𝑋)) β†’ 𝑉 Fn (0...𝑀))
181 fvelrnb 6953 . . . . . . . . . . . . . . . . . . 19 (𝑉 Fn (0...𝑀) β†’ (𝑋 ∈ ran 𝑉 ↔ βˆƒπ‘– ∈ (0...𝑀)(π‘‰β€˜π‘–) = 𝑋))
18214, 180, 1813syl 18 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (𝑋 ∈ ran 𝑉 ↔ βˆƒπ‘– ∈ (0...𝑀)(π‘‰β€˜π‘–) = 𝑋))
183179, 182mpbid 231 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ βˆƒπ‘– ∈ (0...𝑀)(π‘‰β€˜π‘–) = 𝑋)
184 simpr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ 𝑖 ∈ (0...𝑀))
185134fvmpt2 7010 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑖 ∈ (0...𝑀) ∧ ((π‘‰β€˜π‘–) βˆ’ 𝑋) ∈ (-Ο€[,]Ο€)) β†’ (π‘„β€˜π‘–) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
186184, 133, 185syl2anc 583 . . . . . . . . . . . . . . . . . . . . 21 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ (π‘„β€˜π‘–) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
187186adantr 480 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) ∧ (π‘‰β€˜π‘–) = 𝑋) β†’ (π‘„β€˜π‘–) = ((π‘‰β€˜π‘–) βˆ’ 𝑋))
188 oveq1 7421 . . . . . . . . . . . . . . . . . . . . 21 ((π‘‰β€˜π‘–) = 𝑋 β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) = (𝑋 βˆ’ 𝑋))
189188adantl 481 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) ∧ (π‘‰β€˜π‘–) = 𝑋) β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) = (𝑋 βˆ’ 𝑋))
190115subidd 11581 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝑋 βˆ’ 𝑋) = 0)
191190ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) ∧ (π‘‰β€˜π‘–) = 𝑋) β†’ (𝑋 βˆ’ 𝑋) = 0)
192187, 189, 1913eqtrd 2771 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) ∧ (π‘‰β€˜π‘–) = 𝑋) β†’ (π‘„β€˜π‘–) = 0)
193192ex 412 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ ((π‘‰β€˜π‘–) = 𝑋 β†’ (π‘„β€˜π‘–) = 0))
194193reximdva 3163 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ (βˆƒπ‘– ∈ (0...𝑀)(π‘‰β€˜π‘–) = 𝑋 β†’ βˆƒπ‘– ∈ (0...𝑀)(π‘„β€˜π‘–) = 0))
195183, 194mpd 15 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ βˆƒπ‘– ∈ (0...𝑀)(π‘„β€˜π‘–) = 0)
196113, 134fmptd 7118 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 𝑄:(0...𝑀)βŸΆβ„)
197 ffn 6716 . . . . . . . . . . . . . . . . 17 (𝑄:(0...𝑀)βŸΆβ„ β†’ 𝑄 Fn (0...𝑀))
198 fvelrnb 6953 . . . . . . . . . . . . . . . . 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 2828 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑠 = 0) β†’ 𝑠 ∈ ran 𝑄)
203174, 175, 177, 202fourierdlem12 45430 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑠 = 0) ∧ 𝑖 ∈ (0..^𝑀)) β†’ Β¬ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))))
204203an32s 651 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 = 0) β†’ Β¬ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))))
205204adantlr 714 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) ∧ 𝑠 = 0) β†’ Β¬ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))))
206173, 205pm2.65da 816 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ Β¬ 𝑠 = 0)
207206adantlr 714 . . . . . . . 8 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ Β¬ 𝑠 = 0)
208207iffalsed 4535 . . . . . . 7 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠))
209 elioore 13378 . . . . . . . . . . . 12 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) β†’ 𝑠 ∈ ℝ)
210209adantl 481 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ ℝ)
211 0red 11239 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 0 ∈ ℝ)
212 elioo3g 13377 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↔ (((π‘„β€˜π‘–) ∈ ℝ* ∧ (π‘„β€˜(𝑖 + 1)) ∈ ℝ* ∧ 𝑠 ∈ ℝ*) ∧ ((π‘„β€˜π‘–) < 𝑠 ∧ 𝑠 < (π‘„β€˜(𝑖 + 1)))))
213212biimpi 215 . . . . . . . . . . . . . 14 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) β†’ (((π‘„β€˜π‘–) ∈ ℝ* ∧ (π‘„β€˜(𝑖 + 1)) ∈ ℝ* ∧ 𝑠 ∈ ℝ*) ∧ ((π‘„β€˜π‘–) < 𝑠 ∧ 𝑠 < (π‘„β€˜(𝑖 + 1)))))
214213simprrd 773 . . . . . . . . . . . . 13 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) β†’ 𝑠 < (π‘„β€˜(𝑖 + 1)))
215214adantl 481 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 < (π‘„β€˜(𝑖 + 1)))
216171adantr 480 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜(𝑖 + 1)) = 0)
217215, 216breqtrd 5168 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 < 0)
218210, 211, 217ltnsymd 11385 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ Β¬ 0 < 𝑠)
219218iffalsed 4535 . . . . . . . . 9 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = π‘Š)
220219oveq2d 7430 . . . . . . . 8 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) = ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š))
221220oveq1d 7429 . . . . . . 7 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š) / 𝑠))
22241ad2antrr 725 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘‰β€˜π‘–) ∈ ℝ*)
2235rexrd 11286 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑋 ∈ ℝ*)
224223ad3antrrr 729 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑋 ∈ ℝ*)
225162ad2antrr 725 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑋 ∈ ℝ)
226225, 210readdcld 11265 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) ∈ ℝ)
227115adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑋 ∈ β„‚)
228 iccssre 13430 . . . . . . . . . . . . . . . . . . 19 ((-Ο€ ∈ ℝ ∧ Ο€ ∈ ℝ) β†’ (-Ο€[,]Ο€) βŠ† ℝ)
2293, 2, 228mp2an 691 . . . . . . . . . . . . . . . . . 18 (-Ο€[,]Ο€) βŠ† ℝ
230229, 51sstri 3987 . . . . . . . . . . . . . . . . 17 (-Ο€[,]Ο€) βŠ† β„‚
231186, 133eqeltrd 2828 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ 𝑖 ∈ (0...𝑀)) β†’ (π‘„β€˜π‘–) ∈ (-Ο€[,]Ο€))
2321, 231sylan2 592 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜π‘–) ∈ (-Ο€[,]Ο€))
233230, 232sselid 3976 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜π‘–) ∈ β„‚)
234227, 233addcomd 11438 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑋 + (π‘„β€˜π‘–)) = ((π‘„β€˜π‘–) + 𝑋))
235145oveq1d 7429 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘„β€˜π‘–) + 𝑋) = (((π‘‰β€˜π‘–) βˆ’ 𝑋) + 𝑋))
23617recnd 11264 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜π‘–) ∈ β„‚)
237236, 227npcand 11597 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (((π‘‰β€˜π‘–) βˆ’ 𝑋) + 𝑋) = (π‘‰β€˜π‘–))
238234, 235, 2373eqtrrd 2772 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜π‘–) = (𝑋 + (π‘„β€˜π‘–)))
239238adantr 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘‰β€˜π‘–) = (𝑋 + (π‘„β€˜π‘–)))
240145, 143eqeltrd 2828 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜π‘–) ∈ ℝ)
241240adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜π‘–) ∈ ℝ)
242209adantl 481 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ ℝ)
2435ad2antrr 725 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑋 ∈ ℝ)
244213simprld 771 . . . . . . . . . . . . . . 15 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) β†’ (π‘„β€˜π‘–) < 𝑠)
245244adantl 481 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜π‘–) < 𝑠)
246241, 242, 243, 245ltadd2dd 11395 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + (π‘„β€˜π‘–)) < (𝑋 + 𝑠))
247239, 246eqbrtrd 5164 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘‰β€˜π‘–) < (𝑋 + 𝑠))
248247adantlr 714 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘‰β€˜π‘–) < (𝑋 + 𝑠))
249 ltaddneg 11451 . . . . . . . . . . . . 13 ((𝑠 ∈ ℝ ∧ 𝑋 ∈ ℝ) β†’ (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
250210, 225, 249syl2anc 583 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑠 < 0 ↔ (𝑋 + 𝑠) < 𝑋))
251217, 250mpbid 231 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) < 𝑋)
252222, 224, 226, 248, 251eliood 44806 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) ∈ ((π‘‰β€˜π‘–)(,)𝑋))
253 fvres 6910 . . . . . . . . . . 11 ((𝑋 + 𝑠) ∈ ((π‘‰β€˜π‘–)(,)𝑋) β†’ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) = (πΉβ€˜(𝑋 + 𝑠)))
254253eqcomd 2733 . . . . . . . . . 10 ((𝑋 + 𝑠) ∈ ((π‘‰β€˜π‘–)(,)𝑋) β†’ (πΉβ€˜(𝑋 + 𝑠)) = ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)))
255252, 254syl 17 . . . . . . . . 9 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (πΉβ€˜(𝑋 + 𝑠)) = ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)))
256255oveq1d 7429 . . . . . . . 8 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š) = (((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š))
257256oveq1d 7429 . . . . . . 7 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š) / 𝑠) = ((((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š) / 𝑠))
258208, 221, 2573eqtrd 2771 . . . . . 6 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) = ((((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š) / 𝑠))
259172, 258mpteq12dva 5231 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠))) = (𝑠 ∈ (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0) ↦ ((((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š) / 𝑠)))
260104, 141, 2593eqtrd 2771 . . . 4 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = (𝑠 ∈ (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0) ↦ ((((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š) / 𝑠)))
261260, 171oveq12d 7432 . . 3 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ ((𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))) = ((𝑠 ∈ (((π‘‰β€˜π‘–) βˆ’ 𝑋)(,)0) ↦ ((((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)𝑋))β€˜(𝑋 + 𝑠)) βˆ’ π‘Š) / 𝑠)) limβ„‚ 0))
26297, 101, 2613eltr4d 2843 . 2 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝐴 ∈ ((𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
263 eqid 2727 . . . . 5 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)))
264 eqid 2727 . . . . 5 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ 𝑠) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ 𝑠)
265 eqid 2727 . . . . 5 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠))
26630adantr 480 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝐹:β„βŸΆβ„)
2675adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑋 ∈ ℝ)
268209adantl 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ ℝ)
269267, 268readdcld 11265 . . . . . . . . . 10 ((πœ‘ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) ∈ ℝ)
270266, 269ffvelcdmd 7089 . . . . . . . . 9 ((πœ‘ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ ℝ)
271270recnd 11264 . . . . . . . 8 ((πœ‘ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
272271adantlr 714 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
2732723adantl3 1166 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
274 fourierdlem74.y . . . . . . . . . 10 (πœ‘ β†’ π‘Œ ∈ ℝ)
275274recnd 11264 . . . . . . . . 9 (πœ‘ β†’ π‘Œ ∈ β„‚)
276 limccl 25791 . . . . . . . . . 10 ((𝐹 β†Ύ (-∞(,)𝑋)) limβ„‚ 𝑋) βŠ† β„‚
277276, 36sselid 3976 . . . . . . . . 9 (πœ‘ β†’ π‘Š ∈ β„‚)
278275, 277ifcld 4570 . . . . . . . 8 (πœ‘ β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
279278adantr 480 . . . . . . 7 ((πœ‘ ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
2802793ad2antl1 1183 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
281273, 280subcld 11593 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ β„‚)
282209recnd 11264 . . . . . . 7 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) β†’ 𝑠 ∈ β„‚)
283282adantl 481 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ β„‚)
284 velsn 4640 . . . . . . . 8 (𝑠 ∈ {0} ↔ 𝑠 = 0)
285206, 284sylnibr 329 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ Β¬ 𝑠 ∈ {0})
2862853adantl3 1166 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ Β¬ 𝑠 ∈ {0})
287283, 286eldifd 3955 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ (β„‚ βˆ– {0}))
288 eqid 2727 . . . . . . . . . 10 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠)))
289 eqid 2727 . . . . . . . . . 10 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ π‘Š) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ π‘Š)
290 eqid 2727 . . . . . . . . . 10 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š)) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š))
291277ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ π‘Š ∈ β„‚)
29230adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐹:β„βŸΆβ„)
293 ioossre 13409 . . . . . . . . . . . 12 ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† ℝ
294293a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† ℝ)
29541adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘‰β€˜π‘–) ∈ ℝ*)
296161rexrd 11286 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ*)
297296adantr 480 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ*)
298269adantlr 714 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) ∈ ℝ)
299196adantr 480 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑄:(0...𝑀)βŸΆβ„)
300299, 156ffvelcdmd 7089 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ)
301300adantr 480 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ℝ)
302214adantl 481 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 < (π‘„β€˜(𝑖 + 1)))
303242, 301, 243, 302ltadd2dd 11395 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) < (𝑋 + (π‘„β€˜(𝑖 + 1))))
304164oveq2d 7430 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑋 + (π‘„β€˜(𝑖 + 1))) = (𝑋 + ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋)))
305161recnd 11264 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ β„‚)
306227, 305pncan3d 11596 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑋 + ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋)) = (π‘‰β€˜(𝑖 + 1)))
307304, 306eqtrd 2767 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑋 + (π‘„β€˜(𝑖 + 1))) = (π‘‰β€˜(𝑖 + 1)))
308307adantr 480 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + (π‘„β€˜(𝑖 + 1))) = (π‘‰β€˜(𝑖 + 1)))
309303, 308breqtrd 5168 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) < (π‘‰β€˜(𝑖 + 1)))
310295, 297, 298, 247, 309eliood 44806 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (𝑋 + 𝑠) ∈ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))
311 ioossre 13409 . . . . . . . . . . . 12 ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))) βŠ† ℝ
312311a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))) βŠ† ℝ)
313242, 302ltned 11372 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 β‰  (π‘„β€˜(𝑖 + 1)))
314 fourierdlem74.r . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))))
315307eqcomd 2733 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘‰β€˜(𝑖 + 1)) = (𝑋 + (π‘„β€˜(𝑖 + 1))))
316315oveq2d 7430 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (π‘‰β€˜(𝑖 + 1))) = ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (𝑋 + (π‘„β€˜(𝑖 + 1)))))
317314, 316eleqtrd 2830 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝐹 β†Ύ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1)))) limβ„‚ (𝑋 + (π‘„β€˜(𝑖 + 1)))))
318300recnd 11264 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜(𝑖 + 1)) ∈ β„‚)
319292, 162, 294, 288, 310, 312, 313, 317, 318fourierdlem53 45470 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝑅 ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
320 ioosscn 13410 . . . . . . . . . . . 12 ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† β„‚
321320a1i 11 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) βŠ† β„‚)
322277adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ π‘Š ∈ β„‚)
323289, 321, 322, 318constlimc 44935 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ π‘Š ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ π‘Š) limβ„‚ (π‘„β€˜(𝑖 + 1))))
324288, 289, 290, 272, 291, 319, 323sublimc 44963 . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑅 βˆ’ π‘Š) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š)) limβ„‚ (π‘„β€˜(𝑖 + 1))))
325324adantr 480 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (𝑅 βˆ’ π‘Š) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š)) limβ„‚ (π‘„β€˜(𝑖 + 1))))
326 iftrue 4530 . . . . . . . . . 10 ((π‘‰β€˜(𝑖 + 1)) < 𝑋 β†’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ) = π‘Š)
327326oveq2d 7430 . . . . . . . . 9 ((π‘‰β€˜(𝑖 + 1)) < 𝑋 β†’ (𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) = (𝑅 βˆ’ π‘Š))
328327adantl 481 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) = (𝑅 βˆ’ π‘Š))
329209adantl 481 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ ℝ)
330 0red 11239 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 0 ∈ ℝ)
331300ad2antrr 725 . . . . . . . . . . . . . 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 725 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ 𝑋 ∈ ℝ)
336 simpr 484 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (π‘‰β€˜(𝑖 + 1)) < 𝑋)
337334, 335, 336ltled 11384 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (π‘‰β€˜(𝑖 + 1)) ≀ 𝑋)
338334, 335suble0d 11827 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋) ≀ 0 ↔ (π‘‰β€˜(𝑖 + 1)) ≀ 𝑋))
339337, 338mpbird 257 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋) ≀ 0)
340333, 339eqbrtrd 5164 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (π‘„β€˜(𝑖 + 1)) ≀ 0)
341340adantr 480 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜(𝑖 + 1)) ≀ 0)
342329, 331, 330, 332, 341ltletrd 11396 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 < 0)
343329, 330, 342ltnsymd 11385 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ Β¬ 0 < 𝑠)
344343iffalsed 4535 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = π‘Š)
345344oveq2d 7430 . . . . . . . . . 10 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) = ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š))
346345mpteq2dva 5242 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š)))
347346oveq1d 7429 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) limβ„‚ (π‘„β€˜(𝑖 + 1))) = ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ π‘Š)) limβ„‚ (π‘„β€˜(𝑖 + 1))))
348325, 328, 3473eltr4d 2843 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
3493483adantl3 1166 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
350 simpl1 1189 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ πœ‘)
351 simpl2 1190 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ 𝑖 ∈ (0..^𝑀))
3525ad2antrr 725 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ 𝑋 ∈ ℝ)
3533523adantl3 1166 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ 𝑋 ∈ ℝ)
354161adantr 480 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ)
3553543adantl3 1166 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ)
356 neqne 2943 . . . . . . . . . . 11 (Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ (π‘‰β€˜(𝑖 + 1)) β‰  𝑋)
357356necomd 2991 . . . . . . . . . 10 (Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ 𝑋 β‰  (π‘‰β€˜(𝑖 + 1)))
358357adantr 480 . . . . . . . . 9 ((Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋 ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ 𝑋 β‰  (π‘‰β€˜(𝑖 + 1)))
3593583ad2antl3 1185 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ 𝑋 β‰  (π‘‰β€˜(𝑖 + 1)))
360 simpr 484 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋)
361353, 355, 359, 360lttri5d 44604 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ 𝑋 < (π‘‰β€˜(𝑖 + 1)))
362 eqid 2727 . . . . . . . 8 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ if(0 < 𝑠, π‘Œ, π‘Š)) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ if(0 < 𝑠, π‘Œ, π‘Š))
363272adantlr 714 . . . . . . . 8 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (πΉβ€˜(𝑋 + 𝑠)) ∈ β„‚)
364278ad3antrrr 729 . . . . . . . 8 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
365319adantr 480 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ 𝑅 ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (πΉβ€˜(𝑋 + 𝑠))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
366 eqid 2727 . . . . . . . . . . 11 (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ π‘Œ) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ π‘Œ)
367275adantr 480 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ π‘Œ ∈ β„‚)
368366, 321, 367, 318constlimc 44935 . . . . . . . . . 10 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ π‘Œ ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ π‘Œ) limβ„‚ (π‘„β€˜(𝑖 + 1))))
369368adantr 480 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ π‘Œ ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ π‘Œ) limβ„‚ (π‘„β€˜(𝑖 + 1))))
3705ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ 𝑋 ∈ ℝ)
371161adantr 480 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ)
372 simpr 484 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ 𝑋 < (π‘‰β€˜(𝑖 + 1)))
373370, 371, 372ltnsymd 11385 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋)
374373iffalsed 4535 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ) = π‘Œ)
375 0red 11239 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 0 ∈ ℝ)
376240ad2antrr 725 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜π‘–) ∈ ℝ)
377209adantl 481 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ ℝ)
378190eqcomd 2733 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ 0 = (𝑋 βˆ’ 𝑋))
379378ad2antrr 725 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ 0 = (𝑋 βˆ’ 𝑋))
38017adantr 480 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ (π‘‰β€˜π‘–) ∈ ℝ)
38141ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ (π‘‰β€˜π‘–) ∈ ℝ*)
382296ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ ℝ*)
383162ad2antrr 725 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ 𝑋 ∈ ℝ)
384 simpr 484 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–))
38517adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ (π‘‰β€˜π‘–) ∈ ℝ)
3865ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ 𝑋 ∈ ℝ)
387385, 386ltnled 11383 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ ((π‘‰β€˜π‘–) < 𝑋 ↔ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)))
388384, 387mpbird 257 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ (π‘‰β€˜π‘–) < 𝑋)
389388adantlr 714 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ (π‘‰β€˜π‘–) < 𝑋)
390 simplr 768 . . . . . . . . . . . . . . . . . . 19 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ 𝑋 < (π‘‰β€˜(𝑖 + 1)))
391381, 382, 383, 389, 390eliood 44806 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ 𝑋 ∈ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))
39211, 12, 13, 179fourierdlem12 45430 . . . . . . . . . . . . . . . . . . 19 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ Β¬ 𝑋 ∈ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))
393392ad2antrr 725 . . . . . . . . . . . . . . . . . 18 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ Β¬ 𝑋 ≀ (π‘‰β€˜π‘–)) β†’ Β¬ 𝑋 ∈ ((π‘‰β€˜π‘–)(,)(π‘‰β€˜(𝑖 + 1))))
394391, 393condan 817 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ 𝑋 ≀ (π‘‰β€˜π‘–))
395370, 380, 370, 394lesub1dd 11852 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ (𝑋 βˆ’ 𝑋) ≀ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
396379, 395eqbrtrd 5164 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ 0 ≀ ((π‘‰β€˜π‘–) βˆ’ 𝑋))
397145eqcomd 2733 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) = (π‘„β€˜π‘–))
398397adantr 480 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ ((π‘‰β€˜π‘–) βˆ’ 𝑋) = (π‘„β€˜π‘–))
399396, 398breqtrd 5168 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ 0 ≀ (π‘„β€˜π‘–))
400399adantr 480 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 0 ≀ (π‘„β€˜π‘–))
401244adantl 481 . . . . . . . . . . . . 13 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π‘„β€˜π‘–) < 𝑠)
402375, 376, 377, 400, 401lelttrd 11394 . . . . . . . . . . . 12 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 0 < 𝑠)
403402iftrued 4532 . . . . . . . . . . 11 ((((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(0 < 𝑠, π‘Œ, π‘Š) = π‘Œ)
404403mpteq2dva 5242 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ if(0 < 𝑠, π‘Œ, π‘Š)) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ π‘Œ))
405404oveq1d 7429 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ if(0 < 𝑠, π‘Œ, π‘Š)) limβ„‚ (π‘„β€˜(𝑖 + 1))) = ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ π‘Œ) limβ„‚ (π‘„β€˜(𝑖 + 1))))
406369, 374, 4053eltr4d 2843 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ if(0 < 𝑠, π‘Œ, π‘Š)) limβ„‚ (π‘„β€˜(𝑖 + 1))))
407288, 362, 263, 363, 364, 365, 406sublimc 44963 . . . . . . 7 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑋 < (π‘‰β€˜(𝑖 + 1))) β†’ (𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
408350, 351, 361, 407syl21anc 837 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) < 𝑋) β†’ (𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
409349, 408pm2.61dan 812 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
410321, 264, 318idlimc 44937 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ 𝑠) limβ„‚ (π‘„β€˜(𝑖 + 1))))
4114103adant3 1130 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘„β€˜(𝑖 + 1)) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ 𝑠) limβ„‚ (π‘„β€˜(𝑖 + 1))))
4121643adant3 1130 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘„β€˜(𝑖 + 1)) = ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋))
4133053adant3 1130 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘‰β€˜(𝑖 + 1)) ∈ β„‚)
4142273adant3 1130 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝑋 ∈ β„‚)
4153563ad2ant3 1133 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘‰β€˜(𝑖 + 1)) β‰  𝑋)
416413, 414, 415subne0d 11602 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ ((π‘‰β€˜(𝑖 + 1)) βˆ’ 𝑋) β‰  0)
417412, 416eqnetrd 3003 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (π‘„β€˜(𝑖 + 1)) β‰  0)
4182063adantl3 1166 . . . . . 6 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ Β¬ 𝑠 = 0)
419418neqned 2942 . . . . 5 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 β‰  0)
420263, 264, 265, 281, 287, 409, 411, 417, 419divlimc 44967 . . . 4 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ ((𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜(𝑖 + 1))) ∈ ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) limβ„‚ (π‘„β€˜(𝑖 + 1))))
421 iffalse 4533 . . . . . 6 (Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ if((π‘‰β€˜(𝑖 + 1)) = 𝑋, 𝐸, ((𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜(𝑖 + 1)))) = ((𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜(𝑖 + 1))))
42298, 421eqtrid 2779 . . . . 5 (Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋 β†’ 𝐴 = ((𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜(𝑖 + 1))))
4234223ad2ant3 1133 . . . 4 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝐴 = ((𝑅 βˆ’ if((π‘‰β€˜(𝑖 + 1)) < 𝑋, π‘Š, π‘Œ)) / (π‘„β€˜(𝑖 + 1))))
424 ioossre 13409 . . . . . . . . . . . . 13 (-∞(,)𝑋) βŠ† ℝ
425424a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ (-∞(,)𝑋) βŠ† ℝ)
42630, 425fssresd 6758 . . . . . . . . . . 11 (πœ‘ β†’ (𝐹 β†Ύ (-∞(,)𝑋)):(-∞(,)𝑋)βŸΆβ„)
427424, 52sstrid 3989 . . . . . . . . . . 11 (πœ‘ β†’ (-∞(,)𝑋) βŠ† β„‚)
42839a1i 11 . . . . . . . . . . . 12 (πœ‘ β†’ -∞ ∈ ℝ*)
4295mnfltd 13128 . . . . . . . . . . . 12 (πœ‘ β†’ -∞ < 𝑋)
43056, 428, 5, 429lptioo2cn 44956 . . . . . . . . . . 11 (πœ‘ β†’ 𝑋 ∈ ((limPtβ€˜(TopOpenβ€˜β„‚fld))β€˜(-∞(,)𝑋)))
431426, 427, 430, 36limcrecl 44940 . . . . . . . . . 10 (πœ‘ β†’ π‘Š ∈ ℝ)
43230, 5, 274, 431, 102fourierdlem9 45427 . . . . . . . . 9 (πœ‘ β†’ 𝐻:(-Ο€[,]Ο€)βŸΆβ„)
433432adantr 480 . . . . . . . 8 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐻:(-Ο€[,]Ο€)βŸΆβ„)
434433, 139feqresmpt 6962 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π»β€˜π‘ )))
435139sselda 3978 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ (-Ο€[,]Ο€))
436 0cnd 11229 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 0 ∈ β„‚)
437278ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(0 < 𝑠, π‘Œ, π‘Š) ∈ β„‚)
438272, 437subcld 11593 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ ((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) ∈ β„‚)
439282adantl 481 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 ∈ β„‚)
440206neqned 2942 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ 𝑠 β‰  0)
441438, 439, 440divcld 12012 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠) ∈ β„‚)
442436, 441ifcld 4570 . . . . . . . . . 10 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) ∈ β„‚)
443102fvmpt2 7010 . . . . . . . . . 10 ((𝑠 ∈ (-Ο€[,]Ο€) ∧ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) ∈ β„‚) β†’ (π»β€˜π‘ ) = if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
444435, 442, 443syl2anc 583 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π»β€˜π‘ ) = if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
445206iffalsed 4535 . . . . . . . . 9 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ if(𝑠 = 0, 0, (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠))
446444, 445eqtrd 2767 . . . . . . . 8 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) β†’ (π»β€˜π‘ ) = (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠))
447446mpteq2dva 5242 . . . . . . 7 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (π»β€˜π‘ )) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
448434, 447eqtrd 2767 . . . . . 6 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
4494483adant3 1130 . . . . 5 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ (𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = (𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)))
450449oveq1d 7429 . . . 4 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ ((𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))) = ((𝑠 ∈ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) ↦ (((πΉβ€˜(𝑋 + 𝑠)) βˆ’ if(0 < 𝑠, π‘Œ, π‘Š)) / 𝑠)) limβ„‚ (π‘„β€˜(𝑖 + 1))))
451420, 423, 4503eltr4d 2843 . . 3 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝐴 ∈ ((𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
4524513expa 1116 . 2 (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ∧ Β¬ (π‘‰β€˜(𝑖 + 1)) = 𝑋) β†’ 𝐴 ∈ ((𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
453262, 452pm2.61dan 812 1 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐴 ∈ ((𝐻 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   β‰  wne 2935  βˆ€wral 3056  βˆƒwrex 3065  {crab 3427   βŠ† wss 3944  ifcif 4524  {csn 4624   class class class wbr 5142   ↦ cmpt 5225  dom cdm 5672  ran crn 5673   β†Ύ cres 5674   Fn wfn 6537  βŸΆwf 6538  β€˜cfv 6542  (class class class)co 7414   ↑m cmap 8836  β„‚cc 11128  β„cr 11129  0cc0 11130  1c1 11131   + caddc 11133  -∞cmnf 11268  β„*cxr 11269   < clt 11270   ≀ cle 11271   βˆ’ cmin 11466  -cneg 11467   / cdiv 11893  β„•cn 12234  (,)cioo 13348  [,]cicc 13351  ...cfz 13508  ..^cfzo 13651  Ο€cpi 16034  TopOpenctopn 17394  topGenctg 17410  β„‚fldccnfld 21266  intcnt 22908   limβ„‚ climc 25778   D cdv 25779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2164  ax-ext 2698  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423  ax-un 7734  ax-inf2 9656  ax-cnex 11186  ax-resscn 11187  ax-1cn 11188  ax-icn 11189  ax-addcl 11190  ax-addrcl 11191  ax-mulcl 11192  ax-mulrcl 11193  ax-mulcom 11194  ax-addass 11195  ax-mulass 11196  ax-distr 11197  ax-i2m1 11198  ax-1ne0 11199  ax-1rid 11200  ax-rnegex 11201  ax-rrecex 11202  ax-cnre 11203  ax-pre-lttri 11204  ax-pre-lttrn 11205  ax-pre-ltadd 11206  ax-pre-mulgt0 11207  ax-pre-sup 11208  ax-addf 11209
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3or 1086  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2936  df-nel 3042  df-ral 3057  df-rex 3066  df-rmo 3371  df-reu 3372  df-rab 3428  df-v 3471  df-sbc 3775  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3963  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7370  df-ov 7417  df-oprab 7418  df-mpo 7419  df-of 7679  df-om 7865  df-1st 7987  df-2nd 7988  df-supp 8160  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-2o 8481  df-er 8718  df-map 8838  df-pm 8839  df-ixp 8908  df-en 8956  df-dom 8957  df-sdom 8958  df-fin 8959  df-fsupp 9378  df-fi 9426  df-sup 9457  df-inf 9458  df-oi 9525  df-card 9954  df-pnf 11272  df-mnf 11273  df-xr 11274  df-ltxr 11275  df-le 11276  df-sub 11468  df-neg 11469  df-div 11894  df-nn 12235  df-2 12297  df-3 12298  df-4 12299  df-5 12300  df-6 12301  df-7 12302  df-8 12303  df-9 12304  df-n0 12495  df-z 12581  df-dec 12700  df-uz 12845  df-q 12955  df-rp 12999  df-xneg 13116  df-xadd 13117  df-xmul 13118  df-ioo 13352  df-ioc 13353  df-ico 13354  df-icc 13355  df-fz 13509  df-fzo 13652  df-fl 13781  df-seq 13991  df-exp 14051  df-fac 14257  df-bc 14286  df-hash 14314  df-shft 15038  df-cj 15070  df-re 15071  df-im 15072  df-sqrt 15206  df-abs 15207  df-limsup 15439  df-clim 15456  df-rlim 15457  df-sum 15657  df-ef 16035  df-sin 16037  df-cos 16038  df-pi 16040  df-struct 17107  df-sets 17124  df-slot 17142  df-ndx 17154  df-base 17172  df-ress 17201  df-plusg 17237  df-mulr 17238  df-starv 17239  df-sca 17240  df-vsca 17241  df-ip 17242  df-tset 17243  df-ple 17244  df-ds 17246  df-unif 17247  df-hom 17248  df-cco 17249  df-rest 17395  df-topn 17396  df-0g 17414  df-gsum 17415  df-topgen 17416  df-pt 17417  df-prds 17420  df-xrs 17475  df-qtop 17480  df-imas 17481  df-xps 17483  df-mre 17557  df-mrc 17558  df-acs 17560  df-mgm 18591  df-sgrp 18670  df-mnd 18686  df-submnd 18732  df-mulg 19015  df-cntz 19259  df-cmn 19728  df-psmet 21258  df-xmet 21259  df-met 21260  df-bl 21261  df-mopn 21262  df-fbas 21263  df-fg 21264  df-cnfld 21267  df-top 22783  df-topon 22800  df-topsp 22822  df-bases 22836  df-cld 22910  df-ntr 22911  df-cls 22912  df-nei 22989  df-lp 23027  df-perf 23028  df-cn 23118  df-cnp 23119  df-haus 23206  df-cmp 23278  df-tx 23453  df-hmeo 23646  df-fil 23737  df-fm 23829  df-flim 23830  df-flf 23831  df-xms 24213  df-ms 24214  df-tms 24215  df-cncf 24785  df-limc 25782  df-dv 25783
This theorem is referenced by:  fourierdlem88  45505  fourierdlem103  45520  fourierdlem104  45521
  Copyright terms: Public domain W3C validator