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 42833
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 484 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐴 ∈ ℝ)
3 fourierdlem92.b . . . 4 (𝜑𝐵 ∈ ℝ)
43adantr 484 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐵 ∈ ℝ)
5 fourierdlem92.p . . 3 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
6 fourierdlem92.m . . . 4 (𝜑𝑀 ∈ ℕ)
76adantr 484 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑀 ∈ ℕ)
8 fourierdlem92.t . . . . 5 (𝜑𝑇 ∈ ℝ)
98adantr 484 . . . 4 ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ)
10 simpr 488 . . . 4 ((𝜑 ∧ 0 < 𝑇) → 0 < 𝑇)
119, 10elrpd 12420 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ+)
12 fourierdlem92.q . . . 4 (𝜑𝑄 ∈ (𝑃𝑀))
1312adantr 484 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑄 ∈ (𝑃𝑀))
14 fourierdlem92.fper . . . 4 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
1514adantlr 714 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
16 fveq2 6649 . . . . 5 (𝑗 = 𝑖 → (𝑄𝑗) = (𝑄𝑖))
1716oveq1d 7154 . . . 4 (𝑗 = 𝑖 → ((𝑄𝑗) + 𝑇) = ((𝑄𝑖) + 𝑇))
1817cbvmptv 5136 . . 3 (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
19 fourierdlem92.f . . . 4 (𝜑𝐹:ℝ⟶ℂ)
2019adantr 484 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐹:ℝ⟶ℂ)
21 fourierdlem92.cncf . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
2221adantlr 714 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
23 fourierdlem92.r . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
2423adantlr 714 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
25 fourierdlem92.l . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
2625adantlr 714 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
27 eqeq1 2805 . . . . 5 (𝑦 = 𝑥 → (𝑦 = (𝑄𝑖) ↔ 𝑥 = (𝑄𝑖)))
28 eqeq1 2805 . . . . . 6 (𝑦 = 𝑥 → (𝑦 = (𝑄‘(𝑖 + 1)) ↔ 𝑥 = (𝑄‘(𝑖 + 1))))
29 fveq2 6649 . . . . . 6 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
3028, 29ifbieq2d 4453 . . . . 5 (𝑦 = 𝑥 → if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦)) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥)))
3127, 30ifbieq2d 4453 . . . 4 (𝑦 = 𝑥 → if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦))) = if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
3231cbvmptv 5136 . . 3 (𝑦 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦)))) = (𝑥 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
33 eqid 2801 . . 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 42822 . 2 ((𝜑 ∧ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
35 simpr 488 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝑇 = 0)
3635oveq2d 7155 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐴 + 𝑇) = (𝐴 + 0))
371recnd 10662 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
3837adantr 484 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝐴 ∈ ℂ)
3938addid1d 10833 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐴 + 0) = 𝐴)
4036, 39eqtrd 2836 . . . . . 6 ((𝜑𝑇 = 0) → (𝐴 + 𝑇) = 𝐴)
4135oveq2d 7155 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐵 + 𝑇) = (𝐵 + 0))
423recnd 10662 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
4342adantr 484 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝐵 ∈ ℂ)
4443addid1d 10833 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐵 + 0) = 𝐵)
4541, 44eqtrd 2836 . . . . . 6 ((𝜑𝑇 = 0) → (𝐵 + 𝑇) = 𝐵)
4640, 45oveq12d 7157 . . . . 5 ((𝜑𝑇 = 0) → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = (𝐴[,]𝐵))
4746itgeq1d 42592 . . . 4 ((𝜑𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
4847adantlr 714 . . 3 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
49 simpll 766 . . . 4 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝜑)
50 simpr 488 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 𝑇 = 0)
51 simplr 768 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 0 < 𝑇)
52 ioran 981 . . . . . . 7 (¬ (𝑇 = 0 ∨ 0 < 𝑇) ↔ (¬ 𝑇 = 0 ∧ ¬ 0 < 𝑇))
5350, 51, 52sylanbrc 586 . . . . . 6 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ (𝑇 = 0 ∨ 0 < 𝑇))
5449, 8syl 17 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 ∈ ℝ)
55 0red 10637 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 ∈ ℝ)
5654, 55lttrid 10771 . . . . . 6 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ ¬ (𝑇 = 0 ∨ 0 < 𝑇)))
5753, 56mpbird 260 . . . . 5 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 < 0)
5854lt0neg1d 11202 . . . . 5 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ 0 < -𝑇))
5957, 58mpbid 235 . . . 4 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 < -𝑇)
601, 8readdcld 10663 . . . . . . . . . . . 12 (𝜑 → (𝐴 + 𝑇) ∈ ℝ)
6160recnd 10662 . . . . . . . . . . 11 (𝜑 → (𝐴 + 𝑇) ∈ ℂ)
628recnd 10662 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
6361, 62negsubd 10996 . . . . . . . . . 10 (𝜑 → ((𝐴 + 𝑇) + -𝑇) = ((𝐴 + 𝑇) − 𝑇))
6437, 62pncand 10991 . . . . . . . . . 10 (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
6563, 64eqtrd 2836 . . . . . . . . 9 (𝜑 → ((𝐴 + 𝑇) + -𝑇) = 𝐴)
663, 8readdcld 10663 . . . . . . . . . . . 12 (𝜑 → (𝐵 + 𝑇) ∈ ℝ)
6766recnd 10662 . . . . . . . . . . 11 (𝜑 → (𝐵 + 𝑇) ∈ ℂ)
6867, 62negsubd 10996 . . . . . . . . . 10 (𝜑 → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇))
6942, 62pncand 10991 . . . . . . . . . 10 (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
7068, 69eqtrd 2836 . . . . . . . . 9 (𝜑 → ((𝐵 + 𝑇) + -𝑇) = 𝐵)
7165, 70oveq12d 7157 . . . . . . . 8 (𝜑 → (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)) = (𝐴[,]𝐵))
7271eqcomd 2807 . . . . . . 7 (𝜑 → (𝐴[,]𝐵) = (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)))
7372itgeq1d 42592 . . . . . 6 (𝜑 → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥)
7473adantr 484 . . . . 5 ((𝜑 ∧ 0 < -𝑇) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥)
751adantr 484 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝐴 ∈ ℝ)
768adantr 484 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝑇 ∈ ℝ)
7775, 76readdcld 10663 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → (𝐴 + 𝑇) ∈ ℝ)
783adantr 484 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝐵 ∈ ℝ)
7978, 76readdcld 10663 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → (𝐵 + 𝑇) ∈ ℝ)
80 eqid 2801 . . . . . 6 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
816adantr 484 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝑀 ∈ ℕ)
8276renegcld 11060 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ)
83 simpr 488 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 0 < -𝑇)
8482, 83elrpd 12420 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ+)
855fourierdlem2 42744 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
866, 85syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
8712, 86mpbid 235 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
8887simpld 498 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (ℝ ↑m (0...𝑀)))
89 elmapi 8415 . . . . . . . . . . . . . . 15 (𝑄 ∈ (ℝ ↑m (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
9088, 89syl 17 . . . . . . . . . . . . . 14 (𝜑𝑄:(0...𝑀)⟶ℝ)
9190ffvelrnda 6832 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) ∈ ℝ)
928adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑇 ∈ ℝ)
9391, 92readdcld 10663 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
94 fourierdlem92.s . . . . . . . . . . . 12 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
9593, 94fmptd 6859 . . . . . . . . . . 11 (𝜑𝑆:(0...𝑀)⟶ℝ)
96 reex 10621 . . . . . . . . . . . . 13 ℝ ∈ V
9796a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ V)
98 ovex 7172 . . . . . . . . . . . . 13 (0...𝑀) ∈ V
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → (0...𝑀) ∈ V)
10097, 99elmapd 8407 . . . . . . . . . . 11 (𝜑 → (𝑆 ∈ (ℝ ↑m (0...𝑀)) ↔ 𝑆:(0...𝑀)⟶ℝ))
10195, 100mpbird 260 . . . . . . . . . 10 (𝜑𝑆 ∈ (ℝ ↑m (0...𝑀)))
10294a1i 11 . . . . . . . . . . . . 13 (𝜑𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇)))
103 fveq2 6649 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
104103oveq1d 7154 . . . . . . . . . . . . . 14 (𝑖 = 0 → ((𝑄𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
105104adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑖 = 0) → ((𝑄𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
106 0zd 11985 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℤ)
1076nnzd 12078 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
108106, 107, 1063jca 1125 . . . . . . . . . . . . . . 15 (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ))
109 0le0 11730 . . . . . . . . . . . . . . . 16 0 ≤ 0
110109a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ 0)
111 nnnn0 11896 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
112111nn0ge0d 11950 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → 0 ≤ 𝑀)
1136, 112syl 17 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ 𝑀)
114108, 110, 113jca32 519 . . . . . . . . . . . . . 14 (𝜑 → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
115 elfz2 12896 . . . . . . . . . . . . . 14 (0 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
116114, 115sylibr 237 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ (0...𝑀))
11790, 116ffvelrnd 6833 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ∈ ℝ)
118117, 8readdcld 10663 . . . . . . . . . . . . 13 (𝜑 → ((𝑄‘0) + 𝑇) ∈ ℝ)
119102, 105, 116, 118fvmptd 6756 . . . . . . . . . . . 12 (𝜑 → (𝑆‘0) = ((𝑄‘0) + 𝑇))
120 simprll 778 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄‘0) = 𝐴)
12187, 120syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘0) = 𝐴)
122121oveq1d 7154 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘0) + 𝑇) = (𝐴 + 𝑇))
123119, 122eqtrd 2836 . . . . . . . . . . 11 (𝜑 → (𝑆‘0) = (𝐴 + 𝑇))
124 fveq2 6649 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝑄𝑖) = (𝑄𝑀))
125124oveq1d 7154 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → ((𝑄𝑖) + 𝑇) = ((𝑄𝑀) + 𝑇))
126125adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑖 = 𝑀) → ((𝑄𝑖) + 𝑇) = ((𝑄𝑀) + 𝑇))
1276nnnn0d 11947 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ0)
128 nn0uz 12272 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
129127, 128eleqtrdi 2903 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ‘0))
130 eluzfz2 12914 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
131129, 130syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (0...𝑀))
13290, 131ffvelrnd 6833 . . . . . . . . . . . . . 14 (𝜑 → (𝑄𝑀) ∈ ℝ)
133132, 8readdcld 10663 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝑀) + 𝑇) ∈ ℝ)
134102, 126, 131, 133fvmptd 6756 . . . . . . . . . . . 12 (𝜑 → (𝑆𝑀) = ((𝑄𝑀) + 𝑇))
135 simprlr 779 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄𝑀) = 𝐵)
13687, 135syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝑀) = 𝐵)
137136oveq1d 7154 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝑀) + 𝑇) = (𝐵 + 𝑇))
138134, 137eqtrd 2836 . . . . . . . . . . 11 (𝜑 → (𝑆𝑀) = (𝐵 + 𝑇))
139123, 138jca 515 . . . . . . . . . 10 (𝜑 → ((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)))
14090adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
141 elfzofz 13052 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
142141adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
143140, 142ffvelrnd 6833 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
144 fzofzp1 13133 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
145144adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
146140, 145ffvelrnd 6833 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
1478adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℝ)
14887simprrd 773 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
149148r19.21bi 3176 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
150143, 146, 147, 149ltadd1dd 11244 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) < ((𝑄‘(𝑖 + 1)) + 𝑇))
151143, 147readdcld 10663 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
15294fvmpt2 6760 . . . . . . . . . . . . 13 ((𝑖 ∈ (0...𝑀) ∧ ((𝑄𝑖) + 𝑇) ∈ ℝ) → (𝑆𝑖) = ((𝑄𝑖) + 𝑇))
153142, 151, 152syl2anc 587 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆𝑖) = ((𝑄𝑖) + 𝑇))
15494, 18eqtr4i 2827 . . . . . . . . . . . . . 14 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇))
155154a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇)))
156 fveq2 6649 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) → (𝑄𝑗) = (𝑄‘(𝑖 + 1)))
157156oveq1d 7154 . . . . . . . . . . . . . 14 (𝑗 = (𝑖 + 1) → ((𝑄𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
158157adantl 485 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
159146, 147readdcld 10663 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
160155, 158, 145, 159fvmptd 6756 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) + 𝑇))
161150, 153, 1603brtr4d 5065 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆𝑖) < (𝑆‘(𝑖 + 1)))
162161ralrimiva 3152 . . . . . . . . . 10 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))
163101, 139, 162jca32 519 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
164 fourierdlem92.h . . . . . . . . . . 11 𝐻 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
165164fourierdlem2 42744 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑆 ∈ (𝐻𝑀) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
1666, 165syl 17 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐻𝑀) ↔ (𝑆 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
167163, 166mpbird 260 . . . . . . . 8 (𝜑𝑆 ∈ (𝐻𝑀))
168164fveq1i 6650 . . . . . . . 8 (𝐻𝑀) = ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀)
169167, 168eleqtrdi 2903 . . . . . . 7 (𝜑𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀))
170169adantr 484 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀))
17160adantr 484 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
17266adantr 484 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ)
173 simpr 488 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
174 eliccre 42135 . . . . . . . . . . . 12 (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
175171, 172, 173, 174syl3anc 1368 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
176175recnd 10662 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ)
17762negcld 10977 . . . . . . . . . . 11 (𝜑 → -𝑇 ∈ ℂ)
178177adantr 484 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℂ)
179176, 178addcld 10653 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℂ)
180 simpl 486 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝜑)
1811adantr 484 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ)
1823adantr 484 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ)
1838renegcld 11060 . . . . . . . . . . . . 13 (𝜑 → -𝑇 ∈ ℝ)
184183adantr 484 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℝ)
185175, 184readdcld 10663 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℝ)
18663, 64eqtr2d 2837 . . . . . . . . . . . . 13 (𝜑𝐴 = ((𝐴 + 𝑇) + -𝑇))
187186adantr 484 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) + -𝑇))
188171rexrd 10684 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ*)
189172rexrd 10684 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ*)
190 iccgelb 12785 . . . . . . . . . . . . . 14 (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ*𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
191188, 189, 173, 190syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
192171, 175, 184, 191leadd1dd 11247 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) + -𝑇) ≤ (𝑥 + -𝑇))
193187, 192eqbrtrd 5055 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 + -𝑇))
194 iccleub 12784 . . . . . . . . . . . . . 14 (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ*𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
195188, 189, 173, 194syl3anc 1368 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
196175, 172, 184, 195leadd1dd 11247 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ ((𝐵 + 𝑇) + -𝑇))
197172recnd 10662 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℂ)
19862adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ)
199197, 198negsubd 10996 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇))
20069adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
201199, 200eqtrd 2836 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = 𝐵)
202196, 201breqtrd 5059 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ 𝐵)
203181, 182, 185, 193, 202eliccd 42134 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))
204180, 203jca 515 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))
205 eleq1 2880 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))
206205anbi2d 631 . . . . . . . . . . 11 (𝑦 = (𝑥 + -𝑇) → ((𝜑𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))))
207 oveq1 7146 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + -𝑇) → (𝑦 + 𝑇) = ((𝑥 + -𝑇) + 𝑇))
208207fveq2d 6653 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥 + -𝑇) + 𝑇)))
209 fveq2 6649 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝐹𝑦) = (𝐹‘(𝑥 + -𝑇)))
210208, 209eqeq12d 2817 . . . . . . . . . . 11 (𝑦 = (𝑥 + -𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))
211206, 210imbi12d 348 . . . . . . . . . 10 (𝑦 = (𝑥 + -𝑇) → (((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))))
212 eleq1 2880 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
213212anbi2d 631 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝜑𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑦 ∈ (𝐴[,]𝐵))))
214 oveq1 7146 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
215214fveq2d 6653 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
216 fveq2 6649 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
217215, 216eqeq12d 2817 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)))
218213, 217imbi12d 348 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))))
219218, 14chvarvv 2005 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
220211, 219vtoclg 3518 . . . . . . . . 9 ((𝑥 + -𝑇) ∈ ℂ → ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))
221179, 204, 220sylc 65 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))
222176, 198negsubd 10996 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) = (𝑥𝑇))
223222oveq1d 7154 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = ((𝑥𝑇) + 𝑇))
224176, 198npcand 10994 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥𝑇) + 𝑇) = 𝑥)
225223, 224eqtrd 2836 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = 𝑥)
226225fveq2d 6653 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹𝑥))
227221, 226eqtr3d 2838 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹𝑥))
228227adantlr 714 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹𝑥))
229 fveq2 6649 . . . . . . . 8 (𝑗 = 𝑖 → (𝑆𝑗) = (𝑆𝑖))
230229oveq1d 7154 . . . . . . 7 (𝑗 = 𝑖 → ((𝑆𝑗) + -𝑇) = ((𝑆𝑖) + -𝑇))
231230cbvmptv 5136 . . . . . 6 (𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑆𝑖) + -𝑇))
23219adantr 484 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝐹:ℝ⟶ℂ)
23319adantr 484 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
234 ioossre 12790 . . . . . . . . . . 11 ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ
235234a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ)
236233, 235feqresmpt 6713 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹𝑥)))
237153, 160oveq12d 7157 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) = (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
238143, 146, 147iooshift 42152 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
239237, 238eqtrd 2836 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
240239mpteq1d 5122 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹𝑥)))
241 simpll 766 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝜑)
242 simplr 768 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑖 ∈ (0..^𝑀))
243238eleq2d 2878 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) ↔ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}))
244243biimpar 481 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
245143rexrd 10684 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
2462453adant3 1129 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) ∈ ℝ*)
247146rexrd 10684 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2482473adant3 1129 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
249 elioore 12760 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) → 𝑥 ∈ ℝ)
250249adantl 485 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
2518adantr 484 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
252250, 251resubcld 11061 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ℝ)
2532523adant2 1128 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ℝ)
254143recnd 10662 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
25562adantr 484 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℂ)
256254, 255pncand 10991 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + 𝑇) − 𝑇) = (𝑄𝑖))
257256eqcomd 2807 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (((𝑄𝑖) + 𝑇) − 𝑇))
2582573adant3 1129 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) = (((𝑄𝑖) + 𝑇) − 𝑇))
2591513adant3 1129 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
2602503adant2 1128 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
26183ad2ant1 1130 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
262151rexrd 10684 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ*)
2632623adant3 1129 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) ∈ ℝ*)
264159rexrd 10684 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
2652643adant3 1129 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
266 simp3 1135 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
267 ioogtlb 42125 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) < 𝑥)
268263, 265, 266, 267syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) < 𝑥)
269259, 260, 261, 268ltsub1dd 11245 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄𝑖) + 𝑇) − 𝑇) < (𝑥𝑇))
270258, 269eqbrtrd 5055 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) < (𝑥𝑇))
2711593adant3 1129 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
272 iooltub 42140 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇))
273263, 265, 266, 272syl3anc 1368 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇))
274260, 271, 261, 273ltsub1dd 11245 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇))
275146recnd 10662 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
276275, 255pncand 10991 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
2772763adant3 1129 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
278274, 277breqtrd 5059 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < (𝑄‘(𝑖 + 1)))
279246, 248, 253, 270, 278eliood 42128 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
280241, 242, 244, 279syl3anc 1368 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
281 fvres 6668 . . . . . . . . . . . 12 ((𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
282280, 281syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
283241, 244, 252syl2anc 587 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ ℝ)
28413ad2ant1 1130 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ∈ ℝ)
28533ad2ant1 1130 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐵 ∈ ℝ)
28664eqcomd 2807 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 = ((𝐴 + 𝑇) − 𝑇))
2872863ad2ant1 1130 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
288603ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
2891adantr 484 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ)
2901rexrd 10684 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ ℝ*)
291290adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ*)
2923rexrd 10684 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ*)
293292adantr 484 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ*)
2945, 6, 12fourierdlem15 42757 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
295294adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
296295, 142ffvelrnd 6833 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ (𝐴[,]𝐵))
297 iccgelb 12785 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄𝑖) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑄𝑖))
298291, 293, 296, 297syl3anc 1368 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ≤ (𝑄𝑖))
299289, 143, 147, 298leadd1dd 11247 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐴 + 𝑇) ≤ ((𝑄𝑖) + 𝑇))
3002993adant3 1129 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ≤ ((𝑄𝑖) + 𝑇))
301288, 259, 260, 300, 268lelttrd 10791 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) < 𝑥)
302288, 260, 261, 301ltsub1dd 11245 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) < (𝑥𝑇))
303287, 302eqbrtrd 5055 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 < (𝑥𝑇))
304284, 253, 303ltled 10781 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ≤ (𝑥𝑇))
3051463adant3 1129 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
306295, 145ffvelrnd 6833 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵))
307 iccleub 12784 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
308291, 293, 306, 307syl3anc 1368 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
3093083adant3 1129 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
310253, 305, 285, 278, 309ltletrd 10793 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < 𝐵)
311253, 285, 310ltled 10781 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ≤ 𝐵)
312284, 285, 253, 304, 311eliccd 42134 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ (𝐴[,]𝐵))
313241, 242, 244, 312syl3anc 1368 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ (𝐴[,]𝐵))
314241, 313jca 515 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)))
315 eleq1 2880 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥𝑇) ∈ (𝐴[,]𝐵)))
316315anbi2d 631 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑇) → ((𝜑𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵))))
317 oveq1 7146 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥𝑇) → (𝑦 + 𝑇) = ((𝑥𝑇) + 𝑇))
318317fveq2d 6653 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥𝑇) + 𝑇)))
319 fveq2 6649 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝐹𝑦) = (𝐹‘(𝑥𝑇)))
320318, 319eqeq12d 2817 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
321316, 320imbi12d 348 . . . . . . . . . . . . 13 (𝑦 = (𝑥𝑇) → (((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))))
322321, 219vtoclg 3518 . . . . . . . . . . . 12 ((𝑥𝑇) ∈ ℝ → ((𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
323283, 314, 322sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))
324244, 249syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ℝ)
325 recn 10620 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
326325adantl 485 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
32762adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
328326, 327npcand 10994 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → ((𝑥𝑇) + 𝑇) = 𝑥)
329328fveq2d 6653 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹𝑥))
330241, 324, 329syl2anc 587 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹𝑥))
331282, 323, 3303eqtr2rd 2843 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹𝑥) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)))
332331mpteq2dva 5128 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))))
333236, 240, 3323eqtrd 2840 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))))
334 ioosscn 12791 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
335334a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
336 eqeq1 2805 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇)))
337336rexbidv 3259 . . . . . . . . . . . 12 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)))
338 oveq1 7146 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇))
339338eqeq2d 2812 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇)))
340339cbvrexvw 3400 . . . . . . . . . . . 12 (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇))
341337, 340syl6bb 290 . . . . . . . . . . 11 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)))
342341cbvrabv 3442 . . . . . . . . . 10 {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}
343 eqid 2801 . . . . . . . . . 10 (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)))
344335, 255, 342, 21, 343cncfshift 42509 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) ∈ ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ))
345239eqcomd 2807 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))))
346345oveq1d 7154 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ) = (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
347344, 346eleqtrd 2895 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
348333, 347eqeltrd 2893 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
349348adantlr 714 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
350 ffdm 6514 . . . . . . . . . . . 12 (𝐹:ℝ⟶ℂ → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
35119, 350syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
352351simpld 498 . . . . . . . . . 10 (𝜑𝐹:dom 𝐹⟶ℂ)
353352adantr 484 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:dom 𝐹⟶ℂ)
354 ioossre 12790 . . . . . . . . . 10 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
355 fdm 6499 . . . . . . . . . . 11 (𝐹:ℝ⟶ℂ → dom 𝐹 = ℝ)
356233, 355syl 17 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → dom 𝐹 = ℝ)
357354, 356sseqtrrid 3971 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
358342eqcomi 2810 . . . . . . . . 9 {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}
359235, 345, 3563sstr4d 3965 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ⊆ dom 𝐹)
360342, 359eqsstrrid 3967 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} ⊆ dom 𝐹)
361 simpll 766 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
362361, 290syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐴 ∈ ℝ*)
363361, 292syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐵 ∈ ℝ*)
364361, 294syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
365 simplr 768 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
366 ioossicc 12815 . . . . . . . . . . . . 13 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
367366sseli 3914 . . . . . . . . . . . 12 (𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑧 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
368367adantl 485 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
369362, 363, 364, 365, 368fourierdlem1 42743 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ (𝐴[,]𝐵))
370 eleq1 2880 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑧 ∈ (𝐴[,]𝐵)))
371370anbi2d 631 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝜑𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑧 ∈ (𝐴[,]𝐵))))
372 oveq1 7146 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑥 + 𝑇) = (𝑧 + 𝑇))
373372fveq2d 6653 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑧 + 𝑇)))
374 fveq2 6649 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
375373, 374eqeq12d 2817 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧)))
376371, 375imbi12d 348 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))))
377376, 14chvarvv 2005 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))
378361, 369, 377syl2anc 587 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))
379353, 335, 357, 255, 358, 360, 378, 23limcperiod 42263 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄𝑖) + 𝑇)))
380358, 345syl5eq 2848 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))))
381380reseq2d 5822 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) = (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))))
382153eqcomd 2807 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) = (𝑆𝑖))
383381, 382oveq12d 7157 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄𝑖) + 𝑇)) = ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
384379, 383eleqtrd 2895 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
385384adantlr 714 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
386353, 335, 357, 255, 358, 360, 378, 25limcperiod 42263 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄‘(𝑖 + 1)) + 𝑇)))
387160eqcomd 2807 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) = (𝑆‘(𝑖 + 1)))
388381, 387oveq12d 7157 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄‘(𝑖 + 1)) + 𝑇)) = ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
389386, 388eleqtrd 2895 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
390389adantlr 714 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
391 eqeq1 2805 . . . . . . . 8 (𝑦 = 𝑥 → (𝑦 = (𝑆𝑖) ↔ 𝑥 = (𝑆𝑖)))
392 eqeq1 2805 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑦 = (𝑆‘(𝑖 + 1)) ↔ 𝑥 = (𝑆‘(𝑖 + 1))))
393392, 29ifbieq2d 4453 . . . . . . . 8 (𝑦 = 𝑥 → if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦)) = if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥)))
394391, 393ifbieq2d 4453 . . . . . . 7 (𝑦 = 𝑥 → if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦))) = if(𝑥 = (𝑆𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
395394cbvmptv 5136 . . . . . 6 (𝑦 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦)))) = (𝑥 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
396 eqid 2801 . . . . . 6 (𝑥 ∈ (((𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇))‘𝑖)[,]((𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇))‘(𝑖 + 1))) ↦ ((𝑦 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦))))‘(𝑥 − -𝑇))) = (𝑥 ∈ (((𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇))‘𝑖)[,]((𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇))‘(𝑖 + 1))) ↦ ((𝑦 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦))))‘(𝑥 − -𝑇)))
39777, 79, 80, 81, 84, 170, 228, 231, 232, 349, 385, 390, 395, 396fourierdlem81 42822 . . . . 5 ((𝜑 ∧ 0 < -𝑇) → ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥)
39874, 397eqtr2d 2837 . . . 4 ((𝜑 ∧ 0 < -𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
39949, 59, 398syl2anc 587 . . 3 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
40048, 399pm2.61dan 812 . 2 ((𝜑 ∧ ¬ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
40134, 400pm2.61dan 812 1 (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3a 1084   = wceq 1538  wcel 2112  wral 3109  wrex 3110  {crab 3113  Vcvv 3444  wss 3884  ifcif 4428   class class class wbr 5033  cmpt 5113  dom cdm 5523  cres 5525  wf 6324  cfv 6328  (class class class)co 7139  m cmap 8393  cc 10528  cr 10529  0cc0 10530  1c1 10531   + caddc 10533  *cxr 10667   < clt 10668  cle 10669  cmin 10863  -cneg 10864  cn 11629  0cn0 11889  cz 11973  cuz 12235  (,)cioo 12730  [,]cicc 12733  ...cfz 12889  ..^cfzo 13032  cnccncf 23485  citg 24226   lim climc 24469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445  ax-inf2 9092  ax-cc 9850  ax-cnex 10586  ax-resscn 10587  ax-1cn 10588  ax-icn 10589  ax-addcl 10590  ax-addrcl 10591  ax-mulcl 10592  ax-mulrcl 10593  ax-mulcom 10594  ax-addass 10595  ax-mulass 10596  ax-distr 10597  ax-i2m1 10598  ax-1ne0 10599  ax-1rid 10600  ax-rnegex 10601  ax-rrecex 10602  ax-cnre 10603  ax-pre-lttri 10604  ax-pre-lttrn 10605  ax-pre-ltadd 10606  ax-pre-mulgt0 10607  ax-pre-sup 10608  ax-addf 10609  ax-mulf 10610
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ne 2991  df-nel 3095  df-ral 3114  df-rex 3115  df-reu 3116  df-rmo 3117  df-rab 3118  df-v 3446  df-sbc 3724  df-csb 3832  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-symdif 4172  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-tp 4533  df-op 4535  df-uni 4804  df-int 4842  df-iun 4886  df-iin 4887  df-disj 4999  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5428  df-eprel 5433  df-po 5442  df-so 5443  df-fr 5482  df-se 5483  df-we 5484  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-pred 6120  df-ord 6166  df-on 6167  df-lim 6168  df-suc 6169  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-f1 6333  df-fo 6334  df-f1o 6335  df-fv 6336  df-isom 6337  df-riota 7097  df-ov 7142  df-oprab 7143  df-mpo 7144  df-of 7393  df-ofr 7394  df-om 7565  df-1st 7675  df-2nd 7676  df-supp 7818  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-omul 8094  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-dju 9318  df-card 9356  df-acn 9359  df-pnf 10670  df-mnf 10671  df-xr 10672  df-ltxr 10673  df-le 10674  df-sub 10865  df-neg 10866  df-div 11291  df-nn 11630  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12382  df-xneg 12499  df-xadd 12500  df-xmul 12501  df-ioo 12734  df-ioc 12735  df-ico 12736  df-icc 12737  df-fz 12890  df-fzo 13033  df-fl 13161  df-mod 13237  df-seq 13369  df-exp 13430  df-hash 13691  df-cj 14454  df-re 14455  df-im 14456  df-sqrt 14590  df-abs 14591  df-limsup 14824  df-clim 14841  df-rlim 14842  df-sum 15039  df-struct 16481  df-ndx 16482  df-slot 16483  df-base 16485  df-sets 16486  df-ress 16487  df-plusg 16574  df-mulr 16575  df-starv 16576  df-sca 16577  df-vsca 16578  df-ip 16579  df-tset 16580  df-ple 16581  df-ds 16583  df-unif 16584  df-hom 16585  df-cco 16586  df-rest 16692  df-topn 16693  df-0g 16711  df-gsum 16712  df-topgen 16713  df-pt 16714  df-prds 16717  df-xrs 16771  df-qtop 16776  df-imas 16777  df-xps 16779  df-mre 16853  df-mrc 16854  df-acs 16856  df-mgm 17848  df-sgrp 17897  df-mnd 17908  df-submnd 17953  df-mulg 18221  df-cntz 18443  df-cmn 18904  df-psmet 20087  df-xmet 20088  df-met 20089  df-bl 20090  df-mopn 20091  df-fbas 20092  df-fg 20093  df-cnfld 20096  df-top 21503  df-topon 21520  df-topsp 21542  df-bases 21555  df-cld 21628  df-ntr 21629  df-cls 21630  df-nei 21707  df-lp 21745  df-perf 21746  df-cn 21836  df-cnp 21837  df-haus 21924  df-cmp 21996  df-tx 22171  df-hmeo 22364  df-fil 22455  df-fm 22547  df-flim 22548  df-flf 22549  df-xms 22931  df-ms 22932  df-tms 22933  df-cncf 23487  df-ovol 24072  df-vol 24073  df-mbf 24227  df-itg1 24228  df-itg2 24229  df-ibl 24230  df-itg 24231  df-0p 24278  df-ditg 24454  df-limc 24473  df-dv 24474
This theorem is referenced by:  fourierdlem107  42848
  Copyright terms: Public domain W3C validator