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	$⊢ φ \to A \in ℝ$
	ostth2lem1.2	$⊢ φ \to B \in ℝ$
	ostth2lem1.3	$⊢ (φ \land n \in ℕ) \to A^{n} \leq n B$
Assertion	ostth2lem1	$⊢ φ \to A \leq 1$

Proof

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

Metamath Proof Explorer

Theorem ostth2lem1

Proof