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

Theorem fourierdlem92 46154
Description: The integral of a piecewise continuous periodic function 𝐹 is unchanged if the domain is shifted by its period 𝑇. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fourierdlem92.a (𝜑𝐴 ∈ ℝ)
fourierdlem92.b (𝜑𝐵 ∈ ℝ)
fourierdlem92.p 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem92.m (𝜑𝑀 ∈ ℕ)
fourierdlem92.t (𝜑𝑇 ∈ ℝ)
fourierdlem92.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem92.fper ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
fourierdlem92.s 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
fourierdlem92.h 𝐻 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem92.f (𝜑𝐹:ℝ⟶ℂ)
fourierdlem92.cncf ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
fourierdlem92.r ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
fourierdlem92.l ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
Assertion
Ref Expression
fourierdlem92 (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
Distinct variable groups:   𝐴,𝑖,𝑚,𝑝   𝑥,𝐴,𝑖   𝐵,𝑖,𝑚,𝑝   𝑥,𝐵   𝑖,𝐹,𝑥   𝑥,𝐿   𝑖,𝑀,𝑥   𝑚,𝑀,𝑝   𝑄,𝑖,𝑥   𝑄,𝑝   𝑥,𝑅   𝑆,𝑖,𝑥   𝑆,𝑝   𝑇,𝑖,𝑥   𝑇,𝑚,𝑝   𝜑,𝑖,𝑥
Allowed substitution hints:   𝜑(𝑚,𝑝)   𝑃(𝑥,𝑖,𝑚,𝑝)   𝑄(𝑚)   𝑅(𝑖,𝑚,𝑝)   𝑆(𝑚)   𝐹(𝑚,𝑝)   𝐻(𝑥,𝑖,𝑚,𝑝)   𝐿(𝑖,𝑚,𝑝)

Proof of Theorem fourierdlem92
Dummy variables 𝑦 𝑤 𝑧 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem92.a . . . 4 (𝜑𝐴 ∈ ℝ)
21adantr 480 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐴 ∈ ℝ)
3 fourierdlem92.b . . . 4 (𝜑𝐵 ∈ ℝ)
43adantr 480 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐵 ∈ ℝ)
5 fourierdlem92.p . . 3 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
6 fourierdlem92.m . . . 4 (𝜑𝑀 ∈ ℕ)
76adantr 480 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑀 ∈ ℕ)
8 fourierdlem92.t . . . . 5 (𝜑𝑇 ∈ ℝ)
98adantr 480 . . . 4 ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ)
10 simpr 484 . . . 4 ((𝜑 ∧ 0 < 𝑇) → 0 < 𝑇)
119, 10elrpd 13072 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ+)
12 fourierdlem92.q . . . 4 (𝜑𝑄 ∈ (𝑃𝑀))
1312adantr 480 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑄 ∈ (𝑃𝑀))
14 fourierdlem92.fper . . . 4 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
1514adantlr 715 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
16 fveq2 6907 . . . . 5 (𝑗 = 𝑖 → (𝑄𝑗) = (𝑄𝑖))
1716oveq1d 7446 . . . 4 (𝑗 = 𝑖 → ((𝑄𝑗) + 𝑇) = ((𝑄𝑖) + 𝑇))
1817cbvmptv 5261 . . 3 (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
19 fourierdlem92.f . . . 4 (𝜑𝐹:ℝ⟶ℂ)
2019adantr 480 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐹:ℝ⟶ℂ)
21 fourierdlem92.cncf . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
2221adantlr 715 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
23 fourierdlem92.r . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
2423adantlr 715 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
25 fourierdlem92.l . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
2625adantlr 715 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
27 eqeq1 2739 . . . . 5 (𝑦 = 𝑥 → (𝑦 = (𝑄𝑖) ↔ 𝑥 = (𝑄𝑖)))
28 eqeq1 2739 . . . . . 6 (𝑦 = 𝑥 → (𝑦 = (𝑄‘(𝑖 + 1)) ↔ 𝑥 = (𝑄‘(𝑖 + 1))))
29 fveq2 6907 . . . . . 6 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
3028, 29ifbieq2d 4557 . . . . 5 (𝑦 = 𝑥 → if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦)) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥)))
3127, 30ifbieq2d 4557 . . . 4 (𝑦 = 𝑥 → if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦))) = if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
3231cbvmptv 5261 . . 3 (𝑦 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦)))) = (𝑥 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
33 eqid 2735 . . 3 (𝑥 ∈ (((𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇))‘𝑖)[,]((𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇))‘(𝑖 + 1))) ↦ ((𝑦 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦))))‘(𝑥𝑇))) = (𝑥 ∈ (((𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇))‘𝑖)[,]((𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇))‘(𝑖 + 1))) ↦ ((𝑦 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦))))‘(𝑥𝑇)))
342, 4, 5, 7, 11, 13, 15, 18, 20, 22, 24, 26, 32, 33fourierdlem81 46143 . 2 ((𝜑 ∧ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
35 simpr 484 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝑇 = 0)
3635oveq2d 7447 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐴 + 𝑇) = (𝐴 + 0))
371recnd 11287 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
3837adantr 480 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝐴 ∈ ℂ)
3938addridd 11459 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐴 + 0) = 𝐴)
4036, 39eqtrd 2775 . . . . . 6 ((𝜑𝑇 = 0) → (𝐴 + 𝑇) = 𝐴)
4135oveq2d 7447 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐵 + 𝑇) = (𝐵 + 0))
423recnd 11287 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
4342adantr 480 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝐵 ∈ ℂ)
4443addridd 11459 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐵 + 0) = 𝐵)
4541, 44eqtrd 2775 . . . . . 6 ((𝜑𝑇 = 0) → (𝐵 + 𝑇) = 𝐵)
4640, 45oveq12d 7449 . . . . 5 ((𝜑𝑇 = 0) → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = (𝐴[,]𝐵))
4746itgeq1d 45913 . . . 4 ((𝜑𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
4847adantlr 715 . . 3 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
49 simpll 767 . . . 4 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝜑)
50 simpr 484 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 𝑇 = 0)
51 simplr 769 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 0 < 𝑇)
52 ioran 985 . . . . . . 7 (¬ (𝑇 = 0 ∨ 0 < 𝑇) ↔ (¬ 𝑇 = 0 ∧ ¬ 0 < 𝑇))
5350, 51, 52sylanbrc 583 . . . . . 6 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ (𝑇 = 0 ∨ 0 < 𝑇))
5449, 8syl 17 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 ∈ ℝ)
55 0red 11262 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 ∈ ℝ)
5654, 55lttrid 11397 . . . . . 6 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ ¬ (𝑇 = 0 ∨ 0 < 𝑇)))
5753, 56mpbird 257 . . . . 5 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 < 0)
5854lt0neg1d 11830 . . . . 5 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ 0 < -𝑇))
5957, 58mpbid 232 . . . 4 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 < -𝑇)
601, 8readdcld 11288 . . . . . . . . . . . 12 (𝜑 → (𝐴 + 𝑇) ∈ ℝ)
6160recnd 11287 . . . . . . . . . . 11 (𝜑 → (𝐴 + 𝑇) ∈ ℂ)
628recnd 11287 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
6361, 62negsubd 11624 . . . . . . . . . 10 (𝜑 → ((𝐴 + 𝑇) + -𝑇) = ((𝐴 + 𝑇) − 𝑇))
6437, 62pncand 11619 . . . . . . . . . 10 (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
6563, 64eqtrd 2775 . . . . . . . . 9 (𝜑 → ((𝐴 + 𝑇) + -𝑇) = 𝐴)
663, 8readdcld 11288 . . . . . . . . . . . 12 (𝜑 → (𝐵 + 𝑇) ∈ ℝ)
6766recnd 11287 . . . . . . . . . . 11 (𝜑 → (𝐵 + 𝑇) ∈ ℂ)
6867, 62negsubd 11624 . . . . . . . . . 10 (𝜑 → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇))
6942, 62pncand 11619 . . . . . . . . . 10 (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
7068, 69eqtrd 2775 . . . . . . . . 9 (𝜑 → ((𝐵 + 𝑇) + -𝑇) = 𝐵)
7165, 70oveq12d 7449 . . . . . . . 8 (𝜑 → (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)) = (𝐴[,]𝐵))
7271eqcomd 2741 . . . . . . 7 (𝜑 → (𝐴[,]𝐵) = (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)))
7372itgeq1d 45913 . . . . . 6 (𝜑 → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥)
7473adantr 480 . . . . 5 ((𝜑 ∧ 0 < -𝑇) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥)
751adantr 480 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝐴 ∈ ℝ)
768adantr 480 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝑇 ∈ ℝ)
7775, 76readdcld 11288 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → (𝐴 + 𝑇) ∈ ℝ)
783adantr 480 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝐵 ∈ ℝ)
7978, 76readdcld 11288 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → (𝐵 + 𝑇) ∈ ℝ)
80 eqid 2735 . . . . . 6 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
816adantr 480 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝑀 ∈ ℕ)
8276renegcld 11688 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ)
83 simpr 484 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 0 < -𝑇)
8482, 83elrpd 13072 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ+)
855fourierdlem2 46065 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
866, 85syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
8712, 86mpbid 232 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
8887simpld 494 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (ℝ ↑m (0...𝑀)))
89 elmapi 8888 . . . . . . . . . . . . . . 15 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
9088, 89syl 17 . . . . . . . . . . . . . 14 (𝜑𝑄:(0...𝑀)⟶ℝ)
9190ffvelcdmda 7104 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) ∈ ℝ)
928adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑇 ∈ ℝ)
9391, 92readdcld 11288 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
94 fourierdlem92.s . . . . . . . . . . . 12 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
9593, 94fmptd 7134 . . . . . . . . . . 11 (𝜑𝑆:(0...𝑀)⟶ℝ)
96 reex 11244 . . . . . . . . . . . . 13 ℝ ∈ V
9796a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ V)
98 ovex 7464 . . . . . . . . . . . . 13 (0...𝑀) ∈ V
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → (0...𝑀) ∈ V)
10097, 99elmapd 8879 . . . . . . . . . . 11 (𝜑 → (𝑆 ∈ (ℝ ↑m (0...𝑀)) ↔ 𝑆:(0...𝑀)⟶ℝ))
10195, 100mpbird 257 . . . . . . . . . 10 (𝜑𝑆 ∈ (ℝ ↑m (0...𝑀)))
10294a1i 11 . . . . . . . . . . . . 13 (𝜑𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇)))
103 fveq2 6907 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
104103oveq1d 7446 . . . . . . . . . . . . . 14 (𝑖 = 0 → ((𝑄𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
105104adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 = 0) → ((𝑄𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
106 0zd 12623 . . . . . . . . . . . . . 14 (𝜑 → 0 ∈ ℤ)
1076nnzd 12638 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ ℤ)
108 0le0 12365 . . . . . . . . . . . . . . 15 0 ≤ 0
109108a1i 11 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ 0)
110 nnnn0 12531 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
111110nn0ge0d 12588 . . . . . . . . . . . . . . 15 (𝑀 ∈ ℕ → 0 ≤ 𝑀)
1126, 111syl 17 . . . . . . . . . . . . . 14 (𝜑 → 0 ≤ 𝑀)
113106, 107, 106, 109, 112elfzd 13552 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ (0...𝑀))
11490, 113ffvelcdmd 7105 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ∈ ℝ)
115114, 8readdcld 11288 . . . . . . . . . . . . 13 (𝜑 → ((𝑄‘0) + 𝑇) ∈ ℝ)
116102, 105, 113, 115fvmptd 7023 . . . . . . . . . . . 12 (𝜑 → (𝑆‘0) = ((𝑄‘0) + 𝑇))
117 simprll 779 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄‘0) = 𝐴)
11887, 117syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘0) = 𝐴)
119118oveq1d 7446 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘0) + 𝑇) = (𝐴 + 𝑇))
120116, 119eqtrd 2775 . . . . . . . . . . 11 (𝜑 → (𝑆‘0) = (𝐴 + 𝑇))
121 fveq2 6907 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝑄𝑖) = (𝑄𝑀))
122121oveq1d 7446 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → ((𝑄𝑖) + 𝑇) = ((𝑄𝑀) + 𝑇))
123122adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 = 𝑀) → ((𝑄𝑖) + 𝑇) = ((𝑄𝑀) + 𝑇))
1246nnnn0d 12585 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ0)
125 nn0uz 12918 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
126124, 125eleqtrdi 2849 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ‘0))
127 eluzfz2 13569 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
128126, 127syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (0...𝑀))
12990, 128ffvelcdmd 7105 . . . . . . . . . . . . . 14 (𝜑 → (𝑄𝑀) ∈ ℝ)
130129, 8readdcld 11288 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝑀) + 𝑇) ∈ ℝ)
131102, 123, 128, 130fvmptd 7023 . . . . . . . . . . . 12 (𝜑 → (𝑆𝑀) = ((𝑄𝑀) + 𝑇))
132 simprlr 780 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄𝑀) = 𝐵)
13387, 132syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝑀) = 𝐵)
134133oveq1d 7446 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝑀) + 𝑇) = (𝐵 + 𝑇))
135131, 134eqtrd 2775 . . . . . . . . . . 11 (𝜑 → (𝑆𝑀) = (𝐵 + 𝑇))
136120, 135jca 511 . . . . . . . . . 10 (𝜑 → ((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)))
13790adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
138 elfzofz 13712 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
139138adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
140137, 139ffvelcdmd 7105 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
141 fzofzp1 13800 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
142141adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
143137, 142ffvelcdmd 7105 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
1448adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℝ)
14587simprrd 774 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
146145r19.21bi 3249 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
147140, 143, 144, 146ltadd1dd 11872 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) < ((𝑄‘(𝑖 + 1)) + 𝑇))
148140, 144readdcld 11288 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
14994fvmpt2 7027 . . . . . . . . . . . . 13 ((𝑖 ∈ (0...𝑀) ∧ ((𝑄𝑖) + 𝑇) ∈ ℝ) → (𝑆𝑖) = ((𝑄𝑖) + 𝑇))
150139, 148, 149syl2anc 584 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆𝑖) = ((𝑄𝑖) + 𝑇))
15194, 18eqtr4i 2766 . . . . . . . . . . . . . 14 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇))
152151a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇)))
153 fveq2 6907 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) → (𝑄𝑗) = (𝑄‘(𝑖 + 1)))
154153oveq1d 7446 . . . . . . . . . . . . . 14 (𝑗 = (𝑖 + 1) → ((𝑄𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
155154adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
156143, 144readdcld 11288 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
157152, 155, 142, 156fvmptd 7023 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) + 𝑇))
158147, 150, 1573brtr4d 5180 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆𝑖) < (𝑆‘(𝑖 + 1)))
159158ralrimiva 3144 . . . . . . . . . 10 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))
160101, 136, 159jca32 515 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
161 fourierdlem92.h . . . . . . . . . . 11 𝐻 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
162161fourierdlem2 46065 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑆 ∈ (𝐻𝑀) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
1636, 162syl 17 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐻𝑀) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
164160, 163mpbird 257 . . . . . . . 8 (𝜑𝑆 ∈ (𝐻𝑀))
165161fveq1i 6908 . . . . . . . 8 (𝐻𝑀) = ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀)
166164, 165eleqtrdi 2849 . . . . . . 7 (𝜑𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀))
167166adantr 480 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀))
16860adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
16966adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ)
170 simpr 484 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
171 eliccre 45458 . . . . . . . . . . . 12 (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
172168, 169, 170, 171syl3anc 1370 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
173172recnd 11287 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ)
17462negcld 11605 . . . . . . . . . . 11 (𝜑 → -𝑇 ∈ ℂ)
175174adantr 480 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℂ)
176173, 175addcld 11278 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℂ)
177 simpl 482 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝜑)
1781adantr 480 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ)
1793adantr 480 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ)
1808renegcld 11688 . . . . . . . . . . . . 13 (𝜑 → -𝑇 ∈ ℝ)
181180adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℝ)
182172, 181readdcld 11288 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℝ)
18363, 64eqtr2d 2776 . . . . . . . . . . . . 13 (𝜑𝐴 = ((𝐴 + 𝑇) + -𝑇))
184183adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) + -𝑇))
185168rexrd 11309 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ*)
186169rexrd 11309 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ*)
187 iccgelb 13440 . . . . . . . . . . . . . 14 (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ*𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
188185, 186, 170, 187syl3anc 1370 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
189168, 172, 181, 188leadd1dd 11875 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) + -𝑇) ≤ (𝑥 + -𝑇))
190184, 189eqbrtrd 5170 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 + -𝑇))
191 iccleub 13439 . . . . . . . . . . . . . 14 (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ*𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
192185, 186, 170, 191syl3anc 1370 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
193172, 169, 181, 192leadd1dd 11875 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ ((𝐵 + 𝑇) + -𝑇))
194169recnd 11287 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℂ)
19562adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ)
196194, 195negsubd 11624 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇))
19769adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
198196, 197eqtrd 2775 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = 𝐵)
199193, 198breqtrd 5174 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ 𝐵)
200178, 179, 182, 190, 199eliccd 45457 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))
201177, 200jca 511 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))
202 eleq1 2827 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))
203202anbi2d 630 . . . . . . . . . . 11 (𝑦 = (𝑥 + -𝑇) → ((𝜑𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))))
204 oveq1 7438 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + -𝑇) → (𝑦 + 𝑇) = ((𝑥 + -𝑇) + 𝑇))
205204fveq2d 6911 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥 + -𝑇) + 𝑇)))
206 fveq2 6907 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝐹𝑦) = (𝐹‘(𝑥 + -𝑇)))
207205, 206eqeq12d 2751 . . . . . . . . . . 11 (𝑦 = (𝑥 + -𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))
208203, 207imbi12d 344 . . . . . . . . . 10 (𝑦 = (𝑥 + -𝑇) → (((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))))
209 eleq1 2827 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
210209anbi2d 630 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝜑𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑦 ∈ (𝐴[,]𝐵))))
211 oveq1 7438 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
212211fveq2d 6911 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
213 fveq2 6907 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
214212, 213eqeq12d 2751 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)))
215210, 214imbi12d 344 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))))
216215, 14chvarvv 1996 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
217208, 216vtoclg 3554 . . . . . . . . 9 ((𝑥 + -𝑇) ∈ ℂ → ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))
218176, 201, 217sylc 65 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))
219173, 195negsubd 11624 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) = (𝑥𝑇))
220219oveq1d 7446 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = ((𝑥𝑇) + 𝑇))
221173, 195npcand 11622 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥𝑇) + 𝑇) = 𝑥)
222220, 221eqtrd 2775 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = 𝑥)
223222fveq2d 6911 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹𝑥))
224218, 223eqtr3d 2777 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹𝑥))
225224adantlr 715 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹𝑥))
226 fveq2 6907 . . . . . . . 8 (𝑗 = 𝑖 → (𝑆𝑗) = (𝑆𝑖))
227226oveq1d 7446 . . . . . . 7 (𝑗 = 𝑖 → ((𝑆𝑗) + -𝑇) = ((𝑆𝑖) + -𝑇))
228227cbvmptv 5261 . . . . . 6 (𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑆𝑖) + -𝑇))
22919adantr 480 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝐹:ℝ⟶ℂ)
23019adantr 480 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
231 ioossre 13445 . . . . . . . . . . 11 ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ
232231a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ)
233230, 232feqresmpt 6978 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹𝑥)))
234150, 157oveq12d 7449 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) = (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
235140, 143, 144iooshift 45475 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
236234, 235eqtrd 2775 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
237236mpteq1d 5243 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹𝑥)))
238 simpll 767 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝜑)
239 simplr 769 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑖 ∈ (0..^𝑀))
240235eleq2d 2825 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) ↔ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}))
241240biimpar 477 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
242140rexrd 11309 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
2432423adant3 1131 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) ∈ ℝ*)
244143rexrd 11309 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2452443adant3 1131 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
246 elioore 13414 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) → 𝑥 ∈ ℝ)
247246adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
2488adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
249247, 248resubcld 11689 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ℝ)
2502493adant2 1130 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ℝ)
251140recnd 11287 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
25262adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℂ)
253251, 252pncand 11619 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + 𝑇) − 𝑇) = (𝑄𝑖))
254253eqcomd 2741 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (((𝑄𝑖) + 𝑇) − 𝑇))
2552543adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) = (((𝑄𝑖) + 𝑇) − 𝑇))
2561483adant3 1131 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
2572473adant2 1130 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
25883ad2ant1 1132 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
259148rexrd 11309 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ*)
2602593adant3 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) ∈ ℝ*)
261156rexrd 11309 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
2622613adant3 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
263 simp3 1137 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
264 ioogtlb 45448 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) < 𝑥)
265260, 262, 263, 264syl3anc 1370 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) < 𝑥)
266256, 257, 258, 265ltsub1dd 11873 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄𝑖) + 𝑇) − 𝑇) < (𝑥𝑇))
267255, 266eqbrtrd 5170 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) < (𝑥𝑇))
2681563adant3 1131 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
269 iooltub 45463 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇))
270260, 262, 263, 269syl3anc 1370 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇))
271257, 268, 258, 270ltsub1dd 11873 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇))
272143recnd 11287 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
273272, 252pncand 11619 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
2742733adant3 1131 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
275271, 274breqtrd 5174 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < (𝑄‘(𝑖 + 1)))
276243, 245, 250, 267, 275eliood 45451 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
277238, 239, 241, 276syl3anc 1370 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
278 fvres 6926 . . . . . . . . . . . 12 ((𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
279277, 278syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
280238, 241, 249syl2anc 584 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ ℝ)
28113ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ∈ ℝ)
28233ad2ant1 1132 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐵 ∈ ℝ)
28364eqcomd 2741 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 = ((𝐴 + 𝑇) − 𝑇))
2842833ad2ant1 1132 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
285603ad2ant1 1132 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
2861adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ)
2871rexrd 11309 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ ℝ*)
288287adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ*)
2893rexrd 11309 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ*)
290289adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ*)
2915, 6, 12fourierdlem15 46078 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
292291adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
293292, 139ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ (𝐴[,]𝐵))
294 iccgelb 13440 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄𝑖) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑄𝑖))
295288, 290, 293, 294syl3anc 1370 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ≤ (𝑄𝑖))
296286, 140, 144, 295leadd1dd 11875 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐴 + 𝑇) ≤ ((𝑄𝑖) + 𝑇))
2972963adant3 1131 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ≤ ((𝑄𝑖) + 𝑇))
298285, 256, 257, 297, 265lelttrd 11417 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) < 𝑥)
299285, 257, 258, 298ltsub1dd 11873 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) < (𝑥𝑇))
300284, 299eqbrtrd 5170 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 < (𝑥𝑇))
301281, 250, 300ltled 11407 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ≤ (𝑥𝑇))
3021433adant3 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
303292, 142ffvelcdmd 7105 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵))
304 iccleub 13439 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
305288, 290, 303, 304syl3anc 1370 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
3063053adant3 1131 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
307250, 302, 282, 275, 306ltletrd 11419 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < 𝐵)
308250, 282, 307ltled 11407 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ≤ 𝐵)
309281, 282, 250, 301, 308eliccd 45457 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ (𝐴[,]𝐵))
310238, 239, 241, 309syl3anc 1370 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ (𝐴[,]𝐵))
311238, 310jca 511 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)))
312 eleq1 2827 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥𝑇) ∈ (𝐴[,]𝐵)))
313312anbi2d 630 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑇) → ((𝜑𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵))))
314 oveq1 7438 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥𝑇) → (𝑦 + 𝑇) = ((𝑥𝑇) + 𝑇))
315314fveq2d 6911 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥𝑇) + 𝑇)))
316 fveq2 6907 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝐹𝑦) = (𝐹‘(𝑥𝑇)))
317315, 316eqeq12d 2751 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
318313, 317imbi12d 344 . . . . . . . . . . . . 13 (𝑦 = (𝑥𝑇) → (((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))))
319318, 216vtoclg 3554 . . . . . . . . . . . 12 ((𝑥𝑇) ∈ ℝ → ((𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
320280, 311, 319sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))
321241, 246syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ℝ)
322 recn 11243 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
323322adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
32462adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
325323, 324npcand 11622 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → ((𝑥𝑇) + 𝑇) = 𝑥)
326325fveq2d 6911 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹𝑥))
327238, 321, 326syl2anc 584 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹𝑥))
328279, 320, 3273eqtr2rd 2782 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹𝑥) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)))
329328mpteq2dva 5248 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))))
330233, 237, 3293eqtrd 2779 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))))
331 ioosscn 13446 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
332331a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
333 eqeq1 2739 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇)))
334333rexbidv 3177 . . . . . . . . . . . 12 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)))
335 oveq1 7438 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇))
336335eqeq2d 2746 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇)))
337336cbvrexvw 3236 . . . . . . . . . . . 12 (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇))
338334, 337bitrdi 287 . . . . . . . . . . 11 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)))
339338cbvrabv 3444 . . . . . . . . . 10 {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}
340 eqid 2735 . . . . . . . . . 10 (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)))
341332, 252, 339, 21, 340cncfshift 45830 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) ∈ ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ))
342236eqcomd 2741 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))))
343342oveq1d 7446 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ) = (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
344341, 343eleqtrd 2841 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
345330, 344eqeltrd 2839 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
346345adantlr 715 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
347 ffdm 6766 . . . . . . . . . . . 12 (𝐹:ℝ⟶ℂ → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
34819, 347syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
349348simpld 494 . . . . . . . . . 10 (𝜑𝐹:dom 𝐹⟶ℂ)
350349adantr 480 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:dom 𝐹⟶ℂ)
351 ioossre 13445 . . . . . . . . . 10 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
352 fdm 6746 . . . . . . . . . . 11 (𝐹:ℝ⟶ℂ → dom 𝐹 = ℝ)
353230, 352syl 17 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → dom 𝐹 = ℝ)
354351, 353sseqtrrid 4049 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
355339eqcomi 2744 . . . . . . . . 9 {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}
356232, 342, 3533sstr4d 4043 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ⊆ dom 𝐹)
357339, 356eqsstrrid 4045 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} ⊆ dom 𝐹)
358 simpll 767 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
359358, 287syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐴 ∈ ℝ*)
360358, 289syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐵 ∈ ℝ*)
361358, 291syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
362 simplr 769 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
363 ioossicc 13470 . . . . . . . . . . . . 13 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
364363sseli 3991 . . . . . . . . . . . 12 (𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑧 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
365364adantl 481 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
366359, 360, 361, 362, 365fourierdlem1 46064 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ (𝐴[,]𝐵))
367 eleq1 2827 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑧 ∈ (𝐴[,]𝐵)))
368367anbi2d 630 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝜑𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑧 ∈ (𝐴[,]𝐵))))
369 oveq1 7438 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑥 + 𝑇) = (𝑧 + 𝑇))
370369fveq2d 6911 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑧 + 𝑇)))
371 fveq2 6907 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
372370, 371eqeq12d 2751 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧)))
373368, 372imbi12d 344 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))))
374373, 14chvarvv 1996 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))
375358, 366, 374syl2anc 584 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))
376350, 332, 354, 252, 355, 357, 375, 23limcperiod 45584 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄𝑖) + 𝑇)))
377355, 342eqtrid 2787 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))))
378377reseq2d 6000 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) = (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))))
379150eqcomd 2741 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) = (𝑆𝑖))
380378, 379oveq12d 7449 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄𝑖) + 𝑇)) = ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
381376, 380eleqtrd 2841 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
382381adantlr 715 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
383350, 332, 354, 252, 355, 357, 375, 25limcperiod 45584 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄‘(𝑖 + 1)) + 𝑇)))
384157eqcomd 2741 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) = (𝑆‘(𝑖 + 1)))
385378, 384oveq12d 7449 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄‘(𝑖 + 1)) + 𝑇)) = ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
386383, 385eleqtrd 2841 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
387386adantlr 715 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
388 eqeq1 2739 . . . . . . . 8 (𝑦 = 𝑥 → (𝑦 = (𝑆𝑖) ↔ 𝑥 = (𝑆𝑖)))
389 eqeq1 2739 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑦 = (𝑆‘(𝑖 + 1)) ↔ 𝑥 = (𝑆‘(𝑖 + 1))))
390389, 29ifbieq2d 4557 . . . . . . . 8 (𝑦 = 𝑥 → if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦)) = if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥)))
391388, 390ifbieq2d 4557 . . . . . . 7 (𝑦 = 𝑥 → if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦))) = if(𝑥 = (𝑆𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
392391cbvmptv 5261 . . . . . 6 (𝑦 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦)))) = (𝑥 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
393 eqid 2735 . . . . . 6 (𝑥 ∈ (((𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇))‘𝑖)[,]((𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇))‘(𝑖 + 1))) ↦ ((𝑦 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦))))‘(𝑥 − -𝑇))) = (𝑥 ∈ (((𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇))‘𝑖)[,]((𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇))‘(𝑖 + 1))) ↦ ((𝑦 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦))))‘(𝑥 − -𝑇)))
39477, 79, 80, 81, 84, 167, 225, 228, 229, 346, 382, 387, 392, 393fourierdlem81 46143 . . . . 5 ((𝜑 ∧ 0 < -𝑇) → ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥)
39574, 394eqtr2d 2776 . . . 4 ((𝜑 ∧ 0 < -𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
39649, 59, 395syl2anc 584 . . 3 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
39748, 396pm2.61dan 813 . 2 ((𝜑 ∧ ¬ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
39834, 397pm2.61dan 813 1 (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1537  wcel 2106  wral 3059  wrex 3068  {crab 3433  Vcvv 3478  wss 3963  ifcif 4531   class class class wbr 5148  cmpt 5231  dom cdm 5689  cres 5691  wf 6559  cfv 6563  (class class class)co 7431  m cmap 8865  cc 11151  cr 11152  0cc0 11153  1c1 11154   + caddc 11156  *cxr 11292   < clt 11293  cle 11294  cmin 11490  -cneg 11491  cn 12264  0cn0 12524  cuz 12876  (,)cioo 13384  [,]cicc 13387  ...cfz 13544  ..^cfzo 13691  cnccncf 24916  citg 25667   lim climc 25912
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-inf2 9679  ax-cc 10473  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230  ax-pre-sup 11231  ax-addf 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-symdif 4259  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-tp 4636  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-iin 4999  df-disj 5116  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-ofr 7698  df-om 7888  df-1st 8013  df-2nd 8014  df-supp 8185  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-2o 8506  df-oadd 8509  df-omul 8510  df-er 8744  df-map 8867  df-pm 8868  df-ixp 8937  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-fsupp 9400  df-fi 9449  df-sup 9480  df-inf 9481  df-oi 9548  df-dju 9939  df-card 9977  df-acn 9980  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-div 11919  df-nn 12265  df-2 12327  df-3 12328  df-4 12329  df-5 12330  df-6 12331  df-7 12332  df-8 12333  df-9 12334  df-n0 12525  df-z 12612  df-dec 12732  df-uz 12877  df-q 12989  df-rp 13033  df-xneg 13152  df-xadd 13153  df-xmul 13154  df-ioo 13388  df-ioc 13389  df-ico 13390  df-icc 13391  df-fz 13545  df-fzo 13692  df-fl 13829  df-mod 13907  df-seq 14040  df-exp 14100  df-hash 14367  df-cj 15135  df-re 15136  df-im 15137  df-sqrt 15271  df-abs 15272  df-limsup 15504  df-clim 15521  df-rlim 15522  df-sum 15720  df-struct 17181  df-sets 17198  df-slot 17216  df-ndx 17228  df-base 17246  df-ress 17275  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-hom 17322  df-cco 17323  df-rest 17469  df-topn 17470  df-0g 17488  df-gsum 17489  df-topgen 17490  df-pt 17491  df-prds 17494  df-xrs 17549  df-qtop 17554  df-imas 17555  df-xps 17557  df-mre 17631  df-mrc 17632  df-acs 17634  df-mgm 18666  df-sgrp 18745  df-mnd 18761  df-submnd 18810  df-mulg 19099  df-cntz 19348  df-cmn 19815  df-psmet 21374  df-xmet 21375  df-met 21376  df-bl 21377  df-mopn 21378  df-fbas 21379  df-fg 21380  df-cnfld 21383  df-top 22916  df-topon 22933  df-topsp 22955  df-bases 22969  df-cld 23043  df-ntr 23044  df-cls 23045  df-nei 23122  df-lp 23160  df-perf 23161  df-cn 23251  df-cnp 23252  df-haus 23339  df-cmp 23411  df-tx 23586  df-hmeo 23779  df-fil 23870  df-fm 23962  df-flim 23963  df-flf 23964  df-xms 24346  df-ms 24347  df-tms 24348  df-cncf 24918  df-ovol 25513  df-vol 25514  df-mbf 25668  df-itg1 25669  df-itg2 25670  df-ibl 25671  df-itg 25672  df-0p 25719  df-ditg 25897  df-limc 25916  df-dv 25917
This theorem is referenced by:  fourierdlem107  46169
  Copyright terms: Public domain W3C validator