Theorem cxp2limlem

Description: A linear factor grows slower than any exponential with base greater than 1 . (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	cxp2limlem	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 𝑛 ∈ ℝ+ ↦ ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ) ⇝𝑟 0 )

Proof

Step	Hyp	Ref	Expression
1		0red	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 ∈ ℝ )
2		2rp	⊢ 2 ∈ ℝ+
3		rplogcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
4		2z	⊢ 2 ∈ ℤ
5		rpexpcl	⊢ ( ( ( log ‘ 𝐴 ) ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℝ+ )
6	3 4 5	sylancl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℝ+ )
7		rpdivcl	⊢ ( ( 2 ∈ ℝ+ ∧ ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℝ+ ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℝ+ )
8	2 6 7	sylancr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℝ+ )
9	8	rpcnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ )
10		divrcnv	⊢ ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ → ( 𝑛 ∈ ℝ+ ↦ ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) ) ⇝𝑟 0 )
11	9 10	syl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 𝑛 ∈ ℝ+ ↦ ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) ) ⇝𝑟 0 )
12	8	rpred	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℝ )
13		rerpdivcl	⊢ ( ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℝ ∧ 𝑛 ∈ ℝ+ ) → ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) ∈ ℝ )
14	12 13	sylan	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) ∈ ℝ )
15		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℝ+ )
16		simpl	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
17		1red	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 1 ∈ ℝ )
18		0lt1	⊢ 0 < 1
19	18	a1i	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 1 )
20		simpr	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 1 < 𝐴 )
21	1 17 16 19 20	lttrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 0 < 𝐴 )
22	16 21	elrpd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ+ )
23		rpre	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ∈ ℝ )
24		rpcxpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑛 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝑛 ) ∈ ℝ+ )
25	22 23 24	syl2an	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝐴 ↑𝑐 𝑛 ) ∈ ℝ+ )
26	15 25	rpdivcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ∈ ℝ+ )
27	26	rpred	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ∈ ℝ )
28	3	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℝ+ )
29	15 28	rpmulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 · ( log ‘ 𝐴 ) ) ∈ ℝ+ )
30	29	rpred	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 · ( log ‘ 𝐴 ) ) ∈ ℝ )
31	30	resqcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) ∈ ℝ )
32	31	rehalfcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) ∈ ℝ )
33		1rp	⊢ 1 ∈ ℝ+
34		rpaddcl	⊢ ( ( 1 ∈ ℝ+ ∧ ( 𝑛 · ( log ‘ 𝐴 ) ) ∈ ℝ+ ) → ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) ∈ ℝ+ )
35	33 29 34	sylancr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) ∈ ℝ+ )
36	35	rpred	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
37	36 32	readdcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) + ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) ) ∈ ℝ )
38	30	reefcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( exp ‘ ( 𝑛 · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
39	32 35	ltaddrp2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) < ( ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) + ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) ) )
40		efgt1p2	⊢ ( ( 𝑛 · ( log ‘ 𝐴 ) ) ∈ ℝ+ → ( ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) + ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) ) < ( exp ‘ ( 𝑛 · ( log ‘ 𝐴 ) ) ) )
41	29 40	syl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 1 + ( 𝑛 · ( log ‘ 𝐴 ) ) ) + ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) ) < ( exp ‘ ( 𝑛 · ( log ‘ 𝐴 ) ) ) )
42	32 37 38 39 41	lttrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) < ( exp ‘ ( 𝑛 · ( log ‘ 𝐴 ) ) ) )
43	23	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℝ )
44	43	recnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ∈ ℂ )
45	44	sqcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 ↑ 2 ) ∈ ℂ )
46		2cnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 2 ∈ ℂ )
47	6	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℝ+ )
48	47	rpcnd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
49		2ne0	⊢ 2 ≠ 0
50	49	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 2 ≠ 0 )
51	47	rpne0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( log ‘ 𝐴 ) ↑ 2 ) ≠ 0 )
52	45 46 48 50 51	divdiv2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) = ( ( ( 𝑛 ↑ 2 ) · ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 2 ) )
53	3	rpcnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( log ‘ 𝐴 ) ∈ ℂ )
54	53	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( log ‘ 𝐴 ) ∈ ℂ )
55	44 54	sqmuld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) = ( ( 𝑛 ↑ 2 ) · ( ( log ‘ 𝐴 ) ↑ 2 ) ) )
56	55	oveq1d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) = ( ( ( 𝑛 ↑ 2 ) · ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 2 ) )
57	52 56	eqtr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) = ( ( ( 𝑛 · ( log ‘ 𝐴 ) ) ↑ 2 ) / 2 ) )
58	16	recnd	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → 𝐴 ∈ ℂ )
59	58	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℂ )
60	22	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ∈ ℝ+ )
61	60	rpne0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝐴 ≠ 0 )
62	59 61 44	cxpefd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝐴 ↑𝑐 𝑛 ) = ( exp ‘ ( 𝑛 · ( log ‘ 𝐴 ) ) ) )
63	42 57 62	3brtr4d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) < ( 𝐴 ↑𝑐 𝑛 ) )
64		rpexpcl	⊢ ( ( 𝑛 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( 𝑛 ↑ 2 ) ∈ ℝ+ )
65	15 4 64	sylancl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 ↑ 2 ) ∈ ℝ+ )
66	8	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℝ+ )
67	65 66	rpdivcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) ∈ ℝ+ )
68	67 25 15	ltdiv2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) < ( 𝐴 ↑𝑐 𝑛 ) ↔ ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) < ( 𝑛 / ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) ) ) )
69	63 68	mpbid	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) < ( 𝑛 / ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) ) )
70	9	adantr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ )
71	65	rpne0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 ↑ 2 ) ≠ 0 )
72	66	rpne0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ≠ 0 )
73	44 45 70 71 72	divdiv2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) ) = ( ( 𝑛 · ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) / ( 𝑛 ↑ 2 ) ) )
74	44	sqvald	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 ↑ 2 ) = ( 𝑛 · 𝑛 ) )
75	74	oveq2d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 · ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) / ( 𝑛 ↑ 2 ) ) = ( ( 𝑛 · ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) / ( 𝑛 · 𝑛 ) ) )
76		rpne0	⊢ ( 𝑛 ∈ ℝ+ → 𝑛 ≠ 0 )
77	76	adantl	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 𝑛 ≠ 0 )
78	70 44 44 77 77	divcan5d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( ( 𝑛 · ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) / ( 𝑛 · 𝑛 ) ) = ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) )
79	73 75 78	3eqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( ( 𝑛 ↑ 2 ) / ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) ) ) = ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) )
80	69 79	breqtrd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) < ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) )
81	27 14 80	ltled	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ≤ ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) )
82	81	adantrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑛 ∈ ℝ+ ∧ 0 ≤ 𝑛 ) ) → ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ≤ ( ( 2 / ( ( log ‘ 𝐴 ) ↑ 2 ) ) / 𝑛 ) )
83	26	rpge0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ 𝑛 ∈ ℝ+ ) → 0 ≤ ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) )
84	83	adantrr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) ∧ ( 𝑛 ∈ ℝ+ ∧ 0 ≤ 𝑛 ) ) → 0 ≤ ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) )
85	1 1 11 14 27 82 84	rlimsqz2	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ( 𝑛 ∈ ℝ+ ↦ ( 𝑛 / ( 𝐴 ↑𝑐 𝑛 ) ) ) ⇝𝑟 0 )