Theorem imo72b2lem2

Description: Lemma for imo72b2 . (Contributed by Stanislas Polu, 9-Mar-2020)

	Ref	Expression
Hypotheses	imo72b2lem2.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	imo72b2lem2.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	imo72b2lem2.3	⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝐶 )
Assertion	imo72b2lem2	⊢ ( 𝜑 → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ≤ 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		imo72b2lem2.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		imo72b2lem2.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3		imo72b2lem2.3	⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ≤ 𝐶 )
4		imaco	⊢ ( ( abs ∘ 𝐹 ) “ ℝ ) = ( abs “ ( 𝐹 “ ℝ ) )
5	4	eqcomi	⊢ ( abs “ ( 𝐹 “ ℝ ) ) = ( ( abs ∘ 𝐹 ) “ ℝ )
6		imassrn	⊢ ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ran ( abs ∘ 𝐹 )
7	6	a1i	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ran ( abs ∘ 𝐹 ) )
8		absf	⊢ abs : ℂ ⟶ ℝ
9	8	a1i	⊢ ( 𝜑 → abs : ℂ ⟶ ℝ )
10		ax-resscn	⊢ ℝ ⊆ ℂ
11	10	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
12	9 11	fssresd	⊢ ( 𝜑 → ( abs ↾ ℝ ) : ℝ ⟶ ℝ )
13	1 12	fco2d	⊢ ( 𝜑 → ( abs ∘ 𝐹 ) : ℝ ⟶ ℝ )
14	13	frnd	⊢ ( 𝜑 → ran ( abs ∘ 𝐹 ) ⊆ ℝ )
15	7 14	sstrd	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ℝ )
16	5 15	eqsstrid	⊢ ( 𝜑 → ( abs “ ( 𝐹 “ ℝ ) ) ⊆ ℝ )
17		0re	⊢ 0 ∈ ℝ
18	17	ne0ii	⊢ ℝ ≠ ∅
19	18	a1i	⊢ ( 𝜑 → ℝ ≠ ∅ )
20	19 13	wnefimgd	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) “ ℝ ) ≠ ∅ )
21	20	necomd	⊢ ( 𝜑 → ∅ ≠ ( ( abs ∘ 𝐹 ) “ ℝ ) )
22	5	a1i	⊢ ( 𝜑 → ( abs “ ( 𝐹 “ ℝ ) ) = ( ( abs ∘ 𝐹 ) “ ℝ ) )
23	21 22	neeqtrrd	⊢ ( 𝜑 → ∅ ≠ ( abs “ ( 𝐹 “ ℝ ) ) )
24	23	necomd	⊢ ( 𝜑 → ( abs “ ( 𝐹 “ ℝ ) ) ≠ ∅ )
25		simpr	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → 𝑐 = 𝐶 )
26	25	breq2d	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( 𝑣 ≤ 𝑐 ↔ 𝑣 ≤ 𝐶 ) )
27	26	ralbidv	⊢ ( ( 𝜑 ∧ 𝑐 = 𝐶 ) → ( ∀ 𝑣 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑣 ≤ 𝑐 ↔ ∀ 𝑣 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑣 ≤ 𝐶 ) )
28	1 3	extoimad	⊢ ( 𝜑 → ∀ 𝑣 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑣 ≤ 𝐶 )
29	2 27 28	rspcedvd	⊢ ( 𝜑 → ∃ 𝑐 ∈ ℝ ∀ 𝑣 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑣 ≤ 𝑐 )
30	1 3	extoimad	⊢ ( 𝜑 → ∀ 𝑡 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑡 ≤ 𝐶 )
31	16 24 29 2 30	suprleubrd	⊢ ( 𝜑 → sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) ≤ 𝐶 )