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 14259

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 12235	. . 3 ⊢ 1 ∈ ℕ
2		1re 11196	. . . . . . . 8 ⊢ 1 ∈ ℝ
3		lttr 11274	. . . . . . . 8 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 1 ∧ 1 < 𝐵) → 𝐴 < 𝐵))
4	2, 3	mp3an2 1473	. . . . . . 7 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((𝐴 < 1 ∧ 1 < 𝐵) → 𝐴 < 𝐵))
5	4	exp4b 435	. . . . . 6 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (𝐴 < 1 → (1 < 𝐵 → 𝐴 < 𝐵))))
6	5	com34 92	. . . . 5 ⊢ (𝐴 ∈ ℝ → (𝐵 ∈ ℝ → (1 < 𝐵 → (𝐴 < 1 → 𝐴 < 𝐵))))
7	6	3imp1 1364	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 1) → 𝐴 < 𝐵)
8		recn 11178	. . . . . . 7 ⊢ (𝐵 ∈ ℝ → 𝐵 ∈ ℂ)
9		exp1 14094	. . . . . . 7 ⊢ (𝐵 ∈ ℂ → (𝐵↑1) = 𝐵)
10	8, 9	syl 18	. . . . . 6 ⊢ (𝐵 ∈ ℝ → (𝐵↑1) = 𝐵)
11	10	3ad2ant2 1150	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵↑1) = 𝐵)
12	11	adantr 485	. . . 4 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 1) → (𝐵↑1) = 𝐵)
13	7, 12	breqtrrd 5133	. . 3 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 1) → 𝐴 < (𝐵↑1))
14		oveq2 7408	. . . . 5 ⊢ (𝑘 = 1 → (𝐵↑𝑘) = (𝐵↑1))
15	14	breq2d 5117	. . . 4 ⊢ (𝑘 = 1 → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑1)))
16	15	rspcev 3584	. . 3 ⊢ ((1 ∈ ℕ ∧ 𝐴 < (𝐵↑1)) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
17	1, 13, 16	sylancr 598	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 𝐴 < 1) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
18		peano2rem 11513	. . . . . . . . . . 11 ⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ∈ ℝ)
19	18	adantr 485	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐴 − 1) ∈ ℝ)
20		peano2rem 11513	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → (𝐵 − 1) ∈ ℝ)
21	20	adantr 485	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵 − 1) ∈ ℝ)
22	21	adantl 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵 − 1) ∈ ℝ)
23		posdif 11695	. . . . . . . . . . . . . 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 11766	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℝ ∧ 1 < 𝐵) → (𝐵 − 1) ≠ 0)
27	26	adantl 486	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵 − 1) ≠ 0)
28	19, 22, 27	redivcld 12034	. . . . . . . . 9 ⊢ ((𝐴 ∈ ℝ ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ)
29	28	adantll 726	. . . . . . . 8 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ)
30	18	adantl 486	. . . . . . . . . 10 ⊢ ((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) → (𝐴 − 1) ∈ ℝ)
31		subge0 11715	. . . . . . . . . . . 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 12075	. . . . . . . . 9 ⊢ ((((𝐴 − 1) ∈ ℝ ∧ 0 ≤ (𝐴 − 1)) ∧ ((𝐵 − 1) ∈ ℝ ∧ 0 < (𝐵 − 1))) → 0 ≤ ((𝐴 − 1) / (𝐵 − 1)))
37	34, 35, 36	syl2an 607	. . . . . . . 8 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 0 ≤ ((𝐴 − 1) / (𝐵 − 1)))
38		flge0nn0 13844	. . . . . . . 8 ⊢ ((((𝐴 − 1) / (𝐵 − 1)) ∈ ℝ ∧ 0 ≤ ((𝐴 − 1) / (𝐵 − 1))) → (⌊‘((𝐴 − 1) / (𝐵 − 1))) ∈ ℕ₀)
39	29, 37, 38	syl2anc 595	. . . . . . 7 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (⌊‘((𝐴 − 1) / (𝐵 − 1))) ∈ ℕ₀)
40		nn0p1nn 12534	. . . . . . 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 12535	. . . . . . . . . . 11 ⊢ ((⌊‘((𝐴 − 1) / (𝐵 − 1))) ∈ ℕ₀ → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ₀)
45	39, 44	syl 18	. . . . . . . . . 10 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ₀)
46	45	nn0red 12557	. . . . . . . . 9 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℝ)
47	43, 46	remulcld 11227	. . . . . . . 8 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ)
48		peano2re 11371	. . . . . . . 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 14105	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ₀) → (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ)
52	50, 45, 51	syl2anc 595	. . . . . . 7 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ)
53		flltp1 13824	. . . . . . . . . 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 12081	. . . . . . . . . 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 1397	. . . . . . . . 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 11672	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℝ ∧ 1 ∈ ℝ ∧ ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ∈ ℝ) → ((𝐴 − 1) < ((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) ↔ 𝐴 < (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1)))
61	2, 60	mp3an2 1473	. . . . . . . . 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 11724	. . . . . . . . . . . 12 ⊢ 0 < 1
65		0re 11198	. . . . . . . . . . . . 13 ⊢ 0 ∈ ℝ
66		lttr 11274	. . . . . . . . . . . . 13 ⊢ ((0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 < 1 ∧ 1 < 𝐵) → 0 < 𝐵))
67	65, 2, 66	mp3an12 1475	. . . . . . . . . . . 12 ⊢ (𝐵 ∈ ℝ → ((0 < 1 ∧ 1 < 𝐵) → 0 < 𝐵))
68	64, 67	mpani 708	. . . . . . . . . . 11 ⊢ (𝐵 ∈ ℝ → (1 < 𝐵 → 0 < 𝐵))
69		ltle 11286	. . . . . . . . . . . 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 14257	. . . . . . . 8 ⊢ ((𝐵 ∈ ℝ ∧ ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) ∈ ℕ₀ ∧ 0 ≤ 𝐵) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ≤ (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))
75	50, 45, 73, 74	syl3anc 1394	. . . . . . 7 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → (((𝐵 − 1) · ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)) + 1) ≤ (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))
76	42, 49, 52, 63, 75	ltletrd 11358	. . . . . 6 ⊢ (((1 ≤ 𝐴 ∧ 𝐴 ∈ ℝ) ∧ (𝐵 ∈ ℝ ∧ 1 < 𝐵)) → 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))
77		oveq2 7408	. . . . . . . 8 ⊢ (𝑘 = ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) → (𝐵↑𝑘) = (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1)))
78	77	breq2d 5117	. . . . . . 7 ⊢ (𝑘 = ((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1) → (𝐴 < (𝐵↑𝑘) ↔ 𝐴 < (𝐵↑((⌊‘((𝐴 − 1) / (𝐵 − 1))) + 1))))
79	78	rspcev 3584	. . . . . 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 1364	. 2 ⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) ∧ 1 ≤ 𝐴) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))
84		simp1 1152	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 𝐴 ∈ ℝ)
85		1red 11197	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → 1 ∈ ℝ)
86	17, 83, 84, 85	ltlecasei 11306	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 1 < 𝐵) → ∃𝑘 ∈ ℕ 𝐴 < (𝐵↑𝑘))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 ∧ w3a 1101 = wceq 1563 ∈ wcel 2145 ≠ wne 2960 ∃wrex 3089 class class class wbr 5105 ‘cfv 6525 (class class class)co 7400 ℂcc 11086 ℝcr 11087 0cc0 11088 1c1 11089 + caddc 11091 · cmul 11093 < clt 11231 ≤ cle 11232 − cmin 11429 / cdiv 11859 ℕcn 12224 ℕ₀cn0 12495 ⌊cfl 13814 ↑cexp 14088

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-sep 5251 ax-nul 5261 ax-pow 5327 ax-pr 5395 ax-un 7722 ax-cnex 11144 ax-resscn 11145 ax-1cn 11146 ax-icn 11147 ax-addcl 11148 ax-addrcl 11149 ax-mulcl 11150 ax-mulrcl 11151 ax-mulcom 11152 ax-addass 11153 ax-mulass 11154 ax-distr 11155 ax-i2m1 11156 ax-1ne0 11157 ax-1rid 11158 ax-rnegex 11159 ax-rrecex 11160 ax-cnre 11161 ax-pre-lttri 11162 ax-pre-lttrn 11163 ax-pre-ltadd 11164 ax-pre-mulgt0 11165 ax-pre-sup 11166

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3370 df-reu 3371 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-pss 3927 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4869 df-iun 4954 df-br 5106 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5547 df-eprel 5552 df-po 5560 df-so 5561 df-fr 5605 df-we 5607 df-xp 5658 df-rel 5659 df-cnv 5660 df-co 5661 df-dm 5662 df-rn 5663 df-res 5664 df-ima 5665 df-pred 6292 df-ord 6353 df-on 6354 df-lim 6355 df-suc 6356 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-f1 6530 df-fo 6531 df-f1o 6532 df-fv 6533 df-riota 7357 df-ov 7403 df-oprab 7404 df-mpo 7405 df-om 7851 df-2nd 7975 df-frecs 8266 df-wrecs 8297 df-recs 8346 df-rdg 8385 df-er 8682 df-en 8932 df-dom 8933 df-sdom 8934 df-sup 9390 df-inf 9391 df-pnf 11233 df-mnf 11234 df-xr 11235 df-ltxr 11236 df-le 11237 df-sub 11431 df-neg 11432 df-div 11860 df-nn 12225 df-n0 12496 df-z 12583 df-uz 12854 df-fl 13816 df-seq 14029 df-exp 14089

This theorem is referenced by: expnlbnd 14260 expmulnbnd 14262 bitsfzolem 16482 bitsfi 16485 pclem 16888 aaliou3lem8 26467 ostth2lem1 27740 ostth3 27760 knoppndvlem18 36980

W3C validator