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 ffvelrnd ( 𝜑 → ( 𝑄𝐼 ) ∈ ( 𝐴 [,] 𝐵 ) )
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 ffvelrnd ( 𝜑 → ( 𝑄 ‘ ( 𝐼 + 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 ) ) ) ⊆ ( 𝐴 (,) 𝐵 ) )