Metamath Proof Explorer


Theorem 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 φ C
o1cxp.2 φ 0 C
o1cxp.3 φ x A B V
o1cxp.4 φ x A B 𝑂1
Assertion o1cxp φ x A B C 𝑂1

Proof

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