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

Theorem fourierdlem92 40733
 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 480 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐴 ∈ ℝ)
3 fourierdlem92.b . . . 4 (𝜑𝐵 ∈ ℝ)
43adantr 480 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐵 ∈ ℝ)
5 fourierdlem92.p . . 3 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
6 fourierdlem92.m . . . 4 (𝜑𝑀 ∈ ℕ)
76adantr 480 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑀 ∈ ℕ)
8 fourierdlem92.t . . . . 5 (𝜑𝑇 ∈ ℝ)
98adantr 480 . . . 4 ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ)
10 simpr 476 . . . 4 ((𝜑 ∧ 0 < 𝑇) → 0 < 𝑇)
119, 10elrpd 11907 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑇 ∈ ℝ+)
12 fourierdlem92.q . . . 4 (𝜑𝑄 ∈ (𝑃𝑀))
1312adantr 480 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝑄 ∈ (𝑃𝑀))
14 fourierdlem92.fper . . . 4 ((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
1514adantlr 751 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥))
16 fveq2 6229 . . . . 5 (𝑗 = 𝑖 → (𝑄𝑗) = (𝑄𝑖))
1716oveq1d 6705 . . . 4 (𝑗 = 𝑖 → ((𝑄𝑗) + 𝑇) = ((𝑄𝑖) + 𝑇))
1817cbvmptv 4783 . . 3 (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
19 fourierdlem92.f . . . 4 (𝜑𝐹:ℝ⟶ℂ)
2019adantr 480 . . 3 ((𝜑 ∧ 0 < 𝑇) → 𝐹:ℝ⟶ℂ)
21 fourierdlem92.cncf . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
2221adantlr 751 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
23 fourierdlem92.r . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
2423adantlr 751 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄𝑖)))
25 fourierdlem92.l . . . 4 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
2625adantlr 751 . . 3 (((𝜑 ∧ 0 < 𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) lim (𝑄‘(𝑖 + 1))))
27 eqeq1 2655 . . . . 5 (𝑦 = 𝑥 → (𝑦 = (𝑄𝑖) ↔ 𝑥 = (𝑄𝑖)))
28 eqeq1 2655 . . . . . 6 (𝑦 = 𝑥 → (𝑦 = (𝑄‘(𝑖 + 1)) ↔ 𝑥 = (𝑄‘(𝑖 + 1))))
29 fveq2 6229 . . . . . 6 (𝑦 = 𝑥 → (𝐹𝑦) = (𝐹𝑥))
3028, 29ifbieq2d 4144 . . . . 5 (𝑦 = 𝑥 → if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦)) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥)))
3127, 30ifbieq2d 4144 . . . 4 (𝑦 = 𝑥 → if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦))) = if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
3231cbvmptv 4783 . . 3 (𝑦 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑦 = (𝑄𝑖), 𝑅, if(𝑦 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑦)))) = (𝑥 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
33 eqid 2651 . . 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 40722 . 2 ((𝜑 ∧ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
35 simpr 476 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝑇 = 0)
3635oveq2d 6706 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐴 + 𝑇) = (𝐴 + 0))
371recnd 10106 . . . . . . . . 9 (𝜑𝐴 ∈ ℂ)
3837adantr 480 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝐴 ∈ ℂ)
3938addid1d 10274 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐴 + 0) = 𝐴)
4036, 39eqtrd 2685 . . . . . 6 ((𝜑𝑇 = 0) → (𝐴 + 𝑇) = 𝐴)
4135oveq2d 6706 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐵 + 𝑇) = (𝐵 + 0))
423recnd 10106 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
4342adantr 480 . . . . . . . 8 ((𝜑𝑇 = 0) → 𝐵 ∈ ℂ)
4443addid1d 10274 . . . . . . 7 ((𝜑𝑇 = 0) → (𝐵 + 0) = 𝐵)
4541, 44eqtrd 2685 . . . . . 6 ((𝜑𝑇 = 0) → (𝐵 + 𝑇) = 𝐵)
4640, 45oveq12d 6708 . . . . 5 ((𝜑𝑇 = 0) → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = (𝐴[,]𝐵))
4746itgeq1d 40490 . . . 4 ((𝜑𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
4847adantlr 751 . . 3 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
49 simpll 805 . . . 4 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝜑)
50 simpr 476 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 𝑇 = 0)
51 simplr 807 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ 0 < 𝑇)
52 ioran 510 . . . . . . 7 (¬ (𝑇 = 0 ∨ 0 < 𝑇) ↔ (¬ 𝑇 = 0 ∧ ¬ 0 < 𝑇))
5350, 51, 52sylanbrc 699 . . . . . 6 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ¬ (𝑇 = 0 ∨ 0 < 𝑇))
5449, 8syl 17 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 ∈ ℝ)
55 0red 10079 . . . . . . 7 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 ∈ ℝ)
5654, 55lttrid 10213 . . . . . 6 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ ¬ (𝑇 = 0 ∨ 0 < 𝑇)))
5753, 56mpbird 247 . . . . 5 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 𝑇 < 0)
5854lt0neg1d 10635 . . . . 5 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → (𝑇 < 0 ↔ 0 < -𝑇))
5957, 58mpbid 222 . . . 4 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → 0 < -𝑇)
601, 8readdcld 10107 . . . . . . . . . . . 12 (𝜑 → (𝐴 + 𝑇) ∈ ℝ)
6160recnd 10106 . . . . . . . . . . 11 (𝜑 → (𝐴 + 𝑇) ∈ ℂ)
628recnd 10106 . . . . . . . . . . 11 (𝜑𝑇 ∈ ℂ)
6361, 62negsubd 10436 . . . . . . . . . 10 (𝜑 → ((𝐴 + 𝑇) + -𝑇) = ((𝐴 + 𝑇) − 𝑇))
6437, 62pncand 10431 . . . . . . . . . 10 (𝜑 → ((𝐴 + 𝑇) − 𝑇) = 𝐴)
6563, 64eqtrd 2685 . . . . . . . . 9 (𝜑 → ((𝐴 + 𝑇) + -𝑇) = 𝐴)
663, 8readdcld 10107 . . . . . . . . . . . 12 (𝜑 → (𝐵 + 𝑇) ∈ ℝ)
6766recnd 10106 . . . . . . . . . . 11 (𝜑 → (𝐵 + 𝑇) ∈ ℂ)
6867, 62negsubd 10436 . . . . . . . . . 10 (𝜑 → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇))
6942, 62pncand 10431 . . . . . . . . . 10 (𝜑 → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
7068, 69eqtrd 2685 . . . . . . . . 9 (𝜑 → ((𝐵 + 𝑇) + -𝑇) = 𝐵)
7165, 70oveq12d 6708 . . . . . . . 8 (𝜑 → (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)) = (𝐴[,]𝐵))
7271eqcomd 2657 . . . . . . 7 (𝜑 → (𝐴[,]𝐵) = (((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇)))
7372itgeq1d 40490 . . . . . 6 (𝜑 → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥)
7473adantr 480 . . . . 5 ((𝜑 ∧ 0 < -𝑇) → ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥 = ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥)
751adantr 480 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝐴 ∈ ℝ)
768adantr 480 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝑇 ∈ ℝ)
7775, 76readdcld 10107 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → (𝐴 + 𝑇) ∈ ℝ)
783adantr 480 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 𝐵 ∈ ℝ)
7978, 76readdcld 10107 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → (𝐵 + 𝑇) ∈ ℝ)
80 eqid 2651 . . . . . 6 (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))}) = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
816adantr 480 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝑀 ∈ ℕ)
8276renegcld 10495 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ)
83 simpr 476 . . . . . . 7 ((𝜑 ∧ 0 < -𝑇) → 0 < -𝑇)
8482, 83elrpd 11907 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → -𝑇 ∈ ℝ+)
855fourierdlem2 40644 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
866, 85syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑄 ∈ (𝑃𝑀) ↔ (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1))))))
8712, 86mpbid 222 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))))
8887simpld 474 . . . . . . . . . . . . . . 15 (𝜑𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)))
89 elmapi 7921 . . . . . . . . . . . . . . 15 (𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
9088, 89syl 17 . . . . . . . . . . . . . 14 (𝜑𝑄:(0...𝑀)⟶ℝ)
9190ffvelrnda 6399 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → (𝑄𝑖) ∈ ℝ)
928adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0...𝑀)) → 𝑇 ∈ ℝ)
9391, 92readdcld 10107 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0...𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
94 fourierdlem92.s . . . . . . . . . . . 12 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇))
9593, 94fmptd 6425 . . . . . . . . . . 11 (𝜑𝑆:(0...𝑀)⟶ℝ)
96 reex 10065 . . . . . . . . . . . . 13 ℝ ∈ V
9796a1i 11 . . . . . . . . . . . 12 (𝜑 → ℝ ∈ V)
98 ovex 6718 . . . . . . . . . . . . 13 (0...𝑀) ∈ V
9998a1i 11 . . . . . . . . . . . 12 (𝜑 → (0...𝑀) ∈ V)
10097, 99elmapd 7913 . . . . . . . . . . 11 (𝜑 → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ↔ 𝑆:(0...𝑀)⟶ℝ))
10195, 100mpbird 247 . . . . . . . . . 10 (𝜑𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)))
10294a1i 11 . . . . . . . . . . . . 13 (𝜑𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄𝑖) + 𝑇)))
103 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑖 = 0 → (𝑄𝑖) = (𝑄‘0))
104103oveq1d 6705 . . . . . . . . . . . . . 14 (𝑖 = 0 → ((𝑄𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
105104adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 = 0) → ((𝑄𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
106 0zd 11427 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ∈ ℤ)
1076nnzd 11519 . . . . . . . . . . . . . . . 16 (𝜑𝑀 ∈ ℤ)
108106, 107, 1063jca 1261 . . . . . . . . . . . . . . 15 (𝜑 → (0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ))
109 0le0 11148 . . . . . . . . . . . . . . . 16 0 ≤ 0
110109a1i 11 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ 0)
111 nnnn0 11337 . . . . . . . . . . . . . . . . 17 (𝑀 ∈ ℕ → 𝑀 ∈ ℕ0)
112111nn0ge0d 11392 . . . . . . . . . . . . . . . 16 (𝑀 ∈ ℕ → 0 ≤ 𝑀)
1136, 112syl 17 . . . . . . . . . . . . . . 15 (𝜑 → 0 ≤ 𝑀)
114108, 110, 113jca32 557 . . . . . . . . . . . . . 14 (𝜑 → ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
115 elfz2 12371 . . . . . . . . . . . . . 14 (0 ∈ (0...𝑀) ↔ ((0 ∈ ℤ ∧ 𝑀 ∈ ℤ ∧ 0 ∈ ℤ) ∧ (0 ≤ 0 ∧ 0 ≤ 𝑀)))
116114, 115sylibr 224 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ (0...𝑀))
11790, 116ffvelrnd 6400 . . . . . . . . . . . . . 14 (𝜑 → (𝑄‘0) ∈ ℝ)
118117, 8readdcld 10107 . . . . . . . . . . . . 13 (𝜑 → ((𝑄‘0) + 𝑇) ∈ ℝ)
119102, 105, 116, 118fvmptd 6327 . . . . . . . . . . . 12 (𝜑 → (𝑆‘0) = ((𝑄‘0) + 𝑇))
120 simprll 819 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄‘0) = 𝐴)
12187, 120syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄‘0) = 𝐴)
122121oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → ((𝑄‘0) + 𝑇) = (𝐴 + 𝑇))
123119, 122eqtrd 2685 . . . . . . . . . . 11 (𝜑 → (𝑆‘0) = (𝐴 + 𝑇))
124 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑖 = 𝑀 → (𝑄𝑖) = (𝑄𝑀))
125124oveq1d 6705 . . . . . . . . . . . . . 14 (𝑖 = 𝑀 → ((𝑄𝑖) + 𝑇) = ((𝑄𝑀) + 𝑇))
126125adantl 481 . . . . . . . . . . . . 13 ((𝜑𝑖 = 𝑀) → ((𝑄𝑖) + 𝑇) = ((𝑄𝑀) + 𝑇))
1276nnnn0d 11389 . . . . . . . . . . . . . . 15 (𝜑𝑀 ∈ ℕ0)
128 nn0uz 11760 . . . . . . . . . . . . . . 15 0 = (ℤ‘0)
129127, 128syl6eleq 2740 . . . . . . . . . . . . . 14 (𝜑𝑀 ∈ (ℤ‘0))
130 eluzfz2 12387 . . . . . . . . . . . . . 14 (𝑀 ∈ (ℤ‘0) → 𝑀 ∈ (0...𝑀))
131129, 130syl 17 . . . . . . . . . . . . 13 (𝜑𝑀 ∈ (0...𝑀))
13290, 131ffvelrnd 6400 . . . . . . . . . . . . . 14 (𝜑 → (𝑄𝑀) ∈ ℝ)
133132, 8readdcld 10107 . . . . . . . . . . . . 13 (𝜑 → ((𝑄𝑀) + 𝑇) ∈ ℝ)
134102, 126, 131, 133fvmptd 6327 . . . . . . . . . . . 12 (𝜑 → (𝑆𝑀) = ((𝑄𝑀) + 𝑇))
135 simprlr 820 . . . . . . . . . . . . . 14 ((𝑄 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))) → (𝑄𝑀) = 𝐵)
13687, 135syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑄𝑀) = 𝐵)
137136oveq1d 6705 . . . . . . . . . . . 12 (𝜑 → ((𝑄𝑀) + 𝑇) = (𝐵 + 𝑇))
138134, 137eqtrd 2685 . . . . . . . . . . 11 (𝜑 → (𝑆𝑀) = (𝐵 + 𝑇))
139123, 138jca 553 . . . . . . . . . 10 (𝜑 → ((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)))
14090adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
141 elfzofz 12524 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
142141adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
143140, 142ffvelrnd 6400 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ)
144 fzofzp1 12605 . . . . . . . . . . . . . . 15 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
145144adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
146140, 145ffvelrnd 6400 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
1478adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℝ)
14887simprrd 812 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄𝑖) < (𝑄‘(𝑖 + 1)))
149148r19.21bi 2961 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) < (𝑄‘(𝑖 + 1)))
150143, 146, 147, 149ltadd1dd 10676 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) < ((𝑄‘(𝑖 + 1)) + 𝑇))
151143, 147readdcld 10107 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
15294fvmpt2 6330 . . . . . . . . . . . . 13 ((𝑖 ∈ (0...𝑀) ∧ ((𝑄𝑖) + 𝑇) ∈ ℝ) → (𝑆𝑖) = ((𝑄𝑖) + 𝑇))
153142, 151, 152syl2anc 694 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆𝑖) = ((𝑄𝑖) + 𝑇))
15494, 18eqtr4i 2676 . . . . . . . . . . . . . 14 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇))
155154a1i 11 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄𝑗) + 𝑇)))
156 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑗 = (𝑖 + 1) → (𝑄𝑗) = (𝑄‘(𝑖 + 1)))
157156oveq1d 6705 . . . . . . . . . . . . . 14 (𝑗 = (𝑖 + 1) → ((𝑄𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
158157adantl 481 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
159146, 147readdcld 10107 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
160155, 158, 145, 159fvmptd 6327 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) + 𝑇))
161150, 153, 1603brtr4d 4717 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑆𝑖) < (𝑆‘(𝑖 + 1)))
162161ralrimiva 2995 . . . . . . . . . 10 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))
163101, 139, 162jca32 557 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1)))))
164 fourierdlem92.h . . . . . . . . . . 11 𝐻 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})
165164fourierdlem2 40644 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑆 ∈ (𝐻𝑀) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
1666, 165syl 17 . . . . . . . . 9 (𝜑 → (𝑆 ∈ (𝐻𝑀) ↔ (𝑆 ∈ (ℝ ↑𝑚 (0...𝑀)) ∧ (((𝑆‘0) = (𝐴 + 𝑇) ∧ (𝑆𝑀) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑆𝑖) < (𝑆‘(𝑖 + 1))))))
167163, 166mpbird 247 . . . . . . . 8 (𝜑𝑆 ∈ (𝐻𝑀))
168164fveq1i 6230 . . . . . . . 8 (𝐻𝑀) = ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀)
169167, 168syl6eleq 2740 . . . . . . 7 (𝜑𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀))
170169adantr 480 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝑆 ∈ ((𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑𝑚 (0...𝑚)) ∣ (((𝑝‘0) = (𝐴 + 𝑇) ∧ (𝑝𝑚) = (𝐵 + 𝑇)) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝𝑖) < (𝑝‘(𝑖 + 1)))})‘𝑀))
17160adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
17266adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ)
173 simpr 476 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇)))
174 eliccre 40046 . . . . . . . . . . . 12 (((𝐴 + 𝑇) ∈ ℝ ∧ (𝐵 + 𝑇) ∈ ℝ ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
175171, 172, 173, 174syl3anc 1366 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℝ)
176175recnd 10106 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ∈ ℂ)
17762negcld 10417 . . . . . . . . . . 11 (𝜑 → -𝑇 ∈ ℂ)
178177adantr 480 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℂ)
179176, 178addcld 10097 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℂ)
180 simpl 472 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝜑)
1811adantr 480 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ∈ ℝ)
1823adantr 480 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐵 ∈ ℝ)
1838renegcld 10495 . . . . . . . . . . . . 13 (𝜑 → -𝑇 ∈ ℝ)
184183adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → -𝑇 ∈ ℝ)
185175, 184readdcld 10107 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ ℝ)
18663, 64eqtr2d 2686 . . . . . . . . . . . . 13 (𝜑𝐴 = ((𝐴 + 𝑇) + -𝑇))
187186adantr 480 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) + -𝑇))
188171rexrd 10127 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ*)
189172rexrd 10127 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℝ*)
190 iccgelb 12268 . . . . . . . . . . . . . 14 (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ*𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
191188, 189, 173, 190syl3anc 1366 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐴 + 𝑇) ≤ 𝑥)
192171, 175, 184, 191leadd1dd 10679 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐴 + 𝑇) + -𝑇) ≤ (𝑥 + -𝑇))
193187, 192eqbrtrd 4707 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝐴 ≤ (𝑥 + -𝑇))
194 iccleub 12267 . . . . . . . . . . . . . 14 (((𝐴 + 𝑇) ∈ ℝ* ∧ (𝐵 + 𝑇) ∈ ℝ*𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
195188, 189, 173, 194syl3anc 1366 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑥 ≤ (𝐵 + 𝑇))
196175, 172, 184, 195leadd1dd 10679 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ ((𝐵 + 𝑇) + -𝑇))
197172recnd 10106 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐵 + 𝑇) ∈ ℂ)
19862adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → 𝑇 ∈ ℂ)
199197, 198negsubd 10436 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = ((𝐵 + 𝑇) − 𝑇))
20069adantr 480 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) − 𝑇) = 𝐵)
201199, 200eqtrd 2685 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝐵 + 𝑇) + -𝑇) = 𝐵)
202196, 201breqtrd 4711 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ≤ 𝐵)
203181, 182, 185, 193, 202eliccd 40044 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))
204180, 203jca 553 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))
205 eleq1 2718 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)))
206205anbi2d 740 . . . . . . . . . . 11 (𝑦 = (𝑥 + -𝑇) → ((𝜑𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵))))
207 oveq1 6697 . . . . . . . . . . . . 13 (𝑦 = (𝑥 + -𝑇) → (𝑦 + 𝑇) = ((𝑥 + -𝑇) + 𝑇))
208207fveq2d 6233 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥 + -𝑇) + 𝑇)))
209 fveq2 6229 . . . . . . . . . . . 12 (𝑦 = (𝑥 + -𝑇) → (𝐹𝑦) = (𝐹‘(𝑥 + -𝑇)))
210208, 209eqeq12d 2666 . . . . . . . . . . 11 (𝑦 = (𝑥 + -𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))
211206, 210imbi12d 333 . . . . . . . . . 10 (𝑦 = (𝑥 + -𝑇) → (((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))))
212 eleq1 2718 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
213212anbi2d 740 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝜑𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑦 ∈ (𝐴[,]𝐵))))
214 oveq1 6697 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
215214fveq2d 6233 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
216 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
217215, 216eqeq12d 2666 . . . . . . . . . . . 12 (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)))
218213, 217imbi12d 333 . . . . . . . . . . 11 (𝑥 = 𝑦 → (((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))))
219218, 14chvarv 2299 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦))
220211, 219vtoclg 3297 . . . . . . . . 9 ((𝑥 + -𝑇) ∈ ℂ → ((𝜑 ∧ (𝑥 + -𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇))))
221179, 204, 220sylc 65 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹‘(𝑥 + -𝑇)))
222176, 198negsubd 10436 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝑥 + -𝑇) = (𝑥𝑇))
223222oveq1d 6705 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = ((𝑥𝑇) + 𝑇))
224176, 198npcand 10434 . . . . . . . . . 10 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥𝑇) + 𝑇) = 𝑥)
225223, 224eqtrd 2685 . . . . . . . . 9 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → ((𝑥 + -𝑇) + 𝑇) = 𝑥)
226225fveq2d 6233 . . . . . . . 8 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘((𝑥 + -𝑇) + 𝑇)) = (𝐹𝑥))
227221, 226eqtr3d 2687 . . . . . . 7 ((𝜑𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹𝑥))
228227adantlr 751 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑥 ∈ ((𝐴 + 𝑇)[,](𝐵 + 𝑇))) → (𝐹‘(𝑥 + -𝑇)) = (𝐹𝑥))
229 fveq2 6229 . . . . . . . 8 (𝑗 = 𝑖 → (𝑆𝑗) = (𝑆𝑖))
230229oveq1d 6705 . . . . . . 7 (𝑗 = 𝑖 → ((𝑆𝑗) + -𝑇) = ((𝑆𝑖) + -𝑇))
231230cbvmptv 4783 . . . . . 6 (𝑗 ∈ (0...𝑀) ↦ ((𝑆𝑗) + -𝑇)) = (𝑖 ∈ (0...𝑀) ↦ ((𝑆𝑖) + -𝑇))
23219adantr 480 . . . . . 6 ((𝜑 ∧ 0 < -𝑇) → 𝐹:ℝ⟶ℂ)
23319adantr 480 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
234 ioossre 12273 . . . . . . . . . . 11 ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ
235234a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ)
236233, 235feqresmpt 6289 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹𝑥)))
237153, 160oveq12d 6708 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) = (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
238143, 146, 147iooshift 40066 . . . . . . . . . . 11 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
239237, 238eqtrd 2685 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
240239mpteq1d 4771 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹𝑥)))
241 simpll 805 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝜑)
242 simplr 807 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑖 ∈ (0..^𝑀))
243238eleq2d 2716 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) ↔ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}))
244243biimpar 501 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
245143rexrd 10127 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℝ*)
2462453adant3 1101 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) ∈ ℝ*)
247146rexrd 10127 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
2482473adant3 1101 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
249 elioore 12243 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)) → 𝑥 ∈ ℝ)
250249adantl 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
2518adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
252250, 251resubcld 10496 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ℝ)
2532523adant2 1100 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ℝ)
254143recnd 10106 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ ℂ)
25562adantr 480 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℂ)
256254, 255pncand 10431 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄𝑖) + 𝑇) − 𝑇) = (𝑄𝑖))
257256eqcomd 2657 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) = (((𝑄𝑖) + 𝑇) − 𝑇))
2582573adant3 1101 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) = (((𝑄𝑖) + 𝑇) − 𝑇))
2591513adant3 1101 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) ∈ ℝ)
2602503adant2 1100 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
26183ad2ant1 1102 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
262151rexrd 10127 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) ∈ ℝ*)
2632623adant3 1101 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) ∈ ℝ*)
264159rexrd 10127 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
2652643adant3 1101 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
266 simp3 1083 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇)))
267 ioogtlb 40035 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) < 𝑥)
268263, 265, 266, 267syl3anc 1366 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄𝑖) + 𝑇) < 𝑥)
269259, 260, 261, 268ltsub1dd 10677 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄𝑖) + 𝑇) − 𝑇) < (𝑥𝑇))
270258, 269eqbrtrd 4707 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄𝑖) < (𝑥𝑇))
2711593adant3 1101 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
272 iooltub 40053 . . . . . . . . . . . . . . . . 17 ((((𝑄𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇))
273263, 265, 266, 272syl3anc 1366 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 < ((𝑄‘(𝑖 + 1)) + 𝑇))
274260, 271, 261, 273ltsub1dd 10677 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇))
275146recnd 10106 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
276275, 255pncand 10431 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
2772763adant3 1101 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
278274, 277breqtrd 4711 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < (𝑄‘(𝑖 + 1)))
279246, 248, 253, 270, 278eliood 40038 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
280241, 242, 244, 279syl3anc 1366 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))
281 fvres 6245 . . . . . . . . . . . 12 ((𝑥𝑇) ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
282280, 281syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)) = (𝐹‘(𝑥𝑇)))
283241, 244, 252syl2anc 694 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ ℝ)
28413ad2ant1 1102 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ∈ ℝ)
28533ad2ant1 1102 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐵 ∈ ℝ)
28664eqcomd 2657 . . . . . . . . . . . . . . . . . 18 (𝜑𝐴 = ((𝐴 + 𝑇) − 𝑇))
2872863ad2ant1 1102 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 = ((𝐴 + 𝑇) − 𝑇))
288603ad2ant1 1102 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ∈ ℝ)
2891adantr 480 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ)
2901rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐴 ∈ ℝ*)
291290adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ*)
2923rexrd 10127 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑𝐵 ∈ ℝ*)
293292adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ*)
2945, 6, 12fourierdlem15 40657 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
295294adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
296295, 142ffvelrnd 6400 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄𝑖) ∈ (𝐴[,]𝐵))
297 iccgelb 12268 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄𝑖) ∈ (𝐴[,]𝐵)) → 𝐴 ≤ (𝑄𝑖))
298291, 293, 296, 297syl3anc 1366 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐴 ≤ (𝑄𝑖))
299289, 143, 147, 298leadd1dd 10679 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐴 + 𝑇) ≤ ((𝑄𝑖) + 𝑇))
3002993adant3 1101 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) ≤ ((𝑄𝑖) + 𝑇))
301288, 259, 260, 300, 268lelttrd 10233 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐴 + 𝑇) < 𝑥)
302288, 260, 261, 301ltsub1dd 10677 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝐴 + 𝑇) − 𝑇) < (𝑥𝑇))
303287, 302eqbrtrd 4707 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 < (𝑥𝑇))
304284, 253, 303ltled 10223 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐴 ≤ (𝑥𝑇))
3051463adant3 1101 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
306295, 145ffvelrnd 6400 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵))
307 iccleub 12267 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ ℝ*𝐵 ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ (𝐴[,]𝐵)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
308291, 293, 306, 307syl3anc 1366 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
3093083adant3 1101 . . . . . . . . . . . . . . . . 17 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ≤ 𝐵)
310253, 305, 285, 278, 309ltletrd 10235 . . . . . . . . . . . . . . . 16 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) < 𝐵)
311253, 285, 310ltled 10223 . . . . . . . . . . . . . . 15 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ≤ 𝐵)
312284, 285, 253, 304, 311eliccd 40044 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ (0..^𝑀) ∧ 𝑥 ∈ (((𝑄𝑖) + 𝑇)(,)((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥𝑇) ∈ (𝐴[,]𝐵))
313241, 242, 244, 312syl3anc 1366 . . . . . . . . . . . . 13 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝑥𝑇) ∈ (𝐴[,]𝐵))
314241, 313jca 553 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)))
315 eleq1 2718 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥𝑇) ∈ (𝐴[,]𝐵)))
316315anbi2d 740 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑇) → ((𝜑𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵))))
317 oveq1 6697 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥𝑇) → (𝑦 + 𝑇) = ((𝑥𝑇) + 𝑇))
318317fveq2d 6233 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥𝑇) + 𝑇)))
319 fveq2 6229 . . . . . . . . . . . . . . 15 (𝑦 = (𝑥𝑇) → (𝐹𝑦) = (𝐹‘(𝑥𝑇)))
320318, 319eqeq12d 2666 . . . . . . . . . . . . . 14 (𝑦 = (𝑥𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦) ↔ (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
321316, 320imbi12d 333 . . . . . . . . . . . . 13 (𝑦 = (𝑥𝑇) → (((𝜑𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹𝑦)) ↔ ((𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))))
322321, 219vtoclg 3297 . . . . . . . . . . . 12 ((𝑥𝑇) ∈ ℝ → ((𝜑 ∧ (𝑥𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇))))
323283, 314, 322sylc 65 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹‘(𝑥𝑇)))
324244, 249syl 17 . . . . . . . . . . . 12 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ℝ)
325 recn 10064 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ → 𝑥 ∈ ℂ)
326325adantl 481 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → 𝑥 ∈ ℂ)
32762adantr 480 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ) → 𝑇 ∈ ℂ)
328326, 327npcand 10434 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ) → ((𝑥𝑇) + 𝑇) = 𝑥)
329328fveq2d 6233 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹𝑥))
330241, 324, 329syl2anc 694 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹‘((𝑥𝑇) + 𝑇)) = (𝐹𝑥))
331282, 323, 3303eqtr2rd 2692 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → (𝐹𝑥) = ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)))
332331mpteq2dva 4777 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ (𝐹𝑥)) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))))
333236, 240, 3323eqtrd 2689 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))))
334 ioosscn 40034 . . . . . . . . . . 11 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
335334a1i 11 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
336 eqeq1 2655 . . . . . . . . . . . . 13 (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇)))
337336rexbidv 3081 . . . . . . . . . . . 12 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)))
338 oveq1 6697 . . . . . . . . . . . . . 14 (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇))
339338eqeq2d 2661 . . . . . . . . . . . . 13 (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇)))
340339cbvrexv 3202 . . . . . . . . . . . 12 (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇))
341337, 340syl6bb 276 . . . . . . . . . . 11 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)))
342341cbvrabv 3230 . . . . . . . . . 10 {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}
343 eqid 2651 . . . . . . . . . 10 (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) = (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇)))
344335, 255, 342, 21, 343cncfshift 40405 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) ∈ ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ))
345239eqcomd 2657 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))))
346345oveq1d 6705 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ) = (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
347344, 346eleqtrd 2732 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↦ ((𝐹 ↾ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥𝑇))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
348333, 347eqeltrd 2730 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
349348adantlr 751 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) ∈ (((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
350 ffdm 6100 . . . . . . . . . . . 12 (𝐹:ℝ⟶ℂ → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
35119, 350syl 17 . . . . . . . . . . 11 (𝜑 → (𝐹:dom 𝐹⟶ℂ ∧ dom 𝐹 ⊆ ℝ))
352351simpld 474 . . . . . . . . . 10 (𝜑𝐹:dom 𝐹⟶ℂ)
353352adantr 480 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐹:dom 𝐹⟶ℂ)
354 ioossre 12273 . . . . . . . . . 10 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
355 fdm 6089 . . . . . . . . . . 11 (𝐹:ℝ⟶ℂ → dom 𝐹 = ℝ)
356233, 355syl 17 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → dom 𝐹 = ℝ)
357354, 356syl5sseqr 3687 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
358342eqcomi 2660 . . . . . . . . 9 {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}
359235, 345, 3563sstr4d 3681 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ⊆ dom 𝐹)
360342, 359syl5eqssr 3683 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} ⊆ dom 𝐹)
361 simpll 805 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
362361, 290syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐴 ∈ ℝ*)
363361, 292syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐵 ∈ ℝ*)
364361, 294syl 17 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
365 simplr 807 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
366 ioossicc 12297 . . . . . . . . . . . . 13 ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1)))
367366sseli 3632 . . . . . . . . . . . 12 (𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑧 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
368367adantl 481 . . . . . . . . . . 11 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ ((𝑄𝑖)[,](𝑄‘(𝑖 + 1))))
369362, 363, 364, 365, 368fourierdlem1 40643 . . . . . . . . . 10 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ (𝐴[,]𝐵))
370 eleq1 2718 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑧 ∈ (𝐴[,]𝐵)))
371370anbi2d 740 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝜑𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑𝑧 ∈ (𝐴[,]𝐵))))
372 oveq1 6697 . . . . . . . . . . . . . 14 (𝑥 = 𝑧 → (𝑥 + 𝑇) = (𝑧 + 𝑇))
373372fveq2d 6233 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑧 + 𝑇)))
374 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
375373, 374eqeq12d 2666 . . . . . . . . . . . 12 (𝑥 = 𝑧 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥) ↔ (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧)))
376371, 375imbi12d 333 . . . . . . . . . . 11 (𝑥 = 𝑧 → (((𝜑𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹𝑥)) ↔ ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))))
377376, 14chvarv 2299 . . . . . . . . . 10 ((𝜑𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))
378361, 369, 377syl2anc 694 . . . . . . . . 9 (((𝜑𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑧 + 𝑇)) = (𝐹𝑧))
379353, 335, 357, 255, 358, 360, 378, 23limcperiod 40178 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄𝑖) + 𝑇)))
380358, 345syl5eq 2697 . . . . . . . . . 10 ((𝜑𝑖 ∈ (0..^𝑀)) → {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)} = ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1))))
381380reseq2d 5428 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) = (𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))))
382153eqcomd 2657 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄𝑖) + 𝑇) = (𝑆𝑖))
383381, 382oveq12d 6708 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄𝑖) + 𝑇)) = ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
384379, 383eleqtrd 2732 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
385384adantlr 751 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆𝑖)))
386353, 335, 357, 255, 358, 360, 378, 25limcperiod 40178 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄‘(𝑖 + 1)) + 𝑇)))
387160eqcomd 2657 . . . . . . . . 9 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) = (𝑆‘(𝑖 + 1)))
388381, 387oveq12d 6708 . . . . . . . 8 ((𝜑𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}) lim ((𝑄‘(𝑖 + 1)) + 𝑇)) = ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
389386, 388eleqtrd 2732 . . . . . . 7 ((𝜑𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
390389adantlr 751 . . . . . 6 (((𝜑 ∧ 0 < -𝑇) ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑆𝑖)(,)(𝑆‘(𝑖 + 1)))) lim (𝑆‘(𝑖 + 1))))
391 eqeq1 2655 . . . . . . . 8 (𝑦 = 𝑥 → (𝑦 = (𝑆𝑖) ↔ 𝑥 = (𝑆𝑖)))
392 eqeq1 2655 . . . . . . . . 9 (𝑦 = 𝑥 → (𝑦 = (𝑆‘(𝑖 + 1)) ↔ 𝑥 = (𝑆‘(𝑖 + 1))))
393392, 29ifbieq2d 4144 . . . . . . . 8 (𝑦 = 𝑥 → if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦)) = if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥)))
394391, 393ifbieq2d 4144 . . . . . . 7 (𝑦 = 𝑥 → if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦))) = if(𝑥 = (𝑆𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
395394cbvmptv 4783 . . . . . 6 (𝑦 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑦 = (𝑆𝑖), 𝑅, if(𝑦 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑦)))) = (𝑥 ∈ ((𝑆𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, (𝐹𝑥))))
396 eqid 2651 . . . . . 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 40722 . . . . 5 ((𝜑 ∧ 0 < -𝑇) → ∫(((𝐴 + 𝑇) + -𝑇)[,]((𝐵 + 𝑇) + -𝑇))(𝐹𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥)
39874, 397eqtr2d 2686 . . . 4 ((𝜑 ∧ 0 < -𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
39949, 59, 398syl2anc 694 . . 3 (((𝜑 ∧ ¬ 0 < 𝑇) ∧ ¬ 𝑇 = 0) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
40048, 399pm2.61dan 849 . 2 ((𝜑 ∧ ¬ 0 < 𝑇) → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
40134, 400pm2.61dan 849 1 (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹𝑥) d𝑥)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 382   ∧ wa 383   ∧ w3a 1054   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ⊆ wss 3607  ifcif 4119   class class class wbr 4685   ↦ cmpt 4762  dom cdm 5143   ↾ cres 5145  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ↑𝑚 cmap 7899  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   + caddc 9977  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304  -cneg 10305  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  (,)cioo 12213  [,]cicc 12216  ...cfz 12364  ..^cfzo 12504  –cn→ccncf 22726  ∫citg 23432   limℂ climc 23671 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cc 9295  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-ofr 6940  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-omul 7610  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-acn 8806  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-sum 14461  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-cmp 21238  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-ovol 23279  df-vol 23280  df-mbf 23433  df-itg1 23434  df-itg2 23435  df-ibl 23436  df-itg 23437  df-0p 23482  df-ditg 23656  df-limc 23675  df-dv 23676 This theorem is referenced by:  fourierdlem107  40748
 Copyright terms: Public domain W3C validator