Metamath Proof Explorer


Theorem fourierdlem81

Description: The integral of a piecewise continuous periodic function F is unchanged if the domain is shifted by its period T . In this lemma, T is assumed to be strictly positive. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses 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 fourierdlem81 ( 𝜑 → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹𝑥 ) d 𝑥 )

Proof

Step Hyp Ref Expression
1 fourierdlem81.a ( 𝜑𝐴 ∈ ℝ )
2 fourierdlem81.b ( 𝜑𝐵 ∈ ℝ )
3 fourierdlem81.p 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
4 fourierdlem81.m ( 𝜑𝑀 ∈ ℕ )
5 fourierdlem81.t ( 𝜑𝑇 ∈ ℝ+ )
6 fourierdlem81.q ( 𝜑𝑄 ∈ ( 𝑃𝑀 ) )
7 fourierdlem81.fper ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
8 fourierdlem81.s 𝑆 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑖 ) + 𝑇 ) )
9 fourierdlem81.f ( 𝜑𝐹 : ℝ ⟶ ℂ )
10 fourierdlem81.cncf ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
11 fourierdlem81.r ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) )
12 fourierdlem81.l ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
13 fourierdlem81.g 𝐺 = ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) )
14 fourierdlem81.h 𝐻 = ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
15 3 fourierdlem2 ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
16 4 15 syl ( 𝜑 → ( 𝑄 ∈ ( 𝑃𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
17 6 16 mpbid ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
18 17 simprd ( 𝜑 → ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
19 18 simpld ( 𝜑 → ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄𝑀 ) = 𝐵 ) )
20 19 simpld ( 𝜑 → ( 𝑄 ‘ 0 ) = 𝐴 )
21 20 eqcomd ( 𝜑𝐴 = ( 𝑄 ‘ 0 ) )
22 19 simprd ( 𝜑 → ( 𝑄𝑀 ) = 𝐵 )
23 22 eqcomd ( 𝜑𝐵 = ( 𝑄𝑀 ) )
24 21 23 oveq12d ( 𝜑 → ( 𝐴 [,] 𝐵 ) = ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) )
25 24 itgeq1d ( 𝜑 → ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ( 𝐹𝑥 ) d 𝑥 )
26 0zd ( 𝜑 → 0 ∈ ℤ )
27 nnuz ℕ = ( ℤ ‘ 1 )
28 0p1e1 ( 0 + 1 ) = 1
29 28 fveq2i ( ℤ ‘ ( 0 + 1 ) ) = ( ℤ ‘ 1 )
30 27 29 eqtr4i ℕ = ( ℤ ‘ ( 0 + 1 ) )
31 4 30 eleqtrdi ( 𝜑𝑀 ∈ ( ℤ ‘ ( 0 + 1 ) ) )
32 17 simpld ( 𝜑𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
33 reex ℝ ∈ V
34 33 a1i ( 𝜑 → ℝ ∈ V )
35 ovex ( 0 ... 𝑀 ) ∈ V
36 35 a1i ( 𝜑 → ( 0 ... 𝑀 ) ∈ V )
37 34 36 elmapd ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ↔ 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ ) )
38 32 37 mpbid ( 𝜑𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
39 18 simprd ( 𝜑 → ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
40 39 r19.21bi ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
41 9 adantr ( ( 𝜑𝑥 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ) → 𝐹 : ℝ ⟶ ℂ )
42 20 1 eqeltrd ( 𝜑 → ( 𝑄 ‘ 0 ) ∈ ℝ )
43 22 2 eqeltrd ( 𝜑 → ( 𝑄𝑀 ) ∈ ℝ )
44 42 43 iccssred ( 𝜑 → ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ⊆ ℝ )
45 44 sselda ( ( 𝜑𝑥 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ) → 𝑥 ∈ ℝ )
46 41 45 ffvelrnd ( ( 𝜑𝑥 ∈ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ) → ( 𝐹𝑥 ) ∈ ℂ )
47 38 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
48 elfzofz ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
49 48 adantl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
50 47 49 ffvelrnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℝ )
51 fzofzp1 ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
52 51 adantl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
53 47 52 ffvelrnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
54 9 feqmptd ( 𝜑𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝐹𝑥 ) ) )
55 54 reseq1d ( 𝜑 → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑥 ∈ ℝ ↦ ( 𝐹𝑥 ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
56 55 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( ( 𝑥 ∈ ℝ ↦ ( 𝐹𝑥 ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
57 ioossre ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
58 57 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
59 58 resmptd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑥 ∈ ℝ ↦ ( 𝐹𝑥 ) ) ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) )
60 56 59 eqtr2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) = ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
61 50 53 10 12 11 iblcncfioo ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ 𝐿1 )
62 60 61 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) ∈ 𝐿1 )
63 9 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐹 : ℝ ⟶ ℂ )
64 50 53 iccssred ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
65 64 sselda ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ℝ )
66 63 65 ffvelrnd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹𝑥 ) ∈ ℂ )
67 50 53 62 66 ibliooicc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) ∈ 𝐿1 )
68 26 31 38 40 46 67 itgspltprt ( 𝜑 → ∫ ( ( 𝑄 ‘ 0 ) [,] ( 𝑄𝑀 ) ) ( 𝐹𝑥 ) d 𝑥 = Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 )
69 8 a1i ( 𝜑𝑆 = ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑖 ) + 𝑇 ) ) )
70 fveq2 ( 𝑖 = 0 → ( 𝑄𝑖 ) = ( 𝑄 ‘ 0 ) )
71 70 oveq1d ( 𝑖 = 0 → ( ( 𝑄𝑖 ) + 𝑇 ) = ( ( 𝑄 ‘ 0 ) + 𝑇 ) )
72 71 adantl ( ( 𝜑𝑖 = 0 ) → ( ( 𝑄𝑖 ) + 𝑇 ) = ( ( 𝑄 ‘ 0 ) + 𝑇 ) )
73 4 nnnn0d ( 𝜑𝑀 ∈ ℕ0 )
74 nn0uz 0 = ( ℤ ‘ 0 )
75 73 74 eleqtrdi ( 𝜑𝑀 ∈ ( ℤ ‘ 0 ) )
76 eluzfz1 ( 𝑀 ∈ ( ℤ ‘ 0 ) → 0 ∈ ( 0 ... 𝑀 ) )
77 75 76 syl ( 𝜑 → 0 ∈ ( 0 ... 𝑀 ) )
78 5 rpred ( 𝜑𝑇 ∈ ℝ )
79 42 78 readdcld ( 𝜑 → ( ( 𝑄 ‘ 0 ) + 𝑇 ) ∈ ℝ )
80 69 72 77 79 fvmptd ( 𝜑 → ( 𝑆 ‘ 0 ) = ( ( 𝑄 ‘ 0 ) + 𝑇 ) )
81 20 oveq1d ( 𝜑 → ( ( 𝑄 ‘ 0 ) + 𝑇 ) = ( 𝐴 + 𝑇 ) )
82 80 81 eqtr2d ( 𝜑 → ( 𝐴 + 𝑇 ) = ( 𝑆 ‘ 0 ) )
83 fveq2 ( 𝑖 = 𝑀 → ( 𝑄𝑖 ) = ( 𝑄𝑀 ) )
84 83 oveq1d ( 𝑖 = 𝑀 → ( ( 𝑄𝑖 ) + 𝑇 ) = ( ( 𝑄𝑀 ) + 𝑇 ) )
85 84 adantl ( ( 𝜑𝑖 = 𝑀 ) → ( ( 𝑄𝑖 ) + 𝑇 ) = ( ( 𝑄𝑀 ) + 𝑇 ) )
86 eluzfz2 ( 𝑀 ∈ ( ℤ ‘ 0 ) → 𝑀 ∈ ( 0 ... 𝑀 ) )
87 75 86 syl ( 𝜑𝑀 ∈ ( 0 ... 𝑀 ) )
88 43 78 readdcld ( 𝜑 → ( ( 𝑄𝑀 ) + 𝑇 ) ∈ ℝ )
89 69 85 87 88 fvmptd ( 𝜑 → ( 𝑆𝑀 ) = ( ( 𝑄𝑀 ) + 𝑇 ) )
90 22 oveq1d ( 𝜑 → ( ( 𝑄𝑀 ) + 𝑇 ) = ( 𝐵 + 𝑇 ) )
91 89 90 eqtr2d ( 𝜑 → ( 𝐵 + 𝑇 ) = ( 𝑆𝑀 ) )
92 82 91 oveq12d ( 𝜑 → ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) = ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) )
93 92 itgeq1d ( 𝜑 → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) ( 𝐹𝑥 ) d 𝑥 )
94 38 ffvelrnda ( ( 𝜑𝑖 ∈ ( 0 ... 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℝ )
95 78 adantr ( ( 𝜑𝑖 ∈ ( 0 ... 𝑀 ) ) → 𝑇 ∈ ℝ )
96 94 95 readdcld ( ( 𝜑𝑖 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) ∈ ℝ )
97 96 8 fmptd ( 𝜑𝑆 : ( 0 ... 𝑀 ) ⟶ ℝ )
98 78 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑇 ∈ ℝ )
99 50 53 98 40 ltadd1dd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
100 48 96 sylan2 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) ∈ ℝ )
101 8 fvmpt2 ( ( 𝑖 ∈ ( 0 ... 𝑀 ) ∧ ( ( 𝑄𝑖 ) + 𝑇 ) ∈ ℝ ) → ( 𝑆𝑖 ) = ( ( 𝑄𝑖 ) + 𝑇 ) )
102 49 100 101 syl2anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆𝑖 ) = ( ( 𝑄𝑖 ) + 𝑇 ) )
103 fveq2 ( 𝑖 = 𝑗 → ( 𝑄𝑖 ) = ( 𝑄𝑗 ) )
104 103 oveq1d ( 𝑖 = 𝑗 → ( ( 𝑄𝑖 ) + 𝑇 ) = ( ( 𝑄𝑗 ) + 𝑇 ) )
105 104 cbvmptv ( 𝑖 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑖 ) + 𝑇 ) ) = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑗 ) + 𝑇 ) )
106 8 105 eqtri 𝑆 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑗 ) + 𝑇 ) )
107 106 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑆 = ( 𝑗 ∈ ( 0 ... 𝑀 ) ↦ ( ( 𝑄𝑗 ) + 𝑇 ) ) )
108 fveq2 ( 𝑗 = ( 𝑖 + 1 ) → ( 𝑄𝑗 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
109 108 oveq1d ( 𝑗 = ( 𝑖 + 1 ) → ( ( 𝑄𝑗 ) + 𝑇 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
110 109 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑗 = ( 𝑖 + 1 ) ) → ( ( 𝑄𝑗 ) + 𝑇 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
111 53 98 readdcld ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ )
112 107 110 52 111 fvmptd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
113 99 102 112 3brtr4d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆𝑖 ) < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
114 9 adantr ( ( 𝜑𝑥 ∈ ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) ) → 𝐹 : ℝ ⟶ ℂ )
115 80 79 eqeltrd ( 𝜑 → ( 𝑆 ‘ 0 ) ∈ ℝ )
116 115 adantr ( ( 𝜑𝑥 ∈ ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) ) → ( 𝑆 ‘ 0 ) ∈ ℝ )
117 89 88 eqeltrd ( 𝜑 → ( 𝑆𝑀 ) ∈ ℝ )
118 117 adantr ( ( 𝜑𝑥 ∈ ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) ) → ( 𝑆𝑀 ) ∈ ℝ )
119 116 118 iccssred ( ( 𝜑𝑥 ∈ ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) ) → ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) ⊆ ℝ )
120 simpr ( ( 𝜑𝑥 ∈ ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) ) → 𝑥 ∈ ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) )
121 119 120 sseldd ( ( 𝜑𝑥 ∈ ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) ) → 𝑥 ∈ ℝ )
122 114 121 ffvelrnd ( ( 𝜑𝑥 ∈ ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) ) → ( 𝐹𝑥 ) ∈ ℂ )
123 102 100 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆𝑖 ) ∈ ℝ )
124 112 111 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
125 ioosscn ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
126 125 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ )
127 eqeq1 ( 𝑤 = 𝑥 → ( 𝑤 = ( 𝑧 + 𝑇 ) ↔ 𝑥 = ( 𝑧 + 𝑇 ) ) )
128 127 rexbidv ( 𝑤 = 𝑥 → ( ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) )
129 oveq1 ( 𝑧 = 𝑦 → ( 𝑧 + 𝑇 ) = ( 𝑦 + 𝑇 ) )
130 129 eqeq2d ( 𝑧 = 𝑦 → ( 𝑥 = ( 𝑧 + 𝑇 ) ↔ 𝑥 = ( 𝑦 + 𝑇 ) ) )
131 130 cbvrexvw ( ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑦 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) )
132 128 131 bitrdi ( 𝑤 = 𝑥 → ( ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) ↔ ∃ 𝑦 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) ) )
133 132 cbvrabv { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } = { 𝑥 ∈ ℂ ∣ ∃ 𝑦 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑦 + 𝑇 ) }
134 fdm ( 𝐹 : ℝ ⟶ ℂ → dom 𝐹 = ℝ )
135 9 134 syl ( 𝜑 → dom 𝐹 = ℝ )
136 135 feq2d ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℂ ↔ 𝐹 : ℝ ⟶ ℂ ) )
137 9 136 mpbird ( 𝜑𝐹 : dom 𝐹 ⟶ ℂ )
138 137 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : dom 𝐹 ⟶ ℂ )
139 elioore ( 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑧 ∈ ℝ )
140 139 adantl ( ( 𝜑𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑧 ∈ ℝ )
141 78 adantr ( ( 𝜑𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑇 ∈ ℝ )
142 140 141 readdcld ( ( 𝜑𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑧 + 𝑇 ) ∈ ℝ )
143 142 adantlr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑧 + 𝑇 ) ∈ ℝ )
144 143 3adant3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑧 + 𝑇 ) ) → ( 𝑧 + 𝑇 ) ∈ ℝ )
145 simp3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑧 + 𝑇 ) ) → 𝑤 = ( 𝑧 + 𝑇 ) )
146 135 3ad2ant1 ( ( 𝜑𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑧 + 𝑇 ) ) → dom 𝐹 = ℝ )
147 146 3adant1r ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑧 + 𝑇 ) ) → dom 𝐹 = ℝ )
148 144 145 147 3eltr4d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑧 + 𝑇 ) ) → 𝑤 ∈ dom 𝐹 )
149 148 3exp ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑤 = ( 𝑧 + 𝑇 ) → 𝑤 ∈ dom 𝐹 ) ) )
150 149 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑤 ∈ ℂ ) → ( 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑤 = ( 𝑧 + 𝑇 ) → 𝑤 ∈ dom 𝐹 ) ) )
151 150 rexlimdv ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑤 ∈ ℂ ) → ( ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) → 𝑤 ∈ dom 𝐹 ) )
152 151 ralrimiva ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑤 ∈ ℂ ( ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) → 𝑤 ∈ dom 𝐹 ) )
153 rabss ( { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ⊆ dom 𝐹 ↔ ∀ 𝑤 ∈ ℂ ( ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) → 𝑤 ∈ dom 𝐹 ) )
154 152 153 sylibr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ⊆ dom 𝐹 )
155 simpll ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝜑 )
156 1 rexrd ( 𝜑𝐴 ∈ ℝ* )
157 156 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐴 ∈ ℝ* )
158 2 rexrd ( 𝜑𝐵 ∈ ℝ* )
159 158 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐵 ∈ ℝ* )
160 3 4 6 fourierdlem15 ( 𝜑𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
161 160 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
162 simplr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
163 ioossicc ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
164 163 sseli ( 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
165 164 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
166 157 159 161 162 165 fourierdlem1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ( 𝐴 [,] 𝐵 ) )
167 155 166 7 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) )
168 126 98 133 138 154 167 10 cncfperiod ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) ∈ ( { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } –cn→ ℂ ) )
169 128 elrab ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ↔ ( 𝑥 ∈ ℂ ∧ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) )
170 169 simprbi ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } → ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) )
171 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) → ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) )
172 nfv 𝑧 ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) )
173 nfre1 𝑧𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 )
174 172 173 nfan 𝑧 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) )
175 nfv 𝑧 ( 𝑥 ∈ ℝ ∧ ( 𝑆𝑖 ) < 𝑥𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
176 simp3 ( ( 𝜑𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → 𝑥 = ( 𝑧 + 𝑇 ) )
177 142 3adant3 ( ( 𝜑𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑧 + 𝑇 ) ∈ ℝ )
178 176 177 eqeltrd ( ( 𝜑𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → 𝑥 ∈ ℝ )
179 178 3adant1r ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → 𝑥 ∈ ℝ )
180 50 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) ∈ ℝ )
181 139 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑧 ∈ ℝ )
182 78 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑇 ∈ ℝ )
183 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
184 50 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
185 184 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
186 53 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
187 186 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
188 elioo2 ( ( ( 𝑄𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ) → ( 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑄𝑖 ) < 𝑧𝑧 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
189 185 187 188 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑧 ∈ ℝ ∧ ( 𝑄𝑖 ) < 𝑧𝑧 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
190 183 189 mpbid ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑧 ∈ ℝ ∧ ( 𝑄𝑖 ) < 𝑧𝑧 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
191 190 simp2d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) < 𝑧 )
192 180 181 182 191 ltadd1dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) < ( 𝑧 + 𝑇 ) )
193 192 3adant3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) < ( 𝑧 + 𝑇 ) )
194 102 3ad2ant1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑆𝑖 ) = ( ( 𝑄𝑖 ) + 𝑇 ) )
195 simp3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → 𝑥 = ( 𝑧 + 𝑇 ) )
196 193 194 195 3brtr4d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑆𝑖 ) < 𝑥 )
197 53 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
198 190 simp3d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑧 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
199 181 197 182 198 ltadd1dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑧 + 𝑇 ) < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
200 199 3adant3 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑧 + 𝑇 ) < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
201 112 3ad2ant1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
202 200 195 201 3brtr4d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → 𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
203 179 196 202 3jca ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑥 ∈ ℝ ∧ ( 𝑆𝑖 ) < 𝑥𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
204 203 3exp ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥 = ( 𝑧 + 𝑇 ) → ( 𝑥 ∈ ℝ ∧ ( 𝑆𝑖 ) < 𝑥𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
205 204 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥 = ( 𝑧 + 𝑇 ) → ( 𝑥 ∈ ℝ ∧ ( 𝑆𝑖 ) < 𝑥𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ) )
206 174 175 205 rexlimd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) → ( ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) → ( 𝑥 ∈ ℝ ∧ ( 𝑆𝑖 ) < 𝑥𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
207 171 206 mpd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑥 ∈ ℝ ∧ ( 𝑆𝑖 ) < 𝑥𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
208 123 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆𝑖 ) ∈ ℝ* )
209 208 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑆𝑖 ) ∈ ℝ* )
210 124 rexrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
211 210 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
212 elioo2 ( ( ( 𝑆𝑖 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ) → ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑆𝑖 ) < 𝑥𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
213 209 211 212 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) → ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑆𝑖 ) < 𝑥𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
214 207 213 mpbird ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) ) → 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
215 170 214 sylan2 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) → 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
216 elioore ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 ∈ ℝ )
217 216 recnd ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 ∈ ℂ )
218 217 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ℂ )
219 184 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
220 186 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
221 216 adantl ( ( 𝜑𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ℝ )
222 78 adantr ( ( 𝜑𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑇 ∈ ℝ )
223 221 222 resubcld ( ( 𝜑𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) ∈ ℝ )
224 223 adantlr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) ∈ ℝ )
225 102 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆𝑖 ) − 𝑇 ) = ( ( ( 𝑄𝑖 ) + 𝑇 ) − 𝑇 ) )
226 50 recnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ℂ )
227 98 recnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑇 ∈ ℂ )
228 226 227 pncand ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄𝑖 ) + 𝑇 ) − 𝑇 ) = ( 𝑄𝑖 ) )
229 225 228 eqtr2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) = ( ( 𝑆𝑖 ) − 𝑇 ) )
230 229 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) = ( ( 𝑆𝑖 ) − 𝑇 ) )
231 123 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆𝑖 ) ∈ ℝ )
232 216 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ℝ )
233 78 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑇 ∈ ℝ )
234 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
235 208 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆𝑖 ) ∈ ℝ* )
236 210 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
237 235 236 212 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↔ ( 𝑥 ∈ ℝ ∧ ( 𝑆𝑖 ) < 𝑥𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
238 234 237 mpbid ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥 ∈ ℝ ∧ ( 𝑆𝑖 ) < 𝑥𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
239 238 simp2d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆𝑖 ) < 𝑥 )
240 231 232 233 239 ltsub1dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑆𝑖 ) − 𝑇 ) < ( 𝑥𝑇 ) )
241 230 240 eqbrtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) < ( 𝑥𝑇 ) )
242 124 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
243 238 simp3d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
244 232 242 233 243 ltsub1dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) < ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) )
245 112 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) − 𝑇 ) )
246 53 recnd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℂ )
247 246 227 pncand ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
248 245 247 eqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
249 248 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
250 244 249 breqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
251 219 220 224 241 250 eliood ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
252 221 recnd ( ( 𝜑𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ℂ )
253 222 recnd ( ( 𝜑𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑇 ∈ ℂ )
254 252 253 npcand ( ( 𝜑𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑥𝑇 ) + 𝑇 ) = 𝑥 )
255 254 eqcomd ( ( 𝜑𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 = ( ( 𝑥𝑇 ) + 𝑇 ) )
256 255 adantlr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 = ( ( 𝑥𝑇 ) + 𝑇 ) )
257 oveq1 ( 𝑧 = ( 𝑥𝑇 ) → ( 𝑧 + 𝑇 ) = ( ( 𝑥𝑇 ) + 𝑇 ) )
258 257 eqeq2d ( 𝑧 = ( 𝑥𝑇 ) → ( 𝑥 = ( 𝑧 + 𝑇 ) ↔ 𝑥 = ( ( 𝑥𝑇 ) + 𝑇 ) ) )
259 258 rspcev ( ( ( 𝑥𝑇 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑥 = ( ( 𝑥𝑇 ) + 𝑇 ) ) → ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) )
260 251 256 259 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 = ( 𝑧 + 𝑇 ) )
261 218 260 169 sylanbrc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } )
262 215 261 impbida ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ↔ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
263 262 eqrdv ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } = ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
264 263 reseq2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) = ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) )
265 9 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 : ℝ ⟶ ℂ )
266 ioossre ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
267 266 a1i ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
268 265 267 feqresmpt ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) )
269 264 268 eqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) = ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) )
270 263 oveq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } –cn→ ℂ ) = ( ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
271 168 269 270 3eltr3d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) ∈ ( ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
272 57 135 sseqtrrid ( 𝜑 → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
273 272 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
274 eqid { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } = { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) }
275 simpll ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝜑 )
276 156 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐴 ∈ ℝ* )
277 158 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐵 ∈ ℝ* )
278 160 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
279 simplr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
280 163 183 sseldi ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑧 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
281 276 277 278 279 280 fourierdlem1 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
282 eleq1 ( 𝑥 = 𝑧 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) )
283 282 anbi2d ( 𝑥 = 𝑧 → ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
284 oveq1 ( 𝑥 = 𝑧 → ( 𝑥 + 𝑇 ) = ( 𝑧 + 𝑇 ) )
285 284 fveq2d ( 𝑥 = 𝑧 → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑧 + 𝑇 ) ) )
286 fveq2 ( 𝑥 = 𝑧 → ( 𝐹𝑥 ) = ( 𝐹𝑧 ) )
287 285 286 eqeq12d ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) ↔ ( 𝐹 ‘ ( 𝑧 + 𝑇 ) ) = ( 𝐹𝑧 ) ) )
288 283 287 imbi12d ( 𝑥 = 𝑧 → ( ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) ) ↔ ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑧 + 𝑇 ) ) = ( 𝐹𝑧 ) ) ) )
289 288 7 chvarvv ( ( 𝜑𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑧 + 𝑇 ) ) = ( 𝐹𝑧 ) )
290 275 281 289 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( 𝑧 + 𝑇 ) ) = ( 𝐹𝑧 ) )
291 138 126 273 227 274 154 290 12 limcperiod ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝐹 ↾ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) lim ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) )
292 112 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) = ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
293 269 292 oveq12d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) lim ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) = ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) lim ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
294 291 293 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) lim ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
295 138 126 273 227 274 154 290 11 limcperiod ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝐹 ↾ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) lim ( ( 𝑄𝑖 ) + 𝑇 ) ) )
296 102 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) = ( 𝑆𝑖 ) )
297 269 296 oveq12d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐹 ↾ { 𝑤 ∈ ℂ ∣ ∃ 𝑧 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑤 = ( 𝑧 + 𝑇 ) } ) lim ( ( 𝑄𝑖 ) + 𝑇 ) ) = ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) lim ( 𝑆𝑖 ) ) )
298 295 297 eleqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) lim ( 𝑆𝑖 ) ) )
299 123 124 271 294 298 iblcncfioo ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) ∈ 𝐿1 )
300 9 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐹 : ℝ ⟶ ℂ )
301 123 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆𝑖 ) ∈ ℝ )
302 124 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
303 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
304 eliccre ( ( ( 𝑆𝑖 ) ∈ ℝ ∧ ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ℝ )
305 301 302 303 304 syl3anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ℝ )
306 300 305 ffvelrnd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹𝑥 ) ∈ ℂ )
307 123 124 299 306 ibliooicc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐹𝑥 ) ) ∈ 𝐿1 )
308 26 31 97 113 122 307 itgspltprt ( 𝜑 → ∫ ( ( 𝑆 ‘ 0 ) [,] ( 𝑆𝑀 ) ) ( 𝐹𝑥 ) d 𝑥 = Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 )
309 iftrue ( 𝑥 = ( 𝑆𝑖 ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = 𝑅 )
310 309 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = 𝑅 )
311 iftrue ( 𝑥 = ( 𝑄𝑖 ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = 𝑅 )
312 iftrue ( 𝑥 = ( 𝑄𝑖 ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = 𝑅 )
313 311 312 eqtr4d ( 𝑥 = ( 𝑄𝑖 ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
314 313 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 = ( 𝑄𝑖 ) ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
315 iffalse ( ¬ 𝑥 = ( 𝑄𝑖 ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) )
316 315 adantr ( ( ¬ 𝑥 = ( 𝑄𝑖 ) ∧ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) )
317 iftrue ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) = 𝐿 )
318 317 adantl ( ( ¬ 𝑥 = ( 𝑄𝑖 ) ∧ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) = 𝐿 )
319 iffalse ( ¬ 𝑥 = ( 𝑄𝑖 ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) )
320 319 adantr ( ( ¬ 𝑥 = ( 𝑄𝑖 ) ∧ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) )
321 iftrue ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = 𝐿 )
322 321 adantl ( ( ¬ 𝑥 = ( 𝑄𝑖 ) ∧ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = 𝐿 )
323 320 322 eqtr2d ( ( ¬ 𝑥 = ( 𝑄𝑖 ) ∧ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝐿 = if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
324 316 318 323 3eqtrd ( ( ¬ 𝑥 = ( 𝑄𝑖 ) ∧ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
325 324 adantll ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
326 315 ad2antlr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) )
327 iffalse ( ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) = ( 𝐹𝑥 ) )
328 327 adantl ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) = ( 𝐹𝑥 ) )
329 319 ad2antlr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) )
330 iffalse ( ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) )
331 330 adantl ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) )
332 184 ad3antrrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
333 186 ad3antrrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
334 65 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 ∈ ℝ )
335 50 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) → ( 𝑄𝑖 ) ∈ ℝ )
336 65 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) → 𝑥 ∈ ℝ )
337 184 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
338 186 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
339 simplr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
340 iccgelb ( ( ( 𝑄𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ*𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) ≤ 𝑥 )
341 337 338 339 340 syl3anc ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) → ( 𝑄𝑖 ) ≤ 𝑥 )
342 neqne ( ¬ 𝑥 = ( 𝑄𝑖 ) → 𝑥 ≠ ( 𝑄𝑖 ) )
343 342 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) → 𝑥 ≠ ( 𝑄𝑖 ) )
344 335 336 341 343 leneltd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) → ( 𝑄𝑖 ) < 𝑥 )
345 344 adantr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄𝑖 ) < 𝑥 )
346 53 ad3antrrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
347 184 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
348 186 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
349 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
350 iccleub ( ( ( 𝑄𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ*𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
351 347 348 349 350 syl3anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
352 351 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
353 neqne ( ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → 𝑥 ≠ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
354 353 necomd ( ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≠ 𝑥 )
355 354 adantl ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≠ 𝑥 )
356 334 346 352 355 leneltd ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
357 332 333 334 345 356 eliood ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
358 fvres ( 𝑥 ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
359 357 358 syl ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
360 329 331 359 3eqtrrd ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐹𝑥 ) = if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
361 326 328 360 3eqtrd ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
362 325 361 pm2.61dan ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑄𝑖 ) ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
363 314 362 pm2.61dan ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) = if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
364 363 mpteq2dva ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( 𝐹𝑥 ) ) ) ) = ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) )
365 13 364 syl5eq ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐺 = ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) )
366 eqeq1 ( 𝑥 = 𝑤 → ( 𝑥 = ( 𝑄𝑖 ) ↔ 𝑤 = ( 𝑄𝑖 ) ) )
367 eqeq1 ( 𝑥 = 𝑤 → ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
368 fveq2 ( 𝑥 = 𝑤 → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) )
369 367 368 ifbieq2d ( 𝑥 = 𝑤 → if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) )
370 366 369 ifbieq2d ( 𝑥 = 𝑤 → if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) )
371 370 cbvmptv ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) = ( 𝑤 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) )
372 365 371 eqtrdi ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐺 = ( 𝑤 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) ) )
373 372 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → 𝐺 = ( 𝑤 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) ) )
374 simpr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) ∧ 𝑤 = ( 𝑥𝑇 ) ) → 𝑤 = ( 𝑥𝑇 ) )
375 oveq1 ( 𝑥 = ( 𝑆𝑖 ) → ( 𝑥𝑇 ) = ( ( 𝑆𝑖 ) − 𝑇 ) )
376 375 ad2antlr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) ∧ 𝑤 = ( 𝑥𝑇 ) ) → ( 𝑥𝑇 ) = ( ( 𝑆𝑖 ) − 𝑇 ) )
377 229 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆𝑖 ) − 𝑇 ) = ( 𝑄𝑖 ) )
378 377 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) ∧ 𝑤 = ( 𝑥𝑇 ) ) → ( ( 𝑆𝑖 ) − 𝑇 ) = ( 𝑄𝑖 ) )
379 374 376 378 3eqtrd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) ∧ 𝑤 = ( 𝑥𝑇 ) ) → 𝑤 = ( 𝑄𝑖 ) )
380 379 iftrued ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) ∧ 𝑤 = ( 𝑥𝑇 ) ) → if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) = 𝑅 )
381 375 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝑥𝑇 ) = ( ( 𝑆𝑖 ) − 𝑇 ) )
382 50 53 40 ltled ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
383 lbicc2 ( ( ( 𝑄𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ ( 𝑄𝑖 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄𝑖 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
384 184 186 382 383 syl3anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
385 377 384 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆𝑖 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
386 385 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → ( ( 𝑆𝑖 ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
387 381 386 eqeltrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝑥𝑇 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
388 limccl ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄𝑖 ) ) ⊆ ℂ
389 388 11 sseldi ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑅 ∈ ℂ )
390 389 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → 𝑅 ∈ ℂ )
391 373 380 387 390 fvmptd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝐺 ‘ ( 𝑥𝑇 ) ) = 𝑅 )
392 310 391 eqtr4d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
393 392 adantlr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
394 iffalse ( ¬ 𝑥 = ( 𝑆𝑖 ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) )
395 394 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) )
396 372 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝐺 = ( 𝑤 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) ) )
397 eqeq1 ( 𝑤 = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) → ( 𝑤 = ( 𝑄𝑖 ) ↔ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄𝑖 ) ) )
398 eqeq1 ( 𝑤 = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) → ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
399 fveq2 ( 𝑤 = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) )
400 398 399 ifbieq2d ( 𝑤 = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) → if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) = if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) ) )
401 397 400 ifbieq2d ( 𝑤 = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) → if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) = if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄𝑖 ) , 𝑅 , if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) ) ) )
402 401 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑤 = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) → if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) = if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄𝑖 ) , 𝑅 , if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) ) ) )
403 eqeq1 ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄𝑖 ) ↔ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄𝑖 ) ) )
404 iftrue ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) ) = 𝐿 )
405 403 404 ifbieq2d ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄𝑖 ) , 𝑅 , if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) ) ) = if ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄𝑖 ) , 𝑅 , 𝐿 ) )
406 248 405 syl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄𝑖 ) , 𝑅 , if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) ) ) = if ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄𝑖 ) , 𝑅 , 𝐿 ) )
407 406 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑤 = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) → if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄𝑖 ) , 𝑅 , if ( ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) ) ) = if ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄𝑖 ) , 𝑅 , 𝐿 ) )
408 50 40 gtned ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≠ ( 𝑄𝑖 ) )
409 408 neneqd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄𝑖 ) )
410 409 iffalsed ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → if ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄𝑖 ) , 𝑅 , 𝐿 ) = 𝐿 )
411 410 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑤 = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) → if ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑄𝑖 ) , 𝑅 , 𝐿 ) = 𝐿 )
412 402 407 411 3eqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑤 = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) → if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) = 𝐿 )
413 412 adantlr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) → if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) = 𝐿 )
414 ubicc2 ( ( ( 𝑄𝑖 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* ∧ ( 𝑄𝑖 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
415 184 186 382 414 syl3anc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
416 248 415 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
417 416 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
418 limccl ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) lim ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℂ
419 418 12 sseldi ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐿 ∈ ℂ )
420 419 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝐿 ∈ ℂ )
421 396 413 417 420 fvmptd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐺 ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) = 𝐿 )
422 oveq1 ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) → ( 𝑥𝑇 ) = ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) )
423 422 fveq2d ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) → ( 𝐺 ‘ ( 𝑥𝑇 ) ) = ( 𝐺 ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) )
424 423 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐺 ‘ ( 𝑥𝑇 ) ) = ( 𝐺 ‘ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) ) )
425 iftrue ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = 𝐿 )
426 425 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = 𝐿 )
427 421 424 426 3eqtr4rd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
428 427 ad4ant14 ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
429 iffalse ( ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) )
430 429 adantl ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) )
431 372 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐺 = ( 𝑤 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) ) )
432 431 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝐺 = ( 𝑤 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) ) )
433 eqeq1 ( 𝑤 = ( 𝑥𝑇 ) → ( 𝑤 = ( 𝑄𝑖 ) ↔ ( 𝑥𝑇 ) = ( 𝑄𝑖 ) ) )
434 eqeq1 ( 𝑤 = ( 𝑥𝑇 ) → ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
435 fveq2 ( 𝑤 = ( 𝑥𝑇 ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) )
436 434 435 ifbieq2d ( 𝑤 = ( 𝑥𝑇 ) → if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) = if ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ) )
437 433 436 ifbieq2d ( 𝑤 = ( 𝑥𝑇 ) → if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) = if ( ( 𝑥𝑇 ) = ( 𝑄𝑖 ) , 𝑅 , if ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ) ) )
438 437 adantl ( ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑥𝑇 ) ) → if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) = if ( ( 𝑥𝑇 ) = ( 𝑄𝑖 ) , 𝑅 , if ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ) ) )
439 305 recnd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ℂ )
440 227 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑇 ∈ ℂ )
441 439 440 npcand ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑥𝑇 ) + 𝑇 ) = 𝑥 )
442 441 eqcomd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 = ( ( 𝑥𝑇 ) + 𝑇 ) )
443 442 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ( 𝑥𝑇 ) = ( 𝑄𝑖 ) ) → 𝑥 = ( ( 𝑥𝑇 ) + 𝑇 ) )
444 oveq1 ( ( 𝑥𝑇 ) = ( 𝑄𝑖 ) → ( ( 𝑥𝑇 ) + 𝑇 ) = ( ( 𝑄𝑖 ) + 𝑇 ) )
445 444 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ( 𝑥𝑇 ) = ( 𝑄𝑖 ) ) → ( ( 𝑥𝑇 ) + 𝑇 ) = ( ( 𝑄𝑖 ) + 𝑇 ) )
446 296 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ( 𝑥𝑇 ) = ( 𝑄𝑖 ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) = ( 𝑆𝑖 ) )
447 443 445 446 3eqtrd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ( 𝑥𝑇 ) = ( 𝑄𝑖 ) ) → 𝑥 = ( 𝑆𝑖 ) )
448 447 stoic1a ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → ¬ ( 𝑥𝑇 ) = ( 𝑄𝑖 ) )
449 448 iffalsed ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → if ( ( 𝑥𝑇 ) = ( 𝑄𝑖 ) , 𝑅 , if ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ) ) = if ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ) )
450 449 ad2antrr ( ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑥𝑇 ) ) → if ( ( 𝑥𝑇 ) = ( 𝑄𝑖 ) , 𝑅 , if ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ) ) = if ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ) )
451 442 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 = ( ( 𝑥𝑇 ) + 𝑇 ) )
452 oveq1 ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → ( ( 𝑥𝑇 ) + 𝑇 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
453 452 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑥𝑇 ) + 𝑇 ) = ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
454 292 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) = ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
455 451 453 454 3eqtrd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
456 455 stoic1a ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ¬ ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
457 456 iffalsed ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → if ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) )
458 457 adantlr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → if ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) )
459 458 adantr ( ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑥𝑇 ) ) → if ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) )
460 438 450 459 3eqtrd ( ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ∧ 𝑤 = ( 𝑥𝑇 ) ) → if ( 𝑤 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑤 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑤 ) ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) )
461 50 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) ∈ ℝ )
462 53 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
463 78 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑇 ∈ ℝ )
464 305 463 resubcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) ∈ ℝ )
465 229 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) = ( ( 𝑆𝑖 ) − 𝑇 ) )
466 208 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆𝑖 ) ∈ ℝ* )
467 210 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
468 iccgelb ( ( ( 𝑆𝑖 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ*𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆𝑖 ) ≤ 𝑥 )
469 466 467 303 468 syl3anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑆𝑖 ) ≤ 𝑥 )
470 301 305 463 469 lesub1dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑆𝑖 ) − 𝑇 ) ≤ ( 𝑥𝑇 ) )
471 465 470 eqbrtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑄𝑖 ) ≤ ( 𝑥𝑇 ) )
472 iccleub ( ( ( 𝑆𝑖 ) ∈ ℝ* ∧ ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ*𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ≤ ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
473 466 467 303 472 syl3anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ≤ ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
474 305 302 463 473 lesub1dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) ≤ ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) )
475 248 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑆 ‘ ( 𝑖 + 1 ) ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
476 474 475 breqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
477 461 462 464 471 476 eliccd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
478 477 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥𝑇 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
479 138 273 fssresd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
480 479 ad3antrrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
481 184 ad3antrrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄𝑖 ) ∈ ℝ* )
482 186 ad3antrrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
483 305 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 ∈ ℝ )
484 98 ad3antrrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝑇 ∈ ℝ )
485 483 484 resubcld ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥𝑇 ) ∈ ℝ )
486 50 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝑄𝑖 ) ∈ ℝ )
487 464 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝑥𝑇 ) ∈ ℝ )
488 471 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝑄𝑖 ) ≤ ( 𝑥𝑇 ) )
489 448 neqned ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝑥𝑇 ) ≠ ( 𝑄𝑖 ) )
490 486 487 488 489 leneltd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝑄𝑖 ) < ( 𝑥𝑇 ) )
491 490 adantr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄𝑖 ) < ( 𝑥𝑇 ) )
492 464 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥𝑇 ) ∈ ℝ )
493 53 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
494 476 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥𝑇 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
495 eqcom ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑥𝑇 ) )
496 455 ex ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑥𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) → 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
497 495 496 syl5bir ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑥𝑇 ) → 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
498 497 con3dimp ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ¬ ( 𝑄 ‘ ( 𝑖 + 1 ) ) = ( 𝑥𝑇 ) )
499 498 neqned ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ≠ ( 𝑥𝑇 ) )
500 492 493 494 499 leneltd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥𝑇 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
501 500 adantlr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥𝑇 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
502 481 482 485 491 501 eliood ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥𝑇 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
503 480 502 ffvelrnd ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) ∈ ℂ )
504 432 460 478 503 fvmptd ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐺 ‘ ( 𝑥𝑇 ) ) = ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) )
505 fvres ( ( 𝑥𝑇 ) ∈ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) = ( 𝐹 ‘ ( 𝑥𝑇 ) ) )
506 502 505 syl ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ ( 𝑥𝑇 ) ) = ( 𝐹 ‘ ( 𝑥𝑇 ) ) )
507 504 506 eqtrd ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐺 ‘ ( 𝑥𝑇 ) ) = ( 𝐹 ‘ ( 𝑥𝑇 ) ) )
508 466 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆𝑖 ) ∈ ℝ* )
509 467 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
510 123 ad2antrr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝑆𝑖 ) ∈ ℝ )
511 305 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → 𝑥 ∈ ℝ )
512 469 adantr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝑆𝑖 ) ≤ 𝑥 )
513 neqne ( ¬ 𝑥 = ( 𝑆𝑖 ) → 𝑥 ≠ ( 𝑆𝑖 ) )
514 513 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → 𝑥 ≠ ( 𝑆𝑖 ) )
515 510 511 512 514 leneltd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → ( 𝑆𝑖 ) < 𝑥 )
516 515 adantr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆𝑖 ) < 𝑥 )
517 302 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
518 473 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 ≤ ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
519 neqne ( ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) → 𝑥 ≠ ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
520 519 necomd ( ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ≠ 𝑥 )
521 520 adantl ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑆 ‘ ( 𝑖 + 1 ) ) ≠ 𝑥 )
522 483 517 518 521 leneltd ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 < ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
523 508 509 483 516 522 eliood ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
524 fvres ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
525 523 524 syl ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
526 441 fveq2d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹 ‘ ( ( 𝑥𝑇 ) + 𝑇 ) ) = ( 𝐹𝑥 ) )
527 526 eqcomd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐹𝑥 ) = ( 𝐹 ‘ ( ( 𝑥𝑇 ) + 𝑇 ) ) )
528 527 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐹𝑥 ) = ( 𝐹 ‘ ( ( 𝑥𝑇 ) + 𝑇 ) ) )
529 439 440 subcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) ∈ ℂ )
530 elex ( ( 𝑥𝑇 ) ∈ ℂ → ( 𝑥𝑇 ) ∈ V )
531 529 530 syl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) ∈ V )
532 531 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥𝑇 ) ∈ V )
533 simp-4l ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝜑 )
534 156 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐴 ∈ ℝ* )
535 158 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐵 ∈ ℝ* )
536 160 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
537 simpr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
538 534 535 536 537 fourierdlem8 ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
539 538 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( 𝐴 [,] 𝐵 ) )
540 539 477 sseldd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑥𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) )
541 540 ad2antrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝑥𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) )
542 533 541 jca ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝜑 ∧ ( 𝑥𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
543 eleq1 ( 𝑦 = ( 𝑥𝑇 ) → ( 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑥𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) )
544 543 anbi2d ( 𝑦 = ( 𝑥𝑇 ) → ( ( 𝜑𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑 ∧ ( 𝑥𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) ) )
545 oveq1 ( 𝑦 = ( 𝑥𝑇 ) → ( 𝑦 + 𝑇 ) = ( ( 𝑥𝑇 ) + 𝑇 ) )
546 545 fveq2d ( 𝑦 = ( 𝑥𝑇 ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹 ‘ ( ( 𝑥𝑇 ) + 𝑇 ) ) )
547 fveq2 ( 𝑦 = ( 𝑥𝑇 ) → ( 𝐹𝑦 ) = ( 𝐹 ‘ ( 𝑥𝑇 ) ) )
548 546 547 eqeq12d ( 𝑦 = ( 𝑥𝑇 ) → ( ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹𝑦 ) ↔ ( 𝐹 ‘ ( ( 𝑥𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥𝑇 ) ) ) )
549 544 548 imbi12d ( 𝑦 = ( 𝑥𝑇 ) → ( ( ( 𝜑𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹𝑦 ) ) ↔ ( ( 𝜑 ∧ ( 𝑥𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( ( 𝑥𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥𝑇 ) ) ) ) )
550 eleq1 ( 𝑥 = 𝑦 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↔ 𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) )
551 550 anbi2d ( 𝑥 = 𝑦 → ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) ↔ ( 𝜑𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) ) )
552 oveq1 ( 𝑥 = 𝑦 → ( 𝑥 + 𝑇 ) = ( 𝑦 + 𝑇 ) )
553 552 fveq2d ( 𝑥 = 𝑦 → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) )
554 fveq2 ( 𝑥 = 𝑦 → ( 𝐹𝑥 ) = ( 𝐹𝑦 ) )
555 553 554 eqeq12d ( 𝑥 = 𝑦 → ( ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) ↔ ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹𝑦 ) ) )
556 551 555 imbi12d ( 𝑥 = 𝑦 → ( ( ( 𝜑𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹𝑥 ) ) ↔ ( ( 𝜑𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹𝑦 ) ) ) )
557 556 7 chvarvv ( ( 𝜑𝑦 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( 𝑦 + 𝑇 ) ) = ( 𝐹𝑦 ) )
558 549 557 vtoclg ( ( 𝑥𝑇 ) ∈ V → ( ( 𝜑 ∧ ( 𝑥𝑇 ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ ( ( 𝑥𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥𝑇 ) ) ) )
559 532 542 558 sylc ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑥𝑇 ) + 𝑇 ) ) = ( 𝐹 ‘ ( 𝑥𝑇 ) ) )
560 525 528 559 3eqtrd ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝑥𝑇 ) ) )
561 507 560 eqtr4d ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐺 ‘ ( 𝑥𝑇 ) ) = ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) )
562 430 561 eqtr4d ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
563 428 562 pm2.61dan ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
564 395 563 eqtrd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
565 393 564 pm2.61dan ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
566 310 390 eqeltrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ∈ ℂ )
567 566 adantlr ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ 𝑥 = ( 𝑆𝑖 ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ∈ ℂ )
568 426 420 eqeltrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ∈ ℂ )
569 568 ad4ant14 ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ∈ ℂ )
570 265 267 fssresd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
571 570 ad3antrrr ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
572 571 523 ffvelrnd ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ∈ ℂ )
573 430 572 eqeltrd ( ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) ∧ ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ∈ ℂ )
574 569 573 pm2.61dan ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ∈ ℂ )
575 395 574 eqeltrd ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 = ( 𝑆𝑖 ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ∈ ℂ )
576 567 575 pm2.61dan ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ∈ ℂ )
577 eqid ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
578 577 fvmpt2 ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ∧ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ∈ ℂ ) → ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) = if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
579 303 576 578 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) = if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
580 nfv 𝑥 ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) )
581 eqid ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
582 580 581 50 53 10 12 11 cncfiooicc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑥 ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑄𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑄 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑄𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ∈ ( ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
583 365 582 eqeltrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐺 ∈ ( ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
584 cncff ( 𝐺 ∈ ( ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → 𝐺 : ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
585 583 584 syl ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐺 : ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
586 585 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝐺 : ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
587 586 477 ffvelrnd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐺 ‘ ( 𝑥𝑇 ) ) ∈ ℂ )
588 14 fvmpt2 ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ∧ ( 𝐺 ‘ ( 𝑥𝑇 ) ) ∈ ℂ ) → ( 𝐻𝑥 ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
589 303 587 588 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻𝑥 ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
590 565 579 589 3eqtr4rd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻𝑥 ) = ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) )
591 590 itgeq2dv ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐻𝑥 ) d 𝑥 = ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) d 𝑥 )
592 ioossicc ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
593 592 sseli ( 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) → 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
594 593 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
595 593 576 sylan2 ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ∈ ℂ )
596 594 595 578 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) = if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) )
597 231 239 gtned ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ≠ ( 𝑆𝑖 ) )
598 597 neneqd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑥 = ( 𝑆𝑖 ) )
599 598 iffalsed ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) = if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) )
600 232 243 ltned ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ≠ ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
601 600 neneqd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ¬ 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) )
602 601 iffalsed ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) )
603 524 adantl ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
604 602 603 eqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) = ( 𝐹𝑥 ) )
605 596 599 604 3eqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) = ( 𝐹𝑥 ) )
606 605 itgeq2dv ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 )
607 579 576 eqeltrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) → ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) ∈ ℂ )
608 123 124 607 itgioo ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) d 𝑥 )
609 123 124 306 itgioo ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 )
610 606 608 609 3eqtr3d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( ( 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ↦ if ( 𝑥 = ( 𝑆𝑖 ) , 𝑅 , if ( 𝑥 = ( 𝑆 ‘ ( 𝑖 + 1 ) ) , 𝐿 , ( ( 𝐹 ↾ ( ( 𝑆𝑖 ) (,) ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ) ‘ 𝑥 ) ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 )
611 591 610 eqtr2d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐻𝑥 ) d 𝑥 )
612 102 112 oveq12d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) = ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) )
613 612 itgeq1d ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐻𝑥 ) d 𝑥 = ∫ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ( 𝐻𝑥 ) d 𝑥 )
614 simpr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) )
615 612 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) = ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
616 615 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) = ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
617 614 616 eleqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 ∈ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) )
618 585 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝐺 : ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
619 50 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑄𝑖 ) ∈ ℝ )
620 53 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
621 100 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) ∈ ℝ )
622 111 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ )
623 eliccre ( ( ( ( 𝑄𝑖 ) + 𝑇 ) ∈ ℝ ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 ∈ ℝ )
624 621 622 614 623 syl3anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 ∈ ℝ )
625 78 ad2antrr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑇 ∈ ℝ )
626 624 625 resubcld ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥𝑇 ) ∈ ℝ )
627 228 eqcomd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄𝑖 ) = ( ( ( 𝑄𝑖 ) + 𝑇 ) − 𝑇 ) )
628 627 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑄𝑖 ) = ( ( ( 𝑄𝑖 ) + 𝑇 ) − 𝑇 ) )
629 621 rexrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) ∈ ℝ* )
630 622 rexrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ* )
631 iccgelb ( ( ( ( 𝑄𝑖 ) + 𝑇 ) ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ*𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) ≤ 𝑥 )
632 629 630 614 631 syl3anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑄𝑖 ) + 𝑇 ) ≤ 𝑥 )
633 621 624 625 632 lesub1dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( ( 𝑄𝑖 ) + 𝑇 ) − 𝑇 ) ≤ ( 𝑥𝑇 ) )
634 628 633 eqbrtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑄𝑖 ) ≤ ( 𝑥𝑇 ) )
635 iccleub ( ( ( ( 𝑄𝑖 ) + 𝑇 ) ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ∈ ℝ*𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 ≤ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
636 629 630 614 635 syl3anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → 𝑥 ≤ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) )
637 624 622 625 636 lesub1dd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥𝑇 ) ≤ ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) − 𝑇 ) )
638 247 adantr ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) − 𝑇 ) = ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
639 637 638 breqtrd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥𝑇 ) ≤ ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
640 619 620 626 634 639 eliccd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑥𝑇 ) ∈ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
641 618 640 ffvelrnd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝐺 ‘ ( 𝑥𝑇 ) ) ∈ ℂ )
642 617 641 588 syl2anc ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝐻𝑥 ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
643 eqidd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝑦 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ↦ ( 𝐺 ‘ ( 𝑦𝑇 ) ) ) = ( 𝑦 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ↦ ( 𝐺 ‘ ( 𝑦𝑇 ) ) ) )
644 oveq1 ( 𝑦 = 𝑥 → ( 𝑦𝑇 ) = ( 𝑥𝑇 ) )
645 644 fveq2d ( 𝑦 = 𝑥 → ( 𝐺 ‘ ( 𝑦𝑇 ) ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
646 645 adantl ( ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) ∧ 𝑦 = 𝑥 ) → ( 𝐺 ‘ ( 𝑦𝑇 ) ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
647 643 646 614 641 fvmptd ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( ( 𝑦 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ↦ ( 𝐺 ‘ ( 𝑦𝑇 ) ) ) ‘ 𝑥 ) = ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
648 642 647 eqtr4d ( ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ) → ( 𝐻𝑥 ) = ( ( 𝑦 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ↦ ( 𝐺 ‘ ( 𝑦𝑇 ) ) ) ‘ 𝑥 ) )
649 648 itgeq2dv ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ( 𝐻𝑥 ) d 𝑥 = ∫ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ( ( 𝑦 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ↦ ( 𝐺 ‘ ( 𝑦𝑇 ) ) ) ‘ 𝑥 ) d 𝑥 )
650 5 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑇 ∈ ℝ+ )
651 645 cbvmptv ( 𝑦 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ↦ ( 𝐺 ‘ ( 𝑦𝑇 ) ) ) = ( 𝑥 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ↦ ( 𝐺 ‘ ( 𝑥𝑇 ) ) )
652 50 53 382 583 650 651 itgiccshift ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ( ( 𝑦 ∈ ( ( ( 𝑄𝑖 ) + 𝑇 ) [,] ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + 𝑇 ) ) ↦ ( 𝐺 ‘ ( 𝑦𝑇 ) ) ) ‘ 𝑥 ) d 𝑥 = ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐺𝑥 ) d 𝑥 )
653 613 649 652 3eqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐻𝑥 ) d 𝑥 = ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐺𝑥 ) d 𝑥 )
654 135 adantr ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → dom 𝐹 = ℝ )
655 64 654 sseqtrrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
656 50 53 138 10 655 11 12 13 itgioocnicc ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ∈ 𝐿1 ∧ ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐺𝑥 ) d 𝑥 = ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 ) )
657 656 simprd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐺𝑥 ) d 𝑥 = ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 )
658 611 653 657 3eqtrd ( ( 𝜑𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 )
659 658 sumeq2dv ( 𝜑 → Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( 𝑆𝑖 ) [,] ( 𝑆 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 = Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 )
660 93 308 659 3eqtrrd ( 𝜑 → Σ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∫ ( ( 𝑄𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹𝑥 ) d 𝑥 )
661 25 68 660 3eqtrrd ( 𝜑 → ∫ ( ( 𝐴 + 𝑇 ) [,] ( 𝐵 + 𝑇 ) ) ( 𝐹𝑥 ) d 𝑥 = ∫ ( 𝐴 [,] 𝐵 ) ( 𝐹𝑥 ) d 𝑥 )