nexple

Description: A lower bound for an exponentiation. (Contributed by Thierry Arnoux, 19-Aug-2017)

		Ref	Expression
	Assertion	nexple	$⊢ (A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \to A \leq B^{A}$

Proof

Step	Hyp	Ref	Expression
1		simpr	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A \in ℕ) \to A \in ℕ$
2		simpl2	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A \in ℕ) \to B \in ℝ$
3		simpl3	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A \in ℕ) \to 2 \leq B$
4		id	$⊢ k = 1 \to k = 1$
5		oveq2	$⊢ k = 1 \to B^{k} = B^{1}$
6	4 5	breq12d	$⊢ k = 1 \to (k \leq B^{k} \leftrightarrow 1 \leq B^{1})$
7	6	imbi2d	$⊢ k = 1 \to (((B \in ℝ \land 2 \leq B) \to k \leq B^{k}) \leftrightarrow ((B \in ℝ \land 2 \leq B) \to 1 \leq B^{1}))$
8		id	$⊢ k = n \to k = n$
9		oveq2	$⊢ k = n \to B^{k} = B^{n}$
10	8 9	breq12d	$⊢ k = n \to (k \leq B^{k} \leftrightarrow n \leq B^{n})$
11	10	imbi2d	$⊢ k = n \to (((B \in ℝ \land 2 \leq B) \to k \leq B^{k}) \leftrightarrow ((B \in ℝ \land 2 \leq B) \to n \leq B^{n}))$
12		id	$⊢ k = n + 1 \to k = n + 1$
13		oveq2	$⊢ k = n + 1 \to B^{k} = B^{n + 1}$
14	12 13	breq12d	$⊢ k = n + 1 \to (k \leq B^{k} \leftrightarrow n + 1 \leq B^{n + 1})$
15	14	imbi2d	$⊢ k = n + 1 \to (((B \in ℝ \land 2 \leq B) \to k \leq B^{k}) \leftrightarrow ((B \in ℝ \land 2 \leq B) \to n + 1 \leq B^{n + 1}))$
16		id	$⊢ k = A \to k = A$
17		oveq2	$⊢ k = A \to B^{k} = B^{A}$
18	16 17	breq12d	$⊢ k = A \to (k \leq B^{k} \leftrightarrow A \leq B^{A})$
19	18	imbi2d	$⊢ k = A \to (((B \in ℝ \land 2 \leq B) \to k \leq B^{k}) \leftrightarrow ((B \in ℝ \land 2 \leq B) \to A \leq B^{A}))$
20		simpl	$⊢ (B \in ℝ \land 2 \leq B) \to B \in ℝ$
21		1nn0	$⊢ 1 \in ℕ_{0}$
22	21	a1i	$⊢ (B \in ℝ \land 2 \leq B) \to 1 \in ℕ_{0}$
23		1red	$⊢ (B \in ℝ \land 2 \leq B) \to 1 \in ℝ$
24		2re	$⊢ 2 \in ℝ$
25	24	a1i	$⊢ (B \in ℝ \land 2 \leq B) \to 2 \in ℝ$
26		1le2	$⊢ 1 \leq 2$
27	26	a1i	$⊢ (B \in ℝ \land 2 \leq B) \to 1 \leq 2$
28		simpr	$⊢ (B \in ℝ \land 2 \leq B) \to 2 \leq B$
29	23 25 20 27 28	letrd	$⊢ (B \in ℝ \land 2 \leq B) \to 1 \leq B$
30	20 22 29	expge1d	$⊢ (B \in ℝ \land 2 \leq B) \to 1 \leq B^{1}$
31		simp1	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n \in ℕ$
32	31	nnnn0d	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n \in ℕ_{0}$
33	32	nn0red	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n \in ℝ$
34		1red	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to 1 \in ℝ$
35	33 34	readdcld	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n + 1 \in ℝ$
36	20	3ad2ant2	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to B \in ℝ$
37	33 36	remulcld	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n B \in ℝ$
38	36 32	reexpcld	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to B^{n} \in ℝ$
39	38 36	remulcld	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to B^{n} B \in ℝ$
40	24	a1i	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to 2 \in ℝ$
41	33 40	remulcld	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n \cdot 2 \in ℝ$
42	31	nnge1d	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to 1 \leq n$
43	34 33 33 42	leadd2dd	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n + 1 \leq n + n$
44	33	recnd	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n \in ℂ$
45	44	times2d	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n \cdot 2 = n + n$
46	43 45	breqtrrd	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n + 1 \leq n \cdot 2$
47	32	nn0ge0d	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to 0 \leq n$
48		simp2r	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to 2 \leq B$
49	40 36 33 47 48	lemul2ad	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n \cdot 2 \leq n B$
50	35 41 37 46 49	letrd	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n + 1 \leq n B$
51		0red	$⊢ (B \in ℝ \land 2 \leq B) \to 0 \in ℝ$
52		0le2	$⊢ 0 \leq 2$
53	52	a1i	$⊢ (B \in ℝ \land 2 \leq B) \to 0 \leq 2$
54	51 25 20 53 28	letrd	$⊢ (B \in ℝ \land 2 \leq B) \to 0 \leq B$
55	54	3ad2ant2	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to 0 \leq B$
56		simp3	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n \leq B^{n}$
57	33 38 36 55 56	lemul1ad	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n B \leq B^{n} B$
58	35 37 39 50 57	letrd	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n + 1 \leq B^{n} B$
59	36	recnd	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to B \in ℂ$
60	59 32	expp1d	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to B^{n + 1} = B^{n} B$
61	58 60	breqtrrd	$⊢ (n \in ℕ \land (B \in ℝ \land 2 \leq B) \land n \leq B^{n}) \to n + 1 \leq B^{n + 1}$
62	61	3exp	$⊢ n \in ℕ \to ((B \in ℝ \land 2 \leq B) \to (n \leq B^{n} \to n + 1 \leq B^{n + 1}))$
63	62	a2d	$⊢ n \in ℕ \to (((B \in ℝ \land 2 \leq B) \to n \leq B^{n}) \to ((B \in ℝ \land 2 \leq B) \to n + 1 \leq B^{n + 1}))$
64	7 11 15 19 30 63	nnind	$⊢ A \in ℕ \to ((B \in ℝ \land 2 \leq B) \to A \leq B^{A})$
65	64	3impib	$⊢ (A \in ℕ \land B \in ℝ \land 2 \leq B) \to A \leq B^{A}$
66	1 2 3 65	syl3anc	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A \in ℕ) \to A \leq B^{A}$
67		0le1	$⊢ 0 \leq 1$
68	67	a1i	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A = 0) \to 0 \leq 1$
69		simpr	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A = 0) \to A = 0$
70	69	oveq2d	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A = 0) \to B^{A} = B^{0}$
71		simpl2	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A = 0) \to B \in ℝ$
72	71	recnd	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A = 0) \to B \in ℂ$
73	72	exp0d	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A = 0) \to B^{0} = 1$
74	70 73	eqtrd	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A = 0) \to B^{A} = 1$
75	68 69 74	3brtr4d	$⊢ ((A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \land A = 0) \to A \leq B^{A}$
76		elnn0	$⊢ A \in ℕ_{0} \leftrightarrow (A \in ℕ \lor A = 0)$
77	76	biimpi	$⊢ A \in ℕ_{0} \to (A \in ℕ \lor A = 0)$
78	77	3ad2ant1	$⊢ (A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \to (A \in ℕ \lor A = 0)$
79	66 75 78	mpjaodan	$⊢ (A \in ℕ_{0} \land B \in ℝ \land 2 \leq B) \to A \leq B^{A}$

Metamath Proof Explorer

Theorem nexple

Proof