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 41055
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 472 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐴 ∈ ℝ)
3 fourierdlem92.b . . . 4 (𝜑𝐵 ∈ ℝ)
43adantr 472 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐵 ∈ ℝ)
5 fourierdlem92.p . . 3 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
6 fourierdlem92.m . . . 4 (𝜑𝑀 ∈ ℕ)
76adantr 472 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑀 ∈ ℕ)
8 fourierdlem92.t . . . . 5 (𝜑𝑇 ∈ ℝ)
98adantr 472 . . . 4 ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ)
10 simpr 477 . . . 4 ((𝜑 ∧ 0 < 𝑇) → 0 < 𝑇)
119, 10elrpd 12070 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ+)
12 fourierdlem92.q . . . 4 (𝜑𝑄 ∈ (𝑃𝑀))
1312adantr 472 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑄 ∈ (𝑃𝑀))
14 fourierdlem92.fper . . . 4 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
1514adantlr 706 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
16 fveq2 6377 . . . . 5 (𝑗 = 𝑖 → (𝑄𝑗) = (𝑄𝑖))
1716oveq1d 6859 . . . 4 (𝑗 = 𝑖 → ((𝑄𝑗) + 𝑇) = ((𝑄𝑖) + 𝑇))
1817cbvmptv 4911 . . 3 (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
19 fourierdlem92.f . . . 4 (𝜑𝐹:ℝ⟶ℂ)
2019adantr 472 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐹:ℝ⟶ℂ)
21 fourierdlem92.cncf . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
2221adantlr 706 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
23 fourierdlem92.r . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
2423adantlr 706 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
25 fourierdlem92.l . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
2625adantlr 706 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
27 eqeq1 2769 . . . . 5 (𝑦 = 𝑥 → (𝑦 = (𝑄𝑖) ↔ 𝑥 = (𝑄𝑖)))
28 eqeq1 2769 . . . . . 6 (𝑦 = 𝑥 → (𝑦 = (𝑄‘(𝑖 + 1)) ↔ 𝑥 = (𝑄‘(𝑖 + 1))))
29 fveq2 6377 . . . . . 6 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
3028, 29ifbieq2d 4270 . . . . 5 (𝑦 = 𝑥 → if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦)) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥)))
3127, 30ifbieq2d 4270 . . . 4 (𝑦 = 𝑥 → if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦))) = if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
3231cbvmptv 4911 . . 3 (𝑦 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦)))) = (𝑥 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
33 eqid 2765 . . 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 41044 . 2 ((𝜑 ∧ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
35 simpr 477 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝑇 = 0)
3635oveq2d 6860 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐴 + 𝑇) = (𝐴 + 0))
371recnd 10324 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
3837adantr 472 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝐴 ∈ ℂ)
3938addid1d 10492 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐴 + 0) = 𝐴)
4036, 39eqtrd 2799 . . . . . 6 ((𝜑𝑇 = 0) → (𝐴 + 𝑇) = 𝐴)
4135oveq2d 6860 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐵 + 𝑇) = (𝐵 + 0))
423recnd 10324 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
4342adantr 472 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝐵 ∈ ℂ)
4443addid1d 10492 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐵 + 0) = 𝐵)
4541, 44eqtrd 2799 . . . . . 6 ((𝜑𝑇 = 0) → (𝐵 + 𝑇) = 𝐵)
4640, 45oveq12d 6862 . . . . 5 ((𝜑𝑇 = 0) → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = (𝐴[,]𝐵))
4746itgeq1d 40813 . . . 4 ((𝜑𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
4847adantlr 706 . . 3 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
49 simpll 783 . . . 4 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝜑)
50 simpr 477 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 𝑇 = 0)
51 simplr 785 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 0 < 𝑇)
52 ioran 1006 . . . . . . 7 (¬ (𝑇 = 0 ∨ 0 < 𝑇) ↔ (¬ 𝑇 = 0 ∧ ¬ 0 < 𝑇))
5350, 51, 52sylanbrc 578 . . . . . 6 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ (𝑇 = 0 ∨ 0 < 𝑇))
5449, 8syl 17 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 ∈ ℝ)
55 0red 10299 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 ∈ ℝ)
5654, 55lttrid 10431 . . . . . 6 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ ¬ (𝑇 = 0 ∨ 0 < 𝑇)))
5753, 56mpbird 248 . . . . 5 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 < 0)
5854lt0neg1d 10853 . . . . 5 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ 0 < -𝑇))
5957, 58mpbid 223 . . . 4 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 < -𝑇)
601, 8readdcld 10325 . . . . . . . . . . . 12 (𝜑 → (𝐴 + 𝑇) ∈ ℝ)
6160recnd 10324 . . . . . . . . . . 11 (𝜑 → (𝐴 + 𝑇) ∈ ℂ)
628recnd 10324 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
6361, 62negsubd 10654 . . . . . . . . . 10 (𝜑 → ((𝐴 + 𝑇) + -𝑇) = ((𝐴 + 𝑇) − 𝑇))
6437, 62pncand 10649 . . . . . . . . . 10 (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
6563, 64eqtrd 2799 . . . . . . . . 9 (𝜑 → ((𝐴 + 𝑇) + -𝑇) = 𝐴)
663, 8readdcld 10325 . . . . . . . . . . . 12 (𝜑 → (𝐵 + 𝑇) ∈ ℝ)
6766recnd 10324 . . . . . . . . . . 11 (𝜑 → (𝐵 + 𝑇) ∈ ℂ)
6867, 62negsubd 10654 . . . . . . . . . 10 (𝜑 → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇))
6942, 62pncand 10649 . . . . . . . . . 10 (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
7068, 69eqtrd 2799 . . . . . . . . 9 (𝜑 → ((𝐵 + 𝑇) + -𝑇) = 𝐵)
7165, 70oveq12d 6862 . . . . . . . 8 (𝜑 → (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)) = (𝐴[,]𝐵))
7271eqcomd 2771 . . . . . . 7 (𝜑 → (𝐴[,]𝐵) = (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)))
7372itgeq1d 40813 . . . . . 6 (𝜑 → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥)
7473adantr 472 . . . . 5 ((𝜑 ∧ 0 < -𝑇) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥)
751adantr 472 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝐴 ∈ ℝ)
768adantr 472 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝑇 ∈ ℝ)
7775, 76readdcld 10325 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → (𝐴 + 𝑇) ∈ ℝ)
783adantr 472 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝐵 ∈ ℝ)
7978, 76readdcld 10325 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → (𝐵 + 𝑇) ∈ ℝ)
80 eqid 2765 . . . . . 6 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
816adantr 472 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝑀 ∈ ℕ)
8276renegcld 10713 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ)
83 simpr 477 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 0 < -𝑇)
8482, 83elrpd 12070 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ+)
855fourierdlem2 40966 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
866, 85syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
8712, 86mpbid 223 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
8887simpld 488 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
89 elmapi 8084 . . . . . . . . . . . . . . 15 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
9088, 89syl 17 . . . . . . . . . . . . . 14 (𝜑𝑄:(0...𝑀)⟶ℝ)
9190ffvelrnda 6551 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) ∈ ℝ)
928adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑇 ∈ ℝ)
9391, 92readdcld 10325 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
94 fourierdlem92.s . . . . . . . . . . . 12 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
9593, 94fmptd 6576 . . . . . . . . . . 11 (𝜑𝑆:(0...𝑀)⟶ℝ)
96 reex 10282 . . . . . . . . . . . . 13 ℝ ∈ V
9796a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ V)
98 ovex 6876 . . . . . . . . . . . . 13 (0...𝑀) ∈ V
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → (0...𝑀) ∈ V)
10097, 99elmapd 8076 . . . . . . . . . . 11 (𝜑 → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ↔ 𝑆:(0...𝑀)⟶ℝ))
10195, 100mpbird 248 . . . . . . . . . 10 (𝜑𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)))
10294a1i 11 . . . . . . . . . . . . 13 (𝜑𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇)))
103 fveq2 6377 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
104103oveq1d 6859 . . . . . . . . . . . . . 14 (𝑖 = 0 → ((𝑄𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
105104adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑖 = 0) → ((𝑄𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
106 0zd 11638 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℤ)
1076nnzd 11731 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
108106, 107, 1063jca 1158 . . . . . . . . . . . . . . 15 (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ))
109 0le0 11382 . . . . . . . . . . . . . . . 16 0 ≤ 0
110109a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ 0)
111 nnnn0 11548 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
112111nn0ge0d 11603 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → 0 ≤ 𝑀)
1136, 112syl 17 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ 𝑀)
114108, 110, 113jca32 511 . . . . . . . . . . . . . 14 (𝜑 → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
115 elfz2 12543 . . . . . . . . . . . . . 14 (0 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
116114, 115sylibr 225 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ (0...𝑀))
11790, 116ffvelrnd 6552 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ∈ ℝ)
118117, 8readdcld 10325 . . . . . . . . . . . . 13 (𝜑 → ((𝑄‘0) + 𝑇) ∈ ℝ)
119102, 105, 116, 118fvmptd 6479 . . . . . . . . . . . 12 (𝜑 → (𝑆‘0) = ((𝑄‘0) + 𝑇))
120 simprll 797 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄‘0) = 𝐴)
12187, 120syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘0) = 𝐴)
122121oveq1d 6859 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘0) + 𝑇) = (𝐴 + 𝑇))
123119, 122eqtrd 2799 . . . . . . . . . . 11 (𝜑 → (𝑆‘0) = (𝐴 + 𝑇))
124 fveq2 6377 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝑄𝑖) = (𝑄𝑀))
125124oveq1d 6859 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → ((𝑄𝑖) + 𝑇) = ((𝑄𝑀) + 𝑇))
126125adantl 473 . . . . . . . . . . . . 13 ((𝜑𝑖 = 𝑀) → ((𝑄𝑖) + 𝑇) = ((𝑄𝑀) + 𝑇))
1276nnnn0d 11600 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ0)
128 nn0uz 11925 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
129127, 128syl6eleq 2854 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ‘0))
130 eluzfz2 12559 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
131129, 130syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (0...𝑀))
13290, 131ffvelrnd 6552 . . . . . . . . . . . . . 14 (𝜑 → (𝑄𝑀) ∈ ℝ)
133132, 8readdcld 10325 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝑀) + 𝑇) ∈ ℝ)
134102, 126, 131, 133fvmptd 6479 . . . . . . . . . . . 12 (𝜑 → (𝑆𝑀) = ((𝑄𝑀) + 𝑇))
135 simprlr 798 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄𝑀) = 𝐵)
13687, 135syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝑀) = 𝐵)
137136oveq1d 6859 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝑀) + 𝑇) = (𝐵 + 𝑇))
138134, 137eqtrd 2799 . . . . . . . . . . 11 (𝜑 → (𝑆𝑀) = (𝐵 + 𝑇))
139123, 138jca 507 . . . . . . . . . 10 (𝜑 → ((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)))
14090adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
141 elfzofz 12696 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
142141adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
143140, 142ffvelrnd 6552 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
144 fzofzp1 12776 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
145144adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
146140, 145ffvelrnd 6552 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
1478adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℝ)
14887simprrd 790 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
149148r19.21bi 3079 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
150143, 146, 147, 149ltadd1dd 10894 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) < ((𝑄‘(𝑖 + 1)) + 𝑇))
151143, 147readdcld 10325 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
15294fvmpt2 6482 . . . . . . . . . . . . 13 ((𝑖 ∈ (0...𝑀) ∧ ((𝑄𝑖) + 𝑇) ∈ ℝ) → (𝑆𝑖) = ((𝑄𝑖) + 𝑇))
153142, 151, 152syl2anc 579 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆𝑖) = ((𝑄𝑖) + 𝑇))
15494, 18eqtr4i 2790 . . . . . . . . . . . . . 14 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇))
155154a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇)))
156 fveq2 6377 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) → (𝑄𝑗) = (𝑄‘(𝑖 + 1)))
157156oveq1d 6859 . . . . . . . . . . . . . 14 (𝑗 = (𝑖 + 1) → ((𝑄𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
158157adantl 473 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
159146, 147readdcld 10325 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
160155, 158, 145, 159fvmptd 6479 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) + 𝑇))
161150, 153, 1603brtr4d 4843 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆𝑖) < (𝑆‘(𝑖 + 1)))
162161ralrimiva 3113 . . . . . . . . . 10 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))
163101, 139, 162jca32 511 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
164 fourierdlem92.h . . . . . . . . . . 11 𝐻 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
165164fourierdlem2 40966 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑆 ∈ (𝐻𝑀) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
1666, 165syl 17 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐻𝑀) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
167163, 166mpbird 248 . . . . . . . 8 (𝜑𝑆 ∈ (𝐻𝑀))
168164fveq1i 6378 . . . . . . . 8 (𝐻𝑀) = ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀)
169167, 168syl6eleq 2854 . . . . . . 7 (𝜑𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀))
170169adantr 472 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀))
17160adantr 472 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
17266adantr 472 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ)
173 simpr 477 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
174 eliccre 40373 . . . . . . . . . . . 12 (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
175171, 172, 173, 174syl3anc 1490 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
176175recnd 10324 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ)
17762negcld 10635 . . . . . . . . . . 11 (𝜑 → -𝑇 ∈ ℂ)
178177adantr 472 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℂ)
179176, 178addcld 10315 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℂ)
180 simpl 474 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝜑)
1811adantr 472 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ)
1823adantr 472 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ)
1838renegcld 10713 . . . . . . . . . . . . 13 (𝜑 → -𝑇 ∈ ℝ)
184183adantr 472 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℝ)
185175, 184readdcld 10325 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℝ)
18663, 64eqtr2d 2800 . . . . . . . . . . . . 13 (𝜑𝐴 = ((𝐴 + 𝑇) + -𝑇))
187186adantr 472 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) + -𝑇))
188171rexrd 10345 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ*)
189172rexrd 10345 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ*)
190 iccgelb 12435 . . . . . . . . . . . . . 14 (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ*𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
191188, 189, 173, 190syl3anc 1490 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
192171, 175, 184, 191leadd1dd 10897 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) + -𝑇) ≤ (𝑥 + -𝑇))
193187, 192eqbrtrd 4833 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 + -𝑇))
194 iccleub 12434 . . . . . . . . . . . . . 14 (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ*𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
195188, 189, 173, 194syl3anc 1490 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
196175, 172, 184, 195leadd1dd 10897 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ ((𝐵 + 𝑇) + -𝑇))
197172recnd 10324 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℂ)
19862adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ)
199197, 198negsubd 10654 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇))
20069adantr 472 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
201199, 200eqtrd 2799 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = 𝐵)
202196, 201breqtrd 4837 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ 𝐵)
203181, 182, 185, 193, 202eliccd 40371 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))
204180, 203jca 507 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))
205 eleq1 2832 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))
206205anbi2d 622 . . . . . . . . . . 11 (𝑦 = (𝑥 + -𝑇) → ((𝜑𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))))
207 oveq1 6851 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + -𝑇) → (𝑦 + 𝑇) = ((𝑥 + -𝑇) + 𝑇))
208207fveq2d 6381 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥 + -𝑇) + 𝑇)))
209 fveq2 6377 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝐹𝑦) = (𝐹‘(𝑥 + -𝑇)))
210208, 209eqeq12d 2780 . . . . . . . . . . 11 (𝑦 = (𝑥 + -𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))
211206, 210imbi12d 335 . . . . . . . . . 10 (𝑦 = (𝑥 + -𝑇) → (((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))))
212 eleq1 2832 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
213212anbi2d 622 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝜑𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑦 ∈ (𝐴[,]𝐵))))
214 oveq1 6851 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
215214fveq2d 6381 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
216 fveq2 6377 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
217215, 216eqeq12d 2780 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)))
218213, 217imbi12d 335 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))))
219218, 14chvarv 2369 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
220211, 219vtoclg 3418 . . . . . . . . 9 ((𝑥 + -𝑇) ∈ ℂ → ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))
221179, 204, 220sylc 65 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))
222176, 198negsubd 10654 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) = (𝑥𝑇))
223222oveq1d 6859 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = ((𝑥𝑇) + 𝑇))
224176, 198npcand 10652 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥𝑇) + 𝑇) = 𝑥)
225223, 224eqtrd 2799 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = 𝑥)
226225fveq2d 6381 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹𝑥))
227221, 226eqtr3d 2801 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹𝑥))
228227adantlr 706 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹𝑥))
229 fveq2 6377 . . . . . . . 8 (𝑗 = 𝑖 → (𝑆𝑗) = (𝑆𝑖))
230229oveq1d 6859 . . . . . . 7 (𝑗 = 𝑖 → ((𝑆𝑗) + -𝑇) = ((𝑆𝑖) + -𝑇))
231230cbvmptv 4911 . . . . . 6 (𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑆𝑖) + -𝑇))
23219adantr 472 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝐹:ℝ⟶ℂ)
23319adantr 472 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
234 ioossre 12440 . . . . . . . . . . 11 ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ
235234a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ)
236233, 235feqresmpt 6441 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹𝑥)))
237153, 160oveq12d 6862 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) = (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
238143, 146, 147iooshift 40390 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
239237, 238eqtrd 2799 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
240239mpteq1d 4899 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹𝑥)))
241 simpll 783 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝜑)
242 simplr 785 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑖 ∈ (0..^𝑀))
243238eleq2d 2830 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) ↔ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}))
244243biimpar 469 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
245143rexrd 10345 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
2462453adant3 1162 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) ∈ ℝ*)
247146rexrd 10345 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2482473adant3 1162 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
249 elioore 12410 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) → 𝑥 ∈ ℝ)
250249adantl 473 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
2518adantr 472 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
252250, 251resubcld 10714 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ℝ)
2532523adant2 1161 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ℝ)
254143recnd 10324 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
25562adantr 472 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℂ)
256254, 255pncand 10649 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + 𝑇) − 𝑇) = (𝑄𝑖))
257256eqcomd 2771 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (((𝑄𝑖) + 𝑇) − 𝑇))
2582573adant3 1162 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) = (((𝑄𝑖) + 𝑇) − 𝑇))
2591513adant3 1162 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
2602503adant2 1161 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
26183ad2ant1 1163 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
262151rexrd 10345 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ*)
2632623adant3 1162 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) ∈ ℝ*)
264159rexrd 10345 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
2652643adant3 1162 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
266 simp3 1168 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
267 ioogtlb 40362 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) < 𝑥)
268263, 265, 266, 267syl3anc 1490 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) < 𝑥)
269259, 260, 261, 268ltsub1dd 10895 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄𝑖) + 𝑇) − 𝑇) < (𝑥𝑇))
270258, 269eqbrtrd 4833 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) < (𝑥𝑇))
2711593adant3 1162 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
272 iooltub 40378 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇))
273263, 265, 266, 272syl3anc 1490 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇))
274260, 271, 261, 273ltsub1dd 10895 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇))
275146recnd 10324 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
276275, 255pncand 10649 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
2772763adant3 1162 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
278274, 277breqtrd 4837 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < (𝑄‘(𝑖 + 1)))
279246, 248, 253, 270, 278eliood 40365 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
280241, 242, 244, 279syl3anc 1490 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
281 fvres 6396 . . . . . . . . . . . 12 ((𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
282280, 281syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
283241, 244, 252syl2anc 579 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ ℝ)
28413ad2ant1 1163 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ∈ ℝ)
28533ad2ant1 1163 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐵 ∈ ℝ)
28664eqcomd 2771 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 = ((𝐴 + 𝑇) − 𝑇))
2872863ad2ant1 1163 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
288603ad2ant1 1163 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
2891adantr 472 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ)
2901rexrd 10345 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ ℝ*)
291290adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ*)
2923rexrd 10345 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ*)
293292adantr 472 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ*)
2945, 6, 12fourierdlem15 40979 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
295294adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
296295, 142ffvelrnd 6552 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ (𝐴[,]𝐵))
297 iccgelb 12435 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄𝑖) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑄𝑖))
298291, 293, 296, 297syl3anc 1490 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ≤ (𝑄𝑖))
299289, 143, 147, 298leadd1dd 10897 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐴 + 𝑇) ≤ ((𝑄𝑖) + 𝑇))
3002993adant3 1162 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ≤ ((𝑄𝑖) + 𝑇))
301288, 259, 260, 300, 268lelttrd 10451 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) < 𝑥)
302288, 260, 261, 301ltsub1dd 10895 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) < (𝑥𝑇))
303287, 302eqbrtrd 4833 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 < (𝑥𝑇))
304284, 253, 303ltled 10441 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ≤ (𝑥𝑇))
3051463adant3 1162 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
306295, 145ffvelrnd 6552 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵))
307 iccleub 12434 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
308291, 293, 306, 307syl3anc 1490 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
3093083adant3 1162 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
310253, 305, 285, 278, 309ltletrd 10453 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < 𝐵)
311253, 285, 310ltled 10441 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ≤ 𝐵)
312284, 285, 253, 304, 311eliccd 40371 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ (𝐴[,]𝐵))
313241, 242, 244, 312syl3anc 1490 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ (𝐴[,]𝐵))
314241, 313jca 507 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)))
315 eleq1 2832 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥𝑇) ∈ (𝐴[,]𝐵)))
316315anbi2d 622 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑇) → ((𝜑𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵))))
317 oveq1 6851 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥𝑇) → (𝑦 + 𝑇) = ((𝑥𝑇) + 𝑇))
318317fveq2d 6381 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥𝑇) + 𝑇)))
319 fveq2 6377 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝐹𝑦) = (𝐹‘(𝑥𝑇)))
320318, 319eqeq12d 2780 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
321316, 320imbi12d 335 . . . . . . . . . . . . 13 (𝑦 = (𝑥𝑇) → (((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))))
322321, 219vtoclg 3418 . . . . . . . . . . . 12 ((𝑥𝑇) ∈ ℝ → ((𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
323283, 314, 322sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))
324244, 249syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ℝ)
325 recn 10281 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
326325adantl 473 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
32762adantr 472 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
328326, 327npcand 10652 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → ((𝑥𝑇) + 𝑇) = 𝑥)
329328fveq2d 6381 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹𝑥))
330241, 324, 329syl2anc 579 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹𝑥))
331282, 323, 3303eqtr2rd 2806 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹𝑥) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)))
332331mpteq2dva 4905 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))))
333236, 240, 3323eqtrd 2803 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))))
334 ioosscn 40361 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
335334a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
336 eqeq1 2769 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇)))
337336rexbidv 3199 . . . . . . . . . . . 12 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)))
338 oveq1 6851 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇))
339338eqeq2d 2775 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇)))
340339cbvrexv 3320 . . . . . . . . . . . 12 (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇))
341337, 340syl6bb 278 . . . . . . . . . . 11 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)))
342341cbvrabv 3348 . . . . . . . . . 10 {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}
343 eqid 2765 . . . . . . . . . 10 (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)))
344335, 255, 342, 21, 343cncfshift 40728 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) ∈ ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ))
345239eqcomd 2771 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))))
346345oveq1d 6859 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ) = (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
347344, 346eleqtrd 2846 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
348333, 347eqeltrd 2844 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
349348adantlr 706 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
350 ffdm 6246 . . . . . . . . . . . 12 (𝐹:ℝ⟶ℂ → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
35119, 350syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
352351simpld 488 . . . . . . . . . 10 (𝜑𝐹:dom 𝐹⟶ℂ)
353352adantr 472 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:dom 𝐹⟶ℂ)
354 ioossre 12440 . . . . . . . . . 10 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
355 fdm 6233 . . . . . . . . . . 11 (𝐹:ℝ⟶ℂ → dom 𝐹 = ℝ)
356233, 355syl 17 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → dom 𝐹 = ℝ)
357354, 356syl5sseqr 3816 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
358342eqcomi 2774 . . . . . . . . 9 {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}
359235, 345, 3563sstr4d 3810 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ⊆ dom 𝐹)
360342, 359syl5eqssr 3812 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} ⊆ dom 𝐹)
361 simpll 783 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
362361, 290syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐴 ∈ ℝ*)
363361, 292syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐵 ∈ ℝ*)
364361, 294syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
365 simplr 785 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
366 ioossicc 12464 . . . . . . . . . . . . 13 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
367366sseli 3759 . . . . . . . . . . . 12 (𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑧 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
368367adantl 473 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
369362, 363, 364, 365, 368fourierdlem1 40965 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ (𝐴[,]𝐵))
370 eleq1 2832 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑧 ∈ (𝐴[,]𝐵)))
371370anbi2d 622 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝜑𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑧 ∈ (𝐴[,]𝐵))))
372 oveq1 6851 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑥 + 𝑇) = (𝑧 + 𝑇))
373372fveq2d 6381 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑧 + 𝑇)))
374 fveq2 6377 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
375373, 374eqeq12d 2780 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧)))
376371, 375imbi12d 335 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))))
377376, 14chvarv 2369 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))
378361, 369, 377syl2anc 579 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))
379353, 335, 357, 255, 358, 360, 378, 23limcperiod 40501 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄𝑖) + 𝑇)))
380358, 345syl5eq 2811 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))))
381380reseq2d 5567 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) = (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))))
382153eqcomd 2771 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) = (𝑆𝑖))
383381, 382oveq12d 6862 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄𝑖) + 𝑇)) = ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
384379, 383eleqtrd 2846 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
385384adantlr 706 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
386353, 335, 357, 255, 358, 360, 378, 25limcperiod 40501 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄‘(𝑖 + 1)) + 𝑇)))
387160eqcomd 2771 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) = (𝑆‘(𝑖 + 1)))
388381, 387oveq12d 6862 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄‘(𝑖 + 1)) + 𝑇)) = ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
389386, 388eleqtrd 2846 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
390389adantlr 706 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
391 eqeq1 2769 . . . . . . . 8 (𝑦 = 𝑥 → (𝑦 = (𝑆𝑖) ↔ 𝑥 = (𝑆𝑖)))
392 eqeq1 2769 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑦 = (𝑆‘(𝑖 + 1)) ↔ 𝑥 = (𝑆‘(𝑖 + 1))))
393392, 29ifbieq2d 4270 . . . . . . . 8 (𝑦 = 𝑥 → if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦)) = if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥)))
394391, 393ifbieq2d 4270 . . . . . . 7 (𝑦 = 𝑥 → if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦))) = if(𝑥 = (𝑆𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
395394cbvmptv 4911 . . . . . 6 (𝑦 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦)))) = (𝑥 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
396 eqid 2765 . . . . . 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 41044 . . . . 5 ((𝜑 ∧ 0 < -𝑇) → ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥)
39874, 397eqtr2d 2800 . . . 4 ((𝜑 ∧ 0 < -𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
39949, 59, 398syl2anc 579 . . 3 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
40048, 399pm2.61dan 847 . 2 ((𝜑 ∧ ¬ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
40134, 400pm2.61dan 847 1 (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 873  w3a 1107   = wceq 1652  wcel 2155  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  wss 3734  ifcif 4245   class class class wbr 4811  cmpt 4890  dom cdm 5279  cres 5281  wf 6066  cfv 6070  (class class class)co 6844  𝑚 cmap 8062  cc 10189  cr 10190  0cc0 10191  1c1 10192   + caddc 10194  *cxr 10329   < clt 10330  cle 10331  cmin 10522  -cneg 10523  cn 11276  0cn0 11540  cz 11626  cuz 11889  (,)cioo 12380  [,]cicc 12383  ...cfz 12536  ..^cfzo 12676  cnccncf 22961  citg 23679   lim climc 23920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4932  ax-sep 4943  ax-nul 4951  ax-pow 5003  ax-pr 5064  ax-un 7149  ax-inf2 8755  ax-cc 9512  ax-cnex 10247  ax-resscn 10248  ax-1cn 10249  ax-icn 10250  ax-addcl 10251  ax-addrcl 10252  ax-mulcl 10253  ax-mulrcl 10254  ax-mulcom 10255  ax-addass 10256  ax-mulass 10257  ax-distr 10258  ax-i2m1 10259  ax-1ne0 10260  ax-1rid 10261  ax-rnegex 10262  ax-rrecex 10263  ax-cnre 10264  ax-pre-lttri 10265  ax-pre-lttrn 10266  ax-pre-ltadd 10267  ax-pre-mulgt0 10268  ax-pre-sup 10269  ax-addf 10270  ax-mulf 10271
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-fal 1666  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-nel 3041  df-ral 3060  df-rex 3061  df-reu 3062  df-rmo 3063  df-rab 3064  df-v 3352  df-sbc 3599  df-csb 3694  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-pss 3750  df-symdif 4007  df-nul 4082  df-if 4246  df-pw 4319  df-sn 4337  df-pr 4339  df-tp 4341  df-op 4343  df-uni 4597  df-int 4636  df-iun 4680  df-iin 4681  df-disj 4780  df-br 4812  df-opab 4874  df-mpt 4891  df-tr 4914  df-id 5187  df-eprel 5192  df-po 5200  df-so 5201  df-fr 5238  df-se 5239  df-we 5240  df-xp 5285  df-rel 5286  df-cnv 5287  df-co 5288  df-dm 5289  df-rn 5290  df-res 5291  df-ima 5292  df-pred 5867  df-ord 5913  df-on 5914  df-lim 5915  df-suc 5916  df-iota 6033  df-fun 6072  df-fn 6073  df-f 6074  df-f1 6075  df-fo 6076  df-f1o 6077  df-fv 6078  df-isom 6079  df-riota 6805  df-ov 6847  df-oprab 6848  df-mpt2 6849  df-of 7097  df-ofr 7098  df-om 7266  df-1st 7368  df-2nd 7369  df-supp 7500  df-wrecs 7612  df-recs 7674  df-rdg 7712  df-1o 7766  df-2o 7767  df-oadd 7770  df-omul 7771  df-er 7949  df-map 8064  df-pm 8065  df-ixp 8116  df-en 8163  df-dom 8164  df-sdom 8165  df-fin 8166  df-fsupp 8485  df-fi 8526  df-sup 8557  df-inf 8558  df-oi 8624  df-card 9018  df-acn 9021  df-cda 9245  df-pnf 10332  df-mnf 10333  df-xr 10334  df-ltxr 10335  df-le 10336  df-sub 10524  df-neg 10525  df-div 10941  df-nn 11277  df-2 11337  df-3 11338  df-4 11339  df-5 11340  df-6 11341  df-7 11342  df-8 11343  df-9 11344  df-n0 11541  df-z 11627  df-dec 11744  df-uz 11890  df-q 11993  df-rp 12032  df-xneg 12149  df-xadd 12150  df-xmul 12151  df-ioo 12384  df-ioc 12385  df-ico 12386  df-icc 12387  df-fz 12537  df-fzo 12677  df-fl 12804  df-mod 12880  df-seq 13012  df-exp 13071  df-hash 13325  df-cj 14127  df-re 14128  df-im 14129  df-sqrt 14263  df-abs 14264  df-limsup 14490  df-clim 14507  df-rlim 14508  df-sum 14705  df-struct 16135  df-ndx 16136  df-slot 16137  df-base 16139  df-sets 16140  df-ress 16141  df-plusg 16230  df-mulr 16231  df-starv 16232  df-sca 16233  df-vsca 16234  df-ip 16235  df-tset 16236  df-ple 16237  df-ds 16239  df-unif 16240  df-hom 16241  df-cco 16242  df-rest 16352  df-topn 16353  df-0g 16371  df-gsum 16372  df-topgen 16373  df-pt 16374  df-prds 16377  df-xrs 16431  df-qtop 16436  df-imas 16437  df-xps 16439  df-mre 16515  df-mrc 16516  df-acs 16518  df-mgm 17511  df-sgrp 17553  df-mnd 17564  df-submnd 17605  df-mulg 17811  df-cntz 18016  df-cmn 18464  df-psmet 20014  df-xmet 20015  df-met 20016  df-bl 20017  df-mopn 20018  df-fbas 20019  df-fg 20020  df-cnfld 20023  df-top 20981  df-topon 20998  df-topsp 21020  df-bases 21033  df-cld 21106  df-ntr 21107  df-cls 21108  df-nei 21185  df-lp 21223  df-perf 21224  df-cn 21314  df-cnp 21315  df-haus 21402  df-cmp 21473  df-tx 21648  df-hmeo 21841  df-fil 21932  df-fm 22024  df-flim 22025  df-flf 22026  df-xms 22407  df-ms 22408  df-tms 22409  df-cncf 22963  df-ovol 23525  df-vol 23526  df-mbf 23680  df-itg1 23681  df-itg2 23682  df-ibl 23683  df-itg 23684  df-0p 23731  df-ditg 23905  df-limc 23924  df-dv 23925
This theorem is referenced by:  fourierdlem107  41070
  Copyright terms: Public domain W3C validator