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

Theorem fourierdlem91 44900
Description: Given a piecewise continuous function and changing the interval and the partition, the limit at the upper bound of each interval of the moved partition is still finite. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem91.p 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = 𝐴 ∧ (π‘β€˜π‘š) = 𝐡) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
fourierdlem91.t 𝑇 = (𝐡 βˆ’ 𝐴)
fourierdlem91.m (πœ‘ β†’ 𝑀 ∈ β„•)
fourierdlem91.q (πœ‘ β†’ 𝑄 ∈ (π‘ƒβ€˜π‘€))
fourierdlem91.f (πœ‘ β†’ 𝐹:β„βŸΆβ„‚)
fourierdlem91.6 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜(π‘₯ + 𝑇)) = (πΉβ€˜π‘₯))
fourierdlem91.fcn ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) ∈ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚))
fourierdlem91.l ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
fourierdlem91.c (πœ‘ β†’ 𝐢 ∈ ℝ)
fourierdlem91.d (πœ‘ β†’ 𝐷 ∈ (𝐢(,)+∞))
fourierdlem91.o 𝑂 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = 𝐢 ∧ (π‘β€˜π‘š) = 𝐷) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
fourierdlem91.h 𝐻 = ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})
fourierdlem91.n 𝑁 = ((β™―β€˜π») βˆ’ 1)
fourierdlem91.s 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
fourierdlem91.e 𝐸 = (π‘₯ ∈ ℝ ↦ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)))
fourierdlem91.J 𝑍 = (𝑦 ∈ (𝐴(,]𝐡) ↦ if(𝑦 = 𝐡, 𝐴, 𝑦))
fourierdlem91.17 (πœ‘ β†’ 𝐽 ∈ (0..^𝑁))
fourierdlem91.u π‘ˆ = ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
fourierdlem91.i 𝐼 = (π‘₯ ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (π‘„β€˜π‘–) ≀ (π‘β€˜(πΈβ€˜π‘₯))}, ℝ, < ))
fourierdlem91.w π‘Š = (𝑖 ∈ (0..^𝑀) ↦ 𝐿)
Assertion
Ref Expression
fourierdlem91 (πœ‘ β†’ if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), (πΉβ€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) ∈ ((𝐹 β†Ύ ((π‘†β€˜π½)(,)(π‘†β€˜(𝐽 + 1)))) limβ„‚ (π‘†β€˜(𝐽 + 1))))
Distinct variable groups:   𝐴,𝑓,π‘˜,𝑦   𝐴,𝑖,π‘₯,π‘˜,𝑦   𝐴,π‘š,𝑝,𝑖   𝐡,𝑓,π‘˜,𝑦   𝐡,𝑖,π‘₯   𝐡,π‘š,𝑝   𝐢,𝑓,𝑦   𝐢,𝑖,π‘š,𝑝   π‘₯,𝐢   𝐷,𝑓,𝑦   𝐷,𝑖,π‘š,𝑝   π‘₯,𝐷   𝑓,𝐸,π‘˜,𝑦   𝑖,𝐸,π‘₯   𝑖,𝐹,π‘₯,𝑦   𝑓,𝐻   π‘₯,𝐻   𝑓,𝐼,π‘˜,𝑦   𝑖,𝐼,π‘₯   𝑖,𝐽,π‘₯,𝑦   𝑖,𝑀,π‘₯   π‘š,𝑀,𝑝   𝑓,𝑁,π‘˜,𝑦   𝑖,𝑁,π‘₯   π‘š,𝑁,𝑝   𝑄,𝑓,π‘˜,𝑦   𝑄,𝑖,π‘₯   𝑄,𝑝   𝑆,𝑓,π‘˜,𝑦   𝑆,𝑖,π‘₯   𝑆,𝑝   𝑇,𝑓,π‘˜,𝑦   𝑇,𝑖,π‘₯   π‘₯,π‘ˆ,𝑦   π‘₯,π‘Š,𝑦   𝑖,𝑍,π‘₯,𝑦   πœ‘,𝑓,π‘˜,𝑦   πœ‘,𝑖,π‘₯
Allowed substitution hints:   πœ‘(π‘š,𝑝)   𝐢(π‘˜)   𝐷(π‘˜)   𝑃(π‘₯,𝑦,𝑓,𝑖,π‘˜,π‘š,𝑝)   𝑄(π‘š)   𝑆(π‘š)   𝑇(π‘š,𝑝)   π‘ˆ(𝑓,𝑖,π‘˜,π‘š,𝑝)   𝐸(π‘š,𝑝)   𝐹(𝑓,π‘˜,π‘š,𝑝)   𝐻(𝑦,𝑖,π‘˜,π‘š,𝑝)   𝐼(π‘š,𝑝)   𝐽(𝑓,π‘˜,π‘š,𝑝)   𝐿(π‘₯,𝑦,𝑓,𝑖,π‘˜,π‘š,𝑝)   𝑀(𝑦,𝑓,π‘˜)   𝑂(π‘₯,𝑦,𝑓,𝑖,π‘˜,π‘š,𝑝)   π‘Š(𝑓,𝑖,π‘˜,π‘š,𝑝)   𝑍(𝑓,π‘˜,π‘š,𝑝)

Proof of Theorem fourierdlem91
Dummy variable 𝑗 is distinct from all other variables.
StepHypRef Expression
1 fourierdlem91.q . . . . . . . . . . . 12 (πœ‘ β†’ 𝑄 ∈ (π‘ƒβ€˜π‘€))
2 fourierdlem91.m . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑀 ∈ β„•)
3 fourierdlem91.p . . . . . . . . . . . . . 14 𝑃 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = 𝐴 ∧ (π‘β€˜π‘š) = 𝐡) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
43fourierdlem2 44812 . . . . . . . . . . . . 13 (𝑀 ∈ β„• β†’ (𝑄 ∈ (π‘ƒβ€˜π‘€) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘„β€˜0) = 𝐴 ∧ (π‘„β€˜π‘€) = 𝐡) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1))))))
52, 4syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ (𝑄 ∈ (π‘ƒβ€˜π‘€) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘„β€˜0) = 𝐴 ∧ (π‘„β€˜π‘€) = 𝐡) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1))))))
61, 5mpbid 231 . . . . . . . . . . 11 (πœ‘ β†’ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((π‘„β€˜0) = 𝐴 ∧ (π‘„β€˜π‘€) = 𝐡) ∧ βˆ€π‘– ∈ (0..^𝑀)(π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1)))))
76simpld 496 . . . . . . . . . 10 (πœ‘ β†’ 𝑄 ∈ (ℝ ↑m (0...𝑀)))
8 elmapi 8840 . . . . . . . . . 10 (𝑄 ∈ (ℝ ↑m (0...𝑀)) β†’ 𝑄:(0...𝑀)βŸΆβ„)
97, 8syl 17 . . . . . . . . 9 (πœ‘ β†’ 𝑄:(0...𝑀)βŸΆβ„)
10 fzossfz 13648 . . . . . . . . . 10 (0..^𝑀) βŠ† (0...𝑀)
11 fourierdlem91.t . . . . . . . . . . . . 13 𝑇 = (𝐡 βˆ’ 𝐴)
12 fourierdlem91.e . . . . . . . . . . . . 13 𝐸 = (π‘₯ ∈ ℝ ↦ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)))
13 fourierdlem91.J . . . . . . . . . . . . 13 𝑍 = (𝑦 ∈ (𝐴(,]𝐡) ↦ if(𝑦 = 𝐡, 𝐴, 𝑦))
14 fourierdlem91.i . . . . . . . . . . . . 13 𝐼 = (π‘₯ ∈ ℝ ↦ sup({𝑖 ∈ (0..^𝑀) ∣ (π‘„β€˜π‘–) ≀ (π‘β€˜(πΈβ€˜π‘₯))}, ℝ, < ))
153, 2, 1, 11, 12, 13, 14fourierdlem37 44847 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐼:β„βŸΆ(0..^𝑀) ∧ (π‘₯ ∈ ℝ β†’ sup({𝑖 ∈ (0..^𝑀) ∣ (π‘„β€˜π‘–) ≀ (π‘β€˜(πΈβ€˜π‘₯))}, ℝ, < ) ∈ {𝑖 ∈ (0..^𝑀) ∣ (π‘„β€˜π‘–) ≀ (π‘β€˜(πΈβ€˜π‘₯))})))
1615simpld 496 . . . . . . . . . . 11 (πœ‘ β†’ 𝐼:β„βŸΆ(0..^𝑀))
17 fourierdlem91.c . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐢 ∈ ℝ)
18 fourierdlem91.d . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ 𝐷 ∈ (𝐢(,)+∞))
19 elioore 13351 . . . . . . . . . . . . . . . . . . 19 (𝐷 ∈ (𝐢(,)+∞) β†’ 𝐷 ∈ ℝ)
2018, 19syl 17 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐷 ∈ ℝ)
21 elioo4g 13381 . . . . . . . . . . . . . . . . . . . . 21 (𝐷 ∈ (𝐢(,)+∞) ↔ ((𝐢 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ) ∧ (𝐢 < 𝐷 ∧ 𝐷 < +∞)))
2218, 21sylib 217 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝐢 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ℝ) ∧ (𝐢 < 𝐷 ∧ 𝐷 < +∞)))
2322simprd 497 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (𝐢 < 𝐷 ∧ 𝐷 < +∞))
2423simpld 496 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ 𝐢 < 𝐷)
25 fourierdlem91.o . . . . . . . . . . . . . . . . . 18 𝑂 = (π‘š ∈ β„• ↦ {𝑝 ∈ (ℝ ↑m (0...π‘š)) ∣ (((π‘β€˜0) = 𝐢 ∧ (π‘β€˜π‘š) = 𝐷) ∧ βˆ€π‘– ∈ (0..^π‘š)(π‘β€˜π‘–) < (π‘β€˜(𝑖 + 1)))})
26 oveq1 7413 . . . . . . . . . . . . . . . . . . . . . 22 (𝑦 = π‘₯ β†’ (𝑦 + (π‘˜ Β· 𝑇)) = (π‘₯ + (π‘˜ Β· 𝑇)))
2726eleq1d 2819 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = π‘₯ β†’ ((𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
2827rexbidv 3179 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = π‘₯ β†’ (βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄))
2928cbvrabv 3443 . . . . . . . . . . . . . . . . . . 19 {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} = {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}
3029uneq2i 4160 . . . . . . . . . . . . . . . . . 18 ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}) = ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})
31 fourierdlem91.n . . . . . . . . . . . . . . . . . . 19 𝑁 = ((β™―β€˜π») βˆ’ 1)
32 fourierdlem91.h . . . . . . . . . . . . . . . . . . . . 21 𝐻 = ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})
3332fveq2i 6892 . . . . . . . . . . . . . . . . . . . 20 (β™―β€˜π») = (β™―β€˜({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))
3433oveq1i 7416 . . . . . . . . . . . . . . . . . . 19 ((β™―β€˜π») βˆ’ 1) = ((β™―β€˜({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})) βˆ’ 1)
3531, 34eqtri 2761 . . . . . . . . . . . . . . . . . 18 𝑁 = ((β™―β€˜({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})) βˆ’ 1)
36 fourierdlem91.s . . . . . . . . . . . . . . . . . . 19 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻))
37 isoeq5 7315 . . . . . . . . . . . . . . . . . . . . 21 (𝐻 = ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}) β†’ (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))))
3832, 37ax-mp 5 . . . . . . . . . . . . . . . . . . . 20 (𝑓 Isom < , < ((0...𝑁), 𝐻) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})))
3938iotabii 6526 . . . . . . . . . . . . . . . . . . 19 (℩𝑓𝑓 Isom < , < ((0...𝑁), 𝐻)) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})))
4036, 39eqtri 2761 . . . . . . . . . . . . . . . . . 18 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})))
4111, 3, 2, 1, 17, 20, 24, 25, 30, 35, 40fourierdlem54 44863 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)) ∧ 𝑆 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))))
4241simpld 496 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (𝑁 ∈ β„• ∧ 𝑆 ∈ (π‘‚β€˜π‘)))
4342simprd 497 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑆 ∈ (π‘‚β€˜π‘))
4442simpld 496 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝑁 ∈ β„•)
4525fourierdlem2 44812 . . . . . . . . . . . . . . . 16 (𝑁 ∈ β„• β†’ (𝑆 ∈ (π‘‚β€˜π‘) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((π‘†β€˜0) = 𝐢 ∧ (π‘†β€˜π‘) = 𝐷) ∧ βˆ€π‘– ∈ (0..^𝑁)(π‘†β€˜π‘–) < (π‘†β€˜(𝑖 + 1))))))
4644, 45syl 17 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝑆 ∈ (π‘‚β€˜π‘) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((π‘†β€˜0) = 𝐢 ∧ (π‘†β€˜π‘) = 𝐷) ∧ βˆ€π‘– ∈ (0..^𝑁)(π‘†β€˜π‘–) < (π‘†β€˜(𝑖 + 1))))))
4743, 46mpbid 231 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝑆 ∈ (ℝ ↑m (0...𝑁)) ∧ (((π‘†β€˜0) = 𝐢 ∧ (π‘†β€˜π‘) = 𝐷) ∧ βˆ€π‘– ∈ (0..^𝑁)(π‘†β€˜π‘–) < (π‘†β€˜(𝑖 + 1)))))
4847simpld 496 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑆 ∈ (ℝ ↑m (0...𝑁)))
49 elmapi 8840 . . . . . . . . . . . . 13 (𝑆 ∈ (ℝ ↑m (0...𝑁)) β†’ 𝑆:(0...𝑁)βŸΆβ„)
5048, 49syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆:(0...𝑁)βŸΆβ„)
51 fourierdlem91.17 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐽 ∈ (0..^𝑁))
52 elfzofz 13645 . . . . . . . . . . . . 13 (𝐽 ∈ (0..^𝑁) β†’ 𝐽 ∈ (0...𝑁))
5351, 52syl 17 . . . . . . . . . . . 12 (πœ‘ β†’ 𝐽 ∈ (0...𝑁))
5450, 53ffvelcdmd 7085 . . . . . . . . . . 11 (πœ‘ β†’ (π‘†β€˜π½) ∈ ℝ)
5516, 54ffvelcdmd 7085 . . . . . . . . . 10 (πœ‘ β†’ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))
5610, 55sselid 3980 . . . . . . . . 9 (πœ‘ β†’ (πΌβ€˜(π‘†β€˜π½)) ∈ (0...𝑀))
579, 56ffvelcdmd 7085 . . . . . . . 8 (πœ‘ β†’ (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ℝ)
5857rexrd 11261 . . . . . . 7 (πœ‘ β†’ (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ℝ*)
5958adantr 482 . . . . . 6 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ℝ*)
60 fzofzp1 13726 . . . . . . . . . 10 ((πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀) β†’ ((πΌβ€˜(π‘†β€˜π½)) + 1) ∈ (0...𝑀))
6155, 60syl 17 . . . . . . . . 9 (πœ‘ β†’ ((πΌβ€˜(π‘†β€˜π½)) + 1) ∈ (0...𝑀))
629, 61ffvelcdmd 7085 . . . . . . . 8 (πœ‘ β†’ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)) ∈ ℝ)
6362rexrd 11261 . . . . . . 7 (πœ‘ β†’ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)) ∈ ℝ*)
6463adantr 482 . . . . . 6 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)) ∈ ℝ*)
653, 2, 1fourierdlem11 44821 . . . . . . . . . . 11 (πœ‘ β†’ (𝐴 ∈ ℝ ∧ 𝐡 ∈ ℝ ∧ 𝐴 < 𝐡))
6665simp1d 1143 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 ∈ ℝ)
6766rexrd 11261 . . . . . . . . 9 (πœ‘ β†’ 𝐴 ∈ ℝ*)
6865simp2d 1144 . . . . . . . . 9 (πœ‘ β†’ 𝐡 ∈ ℝ)
69 iocssre 13401 . . . . . . . . 9 ((𝐴 ∈ ℝ* ∧ 𝐡 ∈ ℝ) β†’ (𝐴(,]𝐡) βŠ† ℝ)
7067, 68, 69syl2anc 585 . . . . . . . 8 (πœ‘ β†’ (𝐴(,]𝐡) βŠ† ℝ)
7165simp3d 1145 . . . . . . . . . 10 (πœ‘ β†’ 𝐴 < 𝐡)
7266, 68, 71, 11, 12fourierdlem4 44814 . . . . . . . . 9 (πœ‘ β†’ 𝐸:β„βŸΆ(𝐴(,]𝐡))
73 fzofzp1 13726 . . . . . . . . . . 11 (𝐽 ∈ (0..^𝑁) β†’ (𝐽 + 1) ∈ (0...𝑁))
7451, 73syl 17 . . . . . . . . . 10 (πœ‘ β†’ (𝐽 + 1) ∈ (0...𝑁))
7550, 74ffvelcdmd 7085 . . . . . . . . 9 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ ℝ)
7672, 75ffvelcdmd 7085 . . . . . . . 8 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ (𝐴(,]𝐡))
7770, 76sseldd 3983 . . . . . . 7 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ℝ)
7877adantr 482 . . . . . 6 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ℝ)
7966, 68iccssred 13408 . . . . . . . . 9 (πœ‘ β†’ (𝐴[,]𝐡) βŠ† ℝ)
8066, 68, 71, 13fourierdlem17 44827 . . . . . . . . . 10 (πœ‘ β†’ 𝑍:(𝐴(,]𝐡)⟢(𝐴[,]𝐡))
8172, 54ffvelcdmd 7085 . . . . . . . . . 10 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜π½)) ∈ (𝐴(,]𝐡))
8280, 81ffvelcdmd 7085 . . . . . . . . 9 (πœ‘ β†’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½))) ∈ (𝐴[,]𝐡))
8379, 82sseldd 3983 . . . . . . . 8 (πœ‘ β†’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½))) ∈ ℝ)
8447simprrd 773 . . . . . . . . . . . . . 14 (πœ‘ β†’ βˆ€π‘– ∈ (0..^𝑁)(π‘†β€˜π‘–) < (π‘†β€˜(𝑖 + 1)))
85 fveq2 6889 . . . . . . . . . . . . . . . 16 (𝑖 = 𝐽 β†’ (π‘†β€˜π‘–) = (π‘†β€˜π½))
86 oveq1 7413 . . . . . . . . . . . . . . . . 17 (𝑖 = 𝐽 β†’ (𝑖 + 1) = (𝐽 + 1))
8786fveq2d 6893 . . . . . . . . . . . . . . . 16 (𝑖 = 𝐽 β†’ (π‘†β€˜(𝑖 + 1)) = (π‘†β€˜(𝐽 + 1)))
8885, 87breq12d 5161 . . . . . . . . . . . . . . 15 (𝑖 = 𝐽 β†’ ((π‘†β€˜π‘–) < (π‘†β€˜(𝑖 + 1)) ↔ (π‘†β€˜π½) < (π‘†β€˜(𝐽 + 1))))
8988rspccva 3612 . . . . . . . . . . . . . 14 ((βˆ€π‘– ∈ (0..^𝑁)(π‘†β€˜π‘–) < (π‘†β€˜(𝑖 + 1)) ∧ 𝐽 ∈ (0..^𝑁)) β†’ (π‘†β€˜π½) < (π‘†β€˜(𝐽 + 1)))
9084, 51, 89syl2anc 585 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘†β€˜π½) < (π‘†β€˜(𝐽 + 1)))
9154, 75posdifd 11798 . . . . . . . . . . . . 13 (πœ‘ β†’ ((π‘†β€˜π½) < (π‘†β€˜(𝐽 + 1)) ↔ 0 < ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))))
9290, 91mpbid 231 . . . . . . . . . . . 12 (πœ‘ β†’ 0 < ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½)))
93 eleq1 2822 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐽 β†’ (𝑗 ∈ (0..^𝑁) ↔ 𝐽 ∈ (0..^𝑁)))
9493anbi2d 630 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐽 β†’ ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) ↔ (πœ‘ ∧ 𝐽 ∈ (0..^𝑁))))
95 oveq1 7413 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝐽 β†’ (𝑗 + 1) = (𝐽 + 1))
9695fveq2d 6893 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝐽 β†’ (π‘†β€˜(𝑗 + 1)) = (π‘†β€˜(𝐽 + 1)))
9796fveq2d 6893 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝐽 β†’ (πΈβ€˜(π‘†β€˜(𝑗 + 1))) = (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
98 fveq2 6889 . . . . . . . . . . . . . . . . . . . 20 (𝑗 = 𝐽 β†’ (π‘†β€˜π‘—) = (π‘†β€˜π½))
9998fveq2d 6893 . . . . . . . . . . . . . . . . . . 19 (𝑗 = 𝐽 β†’ (πΈβ€˜(π‘†β€˜π‘—)) = (πΈβ€˜(π‘†β€˜π½)))
10099fveq2d 6893 . . . . . . . . . . . . . . . . . 18 (𝑗 = 𝐽 β†’ (π‘β€˜(πΈβ€˜(π‘†β€˜π‘—))) = (π‘β€˜(πΈβ€˜(π‘†β€˜π½))))
10197, 100oveq12d 7424 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐽 β†’ ((πΈβ€˜(π‘†β€˜(𝑗 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π‘—)))) = ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½)))))
10296, 98oveq12d 7424 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐽 β†’ ((π‘†β€˜(𝑗 + 1)) βˆ’ (π‘†β€˜π‘—)) = ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½)))
103101, 102eqeq12d 2749 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐽 β†’ (((πΈβ€˜(π‘†β€˜(𝑗 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π‘—)))) = ((π‘†β€˜(𝑗 + 1)) βˆ’ (π‘†β€˜π‘—)) ↔ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½)))) = ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))))
10494, 103imbi12d 345 . . . . . . . . . . . . . . 15 (𝑗 = 𝐽 β†’ (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ ((πΈβ€˜(π‘†β€˜(𝑗 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π‘—)))) = ((π‘†β€˜(𝑗 + 1)) βˆ’ (π‘†β€˜π‘—))) ↔ ((πœ‘ ∧ 𝐽 ∈ (0..^𝑁)) β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½)))) = ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½)))))
10511oveq2i 7417 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘˜ Β· 𝑇) = (π‘˜ Β· (𝐡 βˆ’ 𝐴))
106105oveq2i 7417 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 + (π‘˜ Β· 𝑇)) = (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴)))
107106eleq1i 2825 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄)
108107rexbii 3095 . . . . . . . . . . . . . . . . . . . . . 22 (βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄)
109108rgenw 3066 . . . . . . . . . . . . . . . . . . . . 21 βˆ€π‘¦ ∈ (𝐢[,]𝐷)(βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄)
110 rabbi 3463 . . . . . . . . . . . . . . . . . . . . 21 (βˆ€π‘¦ ∈ (𝐢[,]𝐷)(βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄 ↔ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄) ↔ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄})
111109, 110mpbi 229 . . . . . . . . . . . . . . . . . . . 20 {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄} = {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄}
112111uneq2i 4160 . . . . . . . . . . . . . . . . . . 19 ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}) = ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄})
113112fveq2i 6892 . . . . . . . . . . . . . . . . . 18 (β™―β€˜({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})) = (β™―β€˜({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄}))
114113oveq1i 7416 . . . . . . . . . . . . . . . . 17 ((β™―β€˜({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})) βˆ’ 1) = ((β™―β€˜({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄})) βˆ’ 1)
11535, 114eqtri 2761 . . . . . . . . . . . . . . . 16 𝑁 = ((β™―β€˜({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄})) βˆ’ 1)
116 isoeq5 7315 . . . . . . . . . . . . . . . . . . 19 (({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}) = ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄}) β†’ (𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄}))))
117112, 116ax-mp 5 . . . . . . . . . . . . . . . . . 18 (𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})) ↔ 𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄})))
118117iotabii 6526 . . . . . . . . . . . . . . . . 17 (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· 𝑇)) ∈ ran 𝑄}))) = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄})))
11940, 118eqtri 2761 . . . . . . . . . . . . . . . 16 𝑆 = (℩𝑓𝑓 Isom < , < ((0...𝑁), ({𝐢, 𝐷} βˆͺ {𝑦 ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (𝑦 + (π‘˜ Β· (𝐡 βˆ’ 𝐴))) ∈ ran 𝑄})))
120 eqid 2733 . . . . . . . . . . . . . . . 16 ((π‘†β€˜π‘—) + (𝐡 βˆ’ (πΈβ€˜(π‘†β€˜π‘—)))) = ((π‘†β€˜π‘—) + (𝐡 βˆ’ (πΈβ€˜(π‘†β€˜π‘—))))
1213, 11, 2, 1, 17, 18, 25, 115, 119, 12, 13, 120fourierdlem65 44874 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ ((πΈβ€˜(π‘†β€˜(𝑗 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π‘—)))) = ((π‘†β€˜(𝑗 + 1)) βˆ’ (π‘†β€˜π‘—)))
122104, 121vtoclg 3557 . . . . . . . . . . . . . 14 (𝐽 ∈ (0..^𝑁) β†’ ((πœ‘ ∧ 𝐽 ∈ (0..^𝑁)) β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½)))) = ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))))
123122anabsi7 670 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐽 ∈ (0..^𝑁)) β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½)))) = ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½)))
12451, 123mpdan 686 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½)))) = ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½)))
12592, 124breqtrrd 5176 . . . . . . . . . . 11 (πœ‘ β†’ 0 < ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½)))))
12683, 77posdifd 11798 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) < (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ↔ 0 < ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½))))))
127125, 126mpbird 257 . . . . . . . . . 10 (πœ‘ β†’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½))) < (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
128100, 97oveq12d 7424 . . . . . . . . . . . . . . 15 (𝑗 = 𝐽 β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π‘—)))(,)(πΈβ€˜(π‘†β€˜(𝑗 + 1)))) = ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
12998fveq2d 6893 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐽 β†’ (πΌβ€˜(π‘†β€˜π‘—)) = (πΌβ€˜(π‘†β€˜π½)))
130129fveq2d 6893 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐽 β†’ (π‘„β€˜(πΌβ€˜(π‘†β€˜π‘—))) = (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))))
131129oveq1d 7421 . . . . . . . . . . . . . . . . 17 (𝑗 = 𝐽 β†’ ((πΌβ€˜(π‘†β€˜π‘—)) + 1) = ((πΌβ€˜(π‘†β€˜π½)) + 1))
132131fveq2d 6893 . . . . . . . . . . . . . . . 16 (𝑗 = 𝐽 β†’ (π‘„β€˜((πΌβ€˜(π‘†β€˜π‘—)) + 1)) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))
133130, 132oveq12d 7424 . . . . . . . . . . . . . . 15 (𝑗 = 𝐽 β†’ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π‘—)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π‘—)) + 1))) = ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
134128, 133sseq12d 4015 . . . . . . . . . . . . . 14 (𝑗 = 𝐽 β†’ (((π‘β€˜(πΈβ€˜(π‘†β€˜π‘—)))(,)(πΈβ€˜(π‘†β€˜(𝑗 + 1)))) βŠ† ((π‘„β€˜(πΌβ€˜(π‘†β€˜π‘—)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π‘—)) + 1))) ↔ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βŠ† ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))))
13594, 134imbi12d 345 . . . . . . . . . . . . 13 (𝑗 = 𝐽 β†’ (((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π‘—)))(,)(πΈβ€˜(π‘†β€˜(𝑗 + 1)))) βŠ† ((π‘„β€˜(πΌβ€˜(π‘†β€˜π‘—)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π‘—)) + 1)))) ↔ ((πœ‘ ∧ 𝐽 ∈ (0..^𝑁)) β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βŠ† ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))))
13632, 30eqtri 2761 . . . . . . . . . . . . . 14 𝐻 = ({𝐢, 𝐷} βˆͺ {π‘₯ ∈ (𝐢[,]𝐷) ∣ βˆƒπ‘˜ ∈ β„€ (π‘₯ + (π‘˜ Β· 𝑇)) ∈ ran 𝑄})
137 eqid 2733 . . . . . . . . . . . . . 14 ((π‘†β€˜π‘—) + if(((π‘†β€˜(𝑗 + 1)) βˆ’ (π‘†β€˜π‘—)) < ((π‘„β€˜1) βˆ’ 𝐴), (((π‘†β€˜(𝑗 + 1)) βˆ’ (π‘†β€˜π‘—)) / 2), (((π‘„β€˜1) βˆ’ 𝐴) / 2))) = ((π‘†β€˜π‘—) + if(((π‘†β€˜(𝑗 + 1)) βˆ’ (π‘†β€˜π‘—)) < ((π‘„β€˜1) βˆ’ 𝐴), (((π‘†β€˜(𝑗 + 1)) βˆ’ (π‘†β€˜π‘—)) / 2), (((π‘„β€˜1) βˆ’ 𝐴) / 2)))
13811, 3, 2, 1, 17, 20, 24, 25, 136, 31, 36, 12, 13, 137, 14fourierdlem79 44888 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑗 ∈ (0..^𝑁)) β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π‘—)))(,)(πΈβ€˜(π‘†β€˜(𝑗 + 1)))) βŠ† ((π‘„β€˜(πΌβ€˜(π‘†β€˜π‘—)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π‘—)) + 1))))
139135, 138vtoclg 3557 . . . . . . . . . . . 12 (𝐽 ∈ (0..^𝑁) β†’ ((πœ‘ ∧ 𝐽 ∈ (0..^𝑁)) β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βŠ† ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))))
140139anabsi7 670 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐽 ∈ (0..^𝑁)) β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βŠ† ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
14151, 140mpdan 686 . . . . . . . . . 10 (πœ‘ β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βŠ† ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
14257, 62, 83, 77, 127, 141fourierdlem10 44820 . . . . . . . . 9 (πœ‘ β†’ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½))) ≀ (π‘β€˜(πΈβ€˜(π‘†β€˜π½))) ∧ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ≀ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
143142simpld 496 . . . . . . . 8 (πœ‘ β†’ (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))) ≀ (π‘β€˜(πΈβ€˜(π‘†β€˜π½))))
14457, 83, 77, 143, 127lelttrd 11369 . . . . . . 7 (πœ‘ β†’ (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))) < (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
145144adantr 482 . . . . . 6 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))) < (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
14662adantr 482 . . . . . . 7 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)) ∈ ℝ)
147142simprd 497 . . . . . . . 8 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ≀ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))
148147adantr 482 . . . . . . 7 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ≀ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))
149 neqne 2949 . . . . . . . . 9 (Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) β‰  (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))
150149necomd 2997 . . . . . . . 8 (Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)) β†’ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)) β‰  (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
151150adantl 483 . . . . . . 7 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)) β‰  (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
15278, 146, 148, 151leneltd 11365 . . . . . 6 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) < (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))
15359, 64, 78, 145, 152eliood 44198 . . . . 5 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
154 fvres 6908 . . . . 5 ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) = (πΉβ€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
155153, 154syl 17 . . . 4 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) = (πΉβ€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
156155eqcomd 2739 . . 3 ((πœ‘ ∧ Β¬ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) β†’ (πΉβ€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) = ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
157156ifeq2da 4560 . 2 (πœ‘ β†’ if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), (πΉβ€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) = if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
158 fourierdlem91.f . . . . . 6 (πœ‘ β†’ 𝐹:β„βŸΆβ„‚)
159 fdm 6724 . . . . . . . 8 (𝐹:β„βŸΆβ„‚ β†’ dom 𝐹 = ℝ)
160158, 159syl 17 . . . . . . 7 (πœ‘ β†’ dom 𝐹 = ℝ)
161160feq2d 6701 . . . . . 6 (πœ‘ β†’ (𝐹:dom πΉβŸΆβ„‚ ↔ 𝐹:β„βŸΆβ„‚))
162158, 161mpbird 257 . . . . 5 (πœ‘ β†’ 𝐹:dom πΉβŸΆβ„‚)
163 ioosscn 13383 . . . . . 6 ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βŠ† β„‚
164163a1i 11 . . . . 5 (πœ‘ β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βŠ† β„‚)
165 ioossre 13382 . . . . . 6 ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βŠ† ℝ
166165, 160sseqtrrid 4035 . . . . 5 (πœ‘ β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βŠ† dom 𝐹)
167 fourierdlem91.u . . . . . . 7 π‘ˆ = ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))
16875, 77resubcld 11639 . . . . . . 7 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) ∈ ℝ)
169167, 168eqeltrid 2838 . . . . . 6 (πœ‘ β†’ π‘ˆ ∈ ℝ)
170169recnd 11239 . . . . 5 (πœ‘ β†’ π‘ˆ ∈ β„‚)
171 eqid 2733 . . . . 5 {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)} = {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)}
17283, 77, 169iooshift 44222 . . . . . 6 (πœ‘ β†’ (((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) + π‘ˆ)(,)((πΈβ€˜(π‘†β€˜(𝐽 + 1))) + π‘ˆ)) = {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)})
173 ioossre 13382 . . . . . . 7 (((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) + π‘ˆ)(,)((πΈβ€˜(π‘†β€˜(𝐽 + 1))) + π‘ˆ)) βŠ† ℝ
174173, 160sseqtrrid 4035 . . . . . 6 (πœ‘ β†’ (((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) + π‘ˆ)(,)((πΈβ€˜(π‘†β€˜(𝐽 + 1))) + π‘ˆ)) βŠ† dom 𝐹)
175172, 174eqsstrrd 4021 . . . . 5 (πœ‘ β†’ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)} βŠ† dom 𝐹)
176 elioore 13351 . . . . . 6 (𝑦 ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1)))) β†’ 𝑦 ∈ ℝ)
17768, 66resubcld 11639 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐡 βˆ’ 𝐴) ∈ ℝ)
17811, 177eqeltrid 2838 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝑇 ∈ ℝ)
179178recnd 11239 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑇 ∈ β„‚)
18066, 68posdifd 11798 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐴 < 𝐡 ↔ 0 < (𝐡 βˆ’ 𝐴)))
18171, 180mpbid 231 . . . . . . . . . . . . . 14 (πœ‘ β†’ 0 < (𝐡 βˆ’ 𝐴))
182181, 11breqtrrdi 5190 . . . . . . . . . . . . 13 (πœ‘ β†’ 0 < 𝑇)
183182gt0ne0d 11775 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑇 β‰  0)
184170, 179, 183divcan1d 11988 . . . . . . . . . . 11 (πœ‘ β†’ ((π‘ˆ / 𝑇) Β· 𝑇) = π‘ˆ)
185184eqcomd 2739 . . . . . . . . . 10 (πœ‘ β†’ π‘ˆ = ((π‘ˆ / 𝑇) Β· 𝑇))
186185oveq2d 7422 . . . . . . . . 9 (πœ‘ β†’ (𝑦 + π‘ˆ) = (𝑦 + ((π‘ˆ / 𝑇) Β· 𝑇)))
187186adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ (𝑦 + π‘ˆ) = (𝑦 + ((π‘ˆ / 𝑇) Β· 𝑇)))
188187fveq2d 6893 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ (πΉβ€˜(𝑦 + π‘ˆ)) = (πΉβ€˜(𝑦 + ((π‘ˆ / 𝑇) Β· 𝑇))))
189158adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ 𝐹:β„βŸΆβ„‚)
190178adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ 𝑇 ∈ ℝ)
19177recnd 11239 . . . . . . . . . . . . . 14 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) ∈ β„‚)
19275recnd 11239 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘†β€˜(𝐽 + 1)) ∈ β„‚)
193191, 192negsubdi2d 11584 . . . . . . . . . . . . 13 (πœ‘ β†’ -((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
194193eqcomd 2739 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) = -((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))))
195194oveq1d 7421 . . . . . . . . . . 11 (πœ‘ β†’ (((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) / 𝑇) = (-((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇))
196167oveq1i 7416 . . . . . . . . . . . 12 (π‘ˆ / 𝑇) = (((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) / 𝑇)
197196a1i 11 . . . . . . . . . . 11 (πœ‘ β†’ (π‘ˆ / 𝑇) = (((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) / 𝑇))
19812a1i 11 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐸 = (π‘₯ ∈ ℝ ↦ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇))))
199 id 22 . . . . . . . . . . . . . . . . . 18 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ π‘₯ = (π‘†β€˜(𝐽 + 1)))
200 oveq2 7414 . . . . . . . . . . . . . . . . . . . . 21 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (𝐡 βˆ’ π‘₯) = (𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))))
201200oveq1d 7421 . . . . . . . . . . . . . . . . . . . 20 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ ((𝐡 βˆ’ π‘₯) / 𝑇) = ((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇))
202201fveq2d 6893 . . . . . . . . . . . . . . . . . . 19 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) = (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)))
203202oveq1d 7421 . . . . . . . . . . . . . . . . . 18 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇) = ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇))
204199, 203oveq12d 7424 . . . . . . . . . . . . . . . . 17 (π‘₯ = (π‘†β€˜(𝐽 + 1)) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
205204adantl 483 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘₯ = (π‘†β€˜(𝐽 + 1))) β†’ (π‘₯ + ((βŒŠβ€˜((𝐡 βˆ’ π‘₯) / 𝑇)) Β· 𝑇)) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
20668, 75resubcld 11639 . . . . . . . . . . . . . . . . . . . . 21 (πœ‘ β†’ (𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ ℝ)
207206, 178, 183redivcld 12039 . . . . . . . . . . . . . . . . . . . 20 (πœ‘ β†’ ((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇) ∈ ℝ)
208207flcld 13760 . . . . . . . . . . . . . . . . . . 19 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ β„€)
209208zred 12663 . . . . . . . . . . . . . . . . . 18 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ ℝ)
210209, 178remulcld 11241 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇) ∈ ℝ)
21175, 210readdcld 11240 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)) ∈ ℝ)
212198, 205, 75, 211fvmptd 7003 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))) = ((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)))
213212oveq1d 7421 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) = (((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)) βˆ’ (π‘†β€˜(𝐽 + 1))))
214208zcnd 12664 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) ∈ β„‚)
215214, 179mulcld 11231 . . . . . . . . . . . . . . 15 (πœ‘ β†’ ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇) ∈ β„‚)
216192, 215pncan2d 11570 . . . . . . . . . . . . . 14 (πœ‘ β†’ (((π‘†β€˜(𝐽 + 1)) + ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇)) βˆ’ (π‘†β€˜(𝐽 + 1))) = ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇))
217213, 216eqtrd 2773 . . . . . . . . . . . . 13 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) = ((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇))
218217, 215eqeltrd 2834 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) ∈ β„‚)
219218, 179, 183divnegd 12000 . . . . . . . . . . 11 (πœ‘ β†’ -(((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇) = (-((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇))
220195, 197, 2193eqtr4d 2783 . . . . . . . . . 10 (πœ‘ β†’ (π‘ˆ / 𝑇) = -(((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇))
221217oveq1d 7421 . . . . . . . . . . . . 13 (πœ‘ β†’ (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇) = (((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇) / 𝑇))
222214, 179, 183divcan4d 11993 . . . . . . . . . . . . 13 (πœ‘ β†’ (((βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)) Β· 𝑇) / 𝑇) = (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)))
223221, 222eqtrd 2773 . . . . . . . . . . . 12 (πœ‘ β†’ (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇) = (βŒŠβ€˜((𝐡 βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇)))
224223, 208eqeltrd 2834 . . . . . . . . . . 11 (πœ‘ β†’ (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇) ∈ β„€)
225224znegcld 12665 . . . . . . . . . 10 (πœ‘ β†’ -(((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘†β€˜(𝐽 + 1))) / 𝑇) ∈ β„€)
226220, 225eqeltrd 2834 . . . . . . . . 9 (πœ‘ β†’ (π‘ˆ / 𝑇) ∈ β„€)
227226adantr 482 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ (π‘ˆ / 𝑇) ∈ β„€)
228 simpr 486 . . . . . . . 8 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ 𝑦 ∈ ℝ)
229 fourierdlem91.6 . . . . . . . . 9 ((πœ‘ ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜(π‘₯ + 𝑇)) = (πΉβ€˜π‘₯))
230229adantlr 714 . . . . . . . 8 (((πœ‘ ∧ 𝑦 ∈ ℝ) ∧ π‘₯ ∈ ℝ) β†’ (πΉβ€˜(π‘₯ + 𝑇)) = (πΉβ€˜π‘₯))
231189, 190, 227, 228, 230fperiodmul 44001 . . . . . . 7 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ (πΉβ€˜(𝑦 + ((π‘ˆ / 𝑇) Β· 𝑇))) = (πΉβ€˜π‘¦))
232188, 231eqtrd 2773 . . . . . 6 ((πœ‘ ∧ 𝑦 ∈ ℝ) β†’ (πΉβ€˜(𝑦 + π‘ˆ)) = (πΉβ€˜π‘¦))
233176, 232sylan2 594 . . . . 5 ((πœ‘ ∧ 𝑦 ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) β†’ (πΉβ€˜(𝑦 + π‘ˆ)) = (πΉβ€˜π‘¦))
2346simprrd 773 . . . . . . . 8 (πœ‘ β†’ βˆ€π‘– ∈ (0..^𝑀)(π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1)))
235 fveq2 6889 . . . . . . . . . 10 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (π‘„β€˜π‘–) = (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))))
236 oveq1 7413 . . . . . . . . . . 11 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (𝑖 + 1) = ((πΌβ€˜(π‘†β€˜π½)) + 1))
237236fveq2d 6893 . . . . . . . . . 10 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (π‘„β€˜(𝑖 + 1)) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))
238235, 237breq12d 5161 . . . . . . . . 9 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ ((π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1)) ↔ (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))) < (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
239238rspccva 3612 . . . . . . . 8 ((βˆ€π‘– ∈ (0..^𝑀)(π‘„β€˜π‘–) < (π‘„β€˜(𝑖 + 1)) ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀)) β†’ (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))) < (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))
240234, 55, 239syl2anc 585 . . . . . . 7 (πœ‘ β†’ (π‘„β€˜(πΌβ€˜(π‘†β€˜π½))) < (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))
24155ancli 550 . . . . . . . 8 (πœ‘ β†’ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀)))
242 eleq1 2822 . . . . . . . . . . 11 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (𝑖 ∈ (0..^𝑀) ↔ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀)))
243242anbi2d 630 . . . . . . . . . 10 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) ↔ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))))
244235, 237oveq12d 7424 . . . . . . . . . . . 12 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1))) = ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
245244reseq2d 5980 . . . . . . . . . . 11 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) = (𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))))
246244oveq1d 7421 . . . . . . . . . . 11 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚) = (((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))–cnβ†’β„‚))
247245, 246eleq12d 2828 . . . . . . . . . 10 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) ∈ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚) ↔ (𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) ∈ (((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))–cnβ†’β„‚)))
248243, 247imbi12d 345 . . . . . . . . 9 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) ∈ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚)) ↔ ((πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) ∈ (((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))–cnβ†’β„‚))))
249 fourierdlem91.fcn . . . . . . . . 9 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) ∈ (((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))–cnβ†’β„‚))
250248, 249vtoclg 3557 . . . . . . . 8 ((πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀) β†’ ((πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀)) β†’ (𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) ∈ (((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))–cnβ†’β„‚)))
25155, 241, 250sylc 65 . . . . . . 7 (πœ‘ β†’ (𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) ∈ (((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))–cnβ†’β„‚))
252 nfv 1918 . . . . . . . . . 10 Ⅎ𝑖(πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))
253 fourierdlem91.w . . . . . . . . . . . . 13 π‘Š = (𝑖 ∈ (0..^𝑀) ↦ 𝐿)
254 nfmpt1 5256 . . . . . . . . . . . . 13 Ⅎ𝑖(𝑖 ∈ (0..^𝑀) ↦ 𝐿)
255253, 254nfcxfr 2902 . . . . . . . . . . . 12 β„²π‘–π‘Š
256 nfcv 2904 . . . . . . . . . . . 12 Ⅎ𝑖(πΌβ€˜(π‘†β€˜π½))
257255, 256nffv 6899 . . . . . . . . . . 11 Ⅎ𝑖(π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½)))
258257nfel1 2920 . . . . . . . . . 10 Ⅎ𝑖(π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))
259252, 258nfim 1900 . . . . . . . . 9 Ⅎ𝑖((πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀)) β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
260243biimpar 479 . . . . . . . . . . . . . 14 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ (πœ‘ ∧ 𝑖 ∈ (0..^𝑀)))
2612603adant2 1132 . . . . . . . . . . . . 13 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1)))) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ (πœ‘ ∧ 𝑖 ∈ (0..^𝑀)))
262 fourierdlem91.l . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
263261, 262syl 17 . . . . . . . . . . . 12 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1)))) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
264 fveq2 6889 . . . . . . . . . . . . . . . 16 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (π‘Šβ€˜π‘–) = (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))))
265264eqcomd 2739 . . . . . . . . . . . . . . 15 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) = (π‘Šβ€˜π‘–))
266265adantr 482 . . . . . . . . . . . . . 14 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) = (π‘Šβ€˜π‘–))
267260simprd 497 . . . . . . . . . . . . . . 15 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ 𝑖 ∈ (0..^𝑀))
268 elex 3493 . . . . . . . . . . . . . . . 16 (𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))) β†’ 𝐿 ∈ V)
269260, 262, 2683syl 18 . . . . . . . . . . . . . . 15 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ 𝐿 ∈ V)
270253fvmpt2 7007 . . . . . . . . . . . . . . 15 ((𝑖 ∈ (0..^𝑀) ∧ 𝐿 ∈ V) β†’ (π‘Šβ€˜π‘–) = 𝐿)
271267, 269, 270syl2anc 585 . . . . . . . . . . . . . 14 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ (π‘Šβ€˜π‘–) = 𝐿)
272266, 271eqtrd 2773 . . . . . . . . . . . . 13 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) = 𝐿)
2732723adant2 1132 . . . . . . . . . . . 12 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1)))) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) = 𝐿)
274245, 237oveq12d 7424 . . . . . . . . . . . . . 14 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))) = ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
275274eqcomd 2739 . . . . . . . . . . . . 13 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) = ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
2762753ad2ant1 1134 . . . . . . . . . . . 12 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1)))) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) = ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))
277263, 273, 2763eltr4d 2849 . . . . . . . . . . 11 ((𝑖 = (πΌβ€˜(π‘†β€˜π½)) ∧ ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1)))) ∧ (πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀))) β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
2782773exp 1120 . . . . . . . . . 10 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1)))) β†’ ((πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀)) β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))))
2792622a1i 12 . . . . . . . . . 10 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (((πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀)) β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) β†’ ((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1))))))
280278, 279impbid 211 . . . . . . . . 9 (𝑖 = (πΌβ€˜(π‘†β€˜π½)) β†’ (((πœ‘ ∧ 𝑖 ∈ (0..^𝑀)) β†’ 𝐿 ∈ ((𝐹 β†Ύ ((π‘„β€˜π‘–)(,)(π‘„β€˜(𝑖 + 1)))) limβ„‚ (π‘„β€˜(𝑖 + 1)))) ↔ ((πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀)) β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))))
281259, 280, 262vtoclg1f 3556 . . . . . . . 8 ((πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀) β†’ ((πœ‘ ∧ (πΌβ€˜(π‘†β€˜π½)) ∈ (0..^𝑀)) β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))))
28255, 241, 281sylc 65 . . . . . . 7 (πœ‘ β†’ (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))) ∈ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) limβ„‚ (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))
283 eqid 2733 . . . . . . 7 if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) = if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
284 eqid 2733 . . . . . . 7 ((TopOpenβ€˜β„‚fld) β†Ύt (((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) βˆͺ {(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))})) = ((TopOpenβ€˜β„‚fld) β†Ύt (((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))) βˆͺ {(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))}))
28557, 62, 240, 251, 282, 83, 77, 127, 141, 283, 284fourierdlem33 44843 . . . . . 6 (πœ‘ β†’ if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) ∈ (((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) β†Ύ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) limβ„‚ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
286141resabs1d 6011 . . . . . . 7 (πœ‘ β†’ ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) β†Ύ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) = (𝐹 β†Ύ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
287286oveq1d 7421 . . . . . 6 (πœ‘ β†’ (((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)))) β†Ύ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) limβ„‚ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) = ((𝐹 β†Ύ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) limβ„‚ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
288285, 287eleqtrd 2836 . . . . 5 (πœ‘ β†’ if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) ∈ ((𝐹 β†Ύ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) limβ„‚ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
289162, 164, 166, 170, 171, 175, 233, 288limcperiod 44331 . . . 4 (πœ‘ β†’ if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) ∈ ((𝐹 β†Ύ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)}) limβ„‚ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) + π‘ˆ)))
290167oveq2i 7417 . . . . . 6 ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) + π‘ˆ) = ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) + ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
291191, 192pncan3d 11571 . . . . . 6 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) + ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) = (π‘†β€˜(𝐽 + 1)))
292290, 291eqtrid 2785 . . . . 5 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) + π‘ˆ) = (π‘†β€˜(𝐽 + 1)))
293292oveq2d 7422 . . . 4 (πœ‘ β†’ ((𝐹 β†Ύ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)}) limβ„‚ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) + π‘ˆ)) = ((𝐹 β†Ύ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)}) limβ„‚ (π‘†β€˜(𝐽 + 1))))
294289, 293eleqtrd 2836 . . 3 (πœ‘ β†’ if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) ∈ ((𝐹 β†Ύ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)}) limβ„‚ (π‘†β€˜(𝐽 + 1))))
295167oveq2i 7417 . . . . . . . . 9 ((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) + π‘ˆ) = ((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) + ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))))
296295a1i 11 . . . . . . . 8 (πœ‘ β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) + π‘ˆ) = ((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) + ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
29717, 20iccssred 13408 . . . . . . . . . . . . . . 15 (πœ‘ β†’ (𝐢[,]𝐷) βŠ† ℝ)
298 ax-resscn 11164 . . . . . . . . . . . . . . 15 ℝ βŠ† β„‚
299297, 298sstrdi 3994 . . . . . . . . . . . . . 14 (πœ‘ β†’ (𝐢[,]𝐷) βŠ† β„‚)
30025, 44, 43fourierdlem15 44825 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝑆:(0...𝑁)⟢(𝐢[,]𝐷))
301300, 53ffvelcdmd 7085 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘†β€˜π½) ∈ (𝐢[,]𝐷))
302299, 301sseldd 3983 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘†β€˜π½) ∈ β„‚)
303192, 302subcld 11568 . . . . . . . . . . . 12 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½)) ∈ β„‚)
30483recnd 11239 . . . . . . . . . . . 12 (πœ‘ β†’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½))) ∈ β„‚)
305191, 303, 304subsub23d 43984 . . . . . . . . . . 11 (πœ‘ β†’ (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) = (π‘β€˜(πΈβ€˜(π‘†β€˜π½))) ↔ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½)))) = ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))))
306124, 305mpbird 257 . . . . . . . . . 10 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) = (π‘β€˜(πΈβ€˜(π‘†β€˜π½))))
307306eqcomd 2739 . . . . . . . . 9 (πœ‘ β†’ (π‘β€˜(πΈβ€˜(π‘†β€˜π½))) = ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))))
308307oveq1d 7421 . . . . . . . 8 (πœ‘ β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) + ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) = (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) + ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
309191, 303subcld 11568 . . . . . . . . . 10 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) ∈ β„‚)
310309, 192, 191addsub12d 11591 . . . . . . . . 9 (πœ‘ β†’ (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) + ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) = ((π‘†β€˜(𝐽 + 1)) + (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))))
311191, 303, 191sub32d 11600 . . . . . . . . . . 11 (πœ‘ β†’ (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) = (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))))
312191subidd 11556 . . . . . . . . . . . 12 (πœ‘ β†’ ((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) = 0)
313312oveq1d 7421 . . . . . . . . . . 11 (πœ‘ β†’ (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) = (0 βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))))
314 df-neg 11444 . . . . . . . . . . . 12 -((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½)) = (0 βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½)))
315192, 302negsubdi2d 11584 . . . . . . . . . . . 12 (πœ‘ β†’ -((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½)) = ((π‘†β€˜π½) βˆ’ (π‘†β€˜(𝐽 + 1))))
316314, 315eqtr3id 2787 . . . . . . . . . . 11 (πœ‘ β†’ (0 βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) = ((π‘†β€˜π½) βˆ’ (π‘†β€˜(𝐽 + 1))))
317311, 313, 3163eqtrd 2777 . . . . . . . . . 10 (πœ‘ β†’ (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1)))) = ((π‘†β€˜π½) βˆ’ (π‘†β€˜(𝐽 + 1))))
318317oveq2d 7422 . . . . . . . . 9 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) + (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) = ((π‘†β€˜(𝐽 + 1)) + ((π‘†β€˜π½) βˆ’ (π‘†β€˜(𝐽 + 1)))))
319192, 302pncan3d 11571 . . . . . . . . 9 (πœ‘ β†’ ((π‘†β€˜(𝐽 + 1)) + ((π‘†β€˜π½) βˆ’ (π‘†β€˜(𝐽 + 1)))) = (π‘†β€˜π½))
320310, 318, 3193eqtrd 2777 . . . . . . . 8 (πœ‘ β†’ (((πΈβ€˜(π‘†β€˜(𝐽 + 1))) βˆ’ ((π‘†β€˜(𝐽 + 1)) βˆ’ (π‘†β€˜π½))) + ((π‘†β€˜(𝐽 + 1)) βˆ’ (πΈβ€˜(π‘†β€˜(𝐽 + 1))))) = (π‘†β€˜π½))
321296, 308, 3203eqtrd 2777 . . . . . . 7 (πœ‘ β†’ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) + π‘ˆ) = (π‘†β€˜π½))
322321, 292oveq12d 7424 . . . . . 6 (πœ‘ β†’ (((π‘β€˜(πΈβ€˜(π‘†β€˜π½))) + π‘ˆ)(,)((πΈβ€˜(π‘†β€˜(𝐽 + 1))) + π‘ˆ)) = ((π‘†β€˜π½)(,)(π‘†β€˜(𝐽 + 1))))
323172, 322eqtr3d 2775 . . . . 5 (πœ‘ β†’ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)} = ((π‘†β€˜π½)(,)(π‘†β€˜(𝐽 + 1))))
324323reseq2d 5980 . . . 4 (πœ‘ β†’ (𝐹 β†Ύ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)}) = (𝐹 β†Ύ ((π‘†β€˜π½)(,)(π‘†β€˜(𝐽 + 1)))))
325324oveq1d 7421 . . 3 (πœ‘ β†’ ((𝐹 β†Ύ {π‘₯ ∈ β„‚ ∣ βˆƒπ‘¦ ∈ ((π‘β€˜(πΈβ€˜(π‘†β€˜π½)))(,)(πΈβ€˜(π‘†β€˜(𝐽 + 1))))π‘₯ = (𝑦 + π‘ˆ)}) limβ„‚ (π‘†β€˜(𝐽 + 1))) = ((𝐹 β†Ύ ((π‘†β€˜π½)(,)(π‘†β€˜(𝐽 + 1)))) limβ„‚ (π‘†β€˜(𝐽 + 1))))
326294, 325eleqtrd 2836 . 2 (πœ‘ β†’ if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), ((𝐹 β†Ύ ((π‘„β€˜(πΌβ€˜(π‘†β€˜π½)))(,)(π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1))))β€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) ∈ ((𝐹 β†Ύ ((π‘†β€˜π½)(,)(π‘†β€˜(𝐽 + 1)))) limβ„‚ (π‘†β€˜(𝐽 + 1))))
327157, 326eqeltrd 2834 1 (πœ‘ β†’ if((πΈβ€˜(π‘†β€˜(𝐽 + 1))) = (π‘„β€˜((πΌβ€˜(π‘†β€˜π½)) + 1)), (π‘Šβ€˜(πΌβ€˜(π‘†β€˜π½))), (πΉβ€˜(πΈβ€˜(π‘†β€˜(𝐽 + 1))))) ∈ ((𝐹 β†Ύ ((π‘†β€˜π½)(,)(π‘†β€˜(𝐽 + 1)))) limβ„‚ (π‘†β€˜(𝐽 + 1))))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   β‰  wne 2941  βˆ€wral 3062  βˆƒwrex 3071  {crab 3433  Vcvv 3475   βˆͺ cun 3946   βŠ† wss 3948  ifcif 4528  {csn 4628  {cpr 4630   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676  ran crn 5677   β†Ύ cres 5678  β„©cio 6491  βŸΆwf 6537  β€˜cfv 6541   Isom wiso 6542  (class class class)co 7406   ↑m cmap 8817  supcsup 9432  β„‚cc 11105  β„cr 11106  0cc0 11107  1c1 11108   + caddc 11110   Β· cmul 11112  +∞cpnf 11242  β„*cxr 11244   < clt 11245   ≀ cle 11246   βˆ’ cmin 11441  -cneg 11442   / cdiv 11868  β„•cn 12209  2c2 12264  β„€cz 12555  (,)cioo 13321  (,]cioc 13322  [,]cicc 13324  ...cfz 13481  ..^cfzo 13624  βŒŠcfl 13752  β™―chash 14287   β†Ύt crest 17363  TopOpenctopn 17364  β„‚fldccnfld 20937  β€“cnβ†’ccncf 24384   limβ„‚ climc 25371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722  ax-inf2 9633  ax-cnex 11163  ax-resscn 11164  ax-1cn 11165  ax-icn 11166  ax-addcl 11167  ax-addrcl 11168  ax-mulcl 11169  ax-mulrcl 11170  ax-mulcom 11171  ax-addass 11172  ax-mulass 11173  ax-distr 11174  ax-i2m1 11175  ax-1ne0 11176  ax-1rid 11177  ax-rnegex 11178  ax-rrecex 11179  ax-cnre 11180  ax-pre-lttri 11181  ax-pre-lttrn 11182  ax-pre-ltadd 11183  ax-pre-mulgt0 11184  ax-pre-sup 11185
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6298  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-isom 6550  df-riota 7362  df-ov 7409  df-oprab 7410  df-mpo 7411  df-om 7853  df-1st 7972  df-2nd 7973  df-frecs 8263  df-wrecs 8294  df-recs 8368  df-rdg 8407  df-1o 8463  df-oadd 8467  df-er 8700  df-map 8819  df-pm 8820  df-en 8937  df-dom 8938  df-sdom 8939  df-fin 8940  df-fi 9403  df-sup 9434  df-inf 9435  df-oi 9502  df-dju 9893  df-card 9931  df-pnf 11247  df-mnf 11248  df-xr 11249  df-ltxr 11250  df-le 11251  df-sub 11443  df-neg 11444  df-div 11869  df-nn 12210  df-2 12272  df-3 12273  df-4 12274  df-5 12275  df-6 12276  df-7 12277  df-8 12278  df-9 12279  df-n0 12470  df-xnn0 12542  df-z 12556  df-dec 12675  df-uz 12820  df-q 12930  df-rp 12972  df-xneg 13089  df-xadd 13090  df-xmul 13091  df-ioo 13325  df-ioc 13326  df-ico 13327  df-icc 13328  df-fz 13482  df-fzo 13625  df-fl 13754  df-seq 13964  df-exp 14025  df-hash 14288  df-cj 15043  df-re 15044  df-im 15045  df-sqrt 15179  df-abs 15180  df-struct 17077  df-slot 17112  df-ndx 17124  df-base 17142  df-plusg 17207  df-mulr 17208  df-starv 17209  df-tset 17213  df-ple 17214  df-ds 17216  df-unif 17217  df-rest 17365  df-topn 17366  df-topgen 17386  df-psmet 20929  df-xmet 20930  df-met 20931  df-bl 20932  df-mopn 20933  df-cnfld 20938  df-top 22388  df-topon 22405  df-topsp 22427  df-bases 22441  df-cld 22515  df-ntr 22516  df-cls 22517  df-nei 22594  df-lp 22632  df-cn 22723  df-cnp 22724  df-cmp 22883  df-xms 23818  df-ms 23819  df-cncf 24386  df-limc 25375
This theorem is referenced by:  fourierdlem99  44908  fourierdlem100  44909  fourierdlem107  44916  fourierdlem109  44918
  Copyright terms: Public domain W3C validator