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

Theorem chebbnd1 25206
 Description: The Chebyshev bound: The function π(𝑥) is eventually lower bounded by a positive constant times 𝑥 / log(𝑥). Alternatively stated, the function (𝑥 / log(𝑥)) / π(𝑥) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014.)
Assertion
Ref Expression
chebbnd1 (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π𝑥))) ∈ 𝑂(1)

Proof of Theorem chebbnd1
StepHypRef Expression
1 2re 11128 . . . . 5 2 ∈ ℝ
2 pnfxr 10130 . . . . 5 +∞ ∈ ℝ*
3 icossre 12292 . . . . 5 ((2 ∈ ℝ ∧ +∞ ∈ ℝ*) → (2[,)+∞) ⊆ ℝ)
41, 2, 3mp2an 708 . . . 4 (2[,)+∞) ⊆ ℝ
54a1i 11 . . 3 (⊤ → (2[,)+∞) ⊆ ℝ)
6 elicopnf 12307 . . . . . . . . . 10 (2 ∈ ℝ → (𝑥 ∈ (2[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥)))
71, 6ax-mp 5 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥))
87simplbi 475 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℝ)
9 0red 10079 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → 0 ∈ ℝ)
10 1re 10077 . . . . . . . . . 10 1 ∈ ℝ
1110a1i 11 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → 1 ∈ ℝ)
12 0lt1 10588 . . . . . . . . . 10 0 < 1
1312a1i 11 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → 0 < 1)
141a1i 11 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) → 2 ∈ ℝ)
15 1lt2 11232 . . . . . . . . . . 11 1 < 2
1615a1i 11 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) → 1 < 2)
177simprbi 479 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) → 2 ≤ 𝑥)
1811, 14, 8, 16, 17ltletrd 10235 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → 1 < 𝑥)
199, 11, 8, 13, 18lttrd 10236 . . . . . . . 8 (𝑥 ∈ (2[,)+∞) → 0 < 𝑥)
208, 19elrpd 11907 . . . . . . 7 (𝑥 ∈ (2[,)+∞) → 𝑥 ∈ ℝ+)
218, 18rplogcld 24420 . . . . . . 7 (𝑥 ∈ (2[,)+∞) → (log‘𝑥) ∈ ℝ+)
2220, 21rpdivcld 11927 . . . . . 6 (𝑥 ∈ (2[,)+∞) → (𝑥 / (log‘𝑥)) ∈ ℝ+)
23 ppinncl 24945 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 2 ≤ 𝑥) → (π𝑥) ∈ ℕ)
247, 23sylbi 207 . . . . . . 7 (𝑥 ∈ (2[,)+∞) → (π𝑥) ∈ ℕ)
2524nnrpd 11908 . . . . . 6 (𝑥 ∈ (2[,)+∞) → (π𝑥) ∈ ℝ+)
2622, 25rpdivcld 11927 . . . . 5 (𝑥 ∈ (2[,)+∞) → ((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ+)
2726rpcnd 11912 . . . 4 (𝑥 ∈ (2[,)+∞) → ((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℂ)
2827adantl 481 . . 3 ((⊤ ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℂ)
29 8re 11143 . . . 4 8 ∈ ℝ
3029a1i 11 . . 3 (⊤ → 8 ∈ ℝ)
31 2rp 11875 . . . . . . . 8 2 ∈ ℝ+
32 relogcl 24367 . . . . . . . 8 (2 ∈ ℝ+ → (log‘2) ∈ ℝ)
3331, 32ax-mp 5 . . . . . . 7 (log‘2) ∈ ℝ
34 ere 14863 . . . . . . . . 9 e ∈ ℝ
351, 34remulcli 10092 . . . . . . . 8 (2 · e) ∈ ℝ
36 2pos 11150 . . . . . . . . . 10 0 < 2
37 epos 14979 . . . . . . . . . 10 0 < e
381, 34, 36, 37mulgt0ii 10208 . . . . . . . . 9 0 < (2 · e)
3935, 38gt0ne0ii 10602 . . . . . . . 8 (2 · e) ≠ 0
4035, 39rereccli 10828 . . . . . . 7 (1 / (2 · e)) ∈ ℝ
4133, 40resubcli 10381 . . . . . 6 ((log‘2) − (1 / (2 · e))) ∈ ℝ
42 2t1e2 11214 . . . . . . . . . 10 (2 · 1) = 2
43 egt2lt3 14978 . . . . . . . . . . . . 13 (2 < e ∧ e < 3)
4443simpli 473 . . . . . . . . . . . 12 2 < e
4510, 1, 34lttri 10201 . . . . . . . . . . . 12 ((1 < 2 ∧ 2 < e) → 1 < e)
4615, 44, 45mp2an 708 . . . . . . . . . . 11 1 < e
4710, 34, 1ltmul2i 10983 . . . . . . . . . . . 12 (0 < 2 → (1 < e ↔ (2 · 1) < (2 · e)))
4836, 47ax-mp 5 . . . . . . . . . . 11 (1 < e ↔ (2 · 1) < (2 · e))
4946, 48mpbi 220 . . . . . . . . . 10 (2 · 1) < (2 · e)
5042, 49eqbrtrri 4708 . . . . . . . . 9 2 < (2 · e)
511, 35, 36, 38ltrecii 10978 . . . . . . . . 9 (2 < (2 · e) ↔ (1 / (2 · e)) < (1 / 2))
5250, 51mpbi 220 . . . . . . . 8 (1 / (2 · e)) < (1 / 2)
5343simpri 477 . . . . . . . . . . . 12 e < 3
54 3lt4 11235 . . . . . . . . . . . 12 3 < 4
55 3re 11132 . . . . . . . . . . . . 13 3 ∈ ℝ
56 4re 11135 . . . . . . . . . . . . 13 4 ∈ ℝ
5734, 55, 56lttri 10201 . . . . . . . . . . . 12 ((e < 3 ∧ 3 < 4) → e < 4)
5853, 54, 57mp2an 708 . . . . . . . . . . 11 e < 4
59 epr 14980 . . . . . . . . . . . 12 e ∈ ℝ+
60 4pos 11154 . . . . . . . . . . . . 13 0 < 4
6156, 60elrpii 11873 . . . . . . . . . . . 12 4 ∈ ℝ+
62 logltb 24391 . . . . . . . . . . . 12 ((e ∈ ℝ+ ∧ 4 ∈ ℝ+) → (e < 4 ↔ (log‘e) < (log‘4)))
6359, 61, 62mp2an 708 . . . . . . . . . . 11 (e < 4 ↔ (log‘e) < (log‘4))
6458, 63mpbi 220 . . . . . . . . . 10 (log‘e) < (log‘4)
65 loge 24378 . . . . . . . . . 10 (log‘e) = 1
66 sq2 13000 . . . . . . . . . . . 12 (2↑2) = 4
6766fveq2i 6232 . . . . . . . . . . 11 (log‘(2↑2)) = (log‘4)
68 2z 11447 . . . . . . . . . . . 12 2 ∈ ℤ
69 relogexp 24387 . . . . . . . . . . . 12 ((2 ∈ ℝ+ ∧ 2 ∈ ℤ) → (log‘(2↑2)) = (2 · (log‘2)))
7031, 68, 69mp2an 708 . . . . . . . . . . 11 (log‘(2↑2)) = (2 · (log‘2))
7167, 70eqtr3i 2675 . . . . . . . . . 10 (log‘4) = (2 · (log‘2))
7264, 65, 713brtr3i 4714 . . . . . . . . 9 1 < (2 · (log‘2))
731, 36pm3.2i 470 . . . . . . . . . 10 (2 ∈ ℝ ∧ 0 < 2)
74 ltdivmul 10936 . . . . . . . . . 10 ((1 ∈ ℝ ∧ (log‘2) ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → ((1 / 2) < (log‘2) ↔ 1 < (2 · (log‘2))))
7510, 33, 73, 74mp3an 1464 . . . . . . . . 9 ((1 / 2) < (log‘2) ↔ 1 < (2 · (log‘2)))
7672, 75mpbir 221 . . . . . . . 8 (1 / 2) < (log‘2)
77 halfre 11284 . . . . . . . . 9 (1 / 2) ∈ ℝ
7840, 77, 33lttri 10201 . . . . . . . 8 (((1 / (2 · e)) < (1 / 2) ∧ (1 / 2) < (log‘2)) → (1 / (2 · e)) < (log‘2))
7952, 76, 78mp2an 708 . . . . . . 7 (1 / (2 · e)) < (log‘2)
8040, 33posdifi 10616 . . . . . . 7 ((1 / (2 · e)) < (log‘2) ↔ 0 < ((log‘2) − (1 / (2 · e))))
8179, 80mpbi 220 . . . . . 6 0 < ((log‘2) − (1 / (2 · e)))
8241, 81elrpii 11873 . . . . 5 ((log‘2) − (1 / (2 · e))) ∈ ℝ+
83 rerpdivcl 11899 . . . . 5 ((2 ∈ ℝ ∧ ((log‘2) − (1 / (2 · e))) ∈ ℝ+) → (2 / ((log‘2) − (1 / (2 · e)))) ∈ ℝ)
841, 82, 83mp2an 708 . . . 4 (2 / ((log‘2) − (1 / (2 · e)))) ∈ ℝ
8584a1i 11 . . 3 (⊤ → (2 / ((log‘2) − (1 / (2 · e)))) ∈ ℝ)
86 rpre 11877 . . . . . . . 8 (((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ+ → ((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ)
87 rpge0 11883 . . . . . . . 8 (((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ+ → 0 ≤ ((𝑥 / (log‘𝑥)) / (π𝑥)))
8886, 87absidd 14205 . . . . . . 7 (((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ+ → (abs‘((𝑥 / (log‘𝑥)) / (π𝑥))) = ((𝑥 / (log‘𝑥)) / (π𝑥)))
8926, 88syl 17 . . . . . 6 (𝑥 ∈ (2[,)+∞) → (abs‘((𝑥 / (log‘𝑥)) / (π𝑥))) = ((𝑥 / (log‘𝑥)) / (π𝑥)))
9089adantr 480 . . . . 5 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → (abs‘((𝑥 / (log‘𝑥)) / (π𝑥))) = ((𝑥 / (log‘𝑥)) / (π𝑥)))
91 eqid 2651 . . . . . . . . . 10 (⌊‘(𝑥 / 2)) = (⌊‘(𝑥 / 2))
9291chebbnd1lem3 25205 . . . . . . . . 9 ((𝑥 ∈ ℝ ∧ 8 ≤ 𝑥) → (((log‘2) − (1 / (2 · e))) / 2) < ((π𝑥) · ((log‘𝑥) / 𝑥)))
938, 92sylan 487 . . . . . . . 8 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → (((log‘2) − (1 / (2 · e))) / 2) < ((π𝑥) · ((log‘𝑥) / 𝑥)))
941recni 10090 . . . . . . . . . 10 2 ∈ ℂ
95 2ne0 11151 . . . . . . . . . 10 2 ≠ 0
9641recni 10090 . . . . . . . . . 10 ((log‘2) − (1 / (2 · e))) ∈ ℂ
9741, 81gt0ne0ii 10602 . . . . . . . . . 10 ((log‘2) − (1 / (2 · e))) ≠ 0
98 recdiv 10769 . . . . . . . . . 10 (((2 ∈ ℂ ∧ 2 ≠ 0) ∧ (((log‘2) − (1 / (2 · e))) ∈ ℂ ∧ ((log‘2) − (1 / (2 · e))) ≠ 0)) → (1 / (2 / ((log‘2) − (1 / (2 · e))))) = (((log‘2) − (1 / (2 · e))) / 2))
9994, 95, 96, 97, 98mp4an 709 . . . . . . . . 9 (1 / (2 / ((log‘2) − (1 / (2 · e))))) = (((log‘2) − (1 / (2 · e))) / 2)
10099a1i 11 . . . . . . . 8 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → (1 / (2 / ((log‘2) − (1 / (2 · e))))) = (((log‘2) − (1 / (2 · e))) / 2))
10122rpcnd 11912 . . . . . . . . . . 11 (𝑥 ∈ (2[,)+∞) → (𝑥 / (log‘𝑥)) ∈ ℂ)
10224nncnd 11074 . . . . . . . . . . 11 (𝑥 ∈ (2[,)+∞) → (π𝑥) ∈ ℂ)
10322rpne0d 11915 . . . . . . . . . . 11 (𝑥 ∈ (2[,)+∞) → (𝑥 / (log‘𝑥)) ≠ 0)
10424nnne0d 11103 . . . . . . . . . . 11 (𝑥 ∈ (2[,)+∞) → (π𝑥) ≠ 0)
105101, 102, 103, 104recdivd 10856 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) → (1 / ((𝑥 / (log‘𝑥)) / (π𝑥))) = ((π𝑥) / (𝑥 / (log‘𝑥))))
106102, 101, 103divrecd 10842 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) → ((π𝑥) / (𝑥 / (log‘𝑥))) = ((π𝑥) · (1 / (𝑥 / (log‘𝑥)))))
10720rpcnne0d 11919 . . . . . . . . . . . 12 (𝑥 ∈ (2[,)+∞) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
10821rpcnne0d 11919 . . . . . . . . . . . 12 (𝑥 ∈ (2[,)+∞) → ((log‘𝑥) ∈ ℂ ∧ (log‘𝑥) ≠ 0))
109 recdiv 10769 . . . . . . . . . . . 12 (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ ((log‘𝑥) ∈ ℂ ∧ (log‘𝑥) ≠ 0)) → (1 / (𝑥 / (log‘𝑥))) = ((log‘𝑥) / 𝑥))
110107, 108, 109syl2anc 694 . . . . . . . . . . 11 (𝑥 ∈ (2[,)+∞) → (1 / (𝑥 / (log‘𝑥))) = ((log‘𝑥) / 𝑥))
111110oveq2d 6706 . . . . . . . . . 10 (𝑥 ∈ (2[,)+∞) → ((π𝑥) · (1 / (𝑥 / (log‘𝑥)))) = ((π𝑥) · ((log‘𝑥) / 𝑥)))
112105, 106, 1113eqtrd 2689 . . . . . . . . 9 (𝑥 ∈ (2[,)+∞) → (1 / ((𝑥 / (log‘𝑥)) / (π𝑥))) = ((π𝑥) · ((log‘𝑥) / 𝑥)))
113112adantr 480 . . . . . . . 8 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → (1 / ((𝑥 / (log‘𝑥)) / (π𝑥))) = ((π𝑥) · ((log‘𝑥) / 𝑥)))
11493, 100, 1133brtr4d 4717 . . . . . . 7 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → (1 / (2 / ((log‘2) − (1 / (2 · e))))) < (1 / ((𝑥 / (log‘𝑥)) / (π𝑥))))
11526adantr 480 . . . . . . . 8 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → ((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ+)
116 elrp 11872 . . . . . . . . 9 (((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ+ ↔ (((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ ∧ 0 < ((𝑥 / (log‘𝑥)) / (π𝑥))))
1171, 41, 36, 81divgt0ii 10979 . . . . . . . . . 10 0 < (2 / ((log‘2) − (1 / (2 · e))))
118 ltrec 10943 . . . . . . . . . 10 (((((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ ∧ 0 < ((𝑥 / (log‘𝑥)) / (π𝑥))) ∧ ((2 / ((log‘2) − (1 / (2 · e)))) ∈ ℝ ∧ 0 < (2 / ((log‘2) − (1 / (2 · e)))))) → (((𝑥 / (log‘𝑥)) / (π𝑥)) < (2 / ((log‘2) − (1 / (2 · e)))) ↔ (1 / (2 / ((log‘2) − (1 / (2 · e))))) < (1 / ((𝑥 / (log‘𝑥)) / (π𝑥)))))
11984, 117, 118mpanr12 721 . . . . . . . . 9 ((((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ ∧ 0 < ((𝑥 / (log‘𝑥)) / (π𝑥))) → (((𝑥 / (log‘𝑥)) / (π𝑥)) < (2 / ((log‘2) − (1 / (2 · e)))) ↔ (1 / (2 / ((log‘2) − (1 / (2 · e))))) < (1 / ((𝑥 / (log‘𝑥)) / (π𝑥)))))
120116, 119sylbi 207 . . . . . . . 8 (((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ+ → (((𝑥 / (log‘𝑥)) / (π𝑥)) < (2 / ((log‘2) − (1 / (2 · e)))) ↔ (1 / (2 / ((log‘2) − (1 / (2 · e))))) < (1 / ((𝑥 / (log‘𝑥)) / (π𝑥)))))
121115, 120syl 17 . . . . . . 7 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → (((𝑥 / (log‘𝑥)) / (π𝑥)) < (2 / ((log‘2) − (1 / (2 · e)))) ↔ (1 / (2 / ((log‘2) − (1 / (2 · e))))) < (1 / ((𝑥 / (log‘𝑥)) / (π𝑥)))))
122114, 121mpbird 247 . . . . . 6 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → ((𝑥 / (log‘𝑥)) / (π𝑥)) < (2 / ((log‘2) − (1 / (2 · e)))))
123115rpred 11910 . . . . . . 7 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → ((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ)
124 ltle 10164 . . . . . . 7 ((((𝑥 / (log‘𝑥)) / (π𝑥)) ∈ ℝ ∧ (2 / ((log‘2) − (1 / (2 · e)))) ∈ ℝ) → (((𝑥 / (log‘𝑥)) / (π𝑥)) < (2 / ((log‘2) − (1 / (2 · e)))) → ((𝑥 / (log‘𝑥)) / (π𝑥)) ≤ (2 / ((log‘2) − (1 / (2 · e))))))
125123, 84, 124sylancl 695 . . . . . 6 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → (((𝑥 / (log‘𝑥)) / (π𝑥)) < (2 / ((log‘2) − (1 / (2 · e)))) → ((𝑥 / (log‘𝑥)) / (π𝑥)) ≤ (2 / ((log‘2) − (1 / (2 · e))))))
126122, 125mpd 15 . . . . 5 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → ((𝑥 / (log‘𝑥)) / (π𝑥)) ≤ (2 / ((log‘2) − (1 / (2 · e)))))
12790, 126eqbrtrd 4707 . . . 4 ((𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥) → (abs‘((𝑥 / (log‘𝑥)) / (π𝑥))) ≤ (2 / ((log‘2) − (1 / (2 · e)))))
128127adantl 481 . . 3 ((⊤ ∧ (𝑥 ∈ (2[,)+∞) ∧ 8 ≤ 𝑥)) → (abs‘((𝑥 / (log‘𝑥)) / (π𝑥))) ≤ (2 / ((log‘2) − (1 / (2 · e)))))
1295, 28, 30, 85, 128elo1d 14311 . 2 (⊤ → (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π𝑥))) ∈ 𝑂(1))
130129trud 1533 1 (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π𝑥))) ∈ 𝑂(1)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1523  ⊤wtru 1524   ∈ wcel 2030   ≠ wne 2823   ⊆ wss 3607   class class class wbr 4685   ↦ cmpt 4762  ‘cfv 5926  (class class class)co 6690  ℂcc 9972  ℝcr 9973  0cc0 9974  1c1 9975   · cmul 9979  +∞cpnf 10109  ℝ*cxr 10111   < clt 10112   ≤ cle 10113   − cmin 10304   / cdiv 10722  ℕcn 11058  2c2 11108  3c3 11109  4c4 11110  8c8 11114  ℤcz 11415  ℝ+crp 11870  [,)cico 12215  ⌊cfl 12631  ↑cexp 12900  abscabs 14018  𝑂(1)co1 14261  eceu 14837  logclog 24346  πcppi 24865 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052  ax-addf 10053  ax-mulf 10054 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-of 6939  df-om 7108  df-1st 7210  df-2nd 7211  df-supp 7341  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-ixp 7951  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-fsupp 8317  df-fi 8358  df-sup 8389  df-inf 8390  df-oi 8456  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-4 11119  df-5 11120  df-6 11121  df-7 11122  df-8 11123  df-9 11124  df-n0 11331  df-xnn0 11402  df-z 11416  df-dec 11532  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-ioo 12217  df-ioc 12218  df-ico 12219  df-icc 12220  df-fz 12365  df-fzo 12505  df-fl 12633  df-mod 12709  df-seq 12842  df-exp 12901  df-fac 13101  df-bc 13130  df-hash 13158  df-shft 13851  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-limsup 14246  df-clim 14263  df-rlim 14264  df-o1 14265  df-lo1 14266  df-sum 14461  df-ef 14842  df-e 14843  df-sin 14844  df-cos 14845  df-pi 14847  df-dvds 15028  df-gcd 15264  df-prm 15433  df-pc 15589  df-struct 15906  df-ndx 15907  df-slot 15908  df-base 15910  df-sets 15911  df-ress 15912  df-plusg 16001  df-mulr 16002  df-starv 16003  df-sca 16004  df-vsca 16005  df-ip 16006  df-tset 16007  df-ple 16008  df-ds 16011  df-unif 16012  df-hom 16013  df-cco 16014  df-rest 16130  df-topn 16131  df-0g 16149  df-gsum 16150  df-topgen 16151  df-pt 16152  df-prds 16155  df-xrs 16209  df-qtop 16214  df-imas 16215  df-xps 16217  df-mre 16293  df-mrc 16294  df-acs 16296  df-mgm 17289  df-sgrp 17331  df-mnd 17342  df-submnd 17383  df-mulg 17588  df-cntz 17796  df-cmn 18241  df-psmet 19786  df-xmet 19787  df-met 19788  df-bl 19789  df-mopn 19790  df-fbas 19791  df-fg 19792  df-cnfld 19795  df-top 20747  df-topon 20764  df-topsp 20785  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873  df-nei 20950  df-lp 20988  df-perf 20989  df-cn 21079  df-cnp 21080  df-haus 21167  df-tx 21413  df-hmeo 21606  df-fil 21697  df-fm 21789  df-flim 21790  df-flf 21791  df-xms 22172  df-ms 22173  df-tms 22174  df-cncf 22728  df-limc 23675  df-dv 23676  df-log 24348  df-ppi 24871 This theorem is referenced by:  chtppilimlem2  25208  chto1lb  25212
 Copyright terms: Public domain W3C validator