Theorem ostth2lem1

Description: Lemma for ostth2 , although it is just a simple statement about exponentials which does not involve any specifics of ostth2 . 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)

	Ref	Expression
Hypotheses	ostth2lem1.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	ostth2lem1.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	ostth2lem1.3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ↑ 𝑛 ) ≤ ( 𝑛 · 𝐵 ) )
Assertion	ostth2lem1	⊢ ( 𝜑 → 𝐴 ≤ 1 )

Proof

Step	Hyp	Ref	Expression
1		ostth2lem1.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		ostth2lem1.2	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		ostth2lem1.3	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ℕ ) → ( 𝐴 ↑ 𝑛 ) ≤ ( 𝑛 · 𝐵 ) )
4		2re	⊢ 2 ∈ ℝ
5	2	adantr	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 𝐵 ∈ ℝ )
6		remulcl	⊢ ( ( 2 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 2 · 𝐵 ) ∈ ℝ )
7	4 5 6	sylancr	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ( 2 · 𝐵 ) ∈ ℝ )
8		simpr	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 1 < 𝐴 )
9		1re	⊢ 1 ∈ ℝ
10	1	adantr	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
11		difrp	⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 1 < 𝐴 ↔ ( 𝐴 − 1 ) ∈ ℝ+ ) )
12	9 10 11	sylancr	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ( 1 < 𝐴 ↔ ( 𝐴 − 1 ) ∈ ℝ+ ) )
13	8 12	mpbid	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ( 𝐴 − 1 ) ∈ ℝ+ )
14	7 13	rerpdivcld	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ( ( 2 · 𝐵 ) / ( 𝐴 − 1 ) ) ∈ ℝ )
15		expnbnd	⊢ ( ( ( ( 2 · 𝐵 ) / ( 𝐴 − 1 ) ) ∈ ℝ ∧ 𝐴 ∈ ℝ ∧ 1 < 𝐴 ) → ∃ 𝑘 ∈ ℕ ( ( 2 · 𝐵 ) / ( 𝐴 − 1 ) ) < ( 𝐴 ↑ 𝑘 ) )
16	14 10 8 15	syl3anc	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ∃ 𝑘 ∈ ℕ ( ( 2 · 𝐵 ) / ( 𝐴 − 1 ) ) < ( 𝐴 ↑ 𝑘 ) )
17		nnnn0	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℕ0 )
18		reexpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ )
19	10 17 18	syl2an	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ )
20	14	adantr	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝐵 ) / ( 𝐴 − 1 ) ) ∈ ℝ )
21	13	rpred	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ( 𝐴 − 1 ) ∈ ℝ )
22	21	adantr	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 − 1 ) ∈ ℝ )
23		nnre	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
24	23	adantl	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ )
25	22 24	remulcld	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 − 1 ) · 𝑘 ) ∈ ℝ )
26	25 19	remulcld	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) · 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℝ )
27	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℝ )
28		2nn	⊢ 2 ∈ ℕ
29		simpr	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ )
30		nnmulcl	⊢ ( ( 2 ∈ ℕ ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ℕ )
31	28 29 30	sylancr	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ℕ )
32	31	nnnn0d	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ℕ0 )
33	27 32	reexpcld	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ ( 2 · 𝑘 ) ) ∈ ℝ )
34	31	nnred	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) ∈ ℝ )
35	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝐵 ∈ ℝ )
36	34 35	remulcld	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝑘 ) · 𝐵 ) ∈ ℝ )
37		0red	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 0 ∈ ℝ )
38	9	a1i	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 1 ∈ ℝ )
39		0lt1	⊢ 0 < 1
40	39	a1i	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 0 < 1 )
41	37 38 10 40 8	lttrd	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 0 < 𝐴 )
42	10 41	elrpd	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ+ )
43		nnz	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
44		rpexpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝑘 ∈ ℤ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ+ )
45	42 43 44	syl2an	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℝ+ )
46		peano2re	⊢ ( ( ( 𝐴 − 1 ) · 𝑘 ) ∈ ℝ → ( ( ( 𝐴 − 1 ) · 𝑘 ) + 1 ) ∈ ℝ )
47	25 46	syl	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) · 𝑘 ) + 1 ) ∈ ℝ )
48	25	ltp1d	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 − 1 ) · 𝑘 ) < ( ( ( 𝐴 − 1 ) · 𝑘 ) + 1 ) )
49	17	adantl	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℕ0 )
50	42	adantr	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℝ+ )
51	50	rpge0d	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 0 ≤ 𝐴 )
52		bernneq2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ0 ∧ 0 ≤ 𝐴 ) → ( ( ( 𝐴 − 1 ) · 𝑘 ) + 1 ) ≤ ( 𝐴 ↑ 𝑘 ) )
53	27 49 51 52	syl3anc	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) · 𝑘 ) + 1 ) ≤ ( 𝐴 ↑ 𝑘 ) )
54	25 47 19 48 53	ltletrd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 − 1 ) · 𝑘 ) < ( 𝐴 ↑ 𝑘 ) )
55	25 19 45 54	ltmul1dd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) · 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) < ( ( 𝐴 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
56	24	recnd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
57	56	2timesd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝑘 ) = ( 𝑘 + 𝑘 ) )
58	57	oveq2d	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ ( 2 · 𝑘 ) ) = ( 𝐴 ↑ ( 𝑘 + 𝑘 ) ) )
59	27	recnd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝐴 ∈ ℂ )
60	59 49 49	expaddd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ ( 𝑘 + 𝑘 ) ) = ( ( 𝐴 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
61	58 60	eqtrd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ ( 2 · 𝑘 ) ) = ( ( 𝐴 ↑ 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
62	55 61	breqtrrd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) · 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) < ( 𝐴 ↑ ( 2 · 𝑘 ) ) )
63		oveq2	⊢ ( 𝑛 = ( 2 · 𝑘 ) → ( 𝐴 ↑ 𝑛 ) = ( 𝐴 ↑ ( 2 · 𝑘 ) ) )
64		oveq1	⊢ ( 𝑛 = ( 2 · 𝑘 ) → ( 𝑛 · 𝐵 ) = ( ( 2 · 𝑘 ) · 𝐵 ) )
65	63 64	breq12d	⊢ ( 𝑛 = ( 2 · 𝑘 ) → ( ( 𝐴 ↑ 𝑛 ) ≤ ( 𝑛 · 𝐵 ) ↔ ( 𝐴 ↑ ( 2 · 𝑘 ) ) ≤ ( ( 2 · 𝑘 ) · 𝐵 ) ) )
66	3	ralrimiva	⊢ ( 𝜑 → ∀ 𝑛 ∈ ℕ ( 𝐴 ↑ 𝑛 ) ≤ ( 𝑛 · 𝐵 ) )
67	66	ad2antrr	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ ℕ ( 𝐴 ↑ 𝑛 ) ≤ ( 𝑛 · 𝐵 ) )
68	65 67 31	rspcdva	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ ( 2 · 𝑘 ) ) ≤ ( ( 2 · 𝑘 ) · 𝐵 ) )
69	26 33 36 62 68	ltletrd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) · 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) < ( ( 2 · 𝑘 ) · 𝐵 ) )
70	22	recnd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 − 1 ) ∈ ℂ )
71	19	recnd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) ∈ ℂ )
72	70 71 56	mul32d	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) · 𝑘 ) = ( ( ( 𝐴 − 1 ) · 𝑘 ) · ( 𝐴 ↑ 𝑘 ) ) )
73		2cnd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 2 ∈ ℂ )
74	35	recnd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 𝐵 ∈ ℂ )
75	73 74 56	mul32d	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 2 · 𝐵 ) · 𝑘 ) = ( ( 2 · 𝑘 ) · 𝐵 ) )
76	69 72 75	3brtr4d	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) · 𝑘 ) < ( ( 2 · 𝐵 ) · 𝑘 ) )
77	22 19	remulcld	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℝ )
78	7	adantr	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 2 · 𝐵 ) ∈ ℝ )
79		nngt0	⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
80	79	adantl	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 0 < 𝑘 )
81		ltmul1	⊢ ( ( ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) ∈ ℝ ∧ ( 2 · 𝐵 ) ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) < ( 2 · 𝐵 ) ↔ ( ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) · 𝑘 ) < ( ( 2 · 𝐵 ) · 𝑘 ) ) )
82	77 78 24 80 81	syl112anc	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) < ( 2 · 𝐵 ) ↔ ( ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) · 𝑘 ) < ( ( 2 · 𝐵 ) · 𝑘 ) ) )
83	76 82	mpbird	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) < ( 2 · 𝐵 ) )
84	13	rpgt0d	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 0 < ( 𝐴 − 1 ) )
85	84	adantr	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → 0 < ( 𝐴 − 1 ) )
86		ltmuldiv2	⊢ ( ( ( 𝐴 ↑ 𝑘 ) ∈ ℝ ∧ ( 2 · 𝐵 ) ∈ ℝ ∧ ( ( 𝐴 − 1 ) ∈ ℝ ∧ 0 < ( 𝐴 − 1 ) ) ) → ( ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) < ( 2 · 𝐵 ) ↔ ( 𝐴 ↑ 𝑘 ) < ( ( 2 · 𝐵 ) / ( 𝐴 − 1 ) ) ) )
87	19 78 22 85 86	syl112anc	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐴 − 1 ) · ( 𝐴 ↑ 𝑘 ) ) < ( 2 · 𝐵 ) ↔ ( 𝐴 ↑ 𝑘 ) < ( ( 2 · 𝐵 ) / ( 𝐴 − 1 ) ) ) )
88	83 87	mpbid	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐴 ↑ 𝑘 ) < ( ( 2 · 𝐵 ) / ( 𝐴 − 1 ) ) )
89	19 20 88	ltnsymd	⊢ ( ( ( 𝜑 ∧ 1 < 𝐴 ) ∧ 𝑘 ∈ ℕ ) → ¬ ( ( 2 · 𝐵 ) / ( 𝐴 − 1 ) ) < ( 𝐴 ↑ 𝑘 ) )
90	89	nrexdv	⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ¬ ∃ 𝑘 ∈ ℕ ( ( 2 · 𝐵 ) / ( 𝐴 − 1 ) ) < ( 𝐴 ↑ 𝑘 ) )
91	16 90	pm2.65da	⊢ ( 𝜑 → ¬ 1 < 𝐴 )
92		lenlt	⊢ ( ( 𝐴 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 𝐴 ≤ 1 ↔ ¬ 1 < 𝐴 ) )
93	1 9 92	sylancl	⊢ ( 𝜑 → ( 𝐴 ≤ 1 ↔ ¬ 1 < 𝐴 ) )
94	91 93	mpbird	⊢ ( 𝜑 → 𝐴 ≤ 1 )