Metamath Proof Explorer

Theorem fourierdlem38

Description: The function F is continuous on every interval induced by the partition Q . (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem38.cn ⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) )
fourierdlem38.p ⊢ 𝑃 = ( 𝑛 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑛 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑛 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑛 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
fourierdlem38.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
fourierdlem38.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
fourierdlem38.h ⊢ 𝐻 = ( 𝐴 ∪ ( ( - π [,] π ) ∖ dom 𝐹 ) )
fourierdlem38.ranq ⊢ ( 𝜑 → ran 𝑄 = 𝐻 )
Assertion fourierdlem38 ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 fourierdlem38.cn ⊢ ( 𝜑 → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) )
2 fourierdlem38.p ⊢ 𝑃 = ( 𝑛 ∈ ℕ ↦ { 𝑝 ∈ ( ℝ ↑m ( 0 ... 𝑛 ) ) ∣ ( ( ( 𝑝 ‘ 0 ) = - π ∧ ( 𝑝 ‘ 𝑛 ) = π ) ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑛 ) ( 𝑝 ‘ 𝑖 ) < ( 𝑝 ‘ ( 𝑖 + 1 ) ) ) } )
3 fourierdlem38.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
4 fourierdlem38.q ⊢ ( 𝜑 → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
5 fourierdlem38.h ⊢ 𝐻 = ( 𝐴 ∪ ( ( - π [,] π ) ∖ dom 𝐹 ) )
6 fourierdlem38.ranq ⊢ ( 𝜑 → ran 𝑄 = 𝐻 )
7 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
8 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝜑 )
9 ioossicc ⊢ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) )
10 pire ⊢ π ∈ ℝ
11 10 renegcli ⊢ - π ∈ ℝ
12 11 rexri ⊢ - π ∈ ℝ*
13 12 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → - π ∈ ℝ* )
14 10 rexri ⊢ π ∈ ℝ*
15 14 a1i ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → π ∈ ℝ* )
16 2 3 4 fourierdlem15 ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( - π [,] π ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
19 13 15 17 18 fourierdlem8 ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) [,] ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
20 9 19 sstrid ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ ( - π [,] π ) )
21 20 sselda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ ( - π [,] π ) )
22 21 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( - π [,] π ) )
23 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → ¬ 𝑥 ∈ dom 𝐹 )
24 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑖 ∈ ( 0 ..^ 𝑀 ) )
25 3 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑀 ∈ ℕ )
26 4 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑄 ∈ ( 𝑃 ‘ 𝑀 ) )
27 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( - π [,] π ) )
28 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → ¬ 𝑥 ∈ dom 𝐹 )
29 27 28 eldifd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( ( - π [,] π ) ∖ dom 𝐹 ) )
30 elun2 ⊢ ( 𝑥 ∈ ( ( - π [,] π ) ∖ dom 𝐹 ) → 𝑥 ∈ ( 𝐴 ∪ ( ( - π [,] π ) ∖ dom 𝐹 ) ) )
31 29 30 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ( 𝐴 ∪ ( ( - π [,] π ) ∖ dom 𝐹 ) ) )
32 6 5 eqtr2di ⊢ ( 𝜑 → ( 𝐴 ∪ ( ( - π [,] π ) ∖ dom 𝐹 ) ) = ran 𝑄 )
33 32 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → ( 𝐴 ∪ ( ( - π [,] π ) ∖ dom 𝐹 ) ) = ran 𝑄 )
34 31 33 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → 𝑥 ∈ ran 𝑄 )
35 2 25 26 34 fourierdlem12 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( - π [,] π ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ¬ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
36 8 22 23 24 35 syl31anc ⊢ ( ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∧ ¬ 𝑥 ∈ dom 𝐹 ) → ¬ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) )
37 7 36 condan ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) → 𝑥 ∈ dom 𝐹 )
38 37 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 ∈ dom 𝐹 )
39 dfss3 ⊢ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 ↔ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) 𝑥 ∈ dom 𝐹 )
40 38 39 sylibr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 )
41 1 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) )
42 rescncf ⊢ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ⊆ dom 𝐹 → ( 𝐹 ∈ ( dom 𝐹 –cn→ ℂ ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) ) )
43 40 41 42 sylc ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 0 ..^ 𝑀 ) ) → ( 𝐹 ↾ ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) ) ∈ ( ( ( 𝑄 ‘ 𝑖 ) (,) ( 𝑄 ‘ ( 𝑖 + 1 ) ) ) –cn→ ℂ ) )