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 ) ) ) ⊆ ( 𝐴 (,) 𝐵 ) )

Metamath Proof Explorer

Theorem fourierdlem27

Proof