Metamath Proof Explorer

Theorem fourierdlem8

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

Ref Expression
Hypotheses fourierdlem8.a ⊢ φ → A ∈ ℝ *
fourierdlem8.b ⊢ φ → B ∈ ℝ *
fourierdlem8.q ⊢ φ → Q : 0 … M ⟶ A B
fourierdlem8.i ⊢ φ → I ∈ 0 ..^ M
Assertion fourierdlem8 ⊢ φ → Q ⁡ I Q ⁡ I + 1 ⊆ A B

Proof

Step Hyp Ref Expression
1 fourierdlem8.a ⊢ φ → A ∈ ℝ *
2 fourierdlem8.b ⊢ φ → B ∈ ℝ *
3 fourierdlem8.q ⊢ φ → Q : 0 … M ⟶ A B
4 fourierdlem8.i ⊢ φ → I ∈ 0 ..^ M
5 1 adantr ⊢ φ ∧ x ∈ Q ⁡ I Q ⁡ I + 1 → A ∈ ℝ *
6 2 adantr ⊢ φ ∧ x ∈ Q ⁡ I Q ⁡ I + 1 → B ∈ ℝ *
7 3 adantr ⊢ φ ∧ x ∈ Q ⁡ I Q ⁡ I + 1 → Q : 0 … M ⟶ A B
8 4 adantr ⊢ φ ∧ x ∈ Q ⁡ I Q ⁡ I + 1 → I ∈ 0 ..^ M
9 simpr ⊢ φ ∧ x ∈ Q ⁡ I Q ⁡ I + 1 → x ∈ Q ⁡ I Q ⁡ I + 1
10 5 6 7 8 9 fourierdlem1 ⊢ φ ∧ x ∈ Q ⁡ I Q ⁡ I + 1 → x ∈ A B
11 10 ralrimiva ⊢ φ → ∀ x ∈ Q ⁡ I Q ⁡ I + 1 x ∈ A B
12 dfss3 ⊢ Q ⁡ I Q ⁡ I + 1 ⊆ A B ↔ ∀ x ∈ Q ⁡ I Q ⁡ I + 1 x ∈ A B
13 11 12 sylibr ⊢ φ → Q ⁡ I Q ⁡ I + 1 ⊆ A B