cniccbdd

Description: A continuous function on a closed interval is bounded. (Contributed by Mario Carneiro, 7-Sep-2014)

		Ref	Expression
	Assertion	cniccbdd	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x$

Proof

Step	Hyp	Ref	Expression
1		0re	$⊢ 0 \in ℝ$
2		ral0	$⊢ \forall y \in \emptyset \|F (y)\| \leq 0$
3		simp1	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to A \in ℝ$
4	3	rexrd	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to A \in ℝ^{*}$
5		simp2	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to B \in ℝ$
6	5	rexrd	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to B \in ℝ^{*}$
7		icc0	$⊢ (A \in ℝ^{} \land B \in ℝ^{}) \to ([A, B] = \emptyset \leftrightarrow B < A)$
8	4 6 7	syl2anc	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to ([A, B] = \emptyset \leftrightarrow B < A)$
9	8	biimpar	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land B < A) \to [A, B] = \emptyset$
10	9	raleqdv	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land B < A) \to (\forall y \in [A, B] \|F (y)\| \leq 0 \leftrightarrow \forall y \in \emptyset \|F (y)\| \leq 0)$
11	2 10	mpbiri	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land B < A) \to \forall y \in [A, B] \|F (y)\| \leq 0$
12		brralrspcev	$⊢ (0 \in ℝ \land \forall y \in [A, B] \|F (y)\| \leq 0) \to \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x$
13	1 11 12	sylancr	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land B < A) \to \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x$
14	3	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land A \leq B) \to A \in ℝ$
15	5	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land A \leq B) \to B \in ℝ$
16		simpr	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land A \leq B) \to A \leq B$
17		simp3	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to F : [A, B] \underset{cn}{⟶} ℂ$
18		abscncf	$⊢ abs : ℂ \underset{cn}{⟶} ℝ$
19	18	a1i	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to abs : ℂ \underset{cn}{⟶} ℝ$
20	17 19	cncfco	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to (abs \circ F) : [A, B] \underset{cn}{⟶} ℝ$
21	20	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land A \leq B) \to (abs \circ F) : [A, B] \underset{cn}{⟶} ℝ$
22	14 15 16 21	evthicc	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land A \leq B) \to (\exists z \in [A, B] \forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (z) \land \exists z \in [A, B] \forall y \in [A, B] (abs \circ F) (z) \leq (abs \circ F) (y))$
23	22	simpld	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land A \leq B) \to \exists z \in [A, B] \forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (z)$
24		cncff	$⊢ (abs \circ F) : [A, B] \underset{cn}{⟶} ℝ \to (abs \circ F) : [A, B] ⟶ ℝ$
25	20 24	syl	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to (abs \circ F) : [A, B] ⟶ ℝ$
26	25	ffvelcdmda	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land z \in [A, B]) \to (abs \circ F) (z) \in ℝ$
27		cncff	$⊢ F : [A, B] \underset{cn}{⟶} ℂ \to F : [A, B] ⟶ ℂ$
28	17 27	syl	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to F : [A, B] ⟶ ℂ$
29	28	adantr	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land z \in [A, B]) \to F : [A, B] ⟶ ℂ$
30		fvco3	$⊢ (F : [A, B] ⟶ ℂ \land y \in [A, B]) \to (abs \circ F) (y) = \|F (y)\|$
31	29 30	sylan	$⊢ (((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land z \in [A, B]) \land y \in [A, B]) \to (abs \circ F) (y) = \|F (y)\|$
32	31	breq1d	$⊢ (((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land z \in [A, B]) \land y \in [A, B]) \to ((abs \circ F) (y) \leq (abs \circ F) (z) \leftrightarrow \|F (y)\| \leq (abs \circ F) (z))$
33	32	ralbidva	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land z \in [A, B]) \to (\forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (z) \leftrightarrow \forall y \in [A, B] \|F (y)\| \leq (abs \circ F) (z))$
34	33	biimpd	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land z \in [A, B]) \to (\forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (z) \to \forall y \in [A, B] \|F (y)\| \leq (abs \circ F) (z))$
35		brralrspcev	$⊢ ((abs \circ F) (z) \in ℝ \land \forall y \in [A, B] \|F (y)\| \leq (abs \circ F) (z)) \to \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x$
36	26 34 35	syl6an	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land z \in [A, B]) \to (\forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (z) \to \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x)$
37	36	rexlimdva	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to (\exists z \in [A, B] \forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (z) \to \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x)$
38	37	imp	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land \exists z \in [A, B] \forall y \in [A, B] (abs \circ F) (y) \leq (abs \circ F) (z)) \to \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x$
39	23 38	syldan	$⊢ ((A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \land A \leq B) \to \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x$
40	13 39 5 3	ltlecasei	$⊢ (A \in ℝ \land B \in ℝ \land F : [A, B] \underset{cn}{⟶} ℂ) \to \exists x \in ℝ \forall y \in [A, B] \|F (y)\| \leq x$

Metamath Proof Explorer

Theorem cniccbdd

Proof