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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
ivth.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
ivth.3 ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
ivth.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
ivth.5 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
ivth.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
ivth.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
ivth.9 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) )
ivth.10 ⊢ 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑈 }
Assertion ivthlem1 ( 𝜑 → ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 ivth.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 ivth.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 ivth.3 ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
4 ivth.4 ⊢ ( 𝜑 → 𝐴 < 𝐵 )
5 ivth.5 ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) ⊆ 𝐷 )
6 ivth.7 ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐷 –cn→ ℂ ) )
7 ivth.8 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
8 ivth.9 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐴 ) < 𝑈 ∧ 𝑈 < ( 𝐹 ‘ 𝐵 ) ) )
9 ivth.10 ⊢ 𝑆 = { 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ∣ ( 𝐹 ‘ 𝑥 ) ≤ 𝑈 }
10 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
11 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
12 1 2 4 ltled ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
13 lbicc2 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐴 ≤ 𝐵 ) → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
14 10 11 12 13 syl3anc ⊢ ( 𝜑 → 𝐴 ∈ ( 𝐴 [,] 𝐵 ) )
15 fveq2 ⊢ ( 𝑥 = 𝐴 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐴 ) )
16 15 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝐴 ) ∈ ℝ ) )
17 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
18 16 17 14 rspcdva ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ∈ ℝ )
19 8 simpld ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) < 𝑈 )
20 18 3 19 ltled ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐴 ) ≤ 𝑈 )
21 15 breq1d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝑥 ) ≤ 𝑈 ↔ ( 𝐹 ‘ 𝐴 ) ≤ 𝑈 ) )
22 21 9 elrab2 ⊢ ( 𝐴 ∈ 𝑆 ↔ ( 𝐴 ∈ ( 𝐴 [,] 𝐵 ) ∧ ( 𝐹 ‘ 𝐴 ) ≤ 𝑈 ) )
23 14 20 22 sylanbrc ⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
24 9 ssrab3 ⊢ 𝑆 ⊆ ( 𝐴 [,] 𝐵 )
25 24 sseli ⊢ ( 𝑧 ∈ 𝑆 → 𝑧 ∈ ( 𝐴 [,] 𝐵 ) )
26 iccleub ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑧 ≤ 𝐵 )
27 26 3expia ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) → 𝑧 ≤ 𝐵 ) )
28 10 11 27 syl2anc ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) → 𝑧 ≤ 𝐵 ) )
29 25 28 syl5 ⊢ ( 𝜑 → ( 𝑧 ∈ 𝑆 → 𝑧 ≤ 𝐵 ) )
30 29 ralrimiv ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 )
31 23 30 jca ⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) )