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

Metamath Proof Explorer

Theorem fourierdlem1

Description: A partition interval is a subset of the partitioned interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses fourierdlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
fourierdlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
fourierdlem1.q ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
fourierdlem1.i ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝑀 ) )
fourierdlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝑄 ‘ 𝐼 ) [,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
Assertion fourierdlem1 ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )

Proof

Step Hyp Ref Expression
1 fourierdlem1.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 fourierdlem1.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 fourierdlem1.q ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
4 fourierdlem1.i ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝑀 ) )
5 fourierdlem1.x ⊢ ( 𝜑 → 𝑋 ∈ ( ( 𝑄 ‘ 𝐼 ) [,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
6 iccssxr ⊢ ( ( 𝑄 ‘ 𝐼 ) [,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ℝ*
7 6 5 sselid ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
8 iccssxr ⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℝ*
9 elfzofz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 ∈ ( 0 ... 𝑀 ) )
10 4 9 syl ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝑀 ) )
11 3 10 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ( 𝐴 [,] 𝐵 ) )
12 8 11 sselid ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
13 iccgelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑄 ‘ 𝐼 ) ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 𝑄 ‘ 𝐼 ) )
14 1 2 11 13 syl3anc ⊢ ( 𝜑 → 𝐴 ≤ ( 𝑄 ‘ 𝐼 ) )
15 fzofzp1 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
16 4 15 syl ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
17 3 16 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
18 8 17 sselid ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
19 elicc4 ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ℝ* ) → ( 𝑋 ∈ ( ( 𝑄 ‘ 𝐼 ) [,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ↔ ( ( 𝑄 ‘ 𝐼 ) ≤ 𝑋 ∧ 𝑋 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
20 12 18 7 19 syl3anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( ( 𝑄 ‘ 𝐼 ) [,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ↔ ( ( 𝑄 ‘ 𝐼 ) ≤ 𝑋 ∧ 𝑋 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) )
21 5 20 mpbid ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) ≤ 𝑋 ∧ 𝑋 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
22 21 simpld ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ≤ 𝑋 )
23 1 12 7 14 22 xrletrd ⊢ ( 𝜑 → 𝐴 ≤ 𝑋 )
24 iccleub ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑋 ∈ ( ( 𝑄 ‘ 𝐼 ) [,] ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑋 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
25 12 18 5 24 syl3anc ⊢ ( 𝜑 → 𝑋 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
26 elicc4 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ) → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ 𝐵 ) ) )
27 1 2 18 26 syl3anc ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝐴 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ 𝐵 ) ) )
28 17 27 mpbid ⊢ ( 𝜑 → ( 𝐴 ≤ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ 𝐵 ) )
29 28 simprd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ 𝐵 )
30 7 18 2 25 29 xrletrd ⊢ ( 𝜑 → 𝑋 ≤ 𝐵 )
31 elicc1 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
32 1 2 31 syl2anc ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐴 [,] 𝐵 ) ↔ ( 𝑋 ∈ ℝ* ∧ 𝐴 ≤ 𝑋 ∧ 𝑋 ≤ 𝐵 ) ) )
33 7 23 30 32 mpbir3and ⊢ ( 𝜑 → 𝑋 ∈ ( 𝐴 [,] 𝐵 ) )