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

Metamath Proof Explorer

Theorem ivthlem1

Description: Lemma for ivth . The set S of all x values with ( Fx ) less than U is lower bounded by A and upper bounded by B . (Contributed by Mario Carneiro, 17-Jun-2014)

Ref Expression
Hypotheses ivth.1 ⊢ φ → A ∈ ℝ
ivth.2 ⊢ φ → B ∈ ℝ
ivth.3 ⊢ φ → U ∈ ℝ
ivth.4 ⊢ φ → A < B
ivth.5 ⊢ φ → A B ⊆ D
ivth.7 ⊢ φ → F : D ⟶cn ℂ
ivth.8 ⊢ φ ∧ x ∈ A B → F ⁡ x ∈ ℝ
ivth.9 ⊢ φ → F ⁡ A < U ∧ U < F ⁡ B
ivth.10 ⊢ S = x ∈ A B | F ⁡ x ≤ U
Assertion ivthlem1 ⊢ φ → A ∈ S ∧ ∀ z ∈ S z ≤ B

Proof

Step Hyp Ref Expression
1 ivth.1 ⊢ φ → A ∈ ℝ
2 ivth.2 ⊢ φ → B ∈ ℝ
3 ivth.3 ⊢ φ → U ∈ ℝ
4 ivth.4 ⊢ φ → A < B
5 ivth.5 ⊢ φ → A B ⊆ D
6 ivth.7 ⊢ φ → F : D ⟶cn ℂ
7 ivth.8 ⊢ φ ∧ x ∈ A B → F ⁡ x ∈ ℝ
8 ivth.9 ⊢ φ → F ⁡ A < U ∧ U < F ⁡ B
9 ivth.10 ⊢ S = x ∈ A B | F ⁡ x ≤ U
10 1 rexrd ⊢ φ → A ∈ ℝ *
11 2 rexrd ⊢ φ → B ∈ ℝ *
12 1 2 4 ltled ⊢ φ → A ≤ B
13 lbicc2 ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ A ≤ B → A ∈ A B
14 10 11 12 13 syl3anc ⊢ φ → A ∈ A B
15 fveq2 ⊢ x = A → F ⁡ x = F ⁡ A
16 15 eleq1d ⊢ x = A → F ⁡ x ∈ ℝ ↔ F ⁡ A ∈ ℝ
17 7 ralrimiva ⊢ φ → ∀ x ∈ A B F ⁡ x ∈ ℝ
18 16 17 14 rspcdva ⊢ φ → F ⁡ A ∈ ℝ
19 8 simpld ⊢ φ → F ⁡ A < U
20 18 3 19 ltled ⊢ φ → F ⁡ A ≤ U
21 15 breq1d ⊢ x = A → F ⁡ x ≤ U ↔ F ⁡ A ≤ U
22 21 9 elrab2 ⊢ A ∈ S ↔ A ∈ A B ∧ F ⁡ A ≤ U
23 14 20 22 sylanbrc ⊢ φ → A ∈ S
24 9 ssrab3 ⊢ S ⊆ A B
25 24 sseli ⊢ z ∈ S → z ∈ A B
26 iccleub ⊢ A ∈ ℝ * ∧ B ∈ ℝ * ∧ z ∈ A B → z ≤ B
27 26 3expia ⊢ A ∈ ℝ * ∧ B ∈ ℝ * → z ∈ A B → z ≤ B
28 10 11 27 syl2anc ⊢ φ → z ∈ A B → z ≤ B
29 25 28 syl5 ⊢ φ → z ∈ S → z ≤ B
30 29 ralrimiv ⊢ φ → ∀ z ∈ S z ≤ B
31 23 30 jca ⊢ φ → A ∈ S ∧ ∀ z ∈ S z ≤ B