This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- F = ( x e. ( A [,] B ) |-> C )
cncficcgt0.a 
|- ( ph -> A e. RR )
cncficcgt0.b 
|- ( ph -> B e. RR )
cncficcgt0.aleb 
|- ( ph -> A <_ B )
cncficcgt0.fcn 
|- ( ph -> F e. ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) )
Assertion cncficcgt0 
|- ( ph -> E. y e. RR+ A. x e. ( A [,] B ) y <_ ( abs ` C ) )

Proof

Step Hyp Ref Expression
1 cncficcgt0.f 
 |-  F = ( x e. ( A [,] B ) |-> C )
2 cncficcgt0.a 
 |-  ( ph -> A e. RR )
3 cncficcgt0.b 
 |-  ( ph -> B e. RR )
4 cncficcgt0.aleb 
 |-  ( ph -> A <_ B )
5 cncficcgt0.fcn 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) )
6 cncff 
 |-  ( F e. ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) -> F : ( A [,] B ) --> ( RR \ { 0 } ) )
7 ffun 
 |-  ( F : ( A [,] B ) --> ( RR \ { 0 } ) -> Fun F )
8 5 6 7 3syl 
 |-  ( ph -> Fun F )
9 8 adantr 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> Fun F )
10 simpr 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> c e. ( A [,] B ) )
11 5 6 syl 
 |-  ( ph -> F : ( A [,] B ) --> ( RR \ { 0 } ) )
12 11 fdmd 
 |-  ( ph -> dom F = ( A [,] B ) )
13 12 eqcomd 
 |-  ( ph -> ( A [,] B ) = dom F )
14 13 adantr 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> ( A [,] B ) = dom F )
15 10 14 eleqtrd 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> c e. dom F )
16 fvco 
 |-  ( ( Fun F /\ c e. dom F ) -> ( ( abs o. F ) ` c ) = ( abs ` ( F ` c ) ) )
17 9 15 16 syl2anc 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> ( ( abs o. F ) ` c ) = ( abs ` ( F ` c ) ) )
18 11 ffvelcdmda 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> ( F ` c ) e. ( RR \ { 0 } ) )
19 18 eldifad 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> ( F ` c ) e. RR )
20 19 recnd 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> ( F ` c ) e. CC )
21 eldifsni 
 |-  ( ( F ` c ) e. ( RR \ { 0 } ) -> ( F ` c ) =/= 0 )
22 18 21 syl 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> ( F ` c ) =/= 0 )
23 20 22 absrpcld 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> ( abs ` ( F ` c ) ) e. RR+ )
24 17 23 eqeltrd 
 |-  ( ( ph /\ c e. ( A [,] B ) ) -> ( ( abs o. F ) ` c ) e. RR+ )
25 24 adantr 
 |-  ( ( ( ph /\ c e. ( A [,] B ) ) /\ A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) ) -> ( ( abs o. F ) ` c ) e. RR+ )
26 nfv 
 |-  F/ x ( ph /\ c e. ( A [,] B ) )
27 nfcv 
 |-  F/_ x ( A [,] B )
28 nfcv 
 |-  F/_ x abs
29 nfmpt1 
 |-  F/_ x ( x e. ( A [,] B ) |-> C )
30 1 29 nfcxfr 
 |-  F/_ x F
31 28 30 nfco 
 |-  F/_ x ( abs o. F )
32 nfcv 
 |-  F/_ x c
33 31 32 nffv 
 |-  F/_ x ( ( abs o. F ) ` c )
34 nfcv 
 |-  F/_ x <_
35 nfcv 
 |-  F/_ x d
36 31 35 nffv 
 |-  F/_ x ( ( abs o. F ) ` d )
37 33 34 36 nfbr 
 |-  F/ x ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d )
38 27 37 nfralw 
 |-  F/ x A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d )
39 26 38 nfan 
 |-  F/ x ( ( ph /\ c e. ( A [,] B ) ) /\ A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) )
40 fveq2 
 |-  ( d = x -> ( ( abs o. F ) ` d ) = ( ( abs o. F ) ` x ) )
41 40 breq2d 
 |-  ( d = x -> ( ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) <-> ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` x ) ) )
42 41 rspccva 
 |-  ( ( A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) /\ x e. ( A [,] B ) ) -> ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` x ) )
43 42 adantll 
 |-  ( ( ( ( ph /\ c e. ( A [,] B ) ) /\ A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) ) /\ x e. ( A [,] B ) ) -> ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` x ) )
44 absf 
 |-  abs : CC --> RR
45 44 a1i 
 |-  ( ph -> abs : CC --> RR )
46 difss 
 |-  ( RR \ { 0 } ) C_ RR
47 ax-resscn 
 |-  RR C_ CC
48 46 47 sstri 
 |-  ( RR \ { 0 } ) C_ CC
49 48 a1i 
 |-  ( ph -> ( RR \ { 0 } ) C_ CC )
50 11 49 fssd 
 |-  ( ph -> F : ( A [,] B ) --> CC )
51 fcompt 
 |-  ( ( abs : CC --> RR /\ F : ( A [,] B ) --> CC ) -> ( abs o. F ) = ( z e. ( A [,] B ) |-> ( abs ` ( F ` z ) ) ) )
52 45 50 51 syl2anc 
 |-  ( ph -> ( abs o. F ) = ( z e. ( A [,] B ) |-> ( abs ` ( F ` z ) ) ) )
53 nfcv 
 |-  F/_ x z
54 30 53 nffv 
 |-  F/_ x ( F ` z )
55 28 54 nffv 
 |-  F/_ x ( abs ` ( F ` z ) )
56 nfcv 
 |-  F/_ z ( abs ` ( F ` x ) )
57 fveq2 
 |-  ( z = x -> ( F ` z ) = ( F ` x ) )
58 57 fveq2d 
 |-  ( z = x -> ( abs ` ( F ` z ) ) = ( abs ` ( F ` x ) ) )
59 55 56 58 cbvmpt 
 |-  ( z e. ( A [,] B ) |-> ( abs ` ( F ` z ) ) ) = ( x e. ( A [,] B ) |-> ( abs ` ( F ` x ) ) )
60 59 a1i 
 |-  ( ph -> ( z e. ( A [,] B ) |-> ( abs ` ( F ` z ) ) ) = ( x e. ( A [,] B ) |-> ( abs ` ( F ` x ) ) ) )
61 1 a1i 
 |-  ( ph -> F = ( x e. ( A [,] B ) |-> C ) )
62 61 11 feq1dd 
 |-  ( ph -> ( x e. ( A [,] B ) |-> C ) : ( A [,] B ) --> ( RR \ { 0 } ) )
63 62 fvmptelcdm 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> C e. ( RR \ { 0 } ) )
64 61 63 fvmpt2d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( F ` x ) = C )
65 64 fveq2d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( abs ` ( F ` x ) ) = ( abs ` C ) )
66 65 mpteq2dva 
 |-  ( ph -> ( x e. ( A [,] B ) |-> ( abs ` ( F ` x ) ) ) = ( x e. ( A [,] B ) |-> ( abs ` C ) ) )
67 52 60 66 3eqtrd 
 |-  ( ph -> ( abs o. F ) = ( x e. ( A [,] B ) |-> ( abs ` C ) ) )
68 48 63 sselid 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> C e. CC )
69 68 abscld 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( abs ` C ) e. RR )
70 67 69 fvmpt2d 
 |-  ( ( ph /\ x e. ( A [,] B ) ) -> ( ( abs o. F ) ` x ) = ( abs ` C ) )
71 70 ad4ant14 
 |-  ( ( ( ( ph /\ c e. ( A [,] B ) ) /\ A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) ) /\ x e. ( A [,] B ) ) -> ( ( abs o. F ) ` x ) = ( abs ` C ) )
72 43 71 breqtrd 
 |-  ( ( ( ( ph /\ c e. ( A [,] B ) ) /\ A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) ) /\ x e. ( A [,] B ) ) -> ( ( abs o. F ) ` c ) <_ ( abs ` C ) )
73 72 ex 
 |-  ( ( ( ph /\ c e. ( A [,] B ) ) /\ A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) ) -> ( x e. ( A [,] B ) -> ( ( abs o. F ) ` c ) <_ ( abs ` C ) ) )
74 39 73 ralrimi 
 |-  ( ( ( ph /\ c e. ( A [,] B ) ) /\ A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) ) -> A. x e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( abs ` C ) )
75 33 nfeq2 
 |-  F/ x y = ( ( abs o. F ) ` c )
76 breq1 
 |-  ( y = ( ( abs o. F ) ` c ) -> ( y <_ ( abs ` C ) <-> ( ( abs o. F ) ` c ) <_ ( abs ` C ) ) )
77 75 76 ralbid 
 |-  ( y = ( ( abs o. F ) ` c ) -> ( A. x e. ( A [,] B ) y <_ ( abs ` C ) <-> A. x e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( abs ` C ) ) )
78 77 rspcev 
 |-  ( ( ( ( abs o. F ) ` c ) e. RR+ /\ A. x e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( abs ` C ) ) -> E. y e. RR+ A. x e. ( A [,] B ) y <_ ( abs ` C ) )
79 25 74 78 syl2anc 
 |-  ( ( ( ph /\ c e. ( A [,] B ) ) /\ A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) ) -> E. y e. RR+ A. x e. ( A [,] B ) y <_ ( abs ` C ) )
80 ssidd 
 |-  ( ph -> CC C_ CC )
81 cncfss 
 |-  ( ( ( RR \ { 0 } ) C_ CC /\ CC C_ CC ) -> ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) C_ ( ( A [,] B ) -cn-> CC ) )
82 49 80 81 syl2anc 
 |-  ( ph -> ( ( A [,] B ) -cn-> ( RR \ { 0 } ) ) C_ ( ( A [,] B ) -cn-> CC ) )
83 82 5 sseldd 
 |-  ( ph -> F e. ( ( A [,] B ) -cn-> CC ) )
84 abscncf 
 |-  abs e. ( CC -cn-> RR )
85 84 a1i 
 |-  ( ph -> abs e. ( CC -cn-> RR ) )
86 83 85 cncfco 
 |-  ( ph -> ( abs o. F ) e. ( ( A [,] B ) -cn-> RR ) )
87 2 3 4 86 evthicc 
 |-  ( ph -> ( E. a e. ( A [,] B ) A. b e. ( A [,] B ) ( ( abs o. F ) ` b ) <_ ( ( abs o. F ) ` a ) /\ E. c e. ( A [,] B ) A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) ) )
88 87 simprd 
 |-  ( ph -> E. c e. ( A [,] B ) A. d e. ( A [,] B ) ( ( abs o. F ) ` c ) <_ ( ( abs o. F ) ` d ) )
89 79 88 r19.29a 
 |-  ( ph -> E. y e. RR+ A. x e. ( A [,] B ) y <_ ( abs ` C ) )