o1cxp

Description: An eventually bounded function taken to a nonnegative power is eventually bounded. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Hypotheses	o1cxp.1	$⊢ φ \to C \in ℂ$
	o1cxp.2	$⊢ φ \to 0 \leq ℜ (C)$
	o1cxp.3	$⊢ (φ \land x \in A) \to B \in V$
	o1cxp.4	$⊢ φ \to (x \in A ⟼ B) \in 𝑂 (1)$
Assertion	o1cxp	$⊢ φ \to (x \in A ⟼ B^{C}) \in 𝑂 (1)$

Proof

Step	Hyp	Ref	Expression
1		o1cxp.1	$⊢ φ \to C \in ℂ$
2		o1cxp.2	$⊢ φ \to 0 \leq ℜ (C)$
3		o1cxp.3	$⊢ (φ \land x \in A) \to B \in V$
4		o1cxp.4	$⊢ φ \to (x \in A ⟼ B) \in 𝑂 (1)$
5		o1f	$⊢ (x \in A ⟼ B) \in 𝑂 (1) \to (x \in A ⟼ B) : dom (x \in A ⟼ B) ⟶ ℂ$
6	4 5	syl	$⊢ φ \to (x \in A ⟼ B) : dom (x \in A ⟼ B) ⟶ ℂ$
7	3	ralrimiva	$⊢ φ \to \forall x \in A B \in V$
8		dmmptg	$⊢ \forall x \in A B \in V \to dom (x \in A ⟼ B) = A$
9	7 8	syl	$⊢ φ \to dom (x \in A ⟼ B) = A$
10	9	feq2d	$⊢ φ \to ((x \in A ⟼ B) : dom (x \in A ⟼ B) ⟶ ℂ \leftrightarrow (x \in A ⟼ B) : A ⟶ ℂ)$
11	6 10	mpbid	$⊢ φ \to (x \in A ⟼ B) : A ⟶ ℂ$
12		o1bdd	$⊢ ((x \in A ⟼ B) \in 𝑂 (1) \land (x \in A ⟼ B) : A ⟶ ℂ) \to \exists y \in ℝ \exists m \in ℝ \forall z \in A (y \leq z \to \|(x \in A ⟼ B) (z)\| \leq m)$
13	4 11 12	syl2anc	$⊢ φ \to \exists y \in ℝ \exists m \in ℝ \forall z \in A (y \leq z \to \|(x \in A ⟼ B) (z)\| \leq m)$
14		simpr	$⊢ (φ \land x \in A) \to x \in A$
15		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
16	15	fvmpt2	$⊢ (x \in A \land B \in V) \to (x \in A ⟼ B) (x) = B$
17	14 3 16	syl2anc	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
18	17	oveq1d	$⊢ (φ \land x \in A) \to {(x \in A ⟼ B) (x)}^{C} = B^{C}$
19		ovex	$⊢ B^{C} \in V$
20		eqid	$⊢ (x \in A ⟼ B^{C}) = (x \in A ⟼ B^{C})$
21	20	fvmpt2	$⊢ (x \in A \land B^{C} \in V) \to (x \in A ⟼ B^{C}) (x) = B^{C}$
22	14 19 21	sylancl	$⊢ (φ \land x \in A) \to (x \in A ⟼ B^{C}) (x) = B^{C}$
23	18 22	eqtr4d	$⊢ (φ \land x \in A) \to {(x \in A ⟼ B) (x)}^{C} = (x \in A ⟼ B^{C}) (x)$
24	23	ralrimiva	$⊢ φ \to \forall x \in A {(x \in A ⟼ B) (x)}^{C} = (x \in A ⟼ B^{C}) (x)$
25		nfv	$⊢ Ⅎ z {(x \in A ⟼ B) (x)}^{C} = (x \in A ⟼ B^{C}) (x)$
26		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B) (z)$
27		nfcv	$⊢ \underline{Ⅎ} x ↑_{c}$
28		nfcv	$⊢ \underline{Ⅎ} x C$
29	26 27 28	nfov	$⊢ \underline{Ⅎ} x {(x \in A ⟼ B) (z)}^{C}$
30		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B^{C}) (z)$
31	29 30	nfeq	$⊢ Ⅎ x {(x \in A ⟼ B) (z)}^{C} = (x \in A ⟼ B^{C}) (z)$
32		fveq2	$⊢ x = z \to (x \in A ⟼ B) (x) = (x \in A ⟼ B) (z)$
33	32	oveq1d	$⊢ x = z \to {(x \in A ⟼ B) (x)}^{C} = {(x \in A ⟼ B) (z)}^{C}$
34		fveq2	$⊢ x = z \to (x \in A ⟼ B^{C}) (x) = (x \in A ⟼ B^{C}) (z)$
35	33 34	eqeq12d	$⊢ x = z \to ({(x \in A ⟼ B) (x)}^{C} = (x \in A ⟼ B^{C}) (x) \leftrightarrow {(x \in A ⟼ B) (z)}^{C} = (x \in A ⟼ B^{C}) (z))$
36	25 31 35	cbvralw	$⊢ \forall x \in A {(x \in A ⟼ B) (x)}^{C} = (x \in A ⟼ B^{C}) (x) \leftrightarrow \forall z \in A {(x \in A ⟼ B) (z)}^{C} = (x \in A ⟼ B^{C}) (z)$
37	24 36	sylib	$⊢ φ \to \forall z \in A {(x \in A ⟼ B) (z)}^{C} = (x \in A ⟼ B^{C}) (z)$
38	37	r19.21bi	$⊢ (φ \land z \in A) \to {(x \in A ⟼ B) (z)}^{C} = (x \in A ⟼ B^{C}) (z)$
39	38	ad2ant2r	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to {(x \in A ⟼ B) (z)}^{C} = (x \in A ⟼ B^{C}) (z)$
40	39	fveq2d	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to \|{(x \in A ⟼ B) (z)}^{C}\| = \|(x \in A ⟼ B^{C}) (z)\|$
41	11	ffvelcdmda	$⊢ (φ \land z \in A) \to (x \in A ⟼ B) (z) \in ℂ$
42	41	ad2ant2r	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to (x \in A ⟼ B) (z) \in ℂ$
43	1	ad2antrr	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to C \in ℂ$
44	2	ad2antrr	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to 0 \leq ℜ (C)$
45		simprr	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to m \in ℝ$
46		0re	$⊢ 0 \in ℝ$
47		ifcl	$⊢ (m \in ℝ \land 0 \in ℝ) \to if (0 \leq m, m, 0) \in ℝ$
48	45 46 47	sylancl	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to if (0 \leq m, m, 0) \in ℝ$
49	48	adantr	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to if (0 \leq m, m, 0) \in ℝ$
50	42	abscld	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to \|(x \in A ⟼ B) (z)\| \in ℝ$
51	45	adantr	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to m \in ℝ$
52		simprr	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to \|(x \in A ⟼ B) (z)\| \leq m$
53		max2	$⊢ (0 \in ℝ \land m \in ℝ) \to m \leq if (0 \leq m, m, 0)$
54	46 45 53	sylancr	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to m \leq if (0 \leq m, m, 0)$
55	54	adantr	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to m \leq if (0 \leq m, m, 0)$
56	50 51 49 52 55	letrd	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to \|(x \in A ⟼ B) (z)\| \leq if (0 \leq m, m, 0)$
57	42 43 44 49 56	abscxpbnd	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to \|{(x \in A ⟼ B) (z)}^{C}\| \leq {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π}$
58	40 57	eqbrtrrd	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land (z \in A \land \|(x \in A ⟼ B) (z)\| \leq m)) \to \|(x \in A ⟼ B^{C}) (z)\| \leq {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π}$
59	58	expr	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land z \in A) \to (\|(x \in A ⟼ B) (z)\| \leq m \to \|(x \in A ⟼ B^{C}) (z)\| \leq {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π})$
60	59	imim2d	$⊢ ((φ \land (y \in ℝ \land m \in ℝ)) \land z \in A) \to ((y \leq z \to \|(x \in A ⟼ B) (z)\| \leq m) \to (y \leq z \to \|(x \in A ⟼ B^{C}) (z)\| \leq {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π}))$
61	60	ralimdva	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to (\forall z \in A (y \leq z \to \|(x \in A ⟼ B) (z)\| \leq m) \to \forall z \in A (y \leq z \to \|(x \in A ⟼ B^{C}) (z)\| \leq {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π}))$
62	3 4	o1mptrcl	$⊢ (φ \land x \in A) \to B \in ℂ$
63	1	adantr	$⊢ (φ \land x \in A) \to C \in ℂ$
64	62 63	cxpcld	$⊢ (φ \land x \in A) \to B^{C} \in ℂ$
65	64	fmpttd	$⊢ φ \to (x \in A ⟼ B^{C}) : A ⟶ ℂ$
66	65	adantr	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to (x \in A ⟼ B^{C}) : A ⟶ ℂ$
67		o1dm	$⊢ (x \in A ⟼ B) \in 𝑂 (1) \to dom (x \in A ⟼ B) \subseteq ℝ$
68	4 67	syl	$⊢ φ \to dom (x \in A ⟼ B) \subseteq ℝ$
69	9 68	eqsstrrd	$⊢ φ \to A \subseteq ℝ$
70	69	adantr	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to A \subseteq ℝ$
71		simprl	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to y \in ℝ$
72		max1	$⊢ (0 \in ℝ \land m \in ℝ) \to 0 \leq if (0 \leq m, m, 0)$
73	46 45 72	sylancr	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to 0 \leq if (0 \leq m, m, 0)$
74	1	adantr	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to C \in ℂ$
75	74	recld	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to ℜ (C) \in ℝ$
76	48 73 75	recxpcld	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to {if (0 \leq m, m, 0)}^{ℜ (C)} \in ℝ$
77	74	abscld	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to \|C\| \in ℝ$
78		pire	$⊢ π \in ℝ$
79		remulcl	$⊢ (\|C\| \in ℝ \land π \in ℝ) \to \|C\| π \in ℝ$
80	77 78 79	sylancl	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to \|C\| π \in ℝ$
81	80	reefcld	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to e^{\|C\| π} \in ℝ$
82	76 81	remulcld	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π} \in ℝ$
83		elo12r	$⊢ (((x \in A ⟼ B^{C}) : A ⟶ ℂ \land A \subseteq ℝ) \land (y \in ℝ \land {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π} \in ℝ) \land \forall z \in A (y \leq z \to \|(x \in A ⟼ B^{C}) (z)\| \leq {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π})) \to (x \in A ⟼ B^{C}) \in 𝑂 (1)$
84	83	3expia	$⊢ (((x \in A ⟼ B^{C}) : A ⟶ ℂ \land A \subseteq ℝ) \land (y \in ℝ \land {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π} \in ℝ)) \to (\forall z \in A (y \leq z \to \|(x \in A ⟼ B^{C}) (z)\| \leq {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π}) \to (x \in A ⟼ B^{C}) \in 𝑂 (1))$
85	66 70 71 82 84	syl22anc	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to (\forall z \in A (y \leq z \to \|(x \in A ⟼ B^{C}) (z)\| \leq {if (0 \leq m, m, 0)}^{ℜ (C)} e^{\|C\| π}) \to (x \in A ⟼ B^{C}) \in 𝑂 (1))$
86	61 85	syld	$⊢ (φ \land (y \in ℝ \land m \in ℝ)) \to (\forall z \in A (y \leq z \to \|(x \in A ⟼ B) (z)\| \leq m) \to (x \in A ⟼ B^{C}) \in 𝑂 (1))$
87	86	rexlimdvva	$⊢ φ \to (\exists y \in ℝ \exists m \in ℝ \forall z \in A (y \leq z \to \|(x \in A ⟼ B) (z)\| \leq m) \to (x \in A ⟼ B^{C}) \in 𝑂 (1))$
88	13 87	mpd	$⊢ φ \to (x \in A ⟼ B^{C}) \in 𝑂 (1)$

Metamath Proof Explorer

Theorem o1cxp

Proof