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

Metamath Proof Explorer

Theorem fourierdlem27

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

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

Proof

Step Hyp Ref Expression
1 fourierdlem27.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
2 fourierdlem27.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
3 fourierdlem27.q ⊢ ( 𝜑 → 𝑄 : ( 0 ... 𝑀 ) ⟶ ( 𝐴 [,] 𝐵 ) )
4 fourierdlem27.i ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ..^ 𝑀 ) )
5 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝐴 ∈ ℝ* )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝐵 ∈ ℝ* )
7 elioore ⊢ ( 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) → 𝑥 ∈ ℝ )
8 7 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ ℝ )
9 iccssxr ⊢ ( 𝐴 [,] 𝐵 ) ⊆ ℝ*
10 elfzofz ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → 𝐼 ∈ ( 0 ... 𝑀 ) )
11 4 10 syl ⊢ ( 𝜑 → 𝐼 ∈ ( 0 ... 𝑀 ) )
12 3 11 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ( 𝐴 [,] 𝐵 ) )
13 9 12 sselid ⊢ ( 𝜑 → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) ∈ ℝ* )
15 8 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ ℝ* )
16 iccgelb ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑄 ‘ 𝐼 ) ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐴 ≤ ( 𝑄 ‘ 𝐼 ) )
17 1 2 12 16 syl3anc ⊢ ( 𝜑 → 𝐴 ≤ ( 𝑄 ‘ 𝐼 ) )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝐴 ≤ ( 𝑄 ‘ 𝐼 ) )
19 fzofzp1 ⊢ ( 𝐼 ∈ ( 0 ..^ 𝑀 ) → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
20 4 19 syl ⊢ ( 𝜑 → ( 𝐼 + 1 ) ∈ ( 0 ... 𝑀 ) )
21 3 20 ffvelcdmd ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) )
22 9 21 sselid ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* )
24 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) )
25 ioogtlb ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) < 𝑥 )
26 14 23 24 25 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ 𝐼 ) < 𝑥 )
27 5 14 15 18 26 xrlelttrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝐴 < 𝑥 )
28 iooltub ⊢ ( ( ( 𝑄 ‘ 𝐼 ) ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ℝ* ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
29 14 23 24 28 syl3anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 < ( 𝑄 ‘ ( 𝐼 + 1 ) ) )
30 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ ( 𝑄 ‘ ( 𝐼 + 1 ) ) ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ 𝐵 )
31 1 2 21 30 syl3anc ⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ 𝐵 )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → ( 𝑄 ‘ ( 𝐼 + 1 ) ) ≤ 𝐵 )
33 15 23 6 29 32 xrltletrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 < 𝐵 )
34 5 6 8 27 33 eliood ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ) → 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
35 34 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
36 dfss3 ⊢ ( ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( 𝐴 (,) 𝐵 ) ↔ ∀ 𝑥 ∈ ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) 𝑥 ∈ ( 𝐴 (,) 𝐵 ) )
37 35 36 sylibr ⊢ ( 𝜑 → ( ( 𝑄 ‘ 𝐼 ) (,) ( 𝑄 ‘ ( 𝐼 + 1 ) ) ) ⊆ ( 𝐴 (,) 𝐵 ) )