expnbnd - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > expnbnd		GIF version

Theorem expnbnd 10599

Description: Exponentiation with a base greater than 1 has no upper bound. (Contributed by NM, 20-Oct-2007.)

**Assertion**
Ref	Expression
expnbnd	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))

Distinct variable groups: 𝐴,𝑘 𝐵,𝑘

**Proof of Theorem expnbnd**
Step	Hyp	Ref	Expression
1		simp1 992	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐴 ∈ ℝ)
2	1	adantr 274	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 1 < 𝐴) → 𝐴 ∈ ℝ)
3		simp2 993	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐵 ∈ ℝ)
4	3	adantr 274	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 1 < 𝐴) → 𝐵 ∈ ℝ)
5		simpr 109	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 1 < 𝐴) → 1 < 𝐴)
6		simp3 994	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 1 < 𝐵)
7	6	adantr 274	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 1 < 𝐴) → 1 < 𝐵)
8		1red 7935	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 1 ∈ ℝ)
9	1, 8	resubcld 8300	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐴 − 1) ∈ ℝ)
10	3, 8	resubcld 8300	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵 − 1) ∈ ℝ)
11	8, 3	posdifd 8451	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
12	6, 11	mpbid 146	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 0 < (𝐵 − 1))
13	10, 12	gt0ap0d 8548	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵 − 1) # 0)
14	9, 10, 13	redivclapd 8752	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ)
15		arch 9132	. . . . . . 7 ⊢ (((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ → ∃𝑘 ∈ ℕ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘)
16	14, 15	syl 14	. . . . . 6 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘)
17	16	3expa 1198	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘)
18	17	adantrl 475	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) → ∃𝑘 ∈ ℕ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘)
19		simplll 528	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → 𝐴 ∈ ℝ)
20	19	adantr 274	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 𝐴 ∈ ℝ)
21		simpllr 529	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → 𝐵 ∈ ℝ)
22		1red 7935	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → 1 ∈ ℝ)
23	21, 22	resubcld 8300	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → (𝐵 − 1) ∈ ℝ)
24		simpr 109	. . . . . . . . . . 11 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ)
25	24	nnred 8891	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ)
26	23, 25	remulcld 7950	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → ((𝐵 − 1) · 𝑘) ∈ ℝ)
27	26, 22	readdcld 7949	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → (((𝐵 − 1) · 𝑘) + 1) ∈ ℝ)
28	27	adantr 274	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → (((𝐵 − 1) · 𝑘) + 1) ∈ ℝ)
29	24	nnnn0d 9188	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℕ₀)
30		reexpcl 10493	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ₀) → (𝐵↑𝑘) ∈ ℝ)
31	21, 29, 30	syl2anc 409	. . . . . . . 8 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) ∈ ℝ)
32	31	adantr 274	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → (𝐵↑𝑘) ∈ ℝ)
33		simpr 109	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → ((𝐴 − 1) / (𝐵 − 1)) < 𝑘)
34		1red 7935	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 1 ∈ ℝ)
35	20, 34	resubcld 8300	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → (𝐴 − 1) ∈ ℝ)
36		simplr 525	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 𝑘 ∈ ℕ)
37	36	nnred 8891	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 𝑘 ∈ ℝ)
38	21	adantr 274	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 𝐵 ∈ ℝ)
39	38, 34	resubcld 8300	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → (𝐵 − 1) ∈ ℝ)
40		simplrr 531	. . . . . . . . . . . 12 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → 1 < 𝐵)
41	40	adantr 274	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 1 < 𝐵)
42	34, 38	posdifd 8451	. . . . . . . . . . 11 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
43	41, 42	mpbid 146	. . . . . . . . . 10 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 0 < (𝐵 − 1))
44		ltdivmul 8792	. . . . . . . . . 10 ⊢ (((𝐴 − 1) ∈ ℝ ∧ 𝑘 ∈ ℝ ∧ ((𝐵 − 1) ∈ ℝ ∧ 0 < (𝐵 − 1))) → (((𝐴 − 1) / (𝐵 − 1)) < 𝑘 ↔ (𝐴 − 1) < ((𝐵 − 1) · 𝑘)))
45	35, 37, 39, 43, 44	syl112anc 1237	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → (((𝐴 − 1) / (𝐵 − 1)) < 𝑘 ↔ (𝐴 − 1) < ((𝐵 − 1) · 𝑘)))
46	33, 45	mpbid 146	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → (𝐴 − 1) < ((𝐵 − 1) · 𝑘))
47	39, 37	remulcld 7950	. . . . . . . . 9 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → ((𝐵 − 1) · 𝑘) ∈ ℝ)
48	20, 34, 47	ltsubaddd 8460	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → ((𝐴 − 1) < ((𝐵 − 1) · 𝑘) ↔ 𝐴 < (((𝐵 − 1) · 𝑘) + 1)))
49	46, 48	mpbid 146	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 𝐴 < (((𝐵 − 1) · 𝑘) + 1))
50	36	nnnn0d 9188	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 𝑘 ∈ ℕ₀)
51		0red 7921	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → 0 ∈ ℝ)
52		0lt1 8046	. . . . . . . . . . . 12 ⊢ 0 < 1
53		0re 7920	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
54		1re 7919	. . . . . . . . . . . . 13 ⊢ 1 ∈ ℝ
55		lttr 7993	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 1 ∧ 1 < 𝐵) → 0 < 𝐵))
56	53, 54, 55	mp3an12 1322	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → ((0 < 1 ∧ 1 < 𝐵) → 0 < 𝐵))
57	52, 56	mpani 428	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → (1 < 𝐵 → 0 < 𝐵))
58	21, 40, 57	sylc 62	. . . . . . . . . 10 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → 0 < 𝐵)
59	51, 21, 58	ltled 8038	. . . . . . . . 9 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → 0 ≤ 𝐵)
60	59	adantr 274	. . . . . . . 8 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 0 ≤ 𝐵)
61		bernneq2 10597	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ 𝑘 ∈ ℕ₀ ∧ 0 ≤ 𝐵) → (((𝐵 − 1) · 𝑘) + 1) ≤ (𝐵↑𝑘))
62	38, 50, 60, 61	syl3anc 1233	. . . . . . 7 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → (((𝐵 − 1) · 𝑘) + 1) ≤ (𝐵↑𝑘))
63	20, 28, 32, 49, 62	ltletrd 8342	. . . . . 6 ⊢ (((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) ∧ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘) → 𝐴 < (𝐵↑𝑘))
64	63	ex 114	. . . . 5 ⊢ ((((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) ∧ 𝑘 ∈ ℕ) → (((𝐴 − 1) / (𝐵 − 1)) < 𝑘 → 𝐴 < (𝐵↑𝑘)))
65	64	reximdva 2572	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) → (∃𝑘 ∈ ℕ ((𝐴 − 1) / (𝐵 − 1)) < 𝑘 → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)))
66	18, 65	mpd 13	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (1 < 𝐴 ∧ 1 < 𝐵)) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
67	2, 4, 5, 7, 66	syl22anc 1234	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 1 < 𝐴) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
68		1nn 8889	. . 3 ⊢ 1 ∈ ℕ
69		simpr 109	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 𝐵) → 𝐴 < 𝐵)
70		simpl2 996	. . . . . 6 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℝ)
71	70	recnd 7948	. . . . 5 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 𝐵) → 𝐵 ∈ ℂ)
72		exp1 10482	. . . . 5 ⊢ (𝐵 ∈ ℂ → (𝐵↑1) = 𝐵)
73	71, 72	syl 14	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 𝐵) → (𝐵↑1) = 𝐵)
74	69, 73	breqtrrd 4017	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 𝐵) → 𝐴 < (𝐵↑1))
75		oveq2 5861	. . . . 5 ⊢ (𝑘 = 1 → (𝐵↑𝑘) = (𝐵↑1))
76	75	breq2d 4001	. . . 4 ⊢ (𝑘 = 1 → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑1)))
77	76	rspcev 2834	. . 3 ⊢ ((1 ∈ ℕ ∧ 𝐴 < (𝐵↑1)) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
78	68, 74, 77	sylancr 412	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
79		axltwlin 7987	. . . . 5 ⊢ ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (1 < 𝐵 → (1 < 𝐴 ∨ 𝐴 < 𝐵)))
80	54, 79	mp3an1 1319	. . . 4 ⊢ ((𝐵 ∈ ℝ ∧ 𝐴 ∈ ℝ) → (1 < 𝐵 → (1 < 𝐴 ∨ 𝐴 < 𝐵)))
81	80	ancoms 266	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < 𝐵 → (1 < 𝐴 ∨ 𝐴 < 𝐵)))
82	81	3impia 1195	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (1 < 𝐴 ∨ 𝐴 < 𝐵))
83	67, 78, 82	mpjaodan 793	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 703 ∧ w3a 973 = wceq 1348 ∈ wcel 2141 ∃wrex 2449 class class class wbr 3989 (class class class)co 5853 ℂcc 7772 ℝcr 7773 0cc0 7774 1c1 7775 + caddc 7777 · cmul 7779 < clt 7954 ≤ cle 7955 − cmin 8090 / cdiv 8589 ℕcn 8878 ℕ₀cn0 9135 ↑cexp 10475

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893

This theorem depends on definitions: df-bi 116 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-frec 6370 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-n0 9136 df-z 9213 df-uz 9488 df-seqfrec 10402 df-exp 10476

This theorem is referenced by: expnlbnd 10600 pclemub 12241

W3C validator