Theorem ostth2lem1 21265

Description: Lemma for ostth2 21284, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 21284. If a power is upper bounded by a linear term, the exponent must be less than one. Or in big-O notation, n e. o ( A ^ n ) for any 1 < A. (Contributed by Mario Carneiro, 10-Sep-2014.)

Hypotheses

Ref	Expression
ostth2lem1.1	|- ( ph -> A e. RR )
ostth2lem1.2	|- ( ph -> B e. RR )
ostth2lem1.3	|- ( ( ph /\ n e. NN ) -> ( A ^ n ) <_ ( n x. B ) )

Assertion

Ref	Expression
ostth2lem1	|- ( ph -> A <_ 1 )

Distinct variable groups:   A, n   B, n   ph, n

Proof of Theorem ostth2lem1

Dummy variable k is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2re 10025	. . . . . 6 |- 2 e. RR
2		ostth2lem1.2	. . . . . . 7 |- ( ph -> B e. RR )
3	2	adantr 452	. . . . . 6 |- ( ( ph /\ 1 < A ) -> B e. RR )
4		remulcl 9031	. . . . . 6 |- ( ( 2 e. RR /\ B e. RR ) -> ( 2 x. B ) e. RR )
5	1, 3, 4	sylancr 645	. . . . 5 |- ( ( ph /\ 1 < A ) -> ( 2 x. B ) e. RR )
6		simpr 448	. . . . . 6 |- ( ( ph /\ 1 < A ) -> 1 < A )
7		1re 9046	. . . . . . 7 |- 1 e. RR
8		ostth2lem1.1	. . . . . . . 8 |- ( ph -> A e. RR )
9	8	adantr 452	. . . . . . 7 |- ( ( ph /\ 1 < A ) -> A e. RR )
10		difrp 10601	. . . . . . 7 |- ( ( 1 e. RR /\ A e. RR ) -> ( 1 < A <-> ( A - 1 ) e. RR+ ) )
11	7, 9, 10	sylancr 645	. . . . . 6 |- ( ( ph /\ 1 < A ) -> ( 1 < A <-> ( A - 1 ) e. RR+ ) )
12	6, 11	mpbid 202	. . . . 5 |- ( ( ph /\ 1 < A ) -> ( A - 1 ) e. RR+ )
13	5, 12	rerpdivcld 10631	. . . 4 |- ( ( ph /\ 1 < A ) -> ( ( 2 x. B ) / ( A - 1 ) ) e. RR )
14		expnbnd 11463	. . . 4 |- ( ( ( ( 2 x. B ) / ( A - 1 ) ) e. RR /\ A e. RR /\ 1 < A ) -> E. k e. NN ( ( 2 x. B ) / ( A - 1 ) ) < ( A ^ k ) )
15	13, 9, 6, 14	syl3anc 1184	. . 3 |- ( ( ph /\ 1 < A ) -> E. k e. NN ( ( 2 x. B ) / ( A - 1 ) ) < ( A ^ k ) )
16		nnnn0 10184	. . . . . 6 |- ( k e. NN -> k e. NN0 )
17		reexpcl 11353	. . . . . 6 |- ( ( A e. RR /\ k e. NN0 ) -> ( A ^ k ) e. RR )
18	9, 16, 17	syl2an 464	. . . . 5 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ k ) e. RR )
19	13	adantr 452	. . . . 5 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( 2 x. B ) / ( A - 1 ) ) e. RR )
20	12	rpred 10604	. . . . . . . . . . . 12 |- ( ( ph /\ 1 < A ) -> ( A - 1 ) e. RR )
21	20	adantr 452	. . . . . . . . . . 11 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A - 1 ) e. RR )
22		nnre 9963	. . . . . . . . . . . 12 |- ( k e. NN -> k e. RR )
23	22	adantl 453	. . . . . . . . . . 11 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> k e. RR )
24	21, 23	remulcld 9072	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( A - 1 ) x. k ) e. RR )
25	24, 18	remulcld 9072	. . . . . . . . 9 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) e. RR )
26	8	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> A e. RR )
27		2nn 10089	. . . . . . . . . . . 12 |- 2 e. NN
28		simpr 448	. . . . . . . . . . . 12 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> k e. NN )
29		nnmulcl 9979	. . . . . . . . . . . 12 |- ( ( 2 e. NN /\ k e. NN ) -> ( 2 x. k ) e. NN )
30	27, 28, 29	sylancr 645	. . . . . . . . . . 11 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( 2 x. k ) e. NN )
31		nnnn0 10184	. . . . . . . . . . 11 |- ( ( 2 x. k ) e. NN -> ( 2 x. k ) e. NN0 )
32	30, 31	syl 16	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( 2 x. k ) e. NN0 )
33	26, 32	reexpcld 11495	. . . . . . . . 9 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ ( 2 x. k ) ) e. RR )
34	30	nnred 9971	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( 2 x. k ) e. RR )
35	2	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> B e. RR )
36	34, 35	remulcld 9072	. . . . . . . . 9 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( 2 x. k ) x. B ) e. RR )
37		0re 9047	. . . . . . . . . . . . . . 15 |- 0 e. RR
38	37	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ 1 < A ) -> 0 e. RR )
39	7	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ 1 < A ) -> 1 e. RR )
40		0lt1 9506	. . . . . . . . . . . . . . 15 |- 0 < 1
41	40	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ 1 < A ) -> 0 < 1 )
42	38, 39, 9, 41, 6	lttrd 9187	. . . . . . . . . . . . 13 |- ( ( ph /\ 1 < A ) -> 0 < A )
43	9, 42	elrpd 10602	. . . . . . . . . . . 12 |- ( ( ph /\ 1 < A ) -> A e. RR+ )
44		nnz 10259	. . . . . . . . . . . 12 |- ( k e. NN -> k e. ZZ )
45		rpexpcl 11355	. . . . . . . . . . . 12 |- ( ( A e. RR+ /\ k e. ZZ ) -> ( A ^ k ) e. RR+ )
46	43, 44, 45	syl2an 464	. . . . . . . . . . 11 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ k ) e. RR+ )
47		peano2re 9195	. . . . . . . . . . . . 13 |- ( ( ( A - 1 ) x. k ) e. RR -> ( ( ( A - 1 ) x. k ) + 1 ) e. RR )
48	24, 47	syl 16	. . . . . . . . . . . 12 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) + 1 ) e. RR )
49	24	ltp1d 9897	. . . . . . . . . . . 12 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( A - 1 ) x. k ) < ( ( ( A - 1 ) x. k ) + 1 ) )
50	16	adantl 453	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> k e. NN0 )
51	43	adantr 452	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> A e. RR+ )
52	51	rpge0d 10608	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> 0 <_ A )
53		bernneq2 11461	. . . . . . . . . . . . 13 |- ( ( A e. RR /\ k e. NN0 /\ 0 <_ A ) -> ( ( ( A - 1 ) x. k ) + 1 ) <_ ( A ^ k ) )
54	26, 50, 52, 53	syl3anc 1184	. . . . . . . . . . . 12 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) + 1 ) <_ ( A ^ k ) )
55	24, 48, 18, 49, 54	ltletrd 9186	. . . . . . . . . . 11 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( A - 1 ) x. k ) < ( A ^ k ) )
56	24, 18, 46, 55	ltmul1dd 10655	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) < ( ( A ^ k ) x. ( A ^ k ) ) )
57	23	recnd 9070	. . . . . . . . . . . . 13 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> k e. CC )
58	57	2timesd 10166	. . . . . . . . . . . 12 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( 2 x. k ) = ( k + k ) )
59	58	oveq2d 6056	. . . . . . . . . . 11 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ ( 2 x. k ) ) = ( A ^ ( k + k ) ) )
60	26	recnd 9070	. . . . . . . . . . . 12 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> A e. CC )
61	60, 50, 50	expaddd 11480	. . . . . . . . . . 11 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ ( k + k ) ) = ( ( A ^ k ) x. ( A ^ k ) ) )
62	59, 61	eqtrd 2436	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ ( 2 x. k ) ) = ( ( A ^ k ) x. ( A ^ k ) ) )
63	56, 62	breqtrrd 4198	. . . . . . . . 9 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) < ( A ^ ( 2 x. k ) ) )
64		ostth2lem1.3	. . . . . . . . . . . 12 |- ( ( ph /\ n e. NN ) -> ( A ^ n ) <_ ( n x. B ) )
65	64	ralrimiva 2749	. . . . . . . . . . 11 |- ( ph -> A. n e. NN ( A ^ n ) <_ ( n x. B ) )
66	65	ad2antrr 707	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> A. n e. NN ( A ^ n ) <_ ( n x. B ) )
67		oveq2 6048	. . . . . . . . . . . 12 |- ( n = ( 2 x. k ) -> ( A ^ n ) = ( A ^ ( 2 x. k ) ) )
68		oveq1 6047	. . . . . . . . . . . 12 |- ( n = ( 2 x. k ) -> ( n x. B ) = ( ( 2 x. k ) x. B ) )
69	67, 68	breq12d 4185	. . . . . . . . . . 11 |- ( n = ( 2 x. k ) -> ( ( A ^ n ) <_ ( n x. B ) <-> ( A ^ ( 2 x. k ) ) <_ ( ( 2 x. k ) x. B ) ) )
70	69	rspcv 3008	. . . . . . . . . 10 |- ( ( 2 x. k ) e. NN -> ( A. n e. NN ( A ^ n ) <_ ( n x. B ) -> ( A ^ ( 2 x. k ) ) <_ ( ( 2 x. k ) x. B ) ) )
71	30, 66, 70	sylc 58	. . . . . . . . 9 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ ( 2 x. k ) ) <_ ( ( 2 x. k ) x. B ) )
72	25, 33, 36, 63, 71	ltletrd 9186	. . . . . . . 8 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) < ( ( 2 x. k ) x. B ) )
73	21	recnd 9070	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A - 1 ) e. CC )
74	18	recnd 9070	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ k ) e. CC )
75	73, 74, 57	mul32d 9232	. . . . . . . . 9 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) x. k ) = ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) )
76		2cn 10026	. . . . . . . . . . 11 |- 2 e. CC
77	76	a1i 11	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> 2 e. CC )
78	35	recnd 9070	. . . . . . . . . 10 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> B e. CC )
79	77, 78, 57	mul32d 9232	. . . . . . . . 9 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( 2 x. B ) x. k ) = ( ( 2 x. k ) x. B ) )
80	75, 79	breq12d 4185	. . . . . . . 8 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( ( A - 1 ) x. ( A ^ k ) ) x. k ) < ( ( 2 x. B ) x. k ) <-> ( ( ( A - 1 ) x. k ) x. ( A ^ k ) ) < ( ( 2 x. k ) x. B ) ) )
81	72, 80	mpbird 224	. . . . . . 7 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) x. k ) < ( ( 2 x. B ) x. k ) )
82	21, 18	remulcld 9072	. . . . . . . 8 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( A - 1 ) x. ( A ^ k ) ) e. RR )
83	5	adantr 452	. . . . . . . 8 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( 2 x. B ) e. RR )
84		nngt0 9985	. . . . . . . . 9 |- ( k e. NN -> 0 < k )
85	84	adantl 453	. . . . . . . 8 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> 0 < k )
86		ltmul1 9816	. . . . . . . 8 |- ( ( ( ( A - 1 ) x. ( A ^ k ) ) e. RR /\ ( 2 x. B ) e. RR /\ ( k e. RR /\ 0 < k ) ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) < ( 2 x. B ) <-> ( ( ( A - 1 ) x. ( A ^ k ) ) x. k ) < ( ( 2 x. B ) x. k ) ) )
87	82, 83, 23, 85, 86	syl112anc 1188	. . . . . . 7 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) < ( 2 x. B ) <-> ( ( ( A - 1 ) x. ( A ^ k ) ) x. k ) < ( ( 2 x. B ) x. k ) ) )
88	81, 87	mpbird 224	. . . . . 6 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( A - 1 ) x. ( A ^ k ) ) < ( 2 x. B ) )
89	12	rpgt0d 10607	. . . . . . . 8 |- ( ( ph /\ 1 < A ) -> 0 < ( A - 1 ) )
90	89	adantr 452	. . . . . . 7 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> 0 < ( A - 1 ) )
91		ltmuldiv2 9837	. . . . . . 7 |- ( ( ( A ^ k ) e. RR /\ ( 2 x. B ) e. RR /\ ( ( A - 1 ) e. RR /\ 0 < ( A - 1 ) ) ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) < ( 2 x. B ) <-> ( A ^ k ) < ( ( 2 x. B ) / ( A - 1 ) ) ) )
92	18, 83, 21, 90, 91	syl112anc 1188	. . . . . 6 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( ( ( A - 1 ) x. ( A ^ k ) ) < ( 2 x. B ) <-> ( A ^ k ) < ( ( 2 x. B ) / ( A - 1 ) ) ) )
93	88, 92	mpbid 202	. . . . 5 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> ( A ^ k ) < ( ( 2 x. B ) / ( A - 1 ) ) )
94	18, 19, 93	ltnsymd 9178	. . . 4 |- ( ( ( ph /\ 1 < A ) /\ k e. NN ) -> -. ( ( 2 x. B ) / ( A - 1 ) ) < ( A ^ k ) )
95	94	nrexdv 2769	. . 3 |- ( ( ph /\ 1 < A ) -> -. E. k e. NN ( ( 2 x. B ) / ( A - 1 ) ) < ( A ^ k ) )
96	15, 95	pm2.65da 560	. 2 |- ( ph -> -. 1 < A )
97		lenlt 9110	. . 3 |- ( ( A e. RR /\ 1 e. RR ) -> ( A <_ 1 <-> -. 1 < A ) )
98	8, 7, 97	sylancl 644	. 2 |- ( ph -> ( A <_ 1 <-> -. 1 < A ) )
99	96, 98	mpbird 224	1 |- ( ph -> A <_ 1 )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 177   /\ wa 359   = wceq 1649   e. wcel 1721   A.wral 2666   E.wrex 2667   class class class wbr 4172  (class class class)co 6040   CCcc 8944   RRcr 8945   0cc0 8946   1c1 8947   + caddc 8949   x. cmul 8951   < clt 9076   <_ cle 9077   - cmin 9247   / cdiv 9633   NNcn 9956   2c2 10005   NN0cn0 10177   ZZcz 10238   RR+crp 10568   ^cexp 11337

This theorem is referenced by:  ostth2lem4  21283

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pow 4337  ax-pr 4363  ax-un 4660  ax-cnex 9002  ax-resscn 9003  ax-1cn 9004  ax-icn 9005  ax-addcl 9006  ax-addrcl 9007  ax-mulcl 9008  ax-mulrcl 9009  ax-mulcom 9010  ax-addass 9011  ax-mulass 9012  ax-distr 9013  ax-i2m1 9014  ax-1ne0 9015  ax-1rid 9016  ax-rnegex 9017  ax-rrecex 9018  ax-cnre 9019  ax-pre-lttri 9020  ax-pre-lttrn 9021  ax-pre-ltadd 9022  ax-pre-mulgt0 9023  ax-pre-sup 9024

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-nel 2570  df-ral 2671  df-rex 2672  df-reu 2673  df-rmo 2674  df-rab 2675  df-v 2918  df-sbc 3122  df-csb 3212  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-pss 3296  df-nul 3589  df-if 3700  df-pw 3761  df-sn 3780  df-pr 3781  df-tp 3782  df-op 3783  df-uni 3976  df-iun 4055  df-br 4173  df-opab 4227  df-mpt 4228  df-tr 4263  df-eprel 4454  df-id 4458  df-po 4463  df-so 4464  df-fr 4501  df-we 4503  df-ord 4544  df-on 4545  df-lim 4546  df-suc 4547  df-om 4805  df-xp 4843  df-rel 4844  df-cnv 4845  df-co 4846  df-dm 4847  df-rn 4848  df-res 4849  df-ima 4850  df-iota 5377  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-ov 6043  df-oprab 6044  df-mpt2 6045  df-2nd 6309  df-riota 6508  df-recs 6592  df-rdg 6627  df-er 6864  df-en 7069  df-dom 7070  df-sdom 7071  df-sup 7404  df-pnf 9078  df-mnf 9079  df-xr 9080  df-ltxr 9081  df-le 9082  df-sub 9249  df-neg 9250  df-div 9634  df-nn 9957  df-2 10014  df-n0 10178  df-z 10239  df-uz 10445  df-rp 10569  df-fl 11157  df-seq 11279  df-exp 11338