This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fourierdlem97

Description: F is continuous on the intervals induced by the moved partition V . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem97.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
fourierdlem97.g ⊢ 𝐺 = ( ℝ D 𝐹 )
fourierdlem97.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem97.a ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
fourierdlem97.b ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
fourierdlem97.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
fourierdlem97.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem97.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem97.fper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
fourierdlem97.qcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
fourierdlem97.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
fourierdlem97.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
fourierdlem97.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) )
fourierdlem97.v ⊢ 𝑉 = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
fourierdlem97.h ⊢ 𝐻 = ( 𝑠 ∈ ℝ ↦ if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
Assertion fourierdlem97 ( 𝜑 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 fourierdlem97.f ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2 fourierdlem97.g ⊢ 𝐺 = ( ℝ D 𝐹 )
3 fourierdlem97.p ⊢ 𝑃 = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐴 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
4 fourierdlem97.a ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
5 fourierdlem97.b ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
6 fourierdlem97.t ⊢ 𝑇 = ( 𝐵 − 𝐴 )
7 fourierdlem97.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
8 fourierdlem97.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
9 fourierdlem97.fper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
10 fourierdlem97.qcn ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
11 fourierdlem97.c ⊢ ( 𝜑 → 𝐶 ∈ ℝ )
12 fourierdlem97.d ⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) +∞ ) )
13 fourierdlem97.j ⊢ ( 𝜑 → 𝐽 ∈ ( 0 ..^ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) )
14 fourierdlem97.v ⊢ 𝑉 = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
15 fourierdlem97.h ⊢ 𝐻 = ( 𝑠 ∈ ℝ ↦ if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
16 ioossre ⊢ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ℝ
17 16 a1i ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ℝ )
18 17 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
19 iftrue ⊢ ( 𝑠 ∈ dom 𝐺 → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ 𝑠 ) )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ dom 𝐺 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ 𝑠 ) )
21 ssid ⊢ ℝ ⊆ ℝ
22 dvfre ⊢ ( ( 𝐹 : ℝ ⟶ ℝ ∧ ℝ ⊆ ℝ ) → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
23 1 21 22 sylancl ⊢ ( 𝜑 → ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
24 2 feq1i ⊢ ( 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ ↔ ( ℝ D 𝐹 ) : dom ( ℝ D 𝐹 ) ⟶ ℝ )
25 23 24 sylibr ⊢ ( 𝜑 → 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ dom 𝐺 ) → 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ )
27 id ⊢ ( 𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom 𝐺 )
28 2 dmeqi ⊢ dom 𝐺 = dom ( ℝ D 𝐹 )
29 27 28 eleqtrdi ⊢ ( 𝑠 ∈ dom 𝐺 → 𝑠 ∈ dom ( ℝ D 𝐹 ) )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ dom 𝐺 ) → 𝑠 ∈ dom ( ℝ D 𝐹 ) )
31 26 30 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑠 ) ∈ ℝ )
32 20 31 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ dom 𝐺 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
33 32 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ 𝑠 ∈ dom 𝐺 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
34 iffalse ⊢ ( ¬ 𝑠 ∈ dom 𝐺 → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = 0 )
35 0red ⊢ ( ¬ 𝑠 ∈ dom 𝐺 → 0 ∈ ℝ )
36 34 35 eqeltrd ⊢ ( ¬ 𝑠 ∈ dom 𝐺 → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
37 36 adantl ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) ∧ ¬ 𝑠 ∈ dom 𝐺 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
38 33 37 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
39 18 38 syldan ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
40 15 fvmpt2 ⊢ ( ( 𝑠 ∈ ℝ ∧ if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
41 18 39 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
42 elioore ⊢ ( 𝐷 ∈ ( 𝐶 (,) +∞ ) → 𝐷 ∈ ℝ )
43 12 42 syl ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
44 11 rexrd ⊢ ( 𝜑 → 𝐶 ∈ ℝ* )
45 pnfxr ⊢ +∞ ∈ ℝ*
46 45 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
47 ioogtlb ⊢ ( ( 𝐶 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐷 ∈ ( 𝐶 (,) +∞ ) ) → 𝐶 < 𝐷 )
48 44 46 12 47 syl3anc ⊢ ( 𝜑 → 𝐶 < 𝐷 )
49 oveq1 ⊢ ( 𝑦 = 𝑥 → ( 𝑦 + ( ℎ · 𝑇 ) ) = ( 𝑥 + ( ℎ · 𝑇 ) ) )
50 49 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑥 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ) )
51 50 rexbidv ⊢ ( 𝑦 = 𝑥 → ( ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ ℎ ∈ ℤ ( 𝑥 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ) )
52 51 cbvrabv ⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑥 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 }
53 52 uneq2i ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑥 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑥 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } )
54 oveq1 ⊢ ( 𝑘 = 𝑙 → ( 𝑘 · 𝑇 ) = ( 𝑙 · 𝑇 ) )
55 54 oveq2d ⊢ ( 𝑘 = 𝑙 → ( 𝑦 + ( 𝑘 · 𝑇 ) ) = ( 𝑦 + ( 𝑙 · 𝑇 ) ) )
56 55 eleq1d ⊢ ( 𝑘 = 𝑙 → ( ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
57 56 cbvrexvw ⊢ ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 )
58 57 a1i ⊢ ( 𝑦 ∈ ( 𝐶 [,] 𝐷 ) → ( ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
59 58 rabbiia ⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 }
60 59 uneq2i ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } )
61 oveq1 ⊢ ( 𝑙 = ℎ → ( 𝑙 · 𝑇 ) = ( ℎ · 𝑇 ) )
62 61 oveq2d ⊢ ( 𝑙 = ℎ → ( 𝑦 + ( 𝑙 · 𝑇 ) ) = ( 𝑦 + ( ℎ · 𝑇 ) ) )
63 62 eleq1d ⊢ ( 𝑙 = ℎ → ( ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ) )
64 63 cbvrexvw ⊢ ( ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 )
65 64 a1i ⊢ ( 𝑦 ∈ ( 𝐶 [,] 𝐷 ) → ( ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 ) )
66 65 rabbiia ⊢ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 }
67 66 uneq2i ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } )
68 60 67 eqtri ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } )
69 68 fveq2i ⊢ ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) )
70 69 oveq1i ⊢ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
71 oveq1 ⊢ ( 𝑘 = ℎ → ( 𝑘 · 𝑇 ) = ( ℎ · 𝑇 ) )
72 71 oveq2d ⊢ ( 𝑘 = ℎ → ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) = ( ( 𝑄 ‘ 0 ) + ( ℎ · 𝑇 ) ) )
73 72 breq1d ⊢ ( 𝑘 = ℎ → ( ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( ( 𝑄 ‘ 0 ) + ( ℎ · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
74 73 cbvrabv ⊢ { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } = { ℎ ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( ℎ · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) }
75 74 supeq1i ⊢ sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) = sup ( { ℎ ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( ℎ · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < )
76 fveq2 ⊢ ( 𝑗 = 𝑒 → ( 𝑄 ‘ 𝑗 ) = ( 𝑄 ‘ 𝑒 ) )
77 76 oveq1d ⊢ ( 𝑗 = 𝑒 → ( ( 𝑄 ‘ 𝑗 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) = ( ( 𝑄 ‘ 𝑒 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) )
78 77 breq1d ⊢ ( 𝑗 = 𝑒 → ( ( ( 𝑄 ‘ 𝑗 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ↔ ( ( 𝑄 ‘ 𝑒 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) ) )
79 78 cbvrabv ⊢ { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } = { 𝑒 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑒 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) }
80 79 supeq1i ⊢ sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) = sup ( { 𝑒 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑒 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < )
81 6 3 7 8 11 43 48 53 70 14 13 75 80 fourierdlem64 ⊢ ( 𝜑 → ( ( sup ( { 𝑗 ∈ ( 0 ..^ 𝑀 ) ∣ ( ( 𝑄 ‘ 𝑗 ) + ( sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) ∈ ( 0 ..^ 𝑀 ) ∧ sup ( { 𝑘 ∈ ℤ ∣ ( ( 𝑄 ‘ 0 ) + ( 𝑘 · 𝑇 ) ) ≤ ( 𝑉 ‘ 𝐽 ) } , ℝ , < ) ∈ ℤ ) ∧ ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑙 ∈ ℤ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) )
82 81 simprd ⊢ ( 𝜑 → ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑙 ∈ ℤ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
83 simpl1 ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝜑 )
84 simpl2l ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
85 cncff ⊢ ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
86 10 85 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ )
87 ffun ⊢ ( 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ → Fun 𝐺 )
88 25 87 syl ⊢ ( 𝜑 → Fun 𝐺 )
89 88 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → Fun 𝐺 )
90 ffvresb ⊢ ( Fun 𝐺 → ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ↔ ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑠 ) ∈ ℂ ) ) )
91 89 90 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) : ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⟶ ℂ ↔ ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑠 ) ∈ ℂ ) ) )
92 86 91 mpbid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ( 𝑠 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑠 ) ∈ ℂ ) )
93 92 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝑠 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑠 ) ∈ ℂ ) )
94 93 simpld ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ dom 𝐺 )
95 94 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑠 ∈ dom 𝐺 )
96 dfss3 ⊢ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐺 ↔ ∀ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑠 ∈ dom 𝐺 )
97 95 96 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐺 )
98 83 84 97 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐺 )
99 simpl2 ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) )
100 83 99 jca ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) )
101 simpl3 ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
102 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) )
103 101 102 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
104 3 fourierdlem2 ⊢ ( 𝑀 ∈ ℕ → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
105 7 104 syl ⊢ ( 𝜑 → ( 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) ↔ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ) )
106 8 105 mpbid ⊢ ( 𝜑 → ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) ∧ ( ( ( 𝑄 ‘ 0 ) = 𝐴 ∧ ( 𝑄 ‘ 𝑀 ) = 𝐵 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑀 ) ( 𝑄 ‘ 𝑖 ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
107 106 simpld ⊢ ( 𝜑 → 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) )
108 elmapi ⊢ ( 𝑄 ∈ ( ℝ ↑m ( 0 ... 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
109 107 108 syl ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
110 109 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ℝ )
111 elfzofz ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
112 111 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ... 𝑀 ) )
113 110 112 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
114 113 rexrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
115 114 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
116 115 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ* )
117 fzofzp1 ⊢ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
118 117 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑖 + 1 ) ∈ ( 0 ... 𝑀 ) )
119 110 118 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
120 119 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
121 120 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ )
122 121 rexrd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑄 ‘ ( 𝑖 + 1 ) ) ∈ ℝ* )
123 elioore ⊢ ( 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) → 𝑡 ∈ ℝ )
124 123 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑡 ∈ ℝ )
125 zre ⊢ ( 𝑙 ∈ ℤ → 𝑙 ∈ ℝ )
126 125 adantl ⊢ ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) → 𝑙 ∈ ℝ )
127 126 ad2antlr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑙 ∈ ℝ )
128 4 5 resubcld ⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) ∈ ℝ )
129 6 128 eqeltrid ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
130 129 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑇 ∈ ℝ )
131 127 130 remulcld ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑙 · 𝑇 ) ∈ ℝ )
132 124 131 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ ℝ )
133 113 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
134 125 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → 𝑙 ∈ ℝ )
135 129 adantr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → 𝑇 ∈ ℝ )
136 134 135 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( 𝑙 · 𝑇 ) ∈ ℝ )
137 133 136 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ )
138 137 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* )
139 138 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* )
140 120 136 readdcld ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ )
141 140 rexrd ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* )
142 141 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* )
143 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
144 ioogtlb ⊢ ( ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) < 𝑡 )
145 139 142 143 144 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) < 𝑡 )
146 133 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) ∈ ℝ )
147 146 131 124 ltaddsubd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) < 𝑡 ↔ ( 𝑄 ‘ 𝑖 ) < ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) )
148 145 147 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑄 ‘ 𝑖 ) < ( 𝑡 − ( 𝑙 · 𝑇 ) ) )
149 iooltub ⊢ ( ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* ∧ ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ∈ ℝ* ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑡 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) )
150 139 142 143 149 syl3anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → 𝑡 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) )
151 124 131 121 ltsubaddd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) ↔ 𝑡 < ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) )
152 150 151 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑡 − ( 𝑙 · 𝑇 ) ) < ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
153 116 122 132 148 152 eliood ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
154 100 103 153 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
155 98 154 sseldd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 )
156 elioore ⊢ ( 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) → 𝑡 ∈ ℝ )
157 recn ⊢ ( 𝑡 ∈ ℝ → 𝑡 ∈ ℂ )
158 157 adantl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑡 ∈ ℂ )
159 zcn ⊢ ( 𝑙 ∈ ℤ → 𝑙 ∈ ℂ )
160 159 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑙 ∈ ℂ )
161 129 recnd ⊢ ( 𝜑 → 𝑇 ∈ ℂ )
162 161 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑇 ∈ ℂ )
163 160 162 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → ( 𝑙 · 𝑇 ) ∈ ℂ )
164 158 163 npcand ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) = 𝑡 )
165 164 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → 𝑡 = ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) )
166 165 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → 𝑡 = ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) )
167 ovex ⊢ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ V
168 eleq1 ⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( 𝑠 ∈ dom 𝐺 ↔ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) )
169 168 anbi2d ⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ dom 𝐺 ) ↔ ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) ) )
170 oveq1 ⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( 𝑠 + ( 𝑙 · 𝑇 ) ) = ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) )
171 170 eleq1d ⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( ( 𝑠 + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ↔ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) )
172 170 fveq2d ⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( 𝐺 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ) )
173 fveq2 ⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) )
174 172 173 eqeq12d ⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( ( 𝐺 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ 𝑠 ) ↔ ( 𝐺 ‘ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) ) )
175 171 174 anbi12d ⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( ( ( 𝑠 + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ 𝑠 ) ) ↔ ( ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) ) ) )
176 169 175 imbi12d ⊢ ( 𝑠 = ( 𝑡 − ( 𝑙 · 𝑇 ) ) → ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ dom 𝐺 ) → ( ( 𝑠 + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ 𝑠 ) ) ) ↔ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → ( ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) ) ) ) )
177 ax-resscn ⊢ ℝ ⊆ ℂ
178 177 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
179 1 178 fssd ⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℂ )
180 179 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) → 𝐹 : ℝ ⟶ ℂ )
181 125 adantl ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) → 𝑙 ∈ ℝ )
182 129 adantr ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) → 𝑇 ∈ ℝ )
183 181 182 remulcld ⊢ ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) → ( 𝑙 · 𝑇 ) ∈ ℝ )
184 179 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℂ )
185 129 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) → 𝑇 ∈ ℝ )
186 simplr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) → 𝑙 ∈ ℤ )
187 simpr ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) → 𝑠 ∈ ℝ )
188 9 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
189 184 185 186 187 188 fperiodmul ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑠 ) )
190 180 183 189 2 fperdvper ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑠 ∈ dom 𝐺 ) → ( ( 𝑠 + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑠 + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ 𝑠 ) ) )
191 167 176 190 vtocl ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → ( ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ) = ( 𝐺 ‘ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ) ) )
192 191 simpld ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 )
193 192 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) + ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 )
194 166 193 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) ∧ ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 ) → 𝑡 ∈ dom 𝐺 )
195 194 ex ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ℝ ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺 ) )
196 156 195 sylan2 ⊢ ( ( ( 𝜑 ∧ 𝑙 ∈ ℤ ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺 ) )
197 196 adantlrl ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺 ) )
198 197 3adantl3 ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( ( 𝑡 − ( 𝑙 · 𝑇 ) ) ∈ dom 𝐺 → 𝑡 ∈ dom 𝐺 ) )
199 155 198 mpd ⊢ ( ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) ∧ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑡 ∈ dom 𝐺 )
200 199 ralrimiva ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ∀ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) 𝑡 ∈ dom 𝐺 )
201 dfss3 ⊢ ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ dom 𝐺 ↔ ∀ 𝑡 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) 𝑡 ∈ dom 𝐺 )
202 200 201 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) ∧ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) ) → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ dom 𝐺 )
203 202 3exp ⊢ ( 𝜑 → ( ( 𝑖 ∈ ( 0 ..^ 𝑀 ) ∧ 𝑙 ∈ ℤ ) → ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ dom 𝐺 ) ) )
204 203 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑖 ∈ ( 0 ..^ 𝑀 ) ∃ 𝑙 ∈ ℤ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ ( ( ( 𝑄 ‘ 𝑖 ) + ( 𝑙 · 𝑇 ) ) (,) ( ( 𝑄 ‘ ( 𝑖 + 1 ) ) + ( 𝑙 · 𝑇 ) ) ) → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ dom 𝐺 ) )
205 82 204 mpd ⊢ ( 𝜑 → ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ⊆ dom 𝐺 )
206 205 sselda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → 𝑠 ∈ dom 𝐺 )
207 206 iftrued ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ 𝑠 ) )
208 41 207 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) → ( 𝐺 ‘ 𝑠 ) = ( 𝐻 ‘ 𝑠 ) )
209 208 mpteq2dva ⊢ ( 𝜑 → ( 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐺 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
210 28 a1i ⊢ ( 𝜑 → dom 𝐺 = dom ( ℝ D 𝐹 ) )
211 210 feq2d ⊢ ( 𝜑 → ( 𝐺 : dom 𝐺 ⟶ ℝ ↔ 𝐺 : dom ( ℝ D 𝐹 ) ⟶ ℝ ) )
212 25 211 mpbird ⊢ ( 𝜑 → 𝐺 : dom 𝐺 ⟶ ℝ )
213 212 205 feqresmpt ⊢ ( 𝜑 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
214 38 15 fmptd ⊢ ( 𝜑 → 𝐻 : ℝ ⟶ ℝ )
215 214 17 feqresmpt ⊢ ( 𝜑 → ( 𝐻 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
216 209 213 215 3eqtr4d ⊢ ( 𝜑 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) = ( 𝐻 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) )
217 214 178 fssd ⊢ ( 𝜑 → 𝐻 : ℝ ⟶ ℂ )
218 15 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → 𝐻 = ( 𝑠 ∈ ℝ ↦ if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ) )
219 eleq1 ⊢ ( 𝑠 = ( 𝑥 + 𝑇 ) → ( 𝑠 ∈ dom 𝐺 ↔ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) )
220 fveq2 ⊢ ( 𝑠 = ( 𝑥 + 𝑇 ) → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
221 219 220 ifbieq1d ⊢ ( 𝑠 = ( 𝑥 + 𝑇 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) )
222 179 129 9 2 fperdvper ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐺 ‘ 𝑥 ) ) )
223 222 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝑥 + 𝑇 ) ∈ dom 𝐺 )
224 223 iftrued ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
225 221 224 sylan9eqr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) ∧ 𝑠 = ( 𝑥 + 𝑇 ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
226 225 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) ∧ 𝑠 = ( 𝑥 + 𝑇 ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
227 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
228 129 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℝ )
229 227 228 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + 𝑇 ) ∈ ℝ )
230 229 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝑥 + 𝑇 ) ∈ ℝ )
231 212 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → 𝐺 : dom 𝐺 ⟶ ℝ )
232 223 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝑥 + 𝑇 ) ∈ dom 𝐺 )
233 231 232 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ∈ ℝ )
234 218 226 230 233 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
235 222 simprd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐺 ‘ 𝑥 ) )
236 235 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐺 ‘ 𝑥 ) )
237 eleq1 ⊢ ( 𝑠 = 𝑥 → ( 𝑠 ∈ dom 𝐺 ↔ 𝑥 ∈ dom 𝐺 ) )
238 fveq2 ⊢ ( 𝑠 = 𝑥 → ( 𝐺 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑥 ) )
239 237 238 ifbieq1d ⊢ ( 𝑠 = 𝑥 → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) )
240 239 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) ∧ 𝑠 = 𝑥 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) )
241 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → 𝑥 ∈ ℝ )
242 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → 𝑥 ∈ dom 𝐺 )
243 242 iftrued ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) = ( 𝐺 ‘ 𝑥 ) )
244 212 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
245 243 244 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ dom 𝐺 ) → if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) ∈ ℝ )
246 245 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) ∈ ℝ )
247 218 240 241 246 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ 𝑥 ) = if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) )
248 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → 𝑥 ∈ dom 𝐺 )
249 248 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) = ( 𝐺 ‘ 𝑥 ) )
250 247 249 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐻 ‘ 𝑥 ) )
251 234 236 250 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐻 ‘ 𝑥 ) )
252 229 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝑥 + 𝑇 ) ∈ ℂ )
253 228 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑇 ∈ ℂ )
254 252 253 negsubd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 + 𝑇 ) + - 𝑇 ) = ( ( 𝑥 + 𝑇 ) − 𝑇 ) )
255 227 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℂ )
256 255 253 pncand ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 + 𝑇 ) − 𝑇 ) = 𝑥 )
257 254 256 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 = ( ( 𝑥 + 𝑇 ) + - 𝑇 ) )
258 257 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → 𝑥 = ( ( 𝑥 + 𝑇 ) + - 𝑇 ) )
259 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( 𝑥 + 𝑇 ) ∈ dom 𝐺 )
260 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → 𝜑 )
261 260 259 jca ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( 𝜑 ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) )
262 eleq1 ⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( 𝑦 ∈ dom 𝐺 ↔ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) )
263 262 anbi2d ⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐺 ) ↔ ( 𝜑 ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) ) )
264 oveq1 ⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( 𝑦 + - 𝑇 ) = ( ( 𝑥 + 𝑇 ) + - 𝑇 ) )
265 264 eleq1d ⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( ( 𝑦 + - 𝑇 ) ∈ dom 𝐺 ↔ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 ) )
266 264 fveq2d ⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( 𝐺 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) )
267 fveq2 ⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) )
268 266 267 eqeq12d ⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( ( 𝐺 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ) )
269 265 268 anbi12d ⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( ( ( 𝑦 + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ) ) )
270 263 269 imbi12d ⊢ ( 𝑦 = ( 𝑥 + 𝑇 ) → ( ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐺 ) → ( ( 𝑦 + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( ( 𝜑 ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ) ) ) )
271 129 renegcld ⊢ ( 𝜑 → - 𝑇 ∈ ℝ )
272 161 mulm1d ⊢ ( 𝜑 → ( - 1 · 𝑇 ) = - 𝑇 )
273 272 eqcomd ⊢ ( 𝜑 → - 𝑇 = ( - 1 · 𝑇 ) )
274 273 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → - 𝑇 = ( - 1 · 𝑇 ) )
275 274 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝑦 + - 𝑇 ) = ( 𝑦 + ( - 1 · 𝑇 ) ) )
276 275 fveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐹 ‘ ( 𝑦 + ( - 1 · 𝑇 ) ) ) )
277 179 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝐹 : ℝ ⟶ ℂ )
278 129 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑇 ∈ ℝ )
279 1zzd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 1 ∈ ℤ )
280 279 znegcld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → - 1 ∈ ℤ )
281 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
282 9 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐹 ‘ 𝑥 ) )
283 277 278 280 281 282 fperiodmul ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + ( - 1 · 𝑇 ) ) ) = ( 𝐹 ‘ 𝑦 ) )
284 276 283 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( 𝐹 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐹 ‘ 𝑦 ) )
285 179 271 284 2 fperdvper ⊢ ( ( 𝜑 ∧ 𝑦 ∈ dom 𝐺 ) → ( ( 𝑦 + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( 𝑦 + - 𝑇 ) ) = ( 𝐺 ‘ 𝑦 ) ) )
286 270 285 vtoclg ⊢ ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 → ( ( 𝜑 ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ) ) )
287 259 261 286 sylc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 ∧ ( 𝐺 ‘ ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ) = ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) ) )
288 287 simpld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → ( ( 𝑥 + 𝑇 ) + - 𝑇 ) ∈ dom 𝐺 )
289 258 288 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 ) → 𝑥 ∈ dom 𝐺 )
290 289 stoic1a ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ¬ ( 𝑥 + 𝑇 ) ∈ dom 𝐺 )
291 290 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) = 0 )
292 15 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → 𝐻 = ( 𝑠 ∈ ℝ ↦ if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ) )
293 221 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) ∧ 𝑠 = ( 𝑥 + 𝑇 ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) )
294 229 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ( 𝑥 + 𝑇 ) ∈ ℝ )
295 0red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → 0 ∈ ℝ )
296 291 295 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) ∈ ℝ )
297 292 293 294 296 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ ( 𝑥 + 𝑇 ) ) = if ( ( 𝑥 + 𝑇 ) ∈ dom 𝐺 , ( 𝐺 ‘ ( 𝑥 + 𝑇 ) ) , 0 ) )
298 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ¬ 𝑥 ∈ dom 𝐺 )
299 298 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → if ( 𝑥 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑥 ) , 0 ) = 0 )
300 239 299 sylan9eqr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) ∧ 𝑠 = 𝑥 ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = 0 )
301 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → 𝑥 ∈ ℝ )
302 292 300 301 295 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ 𝑥 ) = 0 )
303 291 297 302 3eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) ∧ ¬ 𝑥 ∈ dom 𝐺 ) → ( 𝐻 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐻 ‘ 𝑥 ) )
304 251 303 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐻 ‘ ( 𝑥 + 𝑇 ) ) = ( 𝐻 ‘ 𝑥 ) )
305 elioore ⊢ ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) → 𝑠 ∈ ℝ )
306 305 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑠 ∈ ℝ )
307 305 38 sylan2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) ∈ ℝ )
308 306 307 40 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
309 308 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) )
310 94 iftrued ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → if ( 𝑠 ∈ dom 𝐺 , ( 𝐺 ‘ 𝑠 ) , 0 ) = ( 𝐺 ‘ 𝑠 ) )
311 309 310 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → ( 𝐻 ‘ 𝑠 ) = ( 𝐺 ‘ 𝑠 ) )
312 311 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
313 214 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐻 : ℝ ⟶ ℝ )
314 ioossre ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ
315 314 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ℝ )
316 313 315 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐻 ‘ 𝑠 ) ) )
317 212 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐺 : dom 𝐺 ⟶ ℝ )
318 317 97 feqresmpt ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝑠 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ↦ ( 𝐺 ‘ 𝑠 ) ) )
319 312 316 318 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) = ( 𝐺 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) )
320 319 10 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐻 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )
321 eqid ⊢ ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } ) = ( 𝑚 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑚 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = 𝐶 ∧ ( 𝑝 ‘ 𝑚 ) = 𝐷 ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑚 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
322 oveq1 ⊢ ( 𝑧 = 𝑦 → ( 𝑧 + ( 𝑙 · 𝑇 ) ) = ( 𝑦 + ( 𝑙 · 𝑇 ) ) )
323 322 eleq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
324 323 rexbidv ⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ↔ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 ) )
325 324 cbvrabv ⊢ { 𝑧 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } = { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 }
326 325 uneq2i ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑧 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } )
327 326 eqcomi ⊢ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑧 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑧 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } )
328 60 fveq2i ⊢ ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) = ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) )
329 328 oveq1i ⊢ ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) = ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 )
330 isoeq5 ⊢ ( ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) = ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) → ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
331 67 330 ax-mp ⊢ ( 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
332 331 iotabii ⊢ ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ ℎ ∈ ℤ ( 𝑦 + ( ℎ · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
333 isoeq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ↔ 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) )
334 333 cbviotavw ⊢ ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) ) = ( ℩ 𝑔 𝑔 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
335 332 334 14 3eqtr4ri ⊢ 𝑉 = ( ℩ 𝑓 𝑓 Isom < , < ( ( 0 ... ( ( ♯ ‘ ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑘 ∈ ℤ ( 𝑦 + ( 𝑘 · 𝑇 ) ) ∈ ran 𝑄 } ) ) − 1 ) ) , ( { 𝐶 , 𝐷 } ∪ { 𝑦 ∈ ( 𝐶 [,] 𝐷 ) ∣ ∃ 𝑙 ∈ ℤ ( 𝑦 + ( 𝑙 · 𝑇 ) ) ∈ ran 𝑄 } ) ) )
336 id ⊢ ( 𝑣 = 𝑥 → 𝑣 = 𝑥 )
337 oveq2 ⊢ ( 𝑣 = 𝑥 → ( 𝐵 − 𝑣 ) = ( 𝐵 − 𝑥 ) )
338 337 oveq1d ⊢ ( 𝑣 = 𝑥 → ( ( 𝐵 − 𝑣 ) / 𝑇 ) = ( ( 𝐵 − 𝑥 ) / 𝑇 ) )
339 338 fveq2d ⊢ ( 𝑣 = 𝑥 → ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) = ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) )
340 339 oveq1d ⊢ ( 𝑣 = 𝑥 → ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) = ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) )
341 336 340 oveq12d ⊢ ( 𝑣 = 𝑥 → ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) = ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
342 341 cbvmptv ⊢ ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑥 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑥 ) / 𝑇 ) ) · 𝑇 ) ) )
343 eqeq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 = 𝐵 ↔ 𝑧 = 𝐵 ) )
344 id ⊢ ( 𝑢 = 𝑧 → 𝑢 = 𝑧 )
345 343 344 ifbieq2d ⊢ ( 𝑢 = 𝑧 → if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) = if ( 𝑧 = 𝐵 , 𝐴 , 𝑧 ) )
346 345 cbvmptv ⊢ ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) = ( 𝑧 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑧 = 𝐵 , 𝐴 , 𝑧 ) )
347 eqid ⊢ ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) = ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) )
348 eqid ⊢ ( 𝐻 ↾ ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) (,) ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) = ( 𝐻 ↾ ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) (,) ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) )
349 eqid ⊢ ( 𝑧 ∈ ( ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) + ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) (,) ( ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ) ↦ ( ( 𝐻 ↾ ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) (,) ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑧 − ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ) ) = ( 𝑧 ∈ ( ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) + ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) (,) ( ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) + ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ) ↦ ( ( 𝐻 ↾ ( ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ 𝐽 ) ) ) (,) ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ‘ ( 𝑧 − ( ( 𝑉 ‘ ( 𝐽 + 1 ) ) − ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ) ) )
350 fveq2 ⊢ ( 𝑖 = 𝑡 → ( 𝑄 ‘ 𝑖 ) = ( 𝑄 ‘ 𝑡 ) )
351 350 breq1d ⊢ ( 𝑖 = 𝑡 → ( ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ↔ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ) )
352 351 cbvrabv ⊢ { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } = { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) }
353 fveq2 ⊢ ( 𝑤 = 𝑥 → ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) = ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) )
354 353 fveq2d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) = ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) )
355 354 eqcomd ⊢ ( 𝑤 = 𝑥 → ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) = ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) )
356 355 breq2d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) ↔ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) ) )
357 356 rabbidv ⊢ ( 𝑤 = 𝑥 → { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } = { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) } )
358 352 357 eqtr2id ⊢ ( 𝑤 = 𝑥 → { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) } = { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } )
359 358 supeq1d ⊢ ( 𝑤 = 𝑥 → sup ( { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) } , ℝ , < ) = sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
360 359 cbvmptv ⊢ ( 𝑤 ∈ ℝ ↦ sup ( { 𝑡 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑡 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑤 ) ) } , ℝ , < ) ) = ( 𝑥 ∈ ℝ ↦ sup ( { 𝑖 ∈ ( 0 ..^ 𝑀 ) ∣ ( 𝑄 ‘ 𝑖 ) ≤ ( ( 𝑢 ∈ ( 𝐴 (,] 𝐵 ) ↦ if ( 𝑢 = 𝐵 , 𝐴 , 𝑢 ) ) ‘ ( ( 𝑣 ∈ ℝ ↦ ( 𝑣 + ( ( ⌊ ‘ ( ( 𝐵 − 𝑣 ) / 𝑇 ) ) · 𝑇 ) ) ) ‘ 𝑥 ) ) } , ℝ , < ) )
361 3 6 7 8 217 304 320 11 12 321 327 329 335 342 346 13 347 348 349 360 fourierdlem90 ⊢ ( 𝜑 → ( 𝐻 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )
362 216 361 eqeltrd ⊢ ( 𝜑 → ( 𝐺 ↾ ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) ) ∈ ( ( ( 𝑉 ‘ 𝐽 ) (,) ( 𝑉 ‘ ( 𝐽 + 1 ) ) ) –cn→ ℂ ) )