Theorem imo72b2lem1

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

	Ref	Expression
Hypotheses	imo72b2lem1.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
	imo72b2lem1.7	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ≠ 0 )
	imo72b2lem1.6	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 1 )
Assertion	imo72b2lem1	⊢ ( 𝜑 → 0 < sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		imo72b2lem1.1	⊢ ( 𝜑 → 𝐹 : ℝ ⟶ ℝ )
2		imo72b2lem1.7	⊢ ( 𝜑 → ∃ 𝑥 ∈ ℝ ( 𝐹 ‘ 𝑥 ) ≠ 0 )
3		imo72b2lem1.6	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 1 )
4		imaco	⊢ ( ( abs ∘ 𝐹 ) “ ℝ ) = ( abs “ ( 𝐹 “ ℝ ) )
5		imassrn	⊢ ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ran ( abs ∘ 𝐹 )
6		absf	⊢ abs : ℂ ⟶ ℝ
7	6	a1i	⊢ ( 𝜑 → abs : ℂ ⟶ ℝ )
8		ax-resscn	⊢ ℝ ⊆ ℂ
9	8	a1i	⊢ ( 𝜑 → ℝ ⊆ ℂ )
10	7 9	fssresd	⊢ ( 𝜑 → ( abs ↾ ℝ ) : ℝ ⟶ ℝ )
11	1 10	fco2d	⊢ ( 𝜑 → ( abs ∘ 𝐹 ) : ℝ ⟶ ℝ )
12	11	frnd	⊢ ( 𝜑 → ran ( abs ∘ 𝐹 ) ⊆ ℝ )
13	5 12	sstrid	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) “ ℝ ) ⊆ ℝ )
14	4 13	eqsstrrid	⊢ ( 𝜑 → ( abs “ ( 𝐹 “ ℝ ) ) ⊆ ℝ )
15		0re	⊢ 0 ∈ ℝ
16	15	ne0ii	⊢ ℝ ≠ ∅
17	16	a1i	⊢ ( 𝜑 → ℝ ≠ ∅ )
18	17 11	wnefimgd	⊢ ( 𝜑 → ( ( abs ∘ 𝐹 ) “ ℝ ) ≠ ∅ )
19	4 18	eqnetrrid	⊢ ( 𝜑 → ( abs “ ( 𝐹 “ ℝ ) ) ≠ ∅ )
20		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑐 = 1 ) → 𝑐 = 1 )
22	21	breq2d	⊢ ( ( 𝜑 ∧ 𝑐 = 1 ) → ( 𝑡 ≤ 𝑐 ↔ 𝑡 ≤ 1 ) )
23	22	ralbidv	⊢ ( ( 𝜑 ∧ 𝑐 = 1 ) → ( ∀ 𝑡 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑡 ≤ 𝑐 ↔ ∀ 𝑡 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑡 ≤ 1 ) )
24	1 3	extoimad	⊢ ( 𝜑 → ∀ 𝑡 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑡 ≤ 1 )
25	20 23 24	rspcedvd	⊢ ( 𝜑 → ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 𝑡 ≤ 𝑐 )
26		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
27	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → 𝐹 : ℝ ⟶ ℝ )
28		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → 𝑥 ∈ ℝ )
29	27 28	fvco3d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
30	11	funfvima2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( abs ∘ 𝐹 ) “ ℝ ) )
31	30	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) ∈ ( ( abs ∘ 𝐹 ) “ ℝ ) )
32	31 4	eleqtrdi	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) ∈ ( abs “ ( 𝐹 “ ℝ ) ) )
33	29 32	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ( abs “ ( 𝐹 “ ℝ ) ) )
34		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) ∧ 𝑧 = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑧 = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
35	34	breq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) ∧ 𝑧 = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( 0 < 𝑧 ↔ 0 < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
36	1	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
37	36	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℝ )
38	37	recnd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ℂ )
39		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → ( 𝐹 ‘ 𝑥 ) ≠ 0 )
40	38 39	absrpcld	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ ℝ+ )
41	40	rpgt0d	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → 0 < ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
42	33 35 41	rspcedvd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐹 ‘ 𝑥 ) ≠ 0 ) ) → ∃ 𝑧 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 0 < 𝑧 )
43	2 42	rexlimddv	⊢ ( 𝜑 → ∃ 𝑧 ∈ ( abs “ ( 𝐹 “ ℝ ) ) 0 < 𝑧 )
44	14 19 25 26 43	suprlubrd	⊢ ( 𝜑 → 0 < sup ( ( abs “ ( 𝐹 “ ℝ ) ) , ℝ , < ) )