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 \in [A, B] ⟼ C)$
	cncficcgt0.a	$⊢ φ \to A \in ℝ$
	cncficcgt0.b	$⊢ φ \to B \in ℝ$
	cncficcgt0.aleb	$⊢ φ \to A \leq B$
	cncficcgt0.fcn	$⊢ φ \to F : [A, B] \underset{cn}{⟶} (ℝ ∖ \{0\})$
Assertion	cncficcgt0	$⊢ φ \to \exists y \in ℝ^{+} \forall x \in [A, B] y \leq \|C\|$

Proof

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

Metamath Proof Explorer

Theorem cncficcgt0

Proof