Metamath Proof Explorer

Theorem cncficcgt0

Description: A the absolute value of a continuous function on a closed interval, that is never 0, has a strictly positive lower bound. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses cncficcgt0.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐶 )
cncficcgt0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
cncficcgt0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
cncficcgt0.aleb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
cncficcgt0.fcn ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℝ ∖ { 0 } ) ) )
Assertion cncficcgt0 ( 𝜑 → ∃ 𝑦 ∈ ℝ+ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) 𝑦 ≤ ( abs ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 cncficcgt0.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐶 )
2 cncficcgt0.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
3 cncficcgt0.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4 cncficcgt0.aleb ⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
5 cncficcgt0.fcn ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℝ ∖ { 0 } ) ) )
6 cncff ⊢ ( 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℝ ∖ { 0 } ) ) → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ( ℝ ∖ { 0 } ) )
7 ffun ⊢ ( 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ( ℝ ∖ { 0 } ) → Fun 𝐹 )
8 5 6 7 3syl ⊢ ( 𝜑 → Fun 𝐹 )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → Fun 𝐹 )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑐 ∈ ( 𝐴 [,] 𝐵 ) )
11 5 6 syl ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ( ℝ ∖ { 0 } ) )
12 11 fdmd ⊢ ( 𝜑 → dom 𝐹 = ( 𝐴 [,] 𝐵 ) )
13 12 eqcomd ⊢ ( 𝜑 → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐴 [,] 𝐵 ) = dom 𝐹 )
15 10 14 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝑐 ∈ dom 𝐹 )
16 fvco ⊢ ( ( Fun 𝐹 ∧ 𝑐 ∈ dom 𝐹 ) → ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) = ( abs ‘ ( 𝐹 ‘ 𝑐 ) ) )
17 9 15 16 syl2anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) = ( abs ‘ ( 𝐹 ‘ 𝑐 ) ) )
18 11 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ( ℝ ∖ { 0 } ) )
19 18 eldifad ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℝ )
20 19 recnd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ∈ ℂ )
21 eldifsni ⊢ ( ( 𝐹 ‘ 𝑐 ) ∈ ( ℝ ∖ { 0 } ) → ( 𝐹 ‘ 𝑐 ) ≠ 0 )
22 18 21 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑐 ) ≠ 0 )
23 20 22 absrpcld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑐 ) ) ∈ ℝ+ )
24 17 23 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ∈ ℝ+ )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ∈ ℝ+ )
26 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) )
27 nfcv ⊢ Ⅎ 𝑥 ( 𝐴 [,] 𝐵 )
28 nfcv ⊢ Ⅎ 𝑥 abs
29 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐶 )
30 1 29 nfcxfr ⊢ Ⅎ 𝑥 𝐹
31 28 30 nfco ⊢ Ⅎ 𝑥 ( abs ∘ 𝐹 )
32 nfcv ⊢ Ⅎ 𝑥 𝑐
33 31 32 nffv ⊢ Ⅎ 𝑥 ( ( abs ∘ 𝐹 ) ‘ 𝑐 )
34 nfcv ⊢ Ⅎ 𝑥 ≤
35 nfcv ⊢ Ⅎ 𝑥 𝑑
36 31 35 nffv ⊢ Ⅎ 𝑥 ( ( abs ∘ 𝐹 ) ‘ 𝑑 )
37 33 34 36 nfbr ⊢ Ⅎ 𝑥 ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 )
38 27 37 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 )
39 26 38 nfan ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) )
40 fveq2 ⊢ ( 𝑑 = 𝑥 → ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) = ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) )
41 40 breq2d ⊢ ( 𝑑 = 𝑥 → ( ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) ↔ ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) ) )
42 41 rspccva ⊢ ( ( ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) )
43 42 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) )
44 absf ⊢ abs : ℂ ⟶ ℝ
45 44 a1i ⊢ ( 𝜑 → abs : ℂ ⟶ ℝ )
46 difss ⊢ ( ℝ ∖ { 0 } ) ⊆ ℝ
47 ax-resscn ⊢ ℝ ⊆ ℂ
48 46 47 sstri ⊢ ( ℝ ∖ { 0 } ) ⊆ ℂ
49 48 a1i ⊢ ( 𝜑 → ( ℝ ∖ { 0 } ) ⊆ ℂ )
50 11 49 fssd ⊢ ( 𝜑 → 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ )
51 fcompt ⊢ ( ( abs : ℂ ⟶ ℝ ∧ 𝐹 : ( 𝐴 [,] 𝐵 ) ⟶ ℂ ) → ( abs ∘ 𝐹 ) = ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
52 45 50 51 syl2anc ⊢ ( 𝜑 → ( abs ∘ 𝐹 ) = ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) )
53 nfcv ⊢ Ⅎ 𝑥 𝑧
54 30 53 nffv ⊢ Ⅎ 𝑥 ( 𝐹 ‘ 𝑧 )
55 28 54 nffv ⊢ Ⅎ 𝑥 ( abs ‘ ( 𝐹 ‘ 𝑧 ) )
56 nfcv ⊢ Ⅎ 𝑧 ( abs ‘ ( 𝐹 ‘ 𝑥 ) )
57 fveq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑥 ) )
58 57 fveq2d ⊢ ( 𝑧 = 𝑥 → ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
59 55 56 58 cbvmpt ⊢ ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) )
60 59 a1i ⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( abs ‘ ( 𝐹 ‘ 𝑧 ) ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
61 1 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐶 ) )
62 61 11 feq1dd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ 𝐶 ) : ( 𝐴 [,] 𝐵 ) ⟶ ( ℝ ∖ { 0 } ) )
63 62 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ( ℝ ∖ { 0 } ) )
64 61 63 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = 𝐶 )
65 64 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ 𝐶 ) )
66 65 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( abs ‘ 𝐶 ) ) )
67 52 60 66 3eqtrd ⊢ ( 𝜑 → ( abs ∘ 𝐹 ) = ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ↦ ( abs ‘ 𝐶 ) ) )
68 48 63 sseldi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → 𝐶 ∈ ℂ )
69 68 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( abs ‘ 𝐶 ) ∈ ℝ )
70 67 69 fvmpt2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) = ( abs ‘ 𝐶 ) )
71 70 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑥 ) = ( abs ‘ 𝐶 ) )
72 43 71 breqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) ) ∧ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ) → ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( abs ‘ 𝐶 ) )
73 72 ex ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) ) → ( 𝑥 ∈ ( 𝐴 [,] 𝐵 ) → ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( abs ‘ 𝐶 ) ) )
74 39 73 ralrimi ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) ) → ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( abs ‘ 𝐶 ) )
75 33 nfeq2 ⊢ Ⅎ 𝑥 𝑦 = ( ( abs ∘ 𝐹 ) ‘ 𝑐 )
76 breq1 ⊢ ( 𝑦 = ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) → ( 𝑦 ≤ ( abs ‘ 𝐶 ) ↔ ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( abs ‘ 𝐶 ) ) )
77 75 76 ralbid ⊢ ( 𝑦 = ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) → ( ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) 𝑦 ≤ ( abs ‘ 𝐶 ) ↔ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( abs ‘ 𝐶 ) ) )
78 77 rspcev ⊢ ( ( ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ∈ ℝ+ ∧ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( abs ‘ 𝐶 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) 𝑦 ≤ ( abs ‘ 𝐶 ) )
79 25 74 78 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ) ∧ ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) 𝑦 ≤ ( abs ‘ 𝐶 ) )
80 ssidd ⊢ ( 𝜑 → ℂ ⊆ ℂ )
81 cncfss ⊢ ( ( ( ℝ ∖ { 0 } ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℝ ∖ { 0 } ) ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
82 49 80 81 syl2anc ⊢ ( 𝜑 → ( ( 𝐴 [,] 𝐵 ) –cn→ ( ℝ ∖ { 0 } ) ) ⊆ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
83 82 5 sseldd ⊢ ( 𝜑 → 𝐹 ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℂ ) )
84 abscncf ⊢ abs ∈ ( ℂ –cn→ ℝ )
85 84 a1i ⊢ ( 𝜑 → abs ∈ ( ℂ –cn→ ℝ ) )
86 83 85 cncfco ⊢ ( 𝜑 → ( abs ∘ 𝐹 ) ∈ ( ( 𝐴 [,] 𝐵 ) –cn→ ℝ ) )
87 2 3 4 86 evthicc ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑏 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑏 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑎 ) ∧ ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) ) )
88 87 simprd ⊢ ( 𝜑 → ∃ 𝑐 ∈ ( 𝐴 [,] 𝐵 ) ∀ 𝑑 ∈ ( 𝐴 [,] 𝐵 ) ( ( abs ∘ 𝐹 ) ‘ 𝑐 ) ≤ ( ( abs ∘ 𝐹 ) ‘ 𝑑 ) )
89 79 88 r19.29a ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ+ ∀ 𝑥 ∈ ( 𝐴 [,] 𝐵 ) 𝑦 ≤ ( abs ‘ 𝐶 ) )