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 39743
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 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
fourierdlem92.m (𝜑𝑀 ∈ ℕ)
fourierdlem92.t (𝜑𝑇 ∈ ℝ)
fourierdlem92.q (𝜑𝑄 ∈ (𝑃𝑀))
fourierdlem92.fper ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
fourierdlem92.s 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
fourierdlem92.h 𝐻 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (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 481 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐴 ∈ ℝ)
3 fourierdlem92.b . . . 4 (𝜑𝐵 ∈ ℝ)
43adantr 481 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐵 ∈ ℝ)
5 fourierdlem92.p . . 3 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
6 fourierdlem92.m . . . 4 (𝜑𝑀 ∈ ℕ)
76adantr 481 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑀 ∈ ℕ)
8 fourierdlem92.t . . . . 5 (𝜑𝑇 ∈ ℝ)
98adantr 481 . . . 4 ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ)
10 simpr 477 . . . 4 ((𝜑 ∧ 0 < 𝑇) → 0 < 𝑇)
119, 10elrpd 11820 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ+)
12 fourierdlem92.q . . . 4 (𝜑𝑄 ∈ (𝑃𝑀))
1312adantr 481 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑄 ∈ (𝑃𝑀))
14 fourierdlem92.fper . . . 4 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
1514adantlr 750 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
16 fveq2 6153 . . . . 5 (𝑗 = 𝑖 → (𝑄𝑗) = (𝑄𝑖))
1716oveq1d 6625 . . . 4 (𝑗 = 𝑖 → ((𝑄𝑗) + 𝑇) = ((𝑄𝑖) + 𝑇))
1817cbvmptv 4715 . . 3 (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
19 fourierdlem92.f . . . 4 (𝜑𝐹:ℝ⟶ℂ)
2019adantr 481 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐹:ℝ⟶ℂ)
21 fourierdlem92.cncf . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
2221adantlr 750 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
23 fourierdlem92.r . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
2423adantlr 750 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
25 fourierdlem92.l . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
2625adantlr 750 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
27 eqeq1 2625 . . . . 5 (𝑦 = 𝑥 → (𝑦 = (𝑄𝑖) ↔ 𝑥 = (𝑄𝑖)))
28 eqeq1 2625 . . . . . 6 (𝑦 = 𝑥 → (𝑦 = (𝑄‘(𝑖 + 1)) ↔ 𝑥 = (𝑄‘(𝑖 + 1))))
29 fveq2 6153 . . . . . 6 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
3028, 29ifbieq2d 4088 . . . . 5 (𝑦 = 𝑥 → if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦)) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥)))
3127, 30ifbieq2d 4088 . . . 4 (𝑦 = 𝑥 → if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦))) = if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
3231cbvmptv 4715 . . 3 (𝑦 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦)))) = (𝑥 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
33 eqid 2621 . . 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 39732 . 2 ((𝜑 ∧ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
35 simpr 477 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝑇 = 0)
3635oveq2d 6626 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐴 + 𝑇) = (𝐴 + 0))
371recnd 10019 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
3837adantr 481 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝐴 ∈ ℂ)
3938addid1d 10187 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐴 + 0) = 𝐴)
4036, 39eqtrd 2655 . . . . . 6 ((𝜑𝑇 = 0) → (𝐴 + 𝑇) = 𝐴)
4135oveq2d 6626 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐵 + 𝑇) = (𝐵 + 0))
423recnd 10019 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
4342adantr 481 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝐵 ∈ ℂ)
4443addid1d 10187 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐵 + 0) = 𝐵)
4541, 44eqtrd 2655 . . . . . 6 ((𝜑𝑇 = 0) → (𝐵 + 𝑇) = 𝐵)
4640, 45oveq12d 6628 . . . . 5 ((𝜑𝑇 = 0) → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = (𝐴[,]𝐵))
4746itgeq1d 39500 . . . 4 ((𝜑𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
4847adantlr 750 . . 3 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
49 simpll 789 . . . 4 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝜑)
50 simpr 477 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 𝑇 = 0)
51 simplr 791 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 0 < 𝑇)
52 ioran 511 . . . . . . 7 (¬ (𝑇 = 0 ∨ 0 < 𝑇) ↔ (¬ 𝑇 = 0 ∧ ¬ 0 < 𝑇))
5350, 51, 52sylanbrc 697 . . . . . 6 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ (𝑇 = 0 ∨ 0 < 𝑇))
5449, 8syl 17 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 ∈ ℝ)
55 0red 9992 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 ∈ ℝ)
5654, 55lttrid 10126 . . . . . 6 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ ¬ (𝑇 = 0 ∨ 0 < 𝑇)))
5753, 56mpbird 247 . . . . 5 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 < 0)
5854lt0neg1d 10548 . . . . 5 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ 0 < -𝑇))
5957, 58mpbid 222 . . . 4 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 < -𝑇)
601, 8readdcld 10020 . . . . . . . . . . . 12 (𝜑 → (𝐴 + 𝑇) ∈ ℝ)
6160recnd 10019 . . . . . . . . . . 11 (𝜑 → (𝐴 + 𝑇) ∈ ℂ)
628recnd 10019 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
6361, 62negsubd 10349 . . . . . . . . . 10 (𝜑 → ((𝐴 + 𝑇) + -𝑇) = ((𝐴 + 𝑇) − 𝑇))
6437, 62pncand 10344 . . . . . . . . . 10 (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
6563, 64eqtrd 2655 . . . . . . . . 9 (𝜑 → ((𝐴 + 𝑇) + -𝑇) = 𝐴)
663, 8readdcld 10020 . . . . . . . . . . . 12 (𝜑 → (𝐵 + 𝑇) ∈ ℝ)
6766recnd 10019 . . . . . . . . . . 11 (𝜑 → (𝐵 + 𝑇) ∈ ℂ)
6867, 62negsubd 10349 . . . . . . . . . 10 (𝜑 → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇))
6942, 62pncand 10344 . . . . . . . . . 10 (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
7068, 69eqtrd 2655 . . . . . . . . 9 (𝜑 → ((𝐵 + 𝑇) + -𝑇) = 𝐵)
7165, 70oveq12d 6628 . . . . . . . 8 (𝜑 → (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)) = (𝐴[,]𝐵))
7271eqcomd 2627 . . . . . . 7 (𝜑 → (𝐴[,]𝐵) = (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)))
7372itgeq1d 39500 . . . . . 6 (𝜑 → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥)
7473adantr 481 . . . . 5 ((𝜑 ∧ 0 < -𝑇) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥)
751adantr 481 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝐴 ∈ ℝ)
768adantr 481 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝑇 ∈ ℝ)
7775, 76readdcld 10020 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → (𝐴 + 𝑇) ∈ ℝ)
783adantr 481 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝐵 ∈ ℝ)
7978, 76readdcld 10020 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → (𝐵 + 𝑇) ∈ ℝ)
80 eqid 2621 . . . . . 6 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
816adantr 481 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝑀 ∈ ℕ)
8276renegcld 10408 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ)
83 simpr 477 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 0 < -𝑇)
8482, 83elrpd 11820 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ+)
855fourierdlem2 39654 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
866, 85syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
8712, 86mpbid 222 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
8887simpld 475 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
89 elmapi 7830 . . . . . . . . . . . . . . 15 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
9088, 89syl 17 . . . . . . . . . . . . . 14 (𝜑𝑄:(0...𝑀)⟶ℝ)
9190ffvelrnda 6320 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) ∈ ℝ)
928adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑇 ∈ ℝ)
9391, 92readdcld 10020 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
94 fourierdlem92.s . . . . . . . . . . . 12 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
9593, 94fmptd 6346 . . . . . . . . . . 11 (𝜑𝑆:(0...𝑀)⟶ℝ)
96 reex 9978 . . . . . . . . . . . . 13 ℝ ∈ V
9796a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ V)
98 ovex 6638 . . . . . . . . . . . . 13 (0...𝑀) ∈ V
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → (0...𝑀) ∈ V)
10097, 99elmapd 7823 . . . . . . . . . . 11 (𝜑 → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ↔ 𝑆:(0...𝑀)⟶ℝ))
10195, 100mpbird 247 . . . . . . . . . 10 (𝜑𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)))
10294a1i 11 . . . . . . . . . . . . 13 (𝜑𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇)))
103 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
104103oveq1d 6625 . . . . . . . . . . . . . 14 (𝑖 = 0 → ((𝑄𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
105104adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑖 = 0) → ((𝑄𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
106 0zd 11340 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℤ)
1076nnzd 11432 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
108106, 107, 1063jca 1240 . . . . . . . . . . . . . . 15 (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ))
109 0le0 11061 . . . . . . . . . . . . . . . 16 0 ≤ 0
110109a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ 0)
111 nnnn0 11250 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
112111nn0ge0d 11305 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → 0 ≤ 𝑀)
1136, 112syl 17 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ 𝑀)
114108, 110, 113jca32 557 . . . . . . . . . . . . . 14 (𝜑 → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
115 elfz2 12282 . . . . . . . . . . . . . 14 (0 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
116114, 115sylibr 224 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ (0...𝑀))
11790, 116ffvelrnd 6321 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ∈ ℝ)
118117, 8readdcld 10020 . . . . . . . . . . . . 13 (𝜑 → ((𝑄‘0) + 𝑇) ∈ ℝ)
119102, 105, 116, 118fvmptd 6250 . . . . . . . . . . . 12 (𝜑 → (𝑆‘0) = ((𝑄‘0) + 𝑇))
120 simprll 801 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄‘0) = 𝐴)
12187, 120syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘0) = 𝐴)
122121oveq1d 6625 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘0) + 𝑇) = (𝐴 + 𝑇))
123119, 122eqtrd 2655 . . . . . . . . . . 11 (𝜑 → (𝑆‘0) = (𝐴 + 𝑇))
124 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝑄𝑖) = (𝑄𝑀))
125124oveq1d 6625 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → ((𝑄𝑖) + 𝑇) = ((𝑄𝑀) + 𝑇))
126125adantl 482 . . . . . . . . . . . . 13 ((𝜑𝑖 = 𝑀) → ((𝑄𝑖) + 𝑇) = ((𝑄𝑀) + 𝑇))
1276nnnn0d 11302 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ0)
128 nn0uz 11673 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
129127, 128syl6eleq 2708 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ‘0))
130 eluzfz2 12298 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
131129, 130syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (0...𝑀))
13290, 131ffvelrnd 6321 . . . . . . . . . . . . . 14 (𝜑 → (𝑄𝑀) ∈ ℝ)
133132, 8readdcld 10020 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝑀) + 𝑇) ∈ ℝ)
134102, 126, 131, 133fvmptd 6250 . . . . . . . . . . . 12 (𝜑 → (𝑆𝑀) = ((𝑄𝑀) + 𝑇))
135 simprlr 802 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄𝑀) = 𝐵)
13687, 135syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝑀) = 𝐵)
137136oveq1d 6625 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝑀) + 𝑇) = (𝐵 + 𝑇))
138134, 137eqtrd 2655 . . . . . . . . . . 11 (𝜑 → (𝑆𝑀) = (𝐵 + 𝑇))
139123, 138jca 554 . . . . . . . . . 10 (𝜑 → ((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)))
14090adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
141 elfzofz 12433 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
142141adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
143140, 142ffvelrnd 6321 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
144 fzofzp1 12513 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
145144adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
146140, 145ffvelrnd 6321 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
1478adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℝ)
14887simprrd 796 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
149148r19.21bi 2927 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
150143, 146, 147, 149ltadd1dd 10589 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) < ((𝑄‘(𝑖 + 1)) + 𝑇))
151143, 147readdcld 10020 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
15294fvmpt2 6253 . . . . . . . . . . . . 13 ((𝑖 ∈ (0...𝑀) ∧ ((𝑄𝑖) + 𝑇) ∈ ℝ) → (𝑆𝑖) = ((𝑄𝑖) + 𝑇))
153142, 151, 152syl2anc 692 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆𝑖) = ((𝑄𝑖) + 𝑇))
15494, 18eqtr4i 2646 . . . . . . . . . . . . . 14 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇))
155154a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇)))
156 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) → (𝑄𝑗) = (𝑄‘(𝑖 + 1)))
157156oveq1d 6625 . . . . . . . . . . . . . 14 (𝑗 = (𝑖 + 1) → ((𝑄𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
158157adantl 482 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
159146, 147readdcld 10020 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
160155, 158, 145, 159fvmptd 6250 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) + 𝑇))
161150, 153, 1603brtr4d 4650 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆𝑖) < (𝑆‘(𝑖 + 1)))
162161ralrimiva 2961 . . . . . . . . . 10 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))
163101, 139, 162jca32 557 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
164 fourierdlem92.h . . . . . . . . . . 11 𝐻 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
165164fourierdlem2 39654 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑆 ∈ (𝐻𝑀) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
1666, 165syl 17 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐻𝑀) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
167163, 166mpbird 247 . . . . . . . 8 (𝜑𝑆 ∈ (𝐻𝑀))
168164fveq1i 6154 . . . . . . . 8 (𝐻𝑀) = ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀)
169167, 168syl6eleq 2708 . . . . . . 7 (𝜑𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀))
170169adantr 481 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀))
17160adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
17266adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ)
173 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
174 eliccre 39162 . . . . . . . . . . . 12 (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
175171, 172, 173, 174syl3anc 1323 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
176175recnd 10019 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ)
17762negcld 10330 . . . . . . . . . . 11 (𝜑 → -𝑇 ∈ ℂ)
178177adantr 481 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℂ)
179176, 178addcld 10010 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℂ)
180 simpl 473 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝜑)
1811adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ)
1823adantr 481 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ)
1838renegcld 10408 . . . . . . . . . . . . 13 (𝜑 → -𝑇 ∈ ℝ)
184183adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℝ)
185175, 184readdcld 10020 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℝ)
18663, 64eqtr2d 2656 . . . . . . . . . . . . 13 (𝜑𝐴 = ((𝐴 + 𝑇) + -𝑇))
187186adantr 481 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) + -𝑇))
188171rexrd 10040 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ*)
189172rexrd 10040 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ*)
190 iccgelb 12179 . . . . . . . . . . . . . 14 (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ*𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
191188, 189, 173, 190syl3anc 1323 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
192171, 175, 184, 191leadd1dd 10592 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) + -𝑇) ≤ (𝑥 + -𝑇))
193187, 192eqbrtrd 4640 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 + -𝑇))
194 iccleub 12178 . . . . . . . . . . . . . 14 (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ*𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
195188, 189, 173, 194syl3anc 1323 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
196175, 172, 184, 195leadd1dd 10592 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ ((𝐵 + 𝑇) + -𝑇))
197172recnd 10019 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℂ)
19862adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ)
199197, 198negsubd 10349 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇))
20069adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
201199, 200eqtrd 2655 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = 𝐵)
202196, 201breqtrd 4644 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ 𝐵)
203181, 182, 185, 193, 202eliccd 39160 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))
204180, 203jca 554 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))
205 eleq1 2686 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))
206205anbi2d 739 . . . . . . . . . . 11 (𝑦 = (𝑥 + -𝑇) → ((𝜑𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))))
207 oveq1 6617 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + -𝑇) → (𝑦 + 𝑇) = ((𝑥 + -𝑇) + 𝑇))
208207fveq2d 6157 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥 + -𝑇) + 𝑇)))
209 fveq2 6153 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝐹𝑦) = (𝐹‘(𝑥 + -𝑇)))
210208, 209eqeq12d 2636 . . . . . . . . . . 11 (𝑦 = (𝑥 + -𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))
211206, 210imbi12d 334 . . . . . . . . . 10 (𝑦 = (𝑥 + -𝑇) → (((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))))
212 eleq1 2686 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
213212anbi2d 739 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝜑𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑦 ∈ (𝐴[,]𝐵))))
214 oveq1 6617 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
215214fveq2d 6157 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
216 fveq2 6153 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
217215, 216eqeq12d 2636 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)))
218213, 217imbi12d 334 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))))
219218, 14chvarv 2262 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
220211, 219vtoclg 3255 . . . . . . . . 9 ((𝑥 + -𝑇) ∈ ℂ → ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))
221179, 204, 220sylc 65 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))
222176, 198negsubd 10349 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) = (𝑥𝑇))
223222oveq1d 6625 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = ((𝑥𝑇) + 𝑇))
224176, 198npcand 10347 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥𝑇) + 𝑇) = 𝑥)
225223, 224eqtrd 2655 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = 𝑥)
226225fveq2d 6157 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹𝑥))
227221, 226eqtr3d 2657 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹𝑥))
228227adantlr 750 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹𝑥))
229 fveq2 6153 . . . . . . . 8 (𝑗 = 𝑖 → (𝑆𝑗) = (𝑆𝑖))
230229oveq1d 6625 . . . . . . 7 (𝑗 = 𝑖 → ((𝑆𝑗) + -𝑇) = ((𝑆𝑖) + -𝑇))
231230cbvmptv 4715 . . . . . 6 (𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑆𝑖) + -𝑇))
23219adantr 481 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝐹:ℝ⟶ℂ)
23319adantr 481 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
234 ioossre 12184 . . . . . . . . . . 11 ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ
235234a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ)
236233, 235feqresmpt 6212 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹𝑥)))
237153, 160oveq12d 6628 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) = (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
238143, 146, 147iooshift 39182 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
239237, 238eqtrd 2655 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
240239mpteq1d 4703 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹𝑥)))
241 simpll 789 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝜑)
242 simplr 791 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑖 ∈ (0..^𝑀))
243238eleq2d 2684 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) ↔ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}))
244243biimpar 502 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
245143rexrd 10040 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
2462453adant3 1079 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) ∈ ℝ*)
247146rexrd 10040 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2482473adant3 1079 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
249 elioore 12154 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) → 𝑥 ∈ ℝ)
250249adantl 482 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
2518adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
252250, 251resubcld 10409 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ℝ)
2532523adant2 1078 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ℝ)
254143recnd 10019 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
25562adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℂ)
256254, 255pncand 10344 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + 𝑇) − 𝑇) = (𝑄𝑖))
257256eqcomd 2627 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (((𝑄𝑖) + 𝑇) − 𝑇))
2582573adant3 1079 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) = (((𝑄𝑖) + 𝑇) − 𝑇))
2591513adant3 1079 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
2602503adant2 1078 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
26183ad2ant1 1080 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
262151rexrd 10040 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ*)
2632623adant3 1079 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) ∈ ℝ*)
264159rexrd 10040 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
2652643adant3 1079 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
266 simp3 1061 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
267 ioogtlb 39151 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) < 𝑥)
268263, 265, 266, 267syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) < 𝑥)
269259, 260, 261, 268ltsub1dd 10590 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄𝑖) + 𝑇) − 𝑇) < (𝑥𝑇))
270258, 269eqbrtrd 4640 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) < (𝑥𝑇))
2711593adant3 1079 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
272 iooltub 39169 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇))
273263, 265, 266, 272syl3anc 1323 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇))
274260, 271, 261, 273ltsub1dd 10590 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇))
275146recnd 10019 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
276275, 255pncand 10344 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
2772763adant3 1079 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
278274, 277breqtrd 4644 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < (𝑄‘(𝑖 + 1)))
279246, 248, 253, 270, 278eliood 39154 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
280241, 242, 244, 279syl3anc 1323 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
281 fvres 6169 . . . . . . . . . . . 12 ((𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
282280, 281syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
283241, 244, 252syl2anc 692 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ ℝ)
28413ad2ant1 1080 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ∈ ℝ)
28533ad2ant1 1080 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐵 ∈ ℝ)
28664eqcomd 2627 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 = ((𝐴 + 𝑇) − 𝑇))
2872863ad2ant1 1080 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
288603ad2ant1 1080 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
2891adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ)
2901rexrd 10040 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ ℝ*)
291290adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ*)
2923rexrd 10040 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ*)
293292adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ*)
2945, 6, 12fourierdlem15 39667 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
295294adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
296295, 142ffvelrnd 6321 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ (𝐴[,]𝐵))
297 iccgelb 12179 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄𝑖) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑄𝑖))
298291, 293, 296, 297syl3anc 1323 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ≤ (𝑄𝑖))
299289, 143, 147, 298leadd1dd 10592 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐴 + 𝑇) ≤ ((𝑄𝑖) + 𝑇))
3002993adant3 1079 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ≤ ((𝑄𝑖) + 𝑇))
301288, 259, 260, 300, 268lelttrd 10146 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) < 𝑥)
302288, 260, 261, 301ltsub1dd 10590 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) < (𝑥𝑇))
303287, 302eqbrtrd 4640 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 < (𝑥𝑇))
304284, 253, 303ltled 10136 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ≤ (𝑥𝑇))
3051463adant3 1079 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
306295, 145ffvelrnd 6321 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵))
307 iccleub 12178 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
308291, 293, 306, 307syl3anc 1323 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
3093083adant3 1079 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
310253, 305, 285, 278, 309ltletrd 10148 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < 𝐵)
311253, 285, 310ltled 10136 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ≤ 𝐵)
312284, 285, 253, 304, 311eliccd 39160 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ (𝐴[,]𝐵))
313241, 242, 244, 312syl3anc 1323 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ (𝐴[,]𝐵))
314241, 313jca 554 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)))
315 eleq1 2686 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥𝑇) ∈ (𝐴[,]𝐵)))
316315anbi2d 739 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑇) → ((𝜑𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵))))
317 oveq1 6617 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥𝑇) → (𝑦 + 𝑇) = ((𝑥𝑇) + 𝑇))
318317fveq2d 6157 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥𝑇) + 𝑇)))
319 fveq2 6153 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝐹𝑦) = (𝐹‘(𝑥𝑇)))
320318, 319eqeq12d 2636 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
321316, 320imbi12d 334 . . . . . . . . . . . . 13 (𝑦 = (𝑥𝑇) → (((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))))
322321, 219vtoclg 3255 . . . . . . . . . . . 12 ((𝑥𝑇) ∈ ℝ → ((𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
323283, 314, 322sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))
324244, 249syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ℝ)
325 recn 9977 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
326325adantl 482 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
32762adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
328326, 327npcand 10347 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → ((𝑥𝑇) + 𝑇) = 𝑥)
329328fveq2d 6157 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹𝑥))
330241, 324, 329syl2anc 692 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹𝑥))
331282, 323, 3303eqtr2rd 2662 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹𝑥) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)))
332331mpteq2dva 4709 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))))
333236, 240, 3323eqtrd 2659 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))))
334 ioosscn 39150 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
335334a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
336 eqeq1 2625 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇)))
337336rexbidv 3046 . . . . . . . . . . . 12 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)))
338 oveq1 6617 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇))
339338eqeq2d 2631 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇)))
340339cbvrexv 3163 . . . . . . . . . . . 12 (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇))
341337, 340syl6bb 276 . . . . . . . . . . 11 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)))
342341cbvrabv 3188 . . . . . . . . . 10 {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}
343 eqid 2621 . . . . . . . . . 10 (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)))
344335, 255, 342, 21, 343cncfshift 39413 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) ∈ ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ))
345239eqcomd 2627 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))))
346345oveq1d 6625 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ) = (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
347344, 346eleqtrd 2700 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
348333, 347eqeltrd 2698 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
349348adantlr 750 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
350 ffdm 6024 . . . . . . . . . . . 12 (𝐹:ℝ⟶ℂ → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
35119, 350syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
352351simpld 475 . . . . . . . . . 10 (𝜑𝐹:dom 𝐹⟶ℂ)
353352adantr 481 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:dom 𝐹⟶ℂ)
354 ioossre 12184 . . . . . . . . . 10 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
355 fdm 6013 . . . . . . . . . . 11 (𝐹:ℝ⟶ℂ → dom 𝐹 = ℝ)
356233, 355syl 17 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → dom 𝐹 = ℝ)
357354, 356syl5sseqr 3638 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
358342eqcomi 2630 . . . . . . . . 9 {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}
359235, 345, 3563sstr4d 3632 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ⊆ dom 𝐹)
360342, 359syl5eqssr 3634 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} ⊆ dom 𝐹)
361 simpll 789 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
362361, 290syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐴 ∈ ℝ*)
363361, 292syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐵 ∈ ℝ*)
364361, 294syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
365 simplr 791 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
366 ioossicc 12208 . . . . . . . . . . . . 13 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
367366sseli 3583 . . . . . . . . . . . 12 (𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑧 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
368367adantl 482 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
369362, 363, 364, 365, 368fourierdlem1 39653 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ (𝐴[,]𝐵))
370 eleq1 2686 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑧 ∈ (𝐴[,]𝐵)))
371370anbi2d 739 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝜑𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑧 ∈ (𝐴[,]𝐵))))
372 oveq1 6617 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑥 + 𝑇) = (𝑧 + 𝑇))
373372fveq2d 6157 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑧 + 𝑇)))
374 fveq2 6153 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
375373, 374eqeq12d 2636 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧)))
376371, 375imbi12d 334 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))))
377376, 14chvarv 2262 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))
378361, 369, 377syl2anc 692 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))
379353, 335, 357, 255, 358, 360, 378, 23limcperiod 39287 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄𝑖) + 𝑇)))
380358, 345syl5eq 2667 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))))
381380reseq2d 5361 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) = (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))))
382153eqcomd 2627 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) = (𝑆𝑖))
383381, 382oveq12d 6628 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄𝑖) + 𝑇)) = ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
384379, 383eleqtrd 2700 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
385384adantlr 750 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
386353, 335, 357, 255, 358, 360, 378, 25limcperiod 39287 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄‘(𝑖 + 1)) + 𝑇)))
387160eqcomd 2627 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) = (𝑆‘(𝑖 + 1)))
388381, 387oveq12d 6628 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄‘(𝑖 + 1)) + 𝑇)) = ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
389386, 388eleqtrd 2700 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
390389adantlr 750 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
391 eqeq1 2625 . . . . . . . 8 (𝑦 = 𝑥 → (𝑦 = (𝑆𝑖) ↔ 𝑥 = (𝑆𝑖)))
392 eqeq1 2625 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑦 = (𝑆‘(𝑖 + 1)) ↔ 𝑥 = (𝑆‘(𝑖 + 1))))
393392, 29ifbieq2d 4088 . . . . . . . 8 (𝑦 = 𝑥 → if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦)) = if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥)))
394391, 393ifbieq2d 4088 . . . . . . 7 (𝑦 = 𝑥 → if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦))) = if(𝑥 = (𝑆𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
395394cbvmptv 4715 . . . . . 6 (𝑦 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦)))) = (𝑥 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
396 eqid 2621 . . . . . 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 39732 . . . . 5 ((𝜑 ∧ 0 < -𝑇) → ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥)
39874, 397eqtr2d 2656 . . . 4 ((𝜑 ∧ 0 < -𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
39949, 59, 398syl2anc 692 . . 3 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
40048, 399pm2.61dan 831 . 2 ((𝜑 ∧ ¬ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
40134, 400pm2.61dan 831 1 (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384  w3a 1036   = wceq 1480  wcel 1987  wral 2907  wrex 2908  {crab 2911  Vcvv 3189  wss 3559  ifcif 4063   class class class wbr 4618  cmpt 4678  dom cdm 5079  cres 5081  wf 5848  cfv 5852  (class class class)co 6610  𝑚 cmap 7809  cc 9885  cr 9886  0cc0 9887  1c1 9888   + caddc 9890  *cxr 10024   < clt 10025  cle 10026  cmin 10217  -cneg 10218  cn 10971  0cn0 11243  cz 11328  cuz 11638  (,)cioo 12124  [,]cicc 12127  ...cfz 12275  ..^cfzo 12413  cnccncf 22598  citg 23306   lim climc 23545
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-inf2 8489  ax-cc 9208  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964  ax-pre-sup 9965  ax-addf 9966  ax-mulf 9967
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-iin 4493  df-disj 4589  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-of 6857  df-ofr 6858  df-om 7020  df-1st 7120  df-2nd 7121  df-supp 7248  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-2o 7513  df-oadd 7516  df-omul 7517  df-er 7694  df-map 7811  df-pm 7812  df-ixp 7860  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-fsupp 8227  df-fi 8268  df-sup 8299  df-inf 8300  df-oi 8366  df-card 8716  df-acn 8719  df-cda 8941  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-div 10636  df-nn 10972  df-2 11030  df-3 11031  df-4 11032  df-5 11033  df-6 11034  df-7 11035  df-8 11036  df-9 11037  df-n0 11244  df-z 11329  df-dec 11445  df-uz 11639  df-q 11740  df-rp 11784  df-xneg 11897  df-xadd 11898  df-xmul 11899  df-ioo 12128  df-ioc 12129  df-ico 12130  df-icc 12131  df-fz 12276  df-fzo 12414  df-fl 12540  df-mod 12616  df-seq 12749  df-exp 12808  df-hash 13065  df-cj 13780  df-re 13781  df-im 13782  df-sqrt 13916  df-abs 13917  df-limsup 14143  df-clim 14160  df-rlim 14161  df-sum 14358  df-struct 15790  df-ndx 15791  df-slot 15792  df-base 15793  df-sets 15794  df-ress 15795  df-plusg 15882  df-mulr 15883  df-starv 15884  df-sca 15885  df-vsca 15886  df-ip 15887  df-tset 15888  df-ple 15889  df-ds 15892  df-unif 15893  df-hom 15894  df-cco 15895  df-rest 16011  df-topn 16012  df-0g 16030  df-gsum 16031  df-topgen 16032  df-pt 16033  df-prds 16036  df-xrs 16090  df-qtop 16095  df-imas 16096  df-xps 16098  df-mre 16174  df-mrc 16175  df-acs 16177  df-mgm 17170  df-sgrp 17212  df-mnd 17223  df-submnd 17264  df-mulg 17469  df-cntz 17678  df-cmn 18123  df-psmet 19666  df-xmet 19667  df-met 19668  df-bl 19669  df-mopn 19670  df-fbas 19671  df-fg 19672  df-cnfld 19675  df-top 20627  df-topon 20644  df-topsp 20657  df-bases 20670  df-cld 20742  df-ntr 20743  df-cls 20744  df-nei 20821  df-lp 20859  df-perf 20860  df-cn 20950  df-cnp 20951  df-haus 21038  df-cmp 21109  df-tx 21284  df-hmeo 21477  df-fil 21569  df-fm 21661  df-flim 21662  df-flf 21663  df-xms 22044  df-ms 22045  df-tms 22046  df-cncf 22600  df-ovol 23152  df-vol 23153  df-mbf 23307  df-itg1 23308  df-itg2 23309  df-ibl 23310  df-itg 23311  df-0p 23356  df-ditg 23530  df-limc 23549  df-dv 23550
This theorem is referenced by:  fourierdlem107  39758
  Copyright terms: Public domain W3C validator