expubnd

Description: An upper bound on A ^ N when 2 <_ A . (Contributed by NM, 19-Dec-2005)

		Ref	Expression
	Assertion	expubnd	$⊢ (A \in ℝ \land N \in ℕ_{0} \land 2 \leq A) \to A^{N} \leq 2^{N} {(A - 1)}^{N}$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (A \in ℝ \land N \in ℕ_{0} \land 2 \leq A) \to A \in ℝ$
2		2re	$⊢ 2 \in ℝ$
3		peano2rem	$⊢ A \in ℝ \to A - 1 \in ℝ$
4		remulcl	$⊢ (2 \in ℝ \land A - 1 \in ℝ) \to 2 (A - 1) \in ℝ$
5	2 3 4	sylancr	$⊢ A \in ℝ \to 2 (A - 1) \in ℝ$
6	5	3ad2ant1	$⊢ (A \in ℝ \land N \in ℕ_{0} \land 2 \leq A) \to 2 (A - 1) \in ℝ$
7		simp2	$⊢ (A \in ℝ \land N \in ℕ_{0} \land 2 \leq A) \to N \in ℕ_{0}$
8		0le2	$⊢ 0 \leq 2$
9		0re	$⊢ 0 \in ℝ$
10		letr	$⊢ (0 \in ℝ \land 2 \in ℝ \land A \in ℝ) \to ((0 \leq 2 \land 2 \leq A) \to 0 \leq A)$
11	9 2 10	mp3an12	$⊢ A \in ℝ \to ((0 \leq 2 \land 2 \leq A) \to 0 \leq A)$
12	8 11	mpani	$⊢ A \in ℝ \to (2 \leq A \to 0 \leq A)$
13	12	imp	$⊢ (A \in ℝ \land 2 \leq A) \to 0 \leq A$
14		resubcl	$⊢ (A \in ℝ \land 2 \in ℝ) \to A - 2 \in ℝ$
15	2 14	mpan2	$⊢ A \in ℝ \to A - 2 \in ℝ$
16		leadd2	$⊢ (2 \in ℝ \land A \in ℝ \land A - 2 \in ℝ) \to (2 \leq A \leftrightarrow A - 2 + 2 \leq A - 2 + A)$
17	2 16	mp3an1	$⊢ (A \in ℝ \land A - 2 \in ℝ) \to (2 \leq A \leftrightarrow A - 2 + 2 \leq A - 2 + A)$
18	15 17	mpdan	$⊢ A \in ℝ \to (2 \leq A \leftrightarrow A - 2 + 2 \leq A - 2 + A)$
19	18	biimpa	$⊢ (A \in ℝ \land 2 \leq A) \to A - 2 + 2 \leq A - 2 + A$
20		recn	$⊢ A \in ℝ \to A \in ℂ$
21		2cn	$⊢ 2 \in ℂ$
22		npcan	$⊢ (A \in ℂ \land 2 \in ℂ) \to A - 2 + 2 = A$
23	20 21 22	sylancl	$⊢ A \in ℝ \to A - 2 + 2 = A$
24	23	adantr	$⊢ (A \in ℝ \land 2 \leq A) \to A - 2 + 2 = A$
25		ax-1cn	$⊢ 1 \in ℂ$
26		subdi	$⊢ (2 \in ℂ \land A \in ℂ \land 1 \in ℂ) \to 2 (A - 1) = 2 A - 2 \cdot 1$
27	21 25 26	mp3an13	$⊢ A \in ℂ \to 2 (A - 1) = 2 A - 2 \cdot 1$
28		2times	$⊢ A \in ℂ \to 2 A = A + A$
29		2t1e2	$⊢ 2 \cdot 1 = 2$
30	29	a1i	$⊢ A \in ℂ \to 2 \cdot 1 = 2$
31	28 30	oveq12d	$⊢ A \in ℂ \to 2 A - 2 \cdot 1 = A + A - 2$
32		addsub	$⊢ (A \in ℂ \land A \in ℂ \land 2 \in ℂ) \to A + A - 2 = A - 2 + A$
33	21 32	mp3an3	$⊢ (A \in ℂ \land A \in ℂ) \to A + A - 2 = A - 2 + A$
34	33	anidms	$⊢ A \in ℂ \to A + A - 2 = A - 2 + A$
35	27 31 34	3eqtrrd	$⊢ A \in ℂ \to A - 2 + A = 2 (A - 1)$
36	20 35	syl	$⊢ A \in ℝ \to A - 2 + A = 2 (A - 1)$
37	36	adantr	$⊢ (A \in ℝ \land 2 \leq A) \to A - 2 + A = 2 (A - 1)$
38	19 24 37	3brtr3d	$⊢ (A \in ℝ \land 2 \leq A) \to A \leq 2 (A - 1)$
39	13 38	jca	$⊢ (A \in ℝ \land 2 \leq A) \to (0 \leq A \land A \leq 2 (A - 1))$
40	39	3adant2	$⊢ (A \in ℝ \land N \in ℕ_{0} \land 2 \leq A) \to (0 \leq A \land A \leq 2 (A - 1))$
41		leexp1a	$⊢ ((A \in ℝ \land 2 (A - 1) \in ℝ \land N \in ℕ_{0}) \land (0 \leq A \land A \leq 2 (A - 1))) \to A^{N} \leq {2 (A - 1)}^{N}$
42	1 6 7 40 41	syl31anc	$⊢ (A \in ℝ \land N \in ℕ_{0} \land 2 \leq A) \to A^{N} \leq {2 (A - 1)}^{N}$
43	3	recnd	$⊢ A \in ℝ \to A - 1 \in ℂ$
44		mulexp	$⊢ (2 \in ℂ \land A - 1 \in ℂ \land N \in ℕ_{0}) \to {2 (A - 1)}^{N} = 2^{N} {(A - 1)}^{N}$
45	21 44	mp3an1	$⊢ (A - 1 \in ℂ \land N \in ℕ_{0}) \to {2 (A - 1)}^{N} = 2^{N} {(A - 1)}^{N}$
46	43 45	sylan	$⊢ (A \in ℝ \land N \in ℕ_{0}) \to {2 (A - 1)}^{N} = 2^{N} {(A - 1)}^{N}$
47	46	3adant3	$⊢ (A \in ℝ \land N \in ℕ_{0} \land 2 \leq A) \to {2 (A - 1)}^{N} = 2^{N} {(A - 1)}^{N}$
48	42 47	breqtrd	$⊢ (A \in ℝ \land N \in ℕ_{0} \land 2 \leq A) \to A^{N} \leq 2^{N} {(A - 1)}^{N}$

Metamath Proof Explorer

Theorem expubnd

Proof