expmulnbnd

Description: Exponentiation with a mantissa greater than 1 is not bounded by any linear function. (Contributed by Mario Carneiro, 31-Mar-2015)

		Ref	Expression
	Assertion	expmulnbnd	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} A k < B^{k}$

Proof

Step	Hyp	Ref	Expression
1		2re	$⊢ 2 \in ℝ$
2		simp1	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to A \in ℝ$
3		remulcl	$⊢ (2 \in ℝ \land A \in ℝ) \to 2 A \in ℝ$
4	1 2 3	sylancr	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 2 A \in ℝ$
5		simp3	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to 1 < B$
6		1re	$⊢ 1 \in ℝ$
7		simp2	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to B \in ℝ$
8		difrp	$⊢ (1 \in ℝ \land B \in ℝ) \to (1 < B \leftrightarrow B - 1 \in ℝ^{+})$
9	6 7 8	sylancr	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to (1 < B \leftrightarrow B - 1 \in ℝ^{+})$
10	5 9	mpbid	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to B - 1 \in ℝ^{+}$
11	4 10	rerpdivcld	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to \frac{2 A}{B - 1} \in ℝ$
12		expnbnd	$⊢ (\frac{2 A}{B - 1} \in ℝ \land B \in ℝ \land 1 < B) \to \exists n \in ℕ \frac{2 A}{B - 1} < B^{n}$
13	11 7 5 12	syl3anc	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to \exists n \in ℕ \frac{2 A}{B - 1} < B^{n}$
14		2nn0	$⊢ 2 \in ℕ_{0}$
15		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
16	15	ad2antrl	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \to n \in ℕ_{0}$
17		nn0mulcl	$⊢ (2 \in ℕ_{0} \land n \in ℕ_{0}) \to 2 n \in ℕ_{0}$
18	14 16 17	sylancr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \to 2 n \in ℕ_{0}$
19	2	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to A \in ℝ$
20		2nn	$⊢ 2 \in ℕ$
21		simprl	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \to n \in ℕ$
22		nnmulcl	$⊢ (2 \in ℕ \land n \in ℕ) \to 2 n \in ℕ$
23	20 21 22	sylancr	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \to 2 n \in ℕ$
24		eluznn	$⊢ (2 n \in ℕ \land k \in ℤ_{\geq 2 n}) \to k \in ℕ$
25	23 24	sylan	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k \in ℕ$
26	25	nnred	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k \in ℝ$
27	19 26	remulcld	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to A k \in ℝ$
28		0re	$⊢ 0 \in ℝ$
29		ifcl	$⊢ (A \in ℝ \land 0 \in ℝ) \to if (0 \leq A, A, 0) \in ℝ$
30	19 28 29	sylancl	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to if (0 \leq A, A, 0) \in ℝ$
31		remulcl	$⊢ (2 \in ℝ \land if (0 \leq A, A, 0) \in ℝ) \to 2 if (0 \leq A, A, 0) \in ℝ$
32	1 30 31	sylancr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 if (0 \leq A, A, 0) \in ℝ$
33		simplrl	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to n \in ℕ$
34	33	nnred	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to n \in ℝ$
35	26 34	resubcld	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k - n \in ℝ$
36	32 35	remulcld	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 if (0 \leq A, A, 0) (k - n) \in ℝ$
37	7	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B \in ℝ$
38	25	nnnn0d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k \in ℕ_{0}$
39		reexpcl	$⊢ (B \in ℝ \land k \in ℕ_{0}) \to B^{k} \in ℝ$
40	37 38 39	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B^{k} \in ℝ$
41		remulcl	$⊢ (2 \in ℝ \land k - n \in ℝ) \to 2 (k - n) \in ℝ$
42	1 35 41	sylancr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 (k - n) \in ℝ$
43	38	nn0ge0d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 0 \leq k$
44		max1	$⊢ (0 \in ℝ \land A \in ℝ) \to 0 \leq if (0 \leq A, A, 0)$
45	28 19 44	sylancr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 0 \leq if (0 \leq A, A, 0)$
46		remulcl	$⊢ (2 \in ℝ \land n \in ℝ) \to 2 n \in ℝ$
47	1 34 46	sylancr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 n \in ℝ$
48		eluzle	$⊢ k \in ℤ_{\geq 2 n} \to 2 n \leq k$
49	48	adantl	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 n \leq k$
50	47 26 26 49	leadd2dd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k + 2 n \leq k + k$
51	26	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k \in ℂ$
52	51	2timesd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 k = k + k$
53	50 52	breqtrrd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k + 2 n \leq 2 k$
54		remulcl	$⊢ (2 \in ℝ \land k \in ℝ) \to 2 k \in ℝ$
55	1 26 54	sylancr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 k \in ℝ$
56		leaddsub	$⊢ (k \in ℝ \land 2 n \in ℝ \land 2 k \in ℝ) \to (k + 2 n \leq 2 k \leftrightarrow k \leq 2 k - 2 n)$
57	26 47 55 56	syl3anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (k + 2 n \leq 2 k \leftrightarrow k \leq 2 k - 2 n)$
58	53 57	mpbid	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k \leq 2 k - 2 n$
59		2cnd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 \in ℂ$
60	34	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to n \in ℂ$
61	59 51 60	subdid	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 (k - n) = 2 k - 2 n$
62	58 61	breqtrrd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k \leq 2 (k - n)$
63		max2	$⊢ (0 \in ℝ \land A \in ℝ) \to A \leq if (0 \leq A, A, 0)$
64	28 19 63	sylancr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to A \leq if (0 \leq A, A, 0)$
65	26 42 19 30 43 45 62 64	lemul12bd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k A \leq 2 (k - n) if (0 \leq A, A, 0)$
66	19	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to A \in ℂ$
67	66 51	mulcomd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to A k = k A$
68	30	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to if (0 \leq A, A, 0) \in ℂ$
69	35	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k - n \in ℂ$
70	59 68 69	mul32d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 if (0 \leq A, A, 0) (k - n) = 2 (k - n) if (0 \leq A, A, 0)$
71	65 67 70	3brtr4d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to A k \leq 2 if (0 \leq A, A, 0) (k - n)$
72	10	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B - 1 \in ℝ^{+}$
73	72	rpred	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B - 1 \in ℝ$
74	73 35	remulcld	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (B - 1) (k - n) \in ℝ$
75	33	nnnn0d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to n \in ℕ_{0}$
76		reexpcl	$⊢ (B \in ℝ \land n \in ℕ_{0}) \to B^{n} \in ℝ$
77	37 75 76	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B^{n} \in ℝ$
78	74 77	remulcld	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (B - 1) (k - n) B^{n} \in ℝ$
79		simplrr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to \frac{2 A}{B - 1} < B^{n}$
80	1 19 3	sylancr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 A \in ℝ$
81	80 77 72	ltdivmuld	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (\frac{2 A}{B - 1} < B^{n} \leftrightarrow 2 A < (B - 1) B^{n})$
82	79 81	mpbid	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 A < (B - 1) B^{n}$
83	5	ad2antrr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 1 < B$
84		posdif	$⊢ (1 \in ℝ \land B \in ℝ) \to (1 < B \leftrightarrow 0 < B - 1)$
85	6 37 84	sylancr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (1 < B \leftrightarrow 0 < B - 1)$
86	83 85	mpbid	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 0 < B - 1$
87	33	nnzd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to n \in ℤ$
88	28	a1i	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 0 \in ℝ$
89	6	a1i	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 1 \in ℝ$
90		0lt1	$⊢ 0 < 1$
91	90	a1i	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 0 < 1$
92	88 89 37 91 83	lttrd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 0 < B$
93		expgt0	$⊢ (B \in ℝ \land n \in ℤ \land 0 < B) \to 0 < B^{n}$
94	37 87 92 93	syl3anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 0 < B^{n}$
95	73 77 86 94	mulgt0d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 0 < (B - 1) B^{n}$
96		oveq2	$⊢ A = if (0 \leq A, A, 0) \to 2 A = 2 if (0 \leq A, A, 0)$
97	96	breq1d	$⊢ A = if (0 \leq A, A, 0) \to (2 A < (B - 1) B^{n} \leftrightarrow 2 if (0 \leq A, A, 0) < (B - 1) B^{n})$
98		2t0e0	$⊢ 2 \cdot 0 = 0$
99		oveq2	$⊢ 0 = if (0 \leq A, A, 0) \to 2 \cdot 0 = 2 if (0 \leq A, A, 0)$
100	98 99	syl5eqr	$⊢ 0 = if (0 \leq A, A, 0) \to 0 = 2 if (0 \leq A, A, 0)$
101	100	breq1d	$⊢ 0 = if (0 \leq A, A, 0) \to (0 < (B - 1) B^{n} \leftrightarrow 2 if (0 \leq A, A, 0) < (B - 1) B^{n})$
102	97 101	ifboth	$⊢ (2 A < (B - 1) B^{n} \land 0 < (B - 1) B^{n}) \to 2 if (0 \leq A, A, 0) < (B - 1) B^{n}$
103	82 95 102	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 if (0 \leq A, A, 0) < (B - 1) B^{n}$
104	73 77	remulcld	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (B - 1) B^{n} \in ℝ$
105		simpr	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k \in ℤ_{\geq 2 n}$
106	60	2timesd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 n = n + n$
107	106	fveq2d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to ℤ_{\geq 2 n} = ℤ_{\geq (n + n)}$
108	105 107	eleqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k \in ℤ_{\geq (n + n)}$
109		eluzsub	$⊢ (n \in ℤ \land n \in ℤ \land k \in ℤ_{\geq (n + n)}) \to k - n \in ℤ_{\geq n}$
110	87 87 108 109	syl3anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k - n \in ℤ_{\geq n}$
111		eluznn	$⊢ (n \in ℕ \land k - n \in ℤ_{\geq n}) \to k - n \in ℕ$
112	33 110 111	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k - n \in ℕ$
113	112	nngt0d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 0 < k - n$
114		ltmul1	$⊢ (2 if (0 \leq A, A, 0) \in ℝ \land (B - 1) B^{n} \in ℝ \land (k - n \in ℝ \land 0 < k - n)) \to (2 if (0 \leq A, A, 0) < (B - 1) B^{n} \leftrightarrow 2 if (0 \leq A, A, 0) (k - n) < (B - 1) B^{n} (k - n))$
115	32 104 35 113 114	syl112anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (2 if (0 \leq A, A, 0) < (B - 1) B^{n} \leftrightarrow 2 if (0 \leq A, A, 0) (k - n) < (B - 1) B^{n} (k - n))$
116	103 115	mpbid	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 if (0 \leq A, A, 0) (k - n) < (B - 1) B^{n} (k - n)$
117	73	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B - 1 \in ℂ$
118	77	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B^{n} \in ℂ$
119	117 118 69	mul32d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (B - 1) B^{n} (k - n) = (B - 1) (k - n) B^{n}$
120	116 119	breqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 if (0 \leq A, A, 0) (k - n) < (B - 1) (k - n) B^{n}$
121		peano2re	$⊢ (B - 1) (k - n) \in ℝ \to (B - 1) (k - n) + 1 \in ℝ$
122	74 121	syl	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (B - 1) (k - n) + 1 \in ℝ$
123	112	nnnn0d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k - n \in ℕ_{0}$
124		reexpcl	$⊢ (B \in ℝ \land k - n \in ℕ_{0}) \to B^{k - n} \in ℝ$
125	37 123 124	syl2anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B^{k - n} \in ℝ$
126	74	ltp1d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (B - 1) (k - n) < (B - 1) (k - n) + 1$
127	88 37 92	ltled	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 0 \leq B$
128		bernneq2	$⊢ (B \in ℝ \land k - n \in ℕ_{0} \land 0 \leq B) \to (B - 1) (k - n) + 1 \leq B^{k - n}$
129	37 123 127 128	syl3anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (B - 1) (k - n) + 1 \leq B^{k - n}$
130	74 122 125 126 129	ltletrd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (B - 1) (k - n) < B^{k - n}$
131	37	recnd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B \in ℂ$
132	92	gt0ne0d	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B \neq 0$
133		eluzelz	$⊢ k \in ℤ_{\geq 2 n} \to k \in ℤ$
134	133	adantl	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to k \in ℤ$
135		expsub	$⊢ ((B \in ℂ \land B \neq 0) \land (k \in ℤ \land n \in ℤ)) \to B^{k - n} = \frac{B^{k}}{B^{n}}$
136	131 132 134 87 135	syl22anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to B^{k - n} = \frac{B^{k}}{B^{n}}$
137	130 136	breqtrd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (B - 1) (k - n) < \frac{B^{k}}{B^{n}}$
138		ltmuldiv	$⊢ ((B - 1) (k - n) \in ℝ \land B^{k} \in ℝ \land (B^{n} \in ℝ \land 0 < B^{n})) \to ((B - 1) (k - n) B^{n} < B^{k} \leftrightarrow (B - 1) (k - n) < \frac{B^{k}}{B^{n}})$
139	74 40 77 94 138	syl112anc	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to ((B - 1) (k - n) B^{n} < B^{k} \leftrightarrow (B - 1) (k - n) < \frac{B^{k}}{B^{n}})$
140	137 139	mpbird	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to (B - 1) (k - n) B^{n} < B^{k}$
141	36 78 40 120 140	lttrd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to 2 if (0 \leq A, A, 0) (k - n) < B^{k}$
142	27 36 40 71 141	lelttrd	$⊢ (((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \land k \in ℤ_{\geq 2 n}) \to A k < B^{k}$
143	142	ralrimiva	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \to \forall k \in ℤ_{\geq 2 n} A k < B^{k}$
144		fveq2	$⊢ j = 2 n \to ℤ_{\geq j} = ℤ_{\geq 2 n}$
145	144	raleqdv	$⊢ j = 2 n \to (\forall k \in ℤ_{\geq j} A k < B^{k} \leftrightarrow \forall k \in ℤ_{\geq 2 n} A k < B^{k})$
146	145	rspcev	$⊢ (2 n \in ℕ_{0} \land \forall k \in ℤ_{\geq 2 n} A k < B^{k}) \to \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} A k < B^{k}$
147	18 143 146	syl2anc	$⊢ ((A \in ℝ \land B \in ℝ \land 1 < B) \land (n \in ℕ \land \frac{2 A}{B - 1} < B^{n})) \to \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} A k < B^{k}$
148	13 147	rexlimddv	$⊢ (A \in ℝ \land B \in ℝ \land 1 < B) \to \exists j \in ℕ_{0} \forall k \in ℤ_{\geq j} A k < B^{k}$

Metamath Proof Explorer

Theorem expmulnbnd

Proof