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

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

Proof of Theorem fourierdlem81
Dummy variables 𝑦 𝑤 𝑧 𝑗 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fourierdlem81.q . . . . . . . . 9 (𝜑 → 𝑄 ∈ (𝑃‘𝑀))
2 fourierdlem81.m . . . . . . . . . 10 (𝜑 → 𝑀 ∈ ℕ)
3 fourierdlem81.p . . . . . . . . . . 11 𝑃 = (𝑚 ∈ ℕ ↦ {𝑝 ∈ (ℝ ↑m (0...𝑚)) ∣ (((𝑝‘0) = 𝐴 ∧ (𝑝‘𝑚) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑚)(𝑝‘𝑖) < (𝑝‘(𝑖 + 1)))})
43fourierdlem2 47392 . . . . . . . . . 10 (𝑀 ∈ ℕ → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
52, 4syl 18 . . . . . . . . 9 (𝜑 → (𝑄 ∈ (𝑃‘𝑀) ↔ (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))))
61, 5mpbid 235 . . . . . . . 8 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ∧ (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))))
76simprd 501 . . . . . . 7 (𝜑 → (((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵) ∧ ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1))))
87simpld 500 . . . . . 6 (𝜑 → ((𝑄‘0) = 𝐴 ∧ (𝑄‘𝑀) = 𝐵))
98simpld 500 . . . . 5 (𝜑 → (𝑄‘0) = 𝐴)
109eqcomd 2769 . . . 4 (𝜑 → 𝐴 = (𝑄‘0))
118simprd 501 . . . . 5 (𝜑 → (𝑄‘𝑀) = 𝐵)
1211eqcomd 2769 . . . 4 (𝜑 → 𝐵 = (𝑄‘𝑀))
1310, 12oveq12d 7469 . . 3 (𝜑 → (𝐴[,]𝐵) = ((𝑄‘0)[,](𝑄‘𝑀)))
1413itgeq1d 47240 . 2 (𝜑 → ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥 = ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑥) d𝑥)
15 0zd 12745 . . 3 (𝜑 → 0 ∈ ℤ)
16 nnuz 13044 . . . . 5 ℕ = (ℤ≥‘1)
17 0p1e1 12503 . . . . . 6 (0 + 1) = 1
1817fveq2i 6919 . . . . 5 (ℤ≥‘(0 + 1)) = (ℤ≥‘1)
1916, 18eqtr4i 2789 . . . 4 ℕ = (ℤ≥‘(0 + 1))
202, 19eleqtrdi 2874 . . 3 (𝜑 → 𝑀 ∈ (ℤ≥‘(0 + 1)))
216simpld 500 . . . 4 (𝜑 → 𝑄 ∈ (ℝ ↑m (0...𝑀)))
22 reex 11330 . . . . . 6 ℝ ∈ V
2322a1i 11 . . . . 5 (𝜑 → ℝ ∈ V)
24 ovex 7484 . . . . . 6 (0...𝑀) ∈ V
2524a1i 11 . . . . 5 (𝜑 → (0...𝑀) ∈ V)
2623, 25elmapd 8898 . . . 4 (𝜑 → (𝑄 ∈ (ℝ ↑m (0...𝑀)) ↔ 𝑄:(0...𝑀)⟶ℝ))
2721, 26mpbid 235 . . 3 (𝜑 → 𝑄:(0...𝑀)⟶ℝ)
287simprd 501 . . . 4 (𝜑 → ∀𝑖 ∈ (0..^𝑀)(𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
2928r19.21bi 3258 . . 3 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) < (𝑄‘(𝑖 + 1)))
30 fourierdlem81.f . . . . 5 (𝜑 → 𝐹:ℝ⟶ℂ)
3130adantr 486 . . . 4 ((𝜑 ∧ 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝐹:ℝ⟶ℂ)
32 fourierdlem81.a . . . . . . 7 (𝜑 → 𝐴 ∈ ℝ)
339, 32eqeltrd 2864 . . . . . 6 (𝜑 → (𝑄‘0) ∈ ℝ)
34 fourierdlem81.b . . . . . . 7 (𝜑 → 𝐵 ∈ ℝ)
3511, 34eqeltrd 2864 . . . . . 6 (𝜑 → (𝑄‘𝑀) ∈ ℝ)
3633, 35iccssred 13605 . . . . 5 (𝜑 → ((𝑄‘0)[,](𝑄‘𝑀)) ⊆ ℝ)
3736sselda 3913 . . . 4 ((𝜑 ∧ 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → 𝑥 ∈ ℝ)
3831, 37ffvelcdmd 7117 . . 3 ((𝜑 ∧ 𝑥 ∈ ((𝑄‘0)[,](𝑄‘𝑀))) → (𝐹‘𝑥) ∈ ℂ)
3927adantr 486 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶ℝ)
40 elfzofz 13850 . . . . . 6 (𝑖 ∈ (0..^𝑀) → 𝑖 ∈ (0...𝑀))
4140adantl 487 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0...𝑀))
4239, 41ffvelcdmd 7117 . . . 4 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ)
43 fzofzp1 13939 . . . . . 6 (𝑖 ∈ (0..^𝑀) → (𝑖 + 1) ∈ (0...𝑀))
4443adantl 487 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑖 + 1) ∈ (0...𝑀))
4539, 44ffvelcdmd 7117 . . . 4 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
4630feqmptd 6984 . . . . . . . 8 (𝜑 → 𝐹 = (𝑥 ∈ ℝ ↦ (𝐹‘𝑥)))
4746reseq1d 5985 . . . . . . 7 (𝜑 → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
4847adantr 486 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
49 ioossre 13578 . . . . . . . 8 ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ
5049a1i 11 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℝ)
5150resmptd 6050 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑥 ∈ ℝ ↦ (𝐹‘𝑥)) ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) = (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)))
5248, 51eqtr2d 2799 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) = (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))))
53 fourierdlem81.cncf . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ (((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))–cn→ℂ))
54 fourierdlem81.l . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))))
55 fourierdlem81.r . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)))
5642, 45, 53, 54, 55iblcncfioo 47261 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) ∈ 𝐿1)
5752, 56eqeltrd 2864 . . . 4 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) ∈ 𝐿1)
5830ad2antrr 739 . . . . 5 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℂ)
5942, 45iccssred 13605 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ ℝ)
6059sselda 3913 . . . . 5 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑥 ∈ ℝ)
6158, 60ffvelcdmd 7117 . . . 4 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝐹‘𝑥) ∈ ℂ)
6242, 45, 57, 61ibliooicc 47254 . . 3 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) ∈ 𝐿1)
6315, 20, 27, 29, 38, 62itgspltprt 47262 . 2 (𝜑 → ∫((𝑄‘0)[,](𝑄‘𝑀))(𝐹‘𝑥) d𝑥 = Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥)
64 fourierdlem81.s . . . . . . . 8 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) + 𝑇))
6564a1i 11 . . . . . . 7 (𝜑 → 𝑆 = (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) + 𝑇)))
66 fveq2 6916 . . . . . . . . 9 (𝑖 = 0 → (𝑄‘𝑖) = (𝑄‘0))
6766oveq1d 7466 . . . . . . . 8 (𝑖 = 0 → ((𝑄‘𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
6867adantl 487 . . . . . . 7 ((𝜑 ∧ 𝑖 = 0) → ((𝑄‘𝑖) + 𝑇) = ((𝑄‘0) + 𝑇))
692nnnn0d 12707 . . . . . . . . 9 (𝜑 → 𝑀 ∈ ℕ0)
70 nn0uz 13043 . . . . . . . . 9 ℕ0 = (ℤ≥‘0)
7169, 70eleqtrdi 2874 . . . . . . . 8 (𝜑 → 𝑀 ∈ (ℤ≥‘0))
72 eluzfz1 13704 . . . . . . . 8 (𝑀 ∈ (ℤ≥‘0) → 0 ∈ (0...𝑀))
7371, 72syl 18 . . . . . . 7 (𝜑 → 0 ∈ (0...𝑀))
74 fourierdlem81.t . . . . . . . . 9 (𝜑 → 𝑇 ∈ ℝ+)
7574rpred 13204 . . . . . . . 8 (𝜑 → 𝑇 ∈ ℝ)
7633, 75readdcld 11377 . . . . . . 7 (𝜑 → ((𝑄‘0) + 𝑇) ∈ ℝ)
7765, 68, 73, 76fvmptd 7032 . . . . . 6 (𝜑 → (𝑆‘0) = ((𝑄‘0) + 𝑇))
789oveq1d 7466 . . . . . 6 (𝜑 → ((𝑄‘0) + 𝑇) = (𝐴 + 𝑇))
7977, 78eqtr2d 2799 . . . . 5 (𝜑 → (𝐴 + 𝑇) = (𝑆‘0))
80 fveq2 6916 . . . . . . . . 9 (𝑖 = 𝑀 → (𝑄‘𝑖) = (𝑄‘𝑀))
8180oveq1d 7466 . . . . . . . 8 (𝑖 = 𝑀 → ((𝑄‘𝑖) + 𝑇) = ((𝑄‘𝑀) + 𝑇))
8281adantl 487 . . . . . . 7 ((𝜑 ∧ 𝑖 = 𝑀) → ((𝑄‘𝑖) + 𝑇) = ((𝑄‘𝑀) + 𝑇))
83 eluzfz2 13705 . . . . . . . 8 (𝑀 ∈ (ℤ≥‘0) → 𝑀 ∈ (0...𝑀))
8471, 83syl 18 . . . . . . 7 (𝜑 → 𝑀 ∈ (0...𝑀))
8535, 75readdcld 11377 . . . . . . 7 (𝜑 → ((𝑄‘𝑀) + 𝑇) ∈ ℝ)
8665, 82, 84, 85fvmptd 7032 . . . . . 6 (𝜑 → (𝑆‘𝑀) = ((𝑄‘𝑀) + 𝑇))
8711oveq1d 7466 . . . . . 6 (𝜑 → ((𝑄‘𝑀) + 𝑇) = (𝐵 + 𝑇))
8886, 87eqtr2d 2799 . . . . 5 (𝜑 → (𝐵 + 𝑇) = (𝑆‘𝑀))
8979, 88oveq12d 7469 . . . 4 (𝜑 → ((𝐴 + 𝑇)[,](𝐵 + 𝑇)) = ((𝑆‘0)[,](𝑆‘𝑀)))
9089itgeq1d 47240 . . 3 (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫((𝑆‘0)[,](𝑆‘𝑀))(𝐹‘𝑥) d𝑥)
9127ffvelcdmda 7116 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → (𝑄‘𝑖) ∈ ℝ)
9275adantr 486 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → 𝑇 ∈ ℝ)
9391, 92readdcld 11377 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0...𝑀)) → ((𝑄‘𝑖) + 𝑇) ∈ ℝ)
9493, 64fmptd 7146 . . . 4 (𝜑 → 𝑆:(0...𝑀)⟶ℝ)
9575adantr 486 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℝ)
9642, 45, 95, 29ltadd1dd 11967 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑇) < ((𝑄‘(𝑖 + 1)) + 𝑇))
9740, 93sylan2 605 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑇) ∈ ℝ)
9864fvmpt2 7036 . . . . . 6 ((𝑖 ∈ (0...𝑀) ∧ ((𝑄‘𝑖) + 𝑇) ∈ ℝ) → (𝑆‘𝑖) = ((𝑄‘𝑖) + 𝑇))
9941, 97, 98syl2anc 596 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑆‘𝑖) = ((𝑄‘𝑖) + 𝑇))
100 fveq2 6916 . . . . . . . . . 10 (𝑖 = 𝑗 → (𝑄‘𝑖) = (𝑄‘𝑗))
101100oveq1d 7466 . . . . . . . . 9 (𝑖 = 𝑗 → ((𝑄‘𝑖) + 𝑇) = ((𝑄‘𝑗) + 𝑇))
102101cbvmptv 5215 . . . . . . . 8 (𝑖 ∈ (0...𝑀) ↦ ((𝑄‘𝑖) + 𝑇)) = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) + 𝑇))
10364, 102eqtri 2786 . . . . . . 7 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) + 𝑇))
104103a1i 11 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑆 = (𝑗 ∈ (0...𝑀) ↦ ((𝑄‘𝑗) + 𝑇)))
105 fveq2 6916 . . . . . . . 8 (𝑗 = (𝑖 + 1) → (𝑄‘𝑗) = (𝑄‘(𝑖 + 1)))
106105oveq1d 7466 . . . . . . 7 (𝑗 = (𝑖 + 1) → ((𝑄‘𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
107106adantl 487 . . . . . 6 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑗 = (𝑖 + 1)) → ((𝑄‘𝑗) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
10845, 95readdcld 11377 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
109104, 107, 44, 108fvmptd 7032 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑆‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) + 𝑇))
11096, 99, 1093brtr4d 5143 . . . 4 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑆‘𝑖) < (𝑆‘(𝑖 + 1)))
11130adantr 486 . . . . 5 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘0)[,](𝑆‘𝑀))) → 𝐹:ℝ⟶ℂ)
11277, 76eqeltrd 2864 . . . . . . . 8 (𝜑 → (𝑆‘0) ∈ ℝ)
113112adantr 486 . . . . . . 7 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘0)[,](𝑆‘𝑀))) → (𝑆‘0) ∈ ℝ)
11486, 85eqeltrd 2864 . . . . . . . 8 (𝜑 → (𝑆‘𝑀) ∈ ℝ)
115114adantr 486 . . . . . . 7 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘0)[,](𝑆‘𝑀))) → (𝑆‘𝑀) ∈ ℝ)
116113, 115iccssred 13605 . . . . . 6 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘0)[,](𝑆‘𝑀))) → ((𝑆‘0)[,](𝑆‘𝑀)) ⊆ ℝ)
117 simpr 490 . . . . . 6 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘0)[,](𝑆‘𝑀))) → 𝑥 ∈ ((𝑆‘0)[,](𝑆‘𝑀)))
118116, 117sseldd 3914 . . . . 5 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘0)[,](𝑆‘𝑀))) → 𝑥 ∈ ℝ)
119111, 118ffvelcdmd 7117 . . . 4 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘0)[,](𝑆‘𝑀))) → (𝐹‘𝑥) ∈ ℂ)
12099, 97eqeltrd 2864 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑆‘𝑖) ∈ ℝ)
121109, 108eqeltrd 2864 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑆‘(𝑖 + 1)) ∈ ℝ)
122 ioosscn 13579 . . . . . . . . 9 ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ
123122a1i 11 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ℂ)
124 eqeq1 2767 . . . . . . . . . . 11 (𝑤 = 𝑥 → (𝑤 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑧 + 𝑇)))
125124rexbidv 3190 . . . . . . . . . 10 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)))
126 oveq1 7458 . . . . . . . . . . . 12 (𝑧 = 𝑦 → (𝑧 + 𝑇) = (𝑦 + 𝑇))
127126eqeq2d 2774 . . . . . . . . . . 11 (𝑧 = 𝑦 → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = (𝑦 + 𝑇)))
128127cbvrexvw 3245 . . . . . . . . . 10 (∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇))
129125, 128bitrdi 290 . . . . . . . . 9 (𝑤 = 𝑥 → (∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) ↔ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)))
130129cbvrabv 3426 . . . . . . . 8 {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = {𝑥 ∈ ℂ ∣ ∃𝑦 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑦 + 𝑇)}
131 fdm 6749 . . . . . . . . . . . 12 (𝐹:ℝ⟶ℂ → dom 𝐹 = ℝ)
13230, 131syl 18 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = ℝ)
133132feq2d 6723 . . . . . . . . . 10 (𝜑 → (𝐹:dom 𝐹⟶ℂ ↔ 𝐹:ℝ⟶ℂ))
13430, 133mpbird 260 . . . . . . . . 9 (𝜑 → 𝐹:dom 𝐹⟶ℂ)
135134adantr 486 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:dom 𝐹⟶ℂ)
136 elioore 13546 . . . . . . . . . . . . . . . . . 18 (𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑧 ∈ ℝ)
137136adantl 487 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ ℝ)
13875adantr 486 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑇 ∈ ℝ)
139137, 138readdcld 11377 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑧 + 𝑇) ∈ ℝ)
140139adantlr 728 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑧 + 𝑇) ∈ ℝ)
1411403adant3 1150 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑤 = (𝑧 + 𝑇)) → (𝑧 + 𝑇) ∈ ℝ)
142 simp3 1156 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑤 = (𝑧 + 𝑇)) → 𝑤 = (𝑧 + 𝑇))
1431323ad2ant1 1151 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑤 = (𝑧 + 𝑇)) → dom 𝐹 = ℝ)
1441433adant1r 1196 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑤 = (𝑧 + 𝑇)) → dom 𝐹 = ℝ)
145141, 142, 1443eltr4d 2879 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑤 = (𝑧 + 𝑇)) → 𝑤 ∈ dom 𝐹)
1461453exp 1137 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ dom 𝐹)))
147146adantr 486 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 ∈ ℂ) → (𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ dom 𝐹)))
148147rexlimdv 3165 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 ∈ ℂ) → (∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ dom 𝐹))
149148ralrimiva 3158 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∀𝑤 ∈ ℂ (∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ dom 𝐹))
150 rabss 3998 . . . . . . . . 9 ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ⊆ dom 𝐹 ↔ ∀𝑤 ∈ ℂ (∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇) → 𝑤 ∈ dom 𝐹))
151149, 150sylibr 237 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ⊆ dom 𝐹)
152 simpll 779 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
15332rexrd 11398 . . . . . . . . . . 11 (𝜑 → 𝐴 ∈ ℝ*)
154153ad2antrr 739 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐴 ∈ ℝ*)
15534rexrd 11398 . . . . . . . . . . 11 (𝜑 → 𝐵 ∈ ℝ*)
156155ad2antrr 739 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐵 ∈ ℝ*)
1573, 2, 1fourierdlem15 47405 . . . . . . . . . . 11 (𝜑 → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
158157ad2antrr 739 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
159 simplr 781 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
160 ioossicc 13604 . . . . . . . . . . . 12 ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))
161160sseli 3909 . . . . . . . . . . 11 (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
162161adantl 487 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
163154, 156, 158, 159, 162fourierdlem1 47391 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑥 ∈ (𝐴[,]𝐵))
164 fourierdlem81.fper . . . . . . . . 9 ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
165152, 163, 164syl2anc 596 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥))
166123, 95, 130, 135, 151, 165, 53cncfperiod 47162 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) ∈ ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ))
167125elrab 3648 . . . . . . . . . . . . 13 (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↔ (𝑥 ∈ ℂ ∧ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)))
168167simprbi 503 . . . . . . . . . . . 12 (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} → ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇))
169 simpr 490 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)) → ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇))
170 nfv 1949 . . . . . . . . . . . . . . . 16 Ⅎ𝑧(𝜑 ∧ 𝑖 ∈ (0..^𝑀))
171 nfre1 3291 . . . . . . . . . . . . . . . 16 Ⅎ𝑧∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)
172170, 171nfan 1934 . . . . . . . . . . . . . . 15 Ⅎ𝑧((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇))
173 nfv 1949 . . . . . . . . . . . . . . 15 Ⅎ𝑧(𝑥 ∈ ℝ ∧ (𝑆‘𝑖) < 𝑥 ∧ 𝑥 < (𝑆‘(𝑖 + 1)))
174 simp3 1156 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 = (𝑧 + 𝑇))
1751393adant3 1150 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑧 + 𝑇) ∈ ℝ)
176174, 175eqeltrd 2864 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 ∈ ℝ)
1771763adant1r 1196 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 ∈ ℝ)
17842adantr 486 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
179136adantl 487 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ ℝ)
18075ad2antrr 739 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑇 ∈ ℝ)
181 simpr 490 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
18242rexrd 11398 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℝ*)
183182adantr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ*)
18445rexrd 11398 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
185184adantr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
186 elioo2 13557 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ*) → (𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (𝑧 ∈ ℝ ∧ (𝑄‘𝑖) < 𝑧 ∧ 𝑧 < (𝑄‘(𝑖 + 1)))))
187183, 185, 186syl2anc 596 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ↔ (𝑧 ∈ ℝ ∧ (𝑄‘𝑖) < 𝑧 ∧ 𝑧 < (𝑄‘(𝑖 + 1)))))
188181, 187mpbid 235 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑧 ∈ ℝ ∧ (𝑄‘𝑖) < 𝑧 ∧ 𝑧 < (𝑄‘(𝑖 + 1))))
189188simp2d 1161 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) < 𝑧)
190178, 179, 180, 189ltadd1dd 11967 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → ((𝑄‘𝑖) + 𝑇) < (𝑧 + 𝑇))
1911903adant3 1150 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → ((𝑄‘𝑖) + 𝑇) < (𝑧 + 𝑇))
192993ad2ant1 1151 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑆‘𝑖) = ((𝑄‘𝑖) + 𝑇))
193 simp3 1156 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 = (𝑧 + 𝑇))
194191, 192, 1933brtr4d 5143 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑆‘𝑖) < 𝑥)
19545adantr 486 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
196188simp3d 1162 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 < (𝑄‘(𝑖 + 1)))
197179, 195, 180, 196ltadd1dd 11967 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝑧 + 𝑇) < ((𝑄‘(𝑖 + 1)) + 𝑇))
1981973adant3 1150 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑧 + 𝑇) < ((𝑄‘(𝑖 + 1)) + 𝑇))
1991093ad2ant1 1151 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑆‘(𝑖 + 1)) = ((𝑄‘(𝑖 + 1)) + 𝑇))
200198, 193, 1993brtr4d 5143 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → 𝑥 < (𝑆‘(𝑖 + 1)))
201177, 194, 2003jca 1146 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = (𝑧 + 𝑇)) → (𝑥 ∈ ℝ ∧ (𝑆‘𝑖) < 𝑥 ∧ 𝑥 < (𝑆‘(𝑖 + 1))))
2022013exp 1137 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑥 = (𝑧 + 𝑇) → (𝑥 ∈ ℝ ∧ (𝑆‘𝑖) < 𝑥 ∧ 𝑥 < (𝑆‘(𝑖 + 1))))))
203202adantr 486 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)) → (𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → (𝑥 = (𝑧 + 𝑇) → (𝑥 ∈ ℝ ∧ (𝑆‘𝑖) < 𝑥 ∧ 𝑥 < (𝑆‘(𝑖 + 1))))))
204172, 173, 203rexlimd 3273 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)) → (∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇) → (𝑥 ∈ ℝ ∧ (𝑆‘𝑖) < 𝑥 ∧ 𝑥 < (𝑆‘(𝑖 + 1)))))
205169, 204mpd 16 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)) → (𝑥 ∈ ℝ ∧ (𝑆‘𝑖) < 𝑥 ∧ 𝑥 < (𝑆‘(𝑖 + 1))))
206120rexrd 11398 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑆‘𝑖) ∈ ℝ*)
207206adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)) → (𝑆‘𝑖) ∈ ℝ*)
208121rexrd 11398 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑆‘(𝑖 + 1)) ∈ ℝ*)
209208adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)) → (𝑆‘(𝑖 + 1)) ∈ ℝ*)
210 elioo2 13557 . . . . . . . . . . . . . 14 (((𝑆‘𝑖) ∈ ℝ* ∧ (𝑆‘(𝑖 + 1)) ∈ ℝ*) → (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↔ (𝑥 ∈ ℝ ∧ (𝑆‘𝑖) < 𝑥 ∧ 𝑥 < (𝑆‘(𝑖 + 1)))))
211207, 209, 210syl2anc 596 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)) → (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↔ (𝑥 ∈ ℝ ∧ (𝑆‘𝑖) < 𝑥 ∧ 𝑥 < (𝑆‘(𝑖 + 1)))))
212205, 211mpbird 260 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇)) → 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))
213168, 212sylan2 605 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) → 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))
214 elioore 13546 . . . . . . . . . . . . . 14 (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) → 𝑥 ∈ ℝ)
215214recnd 11376 . . . . . . . . . . . . 13 (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) → 𝑥 ∈ ℂ)
216215adantl 487 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 ∈ ℂ)
217182adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ*)
218184adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
219214adantl 487 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 ∈ ℝ)
22075adantr 486 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑇 ∈ ℝ)
221219, 220resubcld 11783 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) ∈ ℝ)
222221adantlr 728 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) ∈ ℝ)
22399oveq1d 7466 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘𝑖) − 𝑇) = (((𝑄‘𝑖) + 𝑇) − 𝑇))
22442recnd 11376 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ℂ)
22595recnd 11376 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℂ)
226224, 225pncand 11709 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) + 𝑇) − 𝑇) = (𝑄‘𝑖))
227223, 226eqtr2d 2799 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = ((𝑆‘𝑖) − 𝑇))
228227adantr 486 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑄‘𝑖) = ((𝑆‘𝑖) − 𝑇))
229120adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑆‘𝑖) ∈ ℝ)
230214adantl 487 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 ∈ ℝ)
23175ad2antrr 739 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑇 ∈ ℝ)
232 simpr 490 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))
233206adantr 486 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑆‘𝑖) ∈ ℝ*)
234208adantr 486 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑆‘(𝑖 + 1)) ∈ ℝ*)
235233, 234, 210syl2anc 596 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↔ (𝑥 ∈ ℝ ∧ (𝑆‘𝑖) < 𝑥 ∧ 𝑥 < (𝑆‘(𝑖 + 1)))))
236232, 235mpbid 235 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑥 ∈ ℝ ∧ (𝑆‘𝑖) < 𝑥 ∧ 𝑥 < (𝑆‘(𝑖 + 1))))
237236simp2d 1161 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑆‘𝑖) < 𝑥)
238229, 230, 231, 237ltsub1dd 11968 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → ((𝑆‘𝑖) − 𝑇) < (𝑥 − 𝑇))
239228, 238eqbrtrd 5133 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑄‘𝑖) < (𝑥 − 𝑇))
240121adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑆‘(𝑖 + 1)) ∈ ℝ)
241236simp3d 1162 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 < (𝑆‘(𝑖 + 1)))
242230, 240, 231, 241ltsub1dd 11968 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) < ((𝑆‘(𝑖 + 1)) − 𝑇))
243109oveq1d 7466 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘(𝑖 + 1)) − 𝑇) = (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇))
24445recnd 11376 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ℂ)
245244, 225pncand 11709 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
246243, 245eqtrd 2798 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)))
247246adantr 486 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → ((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)))
248242, 247breqtrd 5137 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) < (𝑄‘(𝑖 + 1)))
249217, 218, 222, 239, 248eliood 46783 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
250219recnd 11376 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 ∈ ℂ)
251220recnd 11376 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑇 ∈ ℂ)
252250, 251npcand 11712 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → ((𝑥 − 𝑇) + 𝑇) = 𝑥)
253252eqcomd 2769 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 = ((𝑥 − 𝑇) + 𝑇))
254253adantlr 728 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 = ((𝑥 − 𝑇) + 𝑇))
255 oveq1 7458 . . . . . . . . . . . . . . 15 (𝑧 = (𝑥 − 𝑇) → (𝑧 + 𝑇) = ((𝑥 − 𝑇) + 𝑇))
256255eqeq2d 2774 . . . . . . . . . . . . . 14 (𝑧 = (𝑥 − 𝑇) → (𝑥 = (𝑧 + 𝑇) ↔ 𝑥 = ((𝑥 − 𝑇) + 𝑇)))
257256rspcev 3580 . . . . . . . . . . . . 13 (((𝑥 − 𝑇) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ∧ 𝑥 = ((𝑥 − 𝑇) + 𝑇)) → ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇))
258249, 254, 257syl2anc 596 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑥 = (𝑧 + 𝑇))
259216, 258, 167sylanbrc 595 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)})
260213, 259impbida 813 . . . . . . . . . 10 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} ↔ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))))
261260eqrdv 2761 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))
262261reseq2d 5986 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) = (𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))))
26330adantr 486 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐹:ℝ⟶ℂ)
264 ioossre 13578 . . . . . . . . . 10 ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ
265264a1i 11 . . . . . . . . 9 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ℝ)
266263, 265feqresmpt 6985 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) = (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥)))
267262, 266eqtrd 2798 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) = (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥)))
268261oveq1d 7466 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ({𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}–cn→ℂ) = (((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
269166, 267, 2683eltr3d 2878 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) ∈ (((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))–cn→ℂ))
27049, 132sseqtrrid 3956 . . . . . . . . 9 (𝜑 → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
271270adantr 486 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
272 eqid 2763 . . . . . . . 8 {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)} = {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}
273 simpll 779 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝜑)
274153ad2antrr 739 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐴 ∈ ℝ*)
275155ad2antrr 739 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝐵 ∈ ℝ*)
276157ad2antrr 739 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
277 simplr 781 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑖 ∈ (0..^𝑀))
278160, 181sselid 3911 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
279274, 275, 276, 277, 278fourierdlem1 47391 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → 𝑧 ∈ (𝐴[,]𝐵))
280 eleq1 2852 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑧 ∈ (𝐴[,]𝐵)))
281280anbi2d 642 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵))))
282 oveq1 7458 . . . . . . . . . . . . 13 (𝑥 = 𝑧 → (𝑥 + 𝑇) = (𝑧 + 𝑇))
283282fveq2d 6920 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑧 + 𝑇)))
284 fveq2 6916 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧))
285283, 284eqeq12d 2779 . . . . . . . . . . 11 (𝑥 = 𝑧 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑧 + 𝑇)) = (𝐹‘𝑧)))
286281, 285imbi12d 347 . . . . . . . . . 10 (𝑥 = 𝑧 → (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹‘𝑧))))
287286, 164chvarvv 2024 . . . . . . . . 9 ((𝜑 ∧ 𝑧 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑧 + 𝑇)) = (𝐹‘𝑧))
288273, 279, 287syl2anc 596 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) → (𝐹‘(𝑧 + 𝑇)) = (𝐹‘𝑧))
289135, 123, 271, 225, 272, 151, 288, 54limcperiod 46913 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) limℂ ((𝑄‘(𝑖 + 1)) + 𝑇)))
290109eqcomd 2769 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘(𝑖 + 1)) + 𝑇) = (𝑆‘(𝑖 + 1)))
291267, 290oveq12d 7469 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) limℂ ((𝑄‘(𝑖 + 1)) + 𝑇)) = ((𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) limℂ (𝑆‘(𝑖 + 1))))
292289, 291eleqtrd 2866 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ((𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) limℂ (𝑆‘(𝑖 + 1))))
293135, 123, 271, 225, 272, 151, 288, 55limcperiod 46913 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) limℂ ((𝑄‘𝑖) + 𝑇)))
29499eqcomd 2769 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖) + 𝑇) = (𝑆‘𝑖))
295267, 294oveq12d 7469 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝐹 ↾ {𝑤 ∈ ℂ ∣ ∃𝑧 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))𝑤 = (𝑧 + 𝑇)}) limℂ ((𝑄‘𝑖) + 𝑇)) = ((𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) limℂ (𝑆‘𝑖)))
296293, 295eleqtrd 2866 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ((𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) limℂ (𝑆‘𝑖)))
297120, 121, 269, 292, 296iblcncfioo 47261 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) ∈ 𝐿1)
29830ad2antrr 739 . . . . . 6 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝐹:ℝ⟶ℂ)
299120adantr 486 . . . . . . 7 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑆‘𝑖) ∈ ℝ)
300121adantr 486 . . . . . . 7 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑆‘(𝑖 + 1)) ∈ ℝ)
301 simpr 490 . . . . . . 7 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))))
302 eliccre 46790 . . . . . . 7 (((𝑆‘𝑖) ∈ ℝ ∧ (𝑆‘(𝑖 + 1)) ∈ ℝ ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝑥 ∈ ℝ)
303299, 300, 301, 302syl3anc 1399 . . . . . 6 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝑥 ∈ ℝ)
304298, 303ffvelcdmd 7117 . . . . 5 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝐹‘𝑥) ∈ ℂ)
305120, 121, 297, 304ibliooicc 47254 . . . 4 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ (𝐹‘𝑥)) ∈ 𝐿1)
30615, 20, 94, 110, 119, 305itgspltprt 47262 . . 3 (𝜑 → ∫((𝑆‘0)[,](𝑆‘𝑀))(𝐹‘𝑥) d𝑥 = Σ𝑖 ∈ (0..^𝑀)∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥)
307 iftrue 4491 . . . . . . . . . . . 12 (𝑥 = (𝑆‘𝑖) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) = 𝑅)
308307adantl 487 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) = 𝑅)
309 fourierdlem81.g . . . . . . . . . . . . . . 15 𝐺 = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))))
310 iftrue 4491 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑄‘𝑖) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = 𝑅)
311 iftrue 4491 . . . . . . . . . . . . . . . . . . 19 (𝑥 = (𝑄‘𝑖) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))) = 𝑅)
312310, 311eqtr4d 2801 . . . . . . . . . . . . . . . . . 18 (𝑥 = (𝑄‘𝑖) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
313312adantl 487 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ 𝑥 = (𝑄‘𝑖)) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
314 iffalse 4494 . . . . . . . . . . . . . . . . . . . . 21 (¬ 𝑥 = (𝑄‘𝑖) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)))
315314adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑥 = (𝑄‘𝑖) ∧ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)))
316 iftrue 4491 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 = (𝑄‘(𝑖 + 1)) → if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)) = 𝐿)
317316adantl 487 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑥 = (𝑄‘𝑖) ∧ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)) = 𝐿)
318 iffalse 4494 . . . . . . . . . . . . . . . . . . . . . 22 (¬ 𝑥 = (𝑄‘𝑖) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))
319318adantr 486 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑥 = (𝑄‘𝑖) ∧ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))
320 iftrue 4491 . . . . . . . . . . . . . . . . . . . . . 22 (𝑥 = (𝑄‘(𝑖 + 1)) → if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) = 𝐿)
321320adantl 487 . . . . . . . . . . . . . . . . . . . . 21 ((¬ 𝑥 = (𝑄‘𝑖) ∧ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) = 𝐿)
322319, 321eqtr2d 2799 . . . . . . . . . . . . . . . . . . . 20 ((¬ 𝑥 = (𝑄‘𝑖) ∧ 𝑥 = (𝑄‘(𝑖 + 1))) → 𝐿 = if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
323315, 317, 3223eqtrd 2802 . . . . . . . . . . . . . . . . . . 19 ((¬ 𝑥 = (𝑄‘𝑖) ∧ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
324323adantll 727 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
325314ad2antlr 740 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)))
326 iffalse 4494 . . . . . . . . . . . . . . . . . . . 20 (¬ 𝑥 = (𝑄‘(𝑖 + 1)) → if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥))
327326adantl 487 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)) = (𝐹‘𝑥))
328318ad2antlr 740 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))) = if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))
329 iffalse 4494 . . . . . . . . . . . . . . . . . . . . 21 (¬ 𝑥 = (𝑄‘(𝑖 + 1)) → if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))
330329adantl 487 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))
331182ad3antrrr 743 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) ∈ ℝ*)
332184ad3antrrr 743 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
33360ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → 𝑥 ∈ ℝ)
33442ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) → (𝑄‘𝑖) ∈ ℝ)
33560adantr 486 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) → 𝑥 ∈ ℝ)
336182ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) → (𝑄‘𝑖) ∈ ℝ*)
337184ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
338 simplr 781 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) → 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
339 iccgelb 13573 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ 𝑥)
340336, 337, 338, 339syl3anc 1399 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) → (𝑄‘𝑖) ≤ 𝑥)
341 neqne 2967 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ 𝑥 = (𝑄‘𝑖) → 𝑥 ≠ (𝑄‘𝑖))
342341adantl 487 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) → 𝑥 ≠ (𝑄‘𝑖))
343334, 335, 340, 342leneltd 11503 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) → (𝑄‘𝑖) < 𝑥)
344343adantr 486 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) < 𝑥)
34545ad3antrrr 743 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
346182adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ*)
347184adantr 486 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
348 simpr 490 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
349 iccleub 13572 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑥 ≤ (𝑄‘(𝑖 + 1)))
350346, 347, 348, 349syl3anc 1399 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → 𝑥 ≤ (𝑄‘(𝑖 + 1)))
351350ad2antrr 739 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → 𝑥 ≤ (𝑄‘(𝑖 + 1)))
352 neqne 2967 . . . . . . . . . . . . . . . . . . . . . . . . 25 (¬ 𝑥 = (𝑄‘(𝑖 + 1)) → 𝑥 ≠ (𝑄‘(𝑖 + 1)))
353352necomd 3014 . . . . . . . . . . . . . . . . . . . . . . . 24 (¬ 𝑥 = (𝑄‘(𝑖 + 1)) → (𝑄‘(𝑖 + 1)) ≠ 𝑥)
354353adantl 487 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ 𝑥)
355333, 345, 351, 354leneltd 11503 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → 𝑥 < (𝑄‘(𝑖 + 1)))
356331, 332, 333, 344, 355eliood 46783 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → 𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
357 fvres 6935 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥) = (𝐹‘𝑥))
358356, 357syl 18 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥) = (𝐹‘𝑥))
359328, 330, 3583eqtrrd 2803 . . . . . . . . . . . . . . . . . . 19 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → (𝐹‘𝑥) = if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
360325, 327, 3593eqtrd 2802 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) ∧ ¬ 𝑥 = (𝑄‘(𝑖 + 1))) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
361324, 360pm2.61dan 825 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑄‘𝑖)) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
362313, 361pm2.61dan 825 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))) → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥))) = if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
363362mpteq2dva 5204 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, (𝐹‘𝑥)))) = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))))
364309, 363eqtrid 2810 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺 = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))))
365 eqeq1 2767 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → (𝑥 = (𝑄‘𝑖) ↔ 𝑤 = (𝑄‘𝑖)))
366 eqeq1 2767 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → (𝑥 = (𝑄‘(𝑖 + 1)) ↔ 𝑤 = (𝑄‘(𝑖 + 1))))
367 fveq2 6916 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑤 → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))
368366, 367ifbieq2d 4512 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑤 → if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)) = if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤)))
369365, 368ifbieq2d 4512 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))) = if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))))
370369cbvmptv 5215 . . . . . . . . . . . . . 14 (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))) = (𝑤 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))))
371364, 370eqtrdi 2814 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺 = (𝑤 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤)))))
372371adantr 486 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) → 𝐺 = (𝑤 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤)))))
373 simpr 490 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) ∧ 𝑤 = (𝑥 − 𝑇)) → 𝑤 = (𝑥 − 𝑇))
374 oveq1 7458 . . . . . . . . . . . . . . 15 (𝑥 = (𝑆‘𝑖) → (𝑥 − 𝑇) = ((𝑆‘𝑖) − 𝑇))
375374ad2antlr 740 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) ∧ 𝑤 = (𝑥 − 𝑇)) → (𝑥 − 𝑇) = ((𝑆‘𝑖) − 𝑇))
376227eqcomd 2769 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘𝑖) − 𝑇) = (𝑄‘𝑖))
377376ad2antrr 739 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) ∧ 𝑤 = (𝑥 − 𝑇)) → ((𝑆‘𝑖) − 𝑇) = (𝑄‘𝑖))
378373, 375, 3773eqtrd 2802 . . . . . . . . . . . . 13 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) ∧ 𝑤 = (𝑥 − 𝑇)) → 𝑤 = (𝑄‘𝑖))
379378iftrued 4493 . . . . . . . . . . . 12 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) ∧ 𝑤 = (𝑥 − 𝑇)) → if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))) = 𝑅)
380374adantl 487 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) → (𝑥 − 𝑇) = ((𝑆‘𝑖) − 𝑇))
38142, 45, 29ltled 11497 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ≤ (𝑄‘(𝑖 + 1)))
382 lbicc2 13635 . . . . . . . . . . . . . . . 16 (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝑄‘𝑖) ≤ (𝑄‘(𝑖 + 1))) → (𝑄‘𝑖) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
383182, 184, 381, 382syl3anc 1399 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
384376, 383eqeltrd 2864 . . . . . . . . . . . . . 14 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘𝑖) − 𝑇) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
385384adantr 486 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) → ((𝑆‘𝑖) − 𝑇) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
386380, 385eqeltrd 2864 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) → (𝑥 − 𝑇) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
387 limccl 26250 . . . . . . . . . . . . . 14 ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘𝑖)) ⊆ ℂ
388387, 55sselid 3911 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑅 ∈ ℂ)
389388adantr 486 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) → 𝑅 ∈ ℂ)
390372, 379, 386, 389fvmptd 7032 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) → (𝐺‘(𝑥 − 𝑇)) = 𝑅)
391308, 390eqtr4d 2801 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) = (𝐺‘(𝑥 − 𝑇)))
392391adantlr 728 . . . . . . . . 9 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ 𝑥 = (𝑆‘𝑖)) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) = (𝐺‘(𝑥 − 𝑇)))
393 iffalse 4494 . . . . . . . . . . 11 (¬ 𝑥 = (𝑆‘𝑖) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) = if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)))
394393adantl 487 . . . . . . . . . 10 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) = if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)))
395371adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) → 𝐺 = (𝑤 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤)))))
396 eqeq1 2767 . . . . . . . . . . . . . . . . . 18 (𝑤 = ((𝑆‘(𝑖 + 1)) − 𝑇) → (𝑤 = (𝑄‘𝑖) ↔ ((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘𝑖)))
397 eqeq1 2767 . . . . . . . . . . . . . . . . . . 19 (𝑤 = ((𝑆‘(𝑖 + 1)) − 𝑇) → (𝑤 = (𝑄‘(𝑖 + 1)) ↔ ((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1))))
398 fveq2 6916 . . . . . . . . . . . . . . . . . . 19 (𝑤 = ((𝑆‘(𝑖 + 1)) − 𝑇) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑆‘(𝑖 + 1)) − 𝑇)))
399397, 398ifbieq2d 4512 . . . . . . . . . . . . . . . . . 18 (𝑤 = ((𝑆‘(𝑖 + 1)) − 𝑇) → if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤)) = if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑆‘(𝑖 + 1)) − 𝑇))))
400396, 399ifbieq2d 4512 . . . . . . . . . . . . . . . . 17 (𝑤 = ((𝑆‘(𝑖 + 1)) − 𝑇) → if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))) = if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘𝑖), 𝑅, if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑆‘(𝑖 + 1)) − 𝑇)))))
401400adantl 487 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 = ((𝑆‘(𝑖 + 1)) − 𝑇)) → if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))) = if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘𝑖), 𝑅, if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑆‘(𝑖 + 1)) − 𝑇)))))
402 eqeq1 2767 . . . . . . . . . . . . . . . . . . 19 (((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)) → (((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘𝑖) ↔ (𝑄‘(𝑖 + 1)) = (𝑄‘𝑖)))
403 iftrue 4491 . . . . . . . . . . . . . . . . . . 19 (((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)) → if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑆‘(𝑖 + 1)) − 𝑇))) = 𝐿)
404402, 403ifbieq2d 4512 . . . . . . . . . . . . . . . . . 18 (((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)) → if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘𝑖), 𝑅, if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑆‘(𝑖 + 1)) − 𝑇)))) = if((𝑄‘(𝑖 + 1)) = (𝑄‘𝑖), 𝑅, 𝐿))
405246, 404syl 18 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘𝑖), 𝑅, if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑆‘(𝑖 + 1)) − 𝑇)))) = if((𝑄‘(𝑖 + 1)) = (𝑄‘𝑖), 𝑅, 𝐿))
406405adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 = ((𝑆‘(𝑖 + 1)) − 𝑇)) → if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘𝑖), 𝑅, if(((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘((𝑆‘(𝑖 + 1)) − 𝑇)))) = if((𝑄‘(𝑖 + 1)) = (𝑄‘𝑖), 𝑅, 𝐿))
40742, 29gtned 11484 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ≠ (𝑄‘𝑖))
408407neneqd 2964 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ¬ (𝑄‘(𝑖 + 1)) = (𝑄‘𝑖))
409408iffalsed 4496 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → if((𝑄‘(𝑖 + 1)) = (𝑄‘𝑖), 𝑅, 𝐿) = 𝐿)
410409adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 = ((𝑆‘(𝑖 + 1)) − 𝑇)) → if((𝑄‘(𝑖 + 1)) = (𝑄‘𝑖), 𝑅, 𝐿) = 𝐿)
411401, 406, 4103eqtrd 2802 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑤 = ((𝑆‘(𝑖 + 1)) − 𝑇)) → if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))) = 𝐿)
412411adantlr 728 . . . . . . . . . . . . . 14 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) ∧ 𝑤 = ((𝑆‘(𝑖 + 1)) − 𝑇)) → if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))) = 𝐿)
413 ubicc2 13636 . . . . . . . . . . . . . . . . 17 (((𝑄‘𝑖) ∈ ℝ* ∧ (𝑄‘(𝑖 + 1)) ∈ ℝ* ∧ (𝑄‘𝑖) ≤ (𝑄‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
414182, 184, 381, 413syl3anc 1399 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘(𝑖 + 1)) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
415246, 414eqeltrd 2864 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘(𝑖 + 1)) − 𝑇) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
416415adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) → ((𝑆‘(𝑖 + 1)) − 𝑇) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
417 limccl 26250 . . . . . . . . . . . . . . . 16 ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))) limℂ (𝑄‘(𝑖 + 1))) ⊆ ℂ
418417, 54sselid 3911 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐿 ∈ ℂ)
419418adantr 486 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) → 𝐿 ∈ ℂ)
420395, 412, 416, 419fvmptd 7032 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝐺‘((𝑆‘(𝑖 + 1)) − 𝑇)) = 𝐿)
421 oveq1 7458 . . . . . . . . . . . . . . 15 (𝑥 = (𝑆‘(𝑖 + 1)) → (𝑥 − 𝑇) = ((𝑆‘(𝑖 + 1)) − 𝑇))
422421fveq2d 6920 . . . . . . . . . . . . . 14 (𝑥 = (𝑆‘(𝑖 + 1)) → (𝐺‘(𝑥 − 𝑇)) = (𝐺‘((𝑆‘(𝑖 + 1)) − 𝑇)))
423422adantl 487 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝐺‘(𝑥 − 𝑇)) = (𝐺‘((𝑆‘(𝑖 + 1)) − 𝑇)))
424 iftrue 4491 . . . . . . . . . . . . . 14 (𝑥 = (𝑆‘(𝑖 + 1)) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) = 𝐿)
425424adantl 487 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) = 𝐿)
426420, 423, 4253eqtr4rd 2809 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) = (𝐺‘(𝑥 − 𝑇)))
427426ad4ant14 765 . . . . . . . . . . 11 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) = (𝐺‘(𝑥 − 𝑇)))
428 iffalse 4494 . . . . . . . . . . . . 13 (¬ 𝑥 = (𝑆‘(𝑖 + 1)) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) = ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))
429428adantl 487 . . . . . . . . . . . 12 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) = ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))
430371adantr 486 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝐺 = (𝑤 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤)))))
431430ad2antrr 739 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → 𝐺 = (𝑤 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤)))))
432 eqeq1 2767 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝑥 − 𝑇) → (𝑤 = (𝑄‘𝑖) ↔ (𝑥 − 𝑇) = (𝑄‘𝑖)))
433 eqeq1 2767 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝑥 − 𝑇) → (𝑤 = (𝑄‘(𝑖 + 1)) ↔ (𝑥 − 𝑇) = (𝑄‘(𝑖 + 1))))
434 fveq2 6916 . . . . . . . . . . . . . . . . . . 19 (𝑤 = (𝑥 − 𝑇) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))
435433, 434ifbieq2d 4512 . . . . . . . . . . . . . . . . . 18 (𝑤 = (𝑥 − 𝑇) → if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤)) = if((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))))
436432, 435ifbieq2d 4512 . . . . . . . . . . . . . . . . 17 (𝑤 = (𝑥 − 𝑇) → if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))) = if((𝑥 − 𝑇) = (𝑄‘𝑖), 𝑅, if((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))))
437436adantl 487 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) ∧ 𝑤 = (𝑥 − 𝑇)) → if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))) = if((𝑥 − 𝑇) = (𝑄‘𝑖), 𝑅, if((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))))
438303recnd 11376 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝑥 ∈ ℂ)
439225adantr 486 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝑇 ∈ ℂ)
440438, 439npcand 11712 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → ((𝑥 − 𝑇) + 𝑇) = 𝑥)
441440eqcomd 2769 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝑥 = ((𝑥 − 𝑇) + 𝑇))
442441adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ (𝑥 − 𝑇) = (𝑄‘𝑖)) → 𝑥 = ((𝑥 − 𝑇) + 𝑇))
443 oveq1 7458 . . . . . . . . . . . . . . . . . . . . 21 ((𝑥 − 𝑇) = (𝑄‘𝑖) → ((𝑥 − 𝑇) + 𝑇) = ((𝑄‘𝑖) + 𝑇))
444443adantl 487 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ (𝑥 − 𝑇) = (𝑄‘𝑖)) → ((𝑥 − 𝑇) + 𝑇) = ((𝑄‘𝑖) + 𝑇))
445294ad2antrr 739 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ (𝑥 − 𝑇) = (𝑄‘𝑖)) → ((𝑄‘𝑖) + 𝑇) = (𝑆‘𝑖))
446442, 444, 4453eqtrd 2802 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ (𝑥 − 𝑇) = (𝑄‘𝑖)) → 𝑥 = (𝑆‘𝑖))
447446stoic1a 1805 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → ¬ (𝑥 − 𝑇) = (𝑄‘𝑖))
448447iffalsed 4496 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → if((𝑥 − 𝑇) = (𝑄‘𝑖), 𝑅, if((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))) = if((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))))
449448ad2antrr 739 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) ∧ 𝑤 = (𝑥 − 𝑇)) → if((𝑥 − 𝑇) = (𝑄‘𝑖), 𝑅, if((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))) = if((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))))
450441adantr 486 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ (𝑥 − 𝑇) = (𝑄‘(𝑖 + 1))) → 𝑥 = ((𝑥 − 𝑇) + 𝑇))
451 oveq1 7458 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)) → ((𝑥 − 𝑇) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
452451adantl 487 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ (𝑥 − 𝑇) = (𝑄‘(𝑖 + 1))) → ((𝑥 − 𝑇) + 𝑇) = ((𝑄‘(𝑖 + 1)) + 𝑇))
453290ad2antrr 739 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ (𝑥 − 𝑇) = (𝑄‘(𝑖 + 1))) → ((𝑄‘(𝑖 + 1)) + 𝑇) = (𝑆‘(𝑖 + 1)))
454450, 452, 4533eqtrd 2802 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ (𝑥 − 𝑇) = (𝑄‘(𝑖 + 1))) → 𝑥 = (𝑆‘(𝑖 + 1)))
455454stoic1a 1805 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → ¬ (𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)))
456455iffalsed 4496 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → if((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))
457456adantlr 728 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → if((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))
458457adantr 486 . . . . . . . . . . . . . . . 16 ((((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) ∧ 𝑤 = (𝑥 − 𝑇)) → if((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))
459437, 449, 4583eqtrd 2802 . . . . . . . . . . . . . . 15 ((((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) ∧ 𝑤 = (𝑥 − 𝑇)) → if(𝑤 = (𝑄‘𝑖), 𝑅, if(𝑤 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑤))) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))
46042adantr 486 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑄‘𝑖) ∈ ℝ)
46145adantr 486 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
46275ad2antrr 739 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝑇 ∈ ℝ)
463303, 462resubcld 11783 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) ∈ ℝ)
464227adantr 486 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑄‘𝑖) = ((𝑆‘𝑖) − 𝑇))
465206adantr 486 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑆‘𝑖) ∈ ℝ*)
466208adantr 486 . . . . . . . . . . . . . . . . . . . 20 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑆‘(𝑖 + 1)) ∈ ℝ*)
467 iccgelb 13573 . . . . . . . . . . . . . . . . . . . 20 (((𝑆‘𝑖) ∈ ℝ* ∧ (𝑆‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑆‘𝑖) ≤ 𝑥)
468465, 466, 301, 467syl3anc 1399 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑆‘𝑖) ≤ 𝑥)
469299, 303, 462, 468lesub1dd 11972 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → ((𝑆‘𝑖) − 𝑇) ≤ (𝑥 − 𝑇))
470464, 469eqbrtrd 5133 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑄‘𝑖) ≤ (𝑥 − 𝑇))
471 iccleub 13572 . . . . . . . . . . . . . . . . . . . 20 (((𝑆‘𝑖) ∈ ℝ* ∧ (𝑆‘(𝑖 + 1)) ∈ ℝ* ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝑥 ≤ (𝑆‘(𝑖 + 1)))
472465, 466, 301, 471syl3anc 1399 . . . . . . . . . . . . . . . . . . 19 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝑥 ≤ (𝑆‘(𝑖 + 1)))
473303, 300, 462, 472lesub1dd 11972 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) ≤ ((𝑆‘(𝑖 + 1)) − 𝑇))
474246adantr 486 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → ((𝑆‘(𝑖 + 1)) − 𝑇) = (𝑄‘(𝑖 + 1)))
475473, 474breqtrd 5137 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) ≤ (𝑄‘(𝑖 + 1)))
476460, 461, 463, 470, 475eliccd 46789 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
477476ad2antrr 739 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑥 − 𝑇) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
478135, 271fssresd 6779 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
479478ad3antrrr 743 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))):((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1)))⟶ℂ)
480182ad3antrrr 743 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑄‘𝑖) ∈ ℝ*)
481184ad3antrrr 743 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ*)
482303ad2antrr 739 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → 𝑥 ∈ ℝ)
48395ad3antrrr 743 . . . . . . . . . . . . . . . . . 18 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → 𝑇 ∈ ℝ)
484482, 483resubcld 11783 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑥 − 𝑇) ∈ ℝ)
48542ad2antrr 739 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → (𝑄‘𝑖) ∈ ℝ)
486463adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → (𝑥 − 𝑇) ∈ ℝ)
487470adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → (𝑄‘𝑖) ≤ (𝑥 − 𝑇))
488447neqned 2966 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → (𝑥 − 𝑇) ≠ (𝑄‘𝑖))
489485, 486, 487, 488leneltd 11503 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → (𝑄‘𝑖) < (𝑥 − 𝑇))
490489adantr 486 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑄‘𝑖) < (𝑥 − 𝑇))
491463adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑥 − 𝑇) ∈ ℝ)
49245ad2antrr 739 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
493475adantr 486 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑥 − 𝑇) ≤ (𝑄‘(𝑖 + 1)))
494 eqcom 2770 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)) ↔ (𝑄‘(𝑖 + 1)) = (𝑥 − 𝑇))
495454ex 418 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → ((𝑥 − 𝑇) = (𝑄‘(𝑖 + 1)) → 𝑥 = (𝑆‘(𝑖 + 1))))
496494, 495biimtrrid 246 . . . . . . . . . . . . . . . . . . . . 21 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → ((𝑄‘(𝑖 + 1)) = (𝑥 − 𝑇) → 𝑥 = (𝑆‘(𝑖 + 1))))
497496con3dimp 414 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → ¬ (𝑄‘(𝑖 + 1)) = (𝑥 − 𝑇))
498497neqned 2966 . . . . . . . . . . . . . . . . . . 19 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑄‘(𝑖 + 1)) ≠ (𝑥 − 𝑇))
499491, 492, 493, 498leneltd 11503 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑥 − 𝑇) < (𝑄‘(𝑖 + 1)))
500499adantlr 728 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑥 − 𝑇) < (𝑄‘(𝑖 + 1)))
501480, 481, 484, 490, 500eliood 46783 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑥 − 𝑇) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))
502479, 501ffvelcdmd 7117 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)) ∈ ℂ)
503431, 459, 477, 502fvmptd 7032 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝐺‘(𝑥 − 𝑇)) = ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)))
504 fvres 6935 . . . . . . . . . . . . . . 15 ((𝑥 − 𝑇) ∈ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)) = (𝐹‘(𝑥 − 𝑇)))
505501, 504syl 18 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘(𝑥 − 𝑇)) = (𝐹‘(𝑥 − 𝑇)))
506503, 505eqtrd 2798 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝐺‘(𝑥 − 𝑇)) = (𝐹‘(𝑥 − 𝑇)))
507465ad2antrr 739 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑆‘𝑖) ∈ ℝ*)
508466ad2antrr 739 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑆‘(𝑖 + 1)) ∈ ℝ*)
509120ad2antrr 739 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → (𝑆‘𝑖) ∈ ℝ)
510303adantr 486 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → 𝑥 ∈ ℝ)
511468adantr 486 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → (𝑆‘𝑖) ≤ 𝑥)
512 neqne 2967 . . . . . . . . . . . . . . . . . . 19 (¬ 𝑥 = (𝑆‘𝑖) → 𝑥 ≠ (𝑆‘𝑖))
513512adantl 487 . . . . . . . . . . . . . . . . . 18 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → 𝑥 ≠ (𝑆‘𝑖))
514509, 510, 511, 513leneltd 11503 . . . . . . . . . . . . . . . . 17 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → (𝑆‘𝑖) < 𝑥)
515514adantr 486 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑆‘𝑖) < 𝑥)
516300ad2antrr 739 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑆‘(𝑖 + 1)) ∈ ℝ)
517472ad2antrr 739 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → 𝑥 ≤ (𝑆‘(𝑖 + 1)))
518 neqne 2967 . . . . . . . . . . . . . . . . . . 19 (¬ 𝑥 = (𝑆‘(𝑖 + 1)) → 𝑥 ≠ (𝑆‘(𝑖 + 1)))
519518necomd 3014 . . . . . . . . . . . . . . . . . 18 (¬ 𝑥 = (𝑆‘(𝑖 + 1)) → (𝑆‘(𝑖 + 1)) ≠ 𝑥)
520519adantl 487 . . . . . . . . . . . . . . . . 17 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑆‘(𝑖 + 1)) ≠ 𝑥)
521482, 516, 517, 520leneltd 11503 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → 𝑥 < (𝑆‘(𝑖 + 1)))
522507, 508, 482, 515, 521eliood 46783 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))
523 fvres 6935 . . . . . . . . . . . . . . 15 (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥) = (𝐹‘𝑥))
524522, 523syl 18 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥) = (𝐹‘𝑥))
525440fveq2d 6920 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘𝑥))
526525eqcomd 2769 . . . . . . . . . . . . . . 15 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝐹‘𝑥) = (𝐹‘((𝑥 − 𝑇) + 𝑇)))
527526ad2antrr 739 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝐹‘𝑥) = (𝐹‘((𝑥 − 𝑇) + 𝑇)))
528438, 439subcld 11708 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) ∈ ℂ)
529 elex 3475 . . . . . . . . . . . . . . . . 17 ((𝑥 − 𝑇) ∈ ℂ → (𝑥 − 𝑇) ∈ V)
530528, 529syl 18 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) ∈ V)
531530ad2antrr 739 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑥 − 𝑇) ∈ V)
532 simp-4l 795 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → 𝜑)
533153adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐴 ∈ ℝ*)
534155adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐵 ∈ ℝ*)
535157adantr 486 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑄:(0...𝑀)⟶(𝐴[,]𝐵))
536 simpr 490 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑖 ∈ (0..^𝑀))
537533, 534, 535, 536fourierdlem8 47398 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
538537adantr 486 . . . . . . . . . . . . . . . . . 18 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ (𝐴[,]𝐵))
539538, 476sseldd 3914 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵))
540539ad2antrr 739 . . . . . . . . . . . . . . . 16 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝑥 − 𝑇) ∈ (𝐴[,]𝐵))
541532, 540jca 521 . . . . . . . . . . . . . . 15 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝜑 ∧ (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)))
542 eleq1 2852 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑥 − 𝑇) → (𝑦 ∈ (𝐴[,]𝐵) ↔ (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)))
543542anbi2d 642 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 − 𝑇) → ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ (𝑥 − 𝑇) ∈ (𝐴[,]𝐵))))
544 oveq1 7458 . . . . . . . . . . . . . . . . . . 19 (𝑦 = (𝑥 − 𝑇) → (𝑦 + 𝑇) = ((𝑥 − 𝑇) + 𝑇))
545544fveq2d 6920 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑥 − 𝑇) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘((𝑥 − 𝑇) + 𝑇)))
546 fveq2 6916 . . . . . . . . . . . . . . . . . 18 (𝑦 = (𝑥 − 𝑇) → (𝐹‘𝑦) = (𝐹‘(𝑥 − 𝑇)))
547545, 546eqeq12d 2779 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑥 − 𝑇) → ((𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦) ↔ (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘(𝑥 − 𝑇))))
548543, 547imbi12d 347 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑥 − 𝑇) → (((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)) ↔ ((𝜑 ∧ (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘(𝑥 − 𝑇)))))
549 eleq1 2852 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝑥 ∈ (𝐴[,]𝐵) ↔ 𝑦 ∈ (𝐴[,]𝐵)))
550549anbi2d 642 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) ↔ (𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵))))
551 oveq1 7458 . . . . . . . . . . . . . . . . . . . 20 (𝑥 = 𝑦 → (𝑥 + 𝑇) = (𝑦 + 𝑇))
552551fveq2d 6920 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘(𝑦 + 𝑇)))
553 fveq2 6916 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦))
554552, 553eqeq12d 2779 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑦 → ((𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥) ↔ (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦)))
555550, 554imbi12d 347 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑥 + 𝑇)) = (𝐹‘𝑥)) ↔ ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))))
556555, 164chvarvv 2024 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ 𝑦 ∈ (𝐴[,]𝐵)) → (𝐹‘(𝑦 + 𝑇)) = (𝐹‘𝑦))
557548, 556vtoclg 3521 . . . . . . . . . . . . . . 15 ((𝑥 − 𝑇) ∈ V → ((𝜑 ∧ (𝑥 − 𝑇) ∈ (𝐴[,]𝐵)) → (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘(𝑥 − 𝑇))))
558531, 541, 557sylc 66 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝐹‘((𝑥 − 𝑇) + 𝑇)) = (𝐹‘(𝑥 − 𝑇)))
559524, 527, 5583eqtrd 2802 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥) = (𝐹‘(𝑥 − 𝑇)))
560506, 559eqtr4d 2801 . . . . . . . . . . . 12 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝐺‘(𝑥 − 𝑇)) = ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))
561429, 560eqtr4d 2801 . . . . . . . . . . 11 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) = (𝐺‘(𝑥 − 𝑇)))
562427, 561pm2.61dan 825 . . . . . . . . . 10 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) = (𝐺‘(𝑥 − 𝑇)))
563394, 562eqtrd 2798 . . . . . . . . 9 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) = (𝐺‘(𝑥 − 𝑇)))
564392, 563pm2.61dan 825 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) = (𝐺‘(𝑥 − 𝑇)))
565308, 389eqeltrd 2864 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘𝑖)) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) ∈ ℂ)
566565adantlr 728 . . . . . . . . . 10 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ 𝑥 = (𝑆‘𝑖)) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) ∈ ℂ)
567425, 419eqeltrd 2864 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) ∈ ℂ)
568567ad4ant14 765 . . . . . . . . . . . 12 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ 𝑥 = (𝑆‘(𝑖 + 1))) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) ∈ ℂ)
569263, 265fssresd 6779 . . . . . . . . . . . . . . 15 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))):((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))⟶ℂ)
570569ad3antrrr 743 . . . . . . . . . . . . . 14 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → (𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))):((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))⟶ℂ)
571570, 522ffvelcdmd 7117 . . . . . . . . . . . . 13 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥) ∈ ℂ)
572429, 571eqeltrd 2864 . . . . . . . . . . . 12 (((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) ∧ ¬ 𝑥 = (𝑆‘(𝑖 + 1))) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) ∈ ℂ)
573568, 572pm2.61dan 825 . . . . . . . . . . 11 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) ∈ ℂ)
574394, 573eqeltrd 2864 . . . . . . . . . 10 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) ∧ ¬ 𝑥 = (𝑆‘𝑖)) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) ∈ ℂ)
575566, 574pm2.61dan 825 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) ∈ ℂ)
576 eqid 2763 . . . . . . . . . 10 (𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)))) = (𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))
577576fvmpt2 7036 . . . . . . . . 9 ((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ∧ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) ∈ ℂ) → ((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥) = if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))
578301, 575, 577syl2anc 596 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → ((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥) = if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))
579 nfv 1949 . . . . . . . . . . . . . 14 Ⅎ𝑥(𝜑 ∧ 𝑖 ∈ (0..^𝑀))
580 eqid 2763 . . . . . . . . . . . . . 14 (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))) = (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥))))
581579, 580, 42, 45, 53, 54, 55cncfiooicc 47177 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑥 ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ↦ if(𝑥 = (𝑄‘𝑖), 𝑅, if(𝑥 = (𝑄‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑄‘𝑖)(,)(𝑄‘(𝑖 + 1))))‘𝑥)))) ∈ (((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))–cn→ℂ))
582364, 581eqeltrd 2864 . . . . . . . . . . . 12 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺 ∈ (((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))–cn→ℂ))
583 cncff 25269 . . . . . . . . . . . 12 (𝐺 ∈ (((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))–cn→ℂ) → 𝐺:((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))⟶ℂ)
584582, 583syl 18 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝐺:((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))⟶ℂ)
585584adantr 486 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → 𝐺:((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))⟶ℂ)
586585, 476ffvelcdmd 7117 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝐺‘(𝑥 − 𝑇)) ∈ ℂ)
587 fourierdlem81.h . . . . . . . . . 10 𝐻 = (𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ (𝐺‘(𝑥 − 𝑇)))
588587fvmpt2 7036 . . . . . . . . 9 ((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ∧ (𝐺‘(𝑥 − 𝑇)) ∈ ℂ) → (𝐻‘𝑥) = (𝐺‘(𝑥 − 𝑇)))
589301, 586, 588syl2anc 596 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝐻‘𝑥) = (𝐺‘(𝑥 − 𝑇)))
590564, 578, 5893eqtr4rd 2809 . . . . . . 7 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → (𝐻‘𝑥) = ((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥))
591590itgeq2dv 26157 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))(𝐻‘𝑥) d𝑥 = ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥) d𝑥)
592 ioossicc 13604 . . . . . . . . . . . 12 ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) ⊆ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))
593592sseli 3909 . . . . . . . . . . 11 (𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))) → 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))))
594593adantl 487 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))))
595593, 575sylan2 605 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) ∈ ℂ)
596594, 595, 577syl2anc 596 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → ((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥) = if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))
597229, 237gtned 11484 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 ≠ (𝑆‘𝑖))
598597neneqd 2964 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → ¬ 𝑥 = (𝑆‘𝑖))
599598iffalsed 4496 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))) = if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)))
600230, 241ltned 11485 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → 𝑥 ≠ (𝑆‘(𝑖 + 1)))
601600neneqd 2964 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → ¬ 𝑥 = (𝑆‘(𝑖 + 1)))
602601iffalsed 4496 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) = ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))
603523adantl 487 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥) = (𝐹‘𝑥))
604602, 603eqtrd 2798 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥)) = (𝐹‘𝑥))
605596, 599, 6043eqtrd 2802 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))) → ((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥) = (𝐹‘𝑥))
606605itgeq2dv 26157 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥) d𝑥 = ∫((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥)
607578, 575eqeltrd 2864 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))) → ((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥) ∈ ℂ)
608120, 121, 607itgioo 26191 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥) d𝑥 = ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥) d𝑥)
609120, 121, 304itgioo 26191 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥 = ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥)
610606, 608, 6093eqtr3d 2806 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))((𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) ↦ if(𝑥 = (𝑆‘𝑖), 𝑅, if(𝑥 = (𝑆‘(𝑖 + 1)), 𝐿, ((𝐹 ↾ ((𝑆‘𝑖)(,)(𝑆‘(𝑖 + 1))))‘𝑥))))‘𝑥) d𝑥 = ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥)
611591, 610eqtr2d 2799 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥 = ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))(𝐻‘𝑥) d𝑥)
61299, 109oveq12d 7469 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))) = (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)))
613612itgeq1d 47240 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))(𝐻‘𝑥) d𝑥 = ∫(((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))(𝐻‘𝑥) d𝑥)
614 simpr 490 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)))
615612eqcomd 2769 . . . . . . . . . . 11 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)) = ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))))
616615adantr 486 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)) = ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))))
617614, 616eleqtrd 2866 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1))))
618584adantr 486 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝐺:((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))⟶ℂ)
61942adantr 486 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘𝑖) ∈ ℝ)
62045adantr 486 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘(𝑖 + 1)) ∈ ℝ)
62197adantr 486 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘𝑖) + 𝑇) ∈ ℝ)
622108adantr 486 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ)
623 eliccre 46790 . . . . . . . . . . . . 13 ((((𝑄‘𝑖) + 𝑇) ∈ ℝ ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
624621, 622, 614, 623syl3anc 1399 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ∈ ℝ)
62575ad2antrr 739 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑇 ∈ ℝ)
626624, 625resubcld 11783 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) ∈ ℝ)
627226eqcomd 2769 . . . . . . . . . . . . 13 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝑄‘𝑖) = (((𝑄‘𝑖) + 𝑇) − 𝑇))
628627adantr 486 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘𝑖) = (((𝑄‘𝑖) + 𝑇) − 𝑇))
629621rexrd 11398 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘𝑖) + 𝑇) ∈ ℝ*)
630622rexrd 11398 . . . . . . . . . . . . . 14 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ*)
631 iccgelb 13573 . . . . . . . . . . . . . 14 ((((𝑄‘𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ* ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘𝑖) + 𝑇) ≤ 𝑥)
632629, 630, 614, 631syl3anc 1399 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑄‘𝑖) + 𝑇) ≤ 𝑥)
633621, 624, 625, 632lesub1dd 11972 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄‘𝑖) + 𝑇) − 𝑇) ≤ (𝑥 − 𝑇))
634628, 633eqbrtrd 5133 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑄‘𝑖) ≤ (𝑥 − 𝑇))
635 iccleub 13572 . . . . . . . . . . . . . 14 ((((𝑄‘𝑖) + 𝑇) ∈ ℝ* ∧ ((𝑄‘(𝑖 + 1)) + 𝑇) ∈ ℝ* ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ≤ ((𝑄‘(𝑖 + 1)) + 𝑇))
636629, 630, 614, 635syl3anc 1399 . . . . . . . . . . . . 13 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → 𝑥 ≤ ((𝑄‘(𝑖 + 1)) + 𝑇))
637624, 622, 625, 636lesub1dd 11972 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) ≤ (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇))
638245adantr 486 . . . . . . . . . . . 12 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (((𝑄‘(𝑖 + 1)) + 𝑇) − 𝑇) = (𝑄‘(𝑖 + 1)))
639637, 638breqtrd 5137 . . . . . . . . . . 11 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) ≤ (𝑄‘(𝑖 + 1)))
640619, 620, 626, 634, 639eliccd 46789 . . . . . . . . . 10 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑥 − 𝑇) ∈ ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))))
641618, 640ffvelcdmd 7117 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐺‘(𝑥 − 𝑇)) ∈ ℂ)
642617, 641, 588syl2anc 596 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐻‘𝑥) = (𝐺‘(𝑥 − 𝑇)))
643 eqidd 2764 . . . . . . . . 9 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝑦 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)) ↦ (𝐺‘(𝑦 − 𝑇))) = (𝑦 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)) ↦ (𝐺‘(𝑦 − 𝑇))))
644 oveq1 7458 . . . . . . . . . . 11 (𝑦 = 𝑥 → (𝑦 − 𝑇) = (𝑥 − 𝑇))
645644fveq2d 6920 . . . . . . . . . 10 (𝑦 = 𝑥 → (𝐺‘(𝑦 − 𝑇)) = (𝐺‘(𝑥 − 𝑇)))
646645adantl 487 . . . . . . . . 9 ((((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) ∧ 𝑦 = 𝑥) → (𝐺‘(𝑦 − 𝑇)) = (𝐺‘(𝑥 − 𝑇)))
647643, 646, 614, 641fvmptd 7032 . . . . . . . 8 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → ((𝑦 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)) ↦ (𝐺‘(𝑦 − 𝑇)))‘𝑥) = (𝐺‘(𝑥 − 𝑇)))
648642, 647eqtr4d 2801 . . . . . . 7 (((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) ∧ 𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))) → (𝐻‘𝑥) = ((𝑦 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)) ↦ (𝐺‘(𝑦 − 𝑇)))‘𝑥))
649648itgeq2dv 26157 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫(((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))(𝐻‘𝑥) d𝑥 = ∫(((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))((𝑦 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)) ↦ (𝐺‘(𝑦 − 𝑇)))‘𝑥) d𝑥)
65074adantr 486 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → 𝑇 ∈ ℝ+)
651645cbvmptv 5215 . . . . . . 7 (𝑦 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)) ↦ (𝐺‘(𝑦 − 𝑇))) = (𝑥 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)) ↦ (𝐺‘(𝑥 − 𝑇)))
65242, 45, 381, 582, 650, 651itgiccshift 47263 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫(((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇))((𝑦 ∈ (((𝑄‘𝑖) + 𝑇)[,]((𝑄‘(𝑖 + 1)) + 𝑇)) ↦ (𝐺‘(𝑦 − 𝑇)))‘𝑥) d𝑥 = ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐺‘𝑥) d𝑥)
653613, 649, 6523eqtrd 2802 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))(𝐻‘𝑥) d𝑥 = ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐺‘𝑥) d𝑥)
654132adantr 486 . . . . . . . 8 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → dom 𝐹 = ℝ)
65559, 654sseqtrrd 3950 . . . . . . 7 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1))) ⊆ dom 𝐹)
65642, 45, 135, 53, 655, 55, 54, 309itgioocnicc 47260 . . . . . 6 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → (𝐺 ∈ 𝐿1 ∧ ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐺‘𝑥) d𝑥 = ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥))
657656simprd 501 . . . . 5 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐺‘𝑥) d𝑥 = ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥)
658611, 653, 6573eqtrd 2802 . . . 4 ((𝜑 ∧ 𝑖 ∈ (0..^𝑀)) → ∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥 = ∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥)
659658sumeq2dv 15913 . . 3 (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑆‘𝑖)[,](𝑆‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥 = Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥)
66090, 306, 6593eqtrrd 2803 . 2 (𝜑 → Σ𝑖 ∈ (0..^𝑀)∫((𝑄‘𝑖)[,](𝑄‘(𝑖 + 1)))(𝐹‘𝑥) d𝑥 = ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥)
66114, 63, 6603eqtrrd 2803 1 (𝜑 → ∫((𝐴 + 𝑇)[,](𝐵 + 𝑇))(𝐹‘𝑥) d𝑥 = ∫(𝐴[,]𝐵)(𝐹‘𝑥) d𝑥)
Colors of variables:    wff setvar class
This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ⊆ wss 3900  ifcif 4485   class class class wbr 5108   ↦ cmpt 5192  dom cdm 5658   ↾ cres 5660  ⟶wf 6562  ‘cfv 6566  (class class class)co 7451   ↑m cmap 8885  ℂcc 11237  ℝcr 11238  0cc0 11239  1c1 11240   + caddc 11242  ℝ*cxr 11381   < clt 11382   ≤ cle 11383   − cmin 11580  ℕcn 12375  ℕ0cn0 12646  ℤ≥cuz 13005  ℝ+crp 13160  (,)cioo 13516  [,]cicc 13519  ...cfz 13679  ..^cfzo 13828  Σcsu 15897  –cn→ccncf 25252  𝐿1cibl 25993  ∫citg 25994   limℂ climc 26237
This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5238  ax-sep 5255  ax-nul 5266  ax-pow 5334  ax-pr 5398  ax-un 7783  ax-inf2 9679  ax-cc 10552  ax-cnex 11295  ax-resscn 11296  ax-1cn 11297  ax-icn 11298  ax-addcl 11299  ax-addrcl 11300  ax-mulcl 11301  ax-mulrcl 11302  ax-mulcom 11303  ax-addass 11304  ax-mulass 11305  ax-distr 11306  ax-i2m1 11307  ax-1ne0 11308  ax-1rid 11309  ax-rnegex 11310  ax-rrecex 11311  ax-cnre 11312  ax-pre-lttri 11313  ax-pre-lttrn 11314  ax-pre-ltadd 11315  ax-pre-mulgt0 11316  ax-pre-sup 11317  ax-addf 11318
This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3066  df-ral 3081  df-rex 3091  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-symdif 4201  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-tp 4593  df-op 4841  df-uni 4873  df-int 4913  df-iun 4958  df-iin 4959  df-disj 5076  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-se 5612  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-isom 6575  df-riota 7408  df-ov 7454  df-oprab 7455  df-mpo 7456  df-of 7725  df-ofr 7726  df-om 7912  df-1st 8035  df-2nd 8036  df-supp 8215  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-1o 8514  df-2o 8515  df-oadd 8518  df-omul 8519  df-er 8755  df-map 8887  df-pm 8888  df-ixp 8964  df-en 9012  df-dom 9013  df-sdom 9014  df-fin 9015  df-fsupp 9392  df-fi 9440  df-sup 9471  df-inf 9472  df-oi 9541  df-dju 10019  df-card 10057  df-acn 10060  df-pnf 11384  df-mnf 11385  df-xr 11386  df-ltxr 11387  df-le 11388  df-sub 11582  df-neg 11583  df-div 12014  df-nn 12376  df-2 12445  df-3 12446  df-4 12447  df-5 12448  df-6 12449  df-7 12450  df-8 12451  df-9 12452  df-n0 12647  df-z 12734  df-dec 12855  df-uz 13006  df-q 13116  df-rp 13161  df-xneg 13281  df-xadd 13282  df-xmul 13283  df-ioo 13520  df-ioc 13521  df-ico 13522  df-icc 13523  df-fz 13680  df-fzo 13829  df-fl 13972  df-mod 14050  df-seq 14185  df-exp 14245  df-hash 14516  df-cj 15309  df-re 15310  df-im 15311  df-sqrt 15445  df-abs 15446  df-limsup 15682  df-clim 15699  df-rlim 15700  df-sum 15898  df-struct 17369  df-sets 17386  df-slot 17404  df-ndx 17416  df-base 17432  df-ress 17453  df-plusg 17486  df-mulr 17487  df-starv 17488  df-sca 17489  df-vsca 17490  df-ip 17491  df-tset 17492  df-ple 17493  df-ds 17495  df-unif 17496  df-hom 17497  df-cco 17498  df-euf 17499  df-rest 17643  df-topn 17644  df-0g 17662  df-gsum 17663  df-topgen 17664  df-pt 17665  df-prds 17668  df-xrs 17724  df-qtop 17729  df-imas 17730  df-xps 17732  df-mre 17806  df-mrc 17807  df-acs 17809  df-mgm 18866  df-sgrp 18958  df-mnd 18974  df-submnd 19029  df-mulg 19328  df-cntz 19582  df-cmn 20047  df-psmet 21721  df-xmet 21722  df-met 21723  df-bl 21724  df-mopn 21725  df-fbas 21726  df-fg 21727  df-cnfld 21730  df-top 23267  df-topon 23284  df-topsp 23306  df-bases 23319  df-cld 23392  df-ntr 23393  df-cls 23394  df-nei 23471  df-lp 23509  df-perf 23510  df-cn 23600  df-cnp 23601  df-haus 23688  df-cmp 23760  df-tx 23936  df-hmeo 24129  df-fil 24220  df-fm 24312  df-flim 24313  df-flf 24314  df-xms 24694  df-ms 24695  df-tms 24696  df-cncf 25254  df-ovol 25840  df-vol 25841  df-mbf 25995  df-itg1 25996  df-itg2 25997  df-ibl 25998  df-itg 25999  df-0p 26046  df-ditg 26222  df-limc 26241  df-dv 26242
This theorem is used by:  fourierdlem92  47481
  Copyright terms: Public domain W3C validator