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 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
o1cxp.2 ⊢ ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐶 ) )
o1cxp.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
o1cxp.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )
Assertion o1cxp ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 o1cxp.1 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2 o1cxp.2 ⊢ ( 𝜑 → 0 ≤ ( ℜ ‘ 𝐶 ) )
3 o1cxp.3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4 o1cxp.4 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) )
5 o1f ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℂ )
6 4 5 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℂ )
7 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 )
8 dmmptg ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑉 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
9 7 8 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = 𝐴 )
10 9 feq2d ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⟶ ℂ ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ) )
11 6 10 mpbid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ )
12 o1bdd ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ℂ ) → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) )
13 4 11 12 syl2anc ⊢ ( 𝜑 → ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
15 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
16 15 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
17 14 3 16 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
18 17 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↑𝑐 𝐶 ) = ( 𝐵 ↑𝑐 𝐶 ) )
19 ovex ⊢ ( 𝐵 ↑𝑐 𝐶 ) ∈ V
20 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) = ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) )
21 20 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝐵 ↑𝑐 𝐶 ) ∈ V ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑥 ) = ( 𝐵 ↑𝑐 𝐶 ) )
22 14 19 21 sylancl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑥 ) = ( 𝐵 ↑𝑐 𝐶 ) )
23 18 22 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑥 ) )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑥 ) )
25 nfv ⊢ Ⅎ 𝑧 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑥 )
26 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 )
27 nfcv ⊢ Ⅎ 𝑥 ↑𝑐
28 nfcv ⊢ Ⅎ 𝑥 𝐶
29 26 27 28 nfov ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↑𝑐 𝐶 )
30 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 )
31 29 30 nfeq ⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 )
32 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) )
33 32 oveq1d ⊢ ( 𝑥 = 𝑧 → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↑𝑐 𝐶 ) = ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↑𝑐 𝐶 ) )
34 fveq2 ⊢ ( 𝑥 = 𝑧 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) )
35 33 34 eqeq12d ⊢ ( 𝑥 = 𝑧 → ( ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑥 ) ↔ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) ) )
36 25 31 35 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑥 ) ↔ ∀ 𝑧 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) )
37 24 36 sylib ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝐴 ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) )
38 37 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) )
39 38 ad2ant2r ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↑𝑐 𝐶 ) = ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) )
40 39 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → ( abs ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↑𝑐 𝐶 ) ) = ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) ) )
41 11 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ℂ )
42 41 ad2ant2r ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ∈ ℂ )
43 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → 𝐶 ∈ ℂ )
44 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → 0 ≤ ( ℜ ‘ 𝐶 ) )
45 simprr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 𝑚 ∈ ℝ )
46 0re ⊢ 0 ∈ ℝ
47 ifcl ⊢ ( ( 𝑚 ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ∈ ℝ )
48 45 46 47 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ∈ ℝ )
49 48 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ∈ ℝ )
50 42 abscld ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ∈ ℝ )
51 45 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → 𝑚 ∈ ℝ )
52 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 )
53 max2 ⊢ ( ( 0 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → 𝑚 ≤ if ( 0 ≤ 𝑚 , 𝑚 , 0 ) )
54 46 45 53 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 𝑚 ≤ if ( 0 ≤ 𝑚 , 𝑚 , 0 ) )
55 54 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → 𝑚 ≤ if ( 0 ≤ 𝑚 , 𝑚 , 0 ) )
56 50 51 49 52 55 letrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ if ( 0 ≤ 𝑚 , 𝑚 , 0 ) )
57 42 43 44 49 56 abscxpbnd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → ( abs ‘ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ↑𝑐 𝐶 ) ) ≤ ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) )
58 40 57 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ ( 𝑧 ∈ 𝐴 ∧ ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) ) → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) ) ≤ ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) )
59 58 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) ) ≤ ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) ) )
60 59 imim2d ⊢ ( ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) → ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) ) ≤ ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) ) ) )
61 60 ralimdva ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) → ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) ) ≤ ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) ) ) )
62 3 4 o1mptrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
63 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
64 62 63 cxpcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐵 ↑𝑐 𝐶 ) ∈ ℂ )
65 64 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) : 𝐴 ⟶ ℂ )
66 65 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) : 𝐴 ⟶ ℂ )
67 o1dm ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑂(1) → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
68 4 67 syl ⊢ ( 𝜑 → dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ ℝ )
69 9 68 eqsstrrd ⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
70 69 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 𝐴 ⊆ ℝ )
71 simprl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 𝑦 ∈ ℝ )
72 max1 ⊢ ( ( 0 ∈ ℝ ∧ 𝑚 ∈ ℝ ) → 0 ≤ if ( 0 ≤ 𝑚 , 𝑚 , 0 ) )
73 46 45 72 sylancr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 0 ≤ if ( 0 ≤ 𝑚 , 𝑚 , 0 ) )
74 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → 𝐶 ∈ ℂ )
75 74 recld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ℜ ‘ 𝐶 ) ∈ ℝ )
76 48 73 75 recxpcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) ∈ ℝ )
77 74 abscld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( abs ‘ 𝐶 ) ∈ ℝ )
78 pire ⊢ π ∈ ℝ
79 remulcl ⊢ ( ( ( abs ‘ 𝐶 ) ∈ ℝ ∧ π ∈ ℝ ) → ( ( abs ‘ 𝐶 ) · π ) ∈ ℝ )
80 77 78 79 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ( abs ‘ 𝐶 ) · π ) ∈ ℝ )
81 80 reefcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ∈ ℝ )
82 76 81 remulcld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) ∈ ℝ )
83 elo12r ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) ∈ ℝ ) ∧ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) ) ≤ ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) ) ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ∈ 𝑂(1) )
84 83 3expia ⊢ ( ( ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℝ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) ∈ ℝ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) ) ≤ ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ∈ 𝑂(1) ) )
85 66 70 71 82 84 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ‘ 𝑧 ) ) ≤ ( ( if ( 0 ≤ 𝑚 , 𝑚 , 0 ) ↑𝑐 ( ℜ ‘ 𝐶 ) ) · ( exp ‘ ( ( abs ‘ 𝐶 ) · π ) ) ) ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ∈ 𝑂(1) ) )
86 61 85 syld ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ ℝ ∧ 𝑚 ∈ ℝ ) ) → ( ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ∈ 𝑂(1) ) )
87 86 rexlimdvva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ℝ ∃ 𝑚 ∈ ℝ ∀ 𝑧 ∈ 𝐴 ( 𝑦 ≤ 𝑧 → ( abs ‘ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑧 ) ) ≤ 𝑚 ) → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ∈ 𝑂(1) ) )
88 13 87 mpd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐵 ↑𝑐 𝐶 ) ) ∈ 𝑂(1) )