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	ffvelrnda	|- ( ( 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	fvmptelrn	|- ( ( 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	sseldi	|- ( ( 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 ) )