expnbnd - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > expnbnd		Structured version Visualization version GIF version

Theorem expnbnd 14270

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		1nn 12245	. . 3 ⊢ 1 ∈ ℕ
2		1re 11209	. . . . . . . 8 ⊢ 1 ∈ ℝ
3		lttr 11287	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 1 ∧ 1 < 𝐵) → 𝐴 < 𝐵))
4	2, 3	mp3an2 1478	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 1 ∧ 1 < 𝐵) → 𝐴 < 𝐵))
5	4	exp4b 435	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 1 → (1 < 𝐵 → 𝐴 < 𝐵))))
6	5	com34 92	. . . . 5 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 < 𝐵 → (𝐴 < 1 → 𝐴 < 𝐵))))
7	6	3imp1 1366	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 1) → 𝐴 < 𝐵)
8		recn 11191	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
9		exp1 14105	. . . . . . 7 ⊢ (𝐵 ∈ ℂ → (𝐵↑1) = 𝐵)
10	8, 9	syl 18	. . . . . 6 ⊢ (𝐵 ∈ ℝ → (𝐵↑1) = 𝐵)
11	10	3ad2ant2 1152	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵↑1) = 𝐵)
12	11	adantr 485	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 1) → (𝐵↑1) = 𝐵)
13	7, 12	breqtrrd 5140	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 1) → 𝐴 < (𝐵↑1))
14		oveq2 7420	. . . . 5 ⊢ (𝑘 = 1 → (𝐵↑𝑘) = (𝐵↑1))
15	14	breq2d 5122	. . . 4 ⊢ (𝑘 = 1 → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑1)))
16	15	rspcev 3582	. . 3 ⊢ ((1 ∈ ℕ ∧ 𝐴 < (𝐵↑1)) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
17	1, 13, 16	sylancr 598	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 1) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
18		peano2rem 11526	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ∈ ℝ)
19	18	adantr 485	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐴 − 1) ∈ ℝ)
20		peano2rem 11526	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈ ℝ)
21	20	adantr 485	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵 − 1) ∈ ℝ)
22	21	adantl 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵 − 1) ∈ ℝ)
23		posdif 11708	. . . . . . . . . . . . . 14 ⊢ ((1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
24	2, 23	mpan 702	. . . . . . . . . . . . 13 ⊢ (𝐵 ∈ ℝ → (1 < 𝐵 ↔ 0 < (𝐵 − 1)))
25	24	biimpa 481	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℝ ∧ 1 < 𝐵) → 0 < (𝐵 − 1))
26	25	gt0ne0d 11779	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵 − 1) ≠ 0)
27	26	adantl 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵 − 1) ≠ 0)
28	19, 22, 27	redivcld 12044	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ)
29	28	adantll 726	. . . . . . . 8 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ)
30	18	adantl 486	. . . . . . . . . 10 ⊢ ((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) → (𝐴 − 1) ∈ ℝ)
31		subge0 11728	. . . . . . . . . . . 12 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ) → (0 ≤ (𝐴 − 1) ↔ 1 ≤ 𝐴))
32	2, 31	mpan2 703	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → (0 ≤ (𝐴 − 1) ↔ 1 ≤ 𝐴))
33	32	biimparc 484	. . . . . . . . . 10 ⊢ ((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) → 0 ≤ (𝐴 − 1))
34	30, 33	jca 520	. . . . . . . . 9 ⊢ ((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) → ((𝐴 − 1) ∈ ℝ ∧ 0 ≤ (𝐴 − 1)))
35	21, 25	jca 520	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ ∧ 1 < 𝐵) → ((𝐵 − 1) ∈ ℝ ∧ 0 < (𝐵 − 1)))
36		divge0 12085	. . . . . . . . 9 ⊢ ((((𝐴 − 1) ∈ ℝ ∧ 0 ≤ (𝐴 − 1)) ∧ ((𝐵 − 1) ∈ ℝ ∧ 0 < (𝐵 − 1))) → 0 ≤ ((𝐴 − 1) / (𝐵 − 1)))
37	34, 35, 36	syl2an 607	. . . . . . . 8 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 ≤ ((𝐴 − 1) / (𝐵 − 1)))
38		flge0nn0 13855	. . . . . . . 8 ⊢ ((((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ ∧ 0 ≤ ((𝐴 − 1) / (𝐵 − 1))) → (⌊‘((𝐴 − 1) / (𝐵 − 1))) ∈ ℕ₀)
39	29, 37, 38	syl2anc 595	. . . . . . 7 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (⌊‘((𝐴 − 1) / (𝐵 − 1))) ∈ ℕ₀)
40		nn0p1nn 12544	. . . . . . 7 ⊢ ((⌊‘((𝐴 − 1) / (𝐵 − 1))) ∈ ℕ₀ → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ)
41	39, 40	syl 18	. . . . . 6 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ)
42		simplr 780	. . . . . . 7 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 ∈ ℝ)
43	21	adantl 486	. . . . . . . . 9 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵 − 1) ∈ ℝ)
44		peano2nn0 12545	. . . . . . . . . . 11 ⊢ ((⌊‘((𝐴 − 1) / (𝐵 − 1))) ∈ ℕ₀ → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ₀)
45	39, 44	syl 18	. . . . . . . . . 10 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ₀)
46	45	nn0red 12567	. . . . . . . . 9 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℝ)
47	43, 46	remulcld 11240	. . . . . . . 8 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ)
48		peano2re 11384	. . . . . . . 8 ⊢ (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ∈ ℝ)
49	47, 48	syl 18	. . . . . . 7 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ∈ ℝ)
50		simprl 782	. . . . . . . 8 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐵 ∈ ℝ)
51		reexpcl 14116	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ₀) → (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ)
52	50, 45, 51	syl2anc 595	. . . . . . 7 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ)
53		flltp1 13835	. . . . . . . . . 10 ⊢ (((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ → ((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))
54	29, 53	syl 18	. . . . . . . . 9 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))
55	30	adantr 485	. . . . . . . . . 10 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐴 − 1) ∈ ℝ)
56	25	adantl 486	. . . . . . . . . 10 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 < (𝐵 − 1))
57		ltdivmul 12091	. . . . . . . . . 10 ⊢ (((𝐴 − 1) ∈ ℝ ∧ ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℝ ∧ ((𝐵 − 1) ∈ ℝ ∧ 0 < (𝐵 − 1))) → (((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ↔ (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))))
58	55, 46, 43, 56, 57	syl112anc 1401	. . . . . . . . 9 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐴 − 1) / (𝐵 − 1)) < ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ↔ (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))))
59	54, 58	mpbid 235	. . . . . . . 8 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))
60		ltsubadd 11685	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ) → ((𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ↔ 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1)))
61	2, 60	mp3an2 1478	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ) → ((𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ↔ 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1)))
62	42, 47, 61	syl2anc 595	. . . . . . . 8 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ↔ 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1)))
63	59, 62	mpbid 235	. . . . . . 7 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1))
64		0lt1 11737	. . . . . . . . . . . 12 ⊢ 0 < 1
65		0re 11211	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
66		lttr 11287	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 1 ∧ 1 < 𝐵) → 0 < 𝐵))
67	65, 2, 66	mp3an12 1480	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → ((0 < 1 ∧ 1 < 𝐵) → 0 < 𝐵))
68	64, 67	mpani 708	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → (1 < 𝐵 → 0 < 𝐵))
69		ltle 11299	. . . . . . . . . . . 12 ⊢ ((0 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (0 < 𝐵 → 0 ≤ 𝐵))
70	65, 69	mpan 702	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → (0 < 𝐵 → 0 ≤ 𝐵))
71	68, 70	syld 48	. . . . . . . . . 10 ⊢ (𝐵 ∈ ℝ → (1 < 𝐵 → 0 ≤ 𝐵))
72	71	imp 411	. . . . . . . . 9 ⊢ ((𝐵 ∈ ℝ ∧ 1 < 𝐵) → 0 ≤ 𝐵)
73	72	adantl 486	. . . . . . . 8 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 ≤ 𝐵)
74		bernneq2 14268	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ₀ ∧ 0 ≤ 𝐵) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ≤ (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))
75	50, 45, 73, 74	syl3anc 1398	. . . . . . 7 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ≤ (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))
76	42, 49, 52, 63, 75	ltletrd 11371	. . . . . 6 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))
77		oveq2 7420	. . . . . . . 8 ⊢ (𝑘 = ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) → (𝐵↑𝑘) = (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))
78	77	breq2d 5122	. . . . . . 7 ⊢ (𝑘 = ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))))
79	78	rspcev 3582	. . . . . 6 ⊢ ((((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ ∧ 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
80	41, 76, 79	syl2anc 595	. . . . 5 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
81	80	exp43 441	. . . 4 ⊢ (1 ≤ 𝐴 → (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 < 𝐵 → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)))))
82	81	com4l 93	. . 3 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 < 𝐵 → (1 ≤ 𝐴 → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘)))))
83	82	3imp1 1366	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 1 ≤ 𝐴) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
84		simp1 1154	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐴 ∈ ℝ)
85		1red 11210	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 1 ∈ ℝ)
86	17, 83, 84, 85	ltlecasei 11319	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∃wrex 3089 class class class wbr 5110 ‘cfv 6538 (class class class)co 7412 ℂcc 11099 ℝcr 11100 0cc0 11101 1c1 11102 + caddc 11104 · cmul 11106 < clt 11244 ≤ cle 11245 − cmin 11442 / cdiv 11872 ℕcn 12234 ℕ₀cn0 12505 ⌊cfl 13825 ↑cexp 14099

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734 ax-cnex 11157 ax-resscn 11158 ax-1cn 11159 ax-icn 11160 ax-addcl 11161 ax-addrcl 11162 ax-mulcl 11163 ax-mulrcl 11164 ax-mulcom 11165 ax-addass 11166 ax-mulass 11167 ax-distr 11168 ax-i2m1 11169 ax-1ne0 11170 ax-1rid 11171 ax-rnegex 11172 ax-rrecex 11173 ax-cnre 11174 ax-pre-lttri 11175 ax-pre-lttrn 11176 ax-pre-ltadd 11177 ax-pre-mulgt0 11178 ax-pre-sup 11179

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7864 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-sup 9403 df-inf 9404 df-pnf 11246 df-mnf 11247 df-xr 11248 df-ltxr 11249 df-le 11250 df-sub 11444 df-neg 11445 df-div 11873 df-nn 12235 df-n0 12506 df-z 12593 df-uz 12864 df-fl 13827 df-seq 14040 df-exp 14100

This theorem is referenced by: expnlbnd 14271 expmulnbnd 14273 bitsfzolem 16493 bitsfi 16496 pclem 16899 aaliou3lem8 26487 ostth2lem1 27760 ostth3 27780 knoppndvlem18 37096

W3C validator