cxploglim2

Description: Every power of the logarithm grows slower than any positive power. (Contributed by Mario Carneiro, 20-May-2016)

		Ref	Expression
	Assertion	cxploglim2	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to (n \in ℝ^{+} ⟼ \frac{{\log n}^{A}}{n^{B}}) \underset{ℝ}{⇝} 0$

Proof

Step	Hyp	Ref	Expression
1		3re	$⊢ 3 \in ℝ$
2	1	a1i	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to 3 \in ℝ$
3		0red	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to 0 \in ℝ$
4	3	recnd	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to 0 \in ℂ$
5		ovexd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to \frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}} \in V$
6		simpr	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to B \in ℝ^{+}$
7		recl	$⊢ A \in ℂ \to ℜ (A) \in ℝ$
8	7	adantr	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to ℜ (A) \in ℝ$
9		1re	$⊢ 1 \in ℝ$
10		ifcl	$⊢ (ℜ (A) \in ℝ \land 1 \in ℝ) \to if (1 \leq ℜ (A), ℜ (A), 1) \in ℝ$
11	8 9 10	sylancl	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to if (1 \leq ℜ (A), ℜ (A), 1) \in ℝ$
12	9	a1i	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to 1 \in ℝ$
13		0lt1	$⊢ 0 < 1$
14	13	a1i	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to 0 < 1$
15		max1	$⊢ (1 \in ℝ \land ℜ (A) \in ℝ) \to 1 \leq if (1 \leq ℜ (A), ℜ (A), 1)$
16	9 8 15	sylancr	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to 1 \leq if (1 \leq ℜ (A), ℜ (A), 1)$
17	3 12 11 14 16	ltletrd	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to 0 < if (1 \leq ℜ (A), ℜ (A), 1)$
18	11 17	elrpd	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to if (1 \leq ℜ (A), ℜ (A), 1) \in ℝ^{+}$
19	6 18	rpdivcld	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to \frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)} \in ℝ^{+}$
20		cxploglim	$⊢ \frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)} \in ℝ^{+} \to (n \in ℝ^{+} ⟼ \frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}}) \underset{ℝ}{⇝} 0$
21	19 20	syl	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to (n \in ℝ^{+} ⟼ \frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}}) \underset{ℝ}{⇝} 0$
22	5 21 18	rlimcxp	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to (n \in ℝ^{+} ⟼ {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}) \underset{ℝ}{⇝} 0$
23	5 21	rlimmptrcl	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to \frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}} \in ℂ$
24	11	adantr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to if (1 \leq ℜ (A), ℜ (A), 1) \in ℝ$
25	24	recnd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to if (1 \leq ℜ (A), ℜ (A), 1) \in ℂ$
26	23 25	cxpcld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} \in ℂ$
27		relogcl	$⊢ n \in ℝ^{+} \to \log n \in ℝ$
28	27	adantl	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to \log n \in ℝ$
29	28	recnd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to \log n \in ℂ$
30		simpll	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to A \in ℂ$
31	29 30	cxpcld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to {\log n}^{A} \in ℂ$
32		simpr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to n \in ℝ^{+}$
33		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
34	33	ad2antlr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to B \in ℝ$
35	32 34	rpcxpcld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to n^{B} \in ℝ^{+}$
36	35	rpcnd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to n^{B} \in ℂ$
37	35	rpne0d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to n^{B} \neq 0$
38	31 36 37	divcld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to \frac{{\log n}^{A}}{n^{B}} \in ℂ$
39	38	adantrr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \frac{{\log n}^{A}}{n^{B}} \in ℂ$
40	39	abscld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|\frac{{\log n}^{A}}{n^{B}}\| \in ℝ$
41		rpre	$⊢ n \in ℝ^{+} \to n \in ℝ$
42	41	ad2antrl	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to n \in ℝ$
43	9	a1i	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to 1 \in ℝ$
44	1	a1i	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to 3 \in ℝ$
45		1lt3	$⊢ 1 < 3$
46	45	a1i	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to 1 < 3$
47		simprr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to 3 \leq n$
48	43 44 42 46 47	ltletrd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to 1 < n$
49	42 48	rplogcld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \log n \in ℝ^{+}$
50	32	adantrr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to n \in ℝ^{+}$
51	33	ad2antlr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to B \in ℝ$
52	18	adantr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to if (1 \leq ℜ (A), ℜ (A), 1) \in ℝ^{+}$
53	51 52	rerpdivcld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)} \in ℝ$
54	50 53	rpcxpcld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}} \in ℝ^{+}$
55	49 54	rpdivcld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}} \in ℝ^{+}$
56	11	adantr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to if (1 \leq ℜ (A), ℜ (A), 1) \in ℝ$
57	55 56	rpcxpcld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} \in ℝ^{+}$
58	57	rpred	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} \in ℝ$
59	26	adantrr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} \in ℂ$
60	59	abscld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|{(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}\| \in ℝ$
61	31	adantrr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {\log n}^{A} \in ℂ$
62	61	abscld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|{\log n}^{A}\| \in ℝ$
63	49 56	rpcxpcld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)} \in ℝ^{+}$
64	63	rpred	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)} \in ℝ$
65	35	adantrr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to n^{B} \in ℝ^{+}$
66		simpll	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to A \in ℂ$
67		abscxp	$⊢ (\log n \in ℝ^{+} \land A \in ℂ) \to \|{\log n}^{A}\| = {\log n}^{ℜ (A)}$
68	49 66 67	syl2anc	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|{\log n}^{A}\| = {\log n}^{ℜ (A)}$
69	66	recld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to ℜ (A) \in ℝ$
70		max2	$⊢ (1 \in ℝ \land ℜ (A) \in ℝ) \to ℜ (A) \leq if (1 \leq ℜ (A), ℜ (A), 1)$
71	9 69 70	sylancr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to ℜ (A) \leq if (1 \leq ℜ (A), ℜ (A), 1)$
72	27	ad2antrl	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \log n \in ℝ$
73		loge	$⊢ \log e = 1$
74		ere	$⊢ e \in ℝ$
75	74	a1i	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to e \in ℝ$
76		egt2lt3	$⊢ (2 < e \land e < 3)$
77	76	simpri	$⊢ e < 3$
78	77	a1i	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to e < 3$
79	75 44 42 78 47	ltletrd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to e < n$
80		epr	$⊢ e \in ℝ^{+}$
81		logltb	$⊢ (e \in ℝ^{+} \land n \in ℝ^{+}) \to (e < n \leftrightarrow \log e < \log n)$
82	80 50 81	sylancr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to (e < n \leftrightarrow \log e < \log n)$
83	79 82	mpbid	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \log e < \log n$
84	73 83	eqbrtrrid	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to 1 < \log n$
85	72 84 69 56	cxpled	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to (ℜ (A) \leq if (1 \leq ℜ (A), ℜ (A), 1) \leftrightarrow {\log n}^{ℜ (A)} \leq {\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)})$
86	71 85	mpbid	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {\log n}^{ℜ (A)} \leq {\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)}$
87	68 86	eqbrtrd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|{\log n}^{A}\| \leq {\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)}$
88	62 64 65 87	lediv1dd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \frac{\|{\log n}^{A}\|}{n^{B}} \leq \frac{{\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)}}{n^{B}}$
89	31 36 37	absdivd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land n \in ℝ^{+}) \to \|\frac{{\log n}^{A}}{n^{B}}\| = \frac{\|{\log n}^{A}\|}{\|n^{B}\|}$
90	89	adantrr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|\frac{{\log n}^{A}}{n^{B}}\| = \frac{\|{\log n}^{A}\|}{\|n^{B}\|}$
91	65	rprege0d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to (n^{B} \in ℝ \land 0 \leq n^{B})$
92		absid	$⊢ (n^{B} \in ℝ \land 0 \leq n^{B}) \to \|n^{B}\| = n^{B}$
93	91 92	syl	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|n^{B}\| = n^{B}$
94	93	oveq2d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \frac{\|{\log n}^{A}\|}{\|n^{B}\|} = \frac{\|{\log n}^{A}\|}{n^{B}}$
95	90 94	eqtrd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|\frac{{\log n}^{A}}{n^{B}}\| = \frac{\|{\log n}^{A}\|}{n^{B}}$
96	49	rprege0d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to (\log n \in ℝ \land 0 \leq \log n)$
97	11	recnd	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to if (1 \leq ℜ (A), ℜ (A), 1) \in ℂ$
98	97	adantr	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to if (1 \leq ℜ (A), ℜ (A), 1) \in ℂ$
99		divcxp	$⊢ ((\log n \in ℝ \land 0 \leq \log n) \land n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}} \in ℝ^{+} \land if (1 \leq ℜ (A), ℜ (A), 1) \in ℂ) \to {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} = \frac{{\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)}}{{(n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}}$
100	96 54 98 99	syl3anc	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} = \frac{{\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)}}{{(n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}}$
101	50 53 98	cxpmuld	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to n^{(\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}) if (1 \leq ℜ (A), ℜ (A), 1)} = {(n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}$
102	51	recnd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to B \in ℂ$
103	52	rpne0d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to if (1 \leq ℜ (A), ℜ (A), 1) \neq 0$
104	102 98 103	divcan1d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to (\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}) if (1 \leq ℜ (A), ℜ (A), 1) = B$
105	104	oveq2d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to n^{(\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}) if (1 \leq ℜ (A), ℜ (A), 1)} = n^{B}$
106	101 105	eqtr3d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {(n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} = n^{B}$
107	106	oveq2d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \frac{{\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)}}{{(n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}} = \frac{{\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)}}{n^{B}}$
108	100 107	eqtrd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} = \frac{{\log n}^{if (1 \leq ℜ (A), ℜ (A), 1)}}{n^{B}}$
109	88 95 108	3brtr4d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|\frac{{\log n}^{A}}{n^{B}}\| \leq {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}$
110	58	leabsd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} \leq \|{(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}\|$
111	40 58 60 109 110	letrd	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|\frac{{\log n}^{A}}{n^{B}}\| \leq \|{(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}\|$
112	39	subid1d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to (\frac{{\log n}^{A}}{n^{B}}) - 0 = \frac{{\log n}^{A}}{n^{B}}$
113	112	fveq2d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|(\frac{{\log n}^{A}}{n^{B}}) - 0\| = \|\frac{{\log n}^{A}}{n^{B}}\|$
114	59	subid1d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} - 0 = {(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}$
115	114	fveq2d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|{(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} - 0\| = \|{(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)}\|$
116	111 113 115	3brtr4d	$⊢ ((A \in ℂ \land B \in ℝ^{+}) \land (n \in ℝ^{+} \land 3 \leq n)) \to \|(\frac{{\log n}^{A}}{n^{B}}) - 0\| \leq \|{(\frac{\log n}{n^{\frac{B}{if (1 \leq ℜ (A), ℜ (A), 1)}}})}^{if (1 \leq ℜ (A), ℜ (A), 1)} - 0\|$
117	2 4 22 26 38 116	rlimsqzlem	$⊢ (A \in ℂ \land B \in ℝ^{+}) \to (n \in ℝ^{+} ⟼ \frac{{\log n}^{A}}{n^{B}}) \underset{ℝ}{⇝} 0$

Metamath Proof Explorer

Theorem cxploglim2

Proof