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	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑆 ∧ ∀ 𝑧 ∈ 𝑆 𝑧 ≤ 𝐵 ) )