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

Theorem log2ublem2 25540
Description: Lemma for log2ub 25542. (Contributed by Mario Carneiro, 17-Apr-2015.)
Hypotheses
Ref Expression
log2ublem2.1 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐵)
log2ublem2.2 𝐵 ∈ ℕ0
log2ublem2.3 𝐹 ∈ ℕ0
log2ublem2.4 𝑁 ∈ ℕ0
log2ublem2.5 (𝑁 − 1) = 𝐾
log2ublem2.6 (𝐵 + 𝐹) = 𝐺
log2ublem2.7 𝑀 ∈ ℕ0
log2ublem2.8 (𝑀 + 𝑁) = 3
log2ublem2.9 ((5 · 7) · (9↑𝑀)) = (((2 · 𝑁) + 1) · 𝐹)
Assertion
Ref Expression
log2ublem2 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐺)
Distinct variable groups:   𝑛,𝐾   𝑛,𝑁
Allowed substitution hints:   𝐵(𝑛)   𝐹(𝑛)   𝐺(𝑛)   𝑀(𝑛)

Proof of Theorem log2ublem2
StepHypRef Expression
1 log2ublem2.1 . 2 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐵)
2 fzfid 13345 . . . 4 (⊤ → (0...𝐾) ∈ Fin)
3 elfznn0 13004 . . . . . 6 (𝑛 ∈ (0...𝐾) → 𝑛 ∈ ℕ0)
43adantl 485 . . . . 5 ((⊤ ∧ 𝑛 ∈ (0...𝐾)) → 𝑛 ∈ ℕ0)
5 2re 11708 . . . . . 6 2 ∈ ℝ
6 3nn 11713 . . . . . . . 8 3 ∈ ℕ
7 2nn0 11911 . . . . . . . . . 10 2 ∈ ℕ0
8 nn0mulcl 11930 . . . . . . . . . 10 ((2 ∈ ℕ0𝑛 ∈ ℕ0) → (2 · 𝑛) ∈ ℕ0)
97, 8mpan 689 . . . . . . . . 9 (𝑛 ∈ ℕ0 → (2 · 𝑛) ∈ ℕ0)
10 nn0p1nn 11933 . . . . . . . . 9 ((2 · 𝑛) ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
119, 10syl 17 . . . . . . . 8 (𝑛 ∈ ℕ0 → ((2 · 𝑛) + 1) ∈ ℕ)
12 nnmulcl 11658 . . . . . . . 8 ((3 ∈ ℕ ∧ ((2 · 𝑛) + 1) ∈ ℕ) → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
136, 11, 12sylancr 590 . . . . . . 7 (𝑛 ∈ ℕ0 → (3 · ((2 · 𝑛) + 1)) ∈ ℕ)
14 9nn 11732 . . . . . . . 8 9 ∈ ℕ
15 nnexpcl 13447 . . . . . . . 8 ((9 ∈ ℕ ∧ 𝑛 ∈ ℕ0) → (9↑𝑛) ∈ ℕ)
1614, 15mpan 689 . . . . . . 7 (𝑛 ∈ ℕ0 → (9↑𝑛) ∈ ℕ)
1713, 16nnmulcld 11687 . . . . . 6 (𝑛 ∈ ℕ0 → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ)
18 nndivre 11675 . . . . . 6 ((2 ∈ ℝ ∧ ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) ∈ ℕ) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
195, 17, 18sylancr 590 . . . . 5 (𝑛 ∈ ℕ0 → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
204, 19syl 17 . . . 4 ((⊤ ∧ 𝑛 ∈ (0...𝐾)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
212, 20fsumrecl 15091 . . 3 (⊤ → Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ)
2221mptru 1545 . 2 Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℝ
23 log2ublem2.4 . . . . . 6 𝑁 ∈ ℕ0
247, 23nn0mulcli 11932 . . . . 5 (2 · 𝑁) ∈ ℕ0
25 nn0p1nn 11933 . . . . 5 ((2 · 𝑁) ∈ ℕ0 → ((2 · 𝑁) + 1) ∈ ℕ)
2624, 25ax-mp 5 . . . 4 ((2 · 𝑁) + 1) ∈ ℕ
276, 26nnmulcli 11659 . . 3 (3 · ((2 · 𝑁) + 1)) ∈ ℕ
28 nnexpcl 13447 . . . 4 ((9 ∈ ℕ ∧ 𝑁 ∈ ℕ0) → (9↑𝑁) ∈ ℕ)
2914, 23, 28mp2an 691 . . 3 (9↑𝑁) ∈ ℕ
3027, 29nnmulcli 11659 . 2 ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℕ
31 log2ublem2.2 . . 3 𝐵 ∈ ℕ0
327, 31nn0mulcli 11932 . 2 (2 · 𝐵) ∈ ℕ0
33 log2ublem2.3 . . 3 𝐹 ∈ ℕ0
347, 33nn0mulcli 11932 . 2 (2 · 𝐹) ∈ ℕ0
35 nn0uz 12277 . . . . . . 7 0 = (ℤ‘0)
3623, 35eleqtri 2914 . . . . . 6 𝑁 ∈ (ℤ‘0)
3736a1i 11 . . . . 5 (⊤ → 𝑁 ∈ (ℤ‘0))
38 elfznn0 13004 . . . . . . 7 (𝑛 ∈ (0...𝑁) → 𝑛 ∈ ℕ0)
3938adantl 485 . . . . . 6 ((⊤ ∧ 𝑛 ∈ (0...𝑁)) → 𝑛 ∈ ℕ0)
4019recnd 10667 . . . . . 6 (𝑛 ∈ ℕ0 → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
4139, 40syl 17 . . . . 5 ((⊤ ∧ 𝑛 ∈ (0...𝑁)) → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) ∈ ℂ)
42 oveq2 7157 . . . . . . . . 9 (𝑛 = 𝑁 → (2 · 𝑛) = (2 · 𝑁))
4342oveq1d 7164 . . . . . . . 8 (𝑛 = 𝑁 → ((2 · 𝑛) + 1) = ((2 · 𝑁) + 1))
4443oveq2d 7165 . . . . . . 7 (𝑛 = 𝑁 → (3 · ((2 · 𝑛) + 1)) = (3 · ((2 · 𝑁) + 1)))
45 oveq2 7157 . . . . . . 7 (𝑛 = 𝑁 → (9↑𝑛) = (9↑𝑁))
4644, 45oveq12d 7167 . . . . . 6 (𝑛 = 𝑁 → ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)) = ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)))
4746oveq2d 7165 . . . . 5 (𝑛 = 𝑁 → (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
4837, 41, 47fsumm1 15106 . . . 4 (⊤ → Σ𝑛 ∈ (0...𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)))))
4948mptru 1545 . . 3 Σ𝑛 ∈ (0...𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
50 log2ublem2.5 . . . . . 6 (𝑁 − 1) = 𝐾
5150oveq2i 7160 . . . . 5 (0...(𝑁 − 1)) = (0...𝐾)
5251sumeq1i 15055 . . . 4 Σ𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
5352oveq1i 7159 . . 3 𝑛 ∈ (0...(𝑁 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)))) = (Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
5449, 53eqtri 2847 . 2 Σ𝑛 ∈ (0...𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = (Σ𝑛 ∈ (0...𝐾)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) + (2 / ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁))))
55 2cn 11709 . . . 4 2 ∈ ℂ
5631nn0cni 11906 . . . 4 𝐵 ∈ ℂ
5733nn0cni 11906 . . . 4 𝐹 ∈ ℂ
5855, 56, 57adddii 10651 . . 3 (2 · (𝐵 + 𝐹)) = ((2 · 𝐵) + (2 · 𝐹))
59 log2ublem2.6 . . . 4 (𝐵 + 𝐹) = 𝐺
6059oveq2i 7160 . . 3 (2 · (𝐵 + 𝐹)) = (2 · 𝐺)
6158, 60eqtr3i 2849 . 2 ((2 · 𝐵) + (2 · 𝐹)) = (2 · 𝐺)
62 7nn 11726 . . . . . . . . 9 7 ∈ ℕ
6362nnnn0i 11902 . . . . . . . 8 7 ∈ ℕ0
64 nnexpcl 13447 . . . . . . . 8 ((3 ∈ ℕ ∧ 7 ∈ ℕ0) → (3↑7) ∈ ℕ)
656, 63, 64mp2an 691 . . . . . . 7 (3↑7) ∈ ℕ
66 5nn 11720 . . . . . . . 8 5 ∈ ℕ
6766, 62nnmulcli 11659 . . . . . . 7 (5 · 7) ∈ ℕ
6865, 67nnmulcli 11659 . . . . . 6 ((3↑7) · (5 · 7)) ∈ ℕ
6968nnrei 11643 . . . . 5 ((3↑7) · (5 · 7)) ∈ ℝ
7069, 5remulcli 10655 . . . 4 (((3↑7) · (5 · 7)) · 2) ∈ ℝ
7170leidi 11172 . . 3 (((3↑7) · (5 · 7)) · 2) ≤ (((3↑7) · (5 · 7)) · 2)
726nnnn0i 11902 . . . . . . . . . . . 12 3 ∈ ℕ0
73 nnexpcl 13447 . . . . . . . . . . . 12 ((9 ∈ ℕ ∧ 3 ∈ ℕ0) → (9↑3) ∈ ℕ)
7414, 72, 73mp2an 691 . . . . . . . . . . 11 (9↑3) ∈ ℕ
7574nncni 11644 . . . . . . . . . 10 (9↑3) ∈ ℂ
7667nncni 11644 . . . . . . . . . 10 (5 · 7) ∈ ℂ
7775, 76mulcomi 10647 . . . . . . . . 9 ((9↑3) · (5 · 7)) = ((5 · 7) · (9↑3))
78 log2ublem2.8 . . . . . . . . . . . . 13 (𝑀 + 𝑁) = 3
79 log2ublem2.7 . . . . . . . . . . . . . . 15 𝑀 ∈ ℕ0
8079nn0cni 11906 . . . . . . . . . . . . . 14 𝑀 ∈ ℂ
8123nn0cni 11906 . . . . . . . . . . . . . 14 𝑁 ∈ ℂ
8280, 81addcomi 10829 . . . . . . . . . . . . 13 (𝑀 + 𝑁) = (𝑁 + 𝑀)
8378, 82eqtr3i 2849 . . . . . . . . . . . 12 3 = (𝑁 + 𝑀)
8483oveq2i 7160 . . . . . . . . . . 11 (9↑3) = (9↑(𝑁 + 𝑀))
8514nncni 11644 . . . . . . . . . . . 12 9 ∈ ℂ
86 expadd 13476 . . . . . . . . . . . 12 ((9 ∈ ℂ ∧ 𝑁 ∈ ℕ0𝑀 ∈ ℕ0) → (9↑(𝑁 + 𝑀)) = ((9↑𝑁) · (9↑𝑀)))
8785, 23, 79, 86mp3an 1458 . . . . . . . . . . 11 (9↑(𝑁 + 𝑀)) = ((9↑𝑁) · (9↑𝑀))
8884, 87eqtri 2847 . . . . . . . . . 10 (9↑3) = ((9↑𝑁) · (9↑𝑀))
8988oveq2i 7160 . . . . . . . . 9 ((5 · 7) · (9↑3)) = ((5 · 7) · ((9↑𝑁) · (9↑𝑀)))
9029nncni 11644 . . . . . . . . . 10 (9↑𝑁) ∈ ℂ
91 nnexpcl 13447 . . . . . . . . . . . 12 ((9 ∈ ℕ ∧ 𝑀 ∈ ℕ0) → (9↑𝑀) ∈ ℕ)
9214, 79, 91mp2an 691 . . . . . . . . . . 11 (9↑𝑀) ∈ ℕ
9392nncni 11644 . . . . . . . . . 10 (9↑𝑀) ∈ ℂ
9476, 90, 93mul12i 10833 . . . . . . . . 9 ((5 · 7) · ((9↑𝑁) · (9↑𝑀))) = ((9↑𝑁) · ((5 · 7) · (9↑𝑀)))
9577, 89, 943eqtri 2851 . . . . . . . 8 ((9↑3) · (5 · 7)) = ((9↑𝑁) · ((5 · 7) · (9↑𝑀)))
96 log2ublem2.9 . . . . . . . . 9 ((5 · 7) · (9↑𝑀)) = (((2 · 𝑁) + 1) · 𝐹)
9796oveq2i 7160 . . . . . . . 8 ((9↑𝑁) · ((5 · 7) · (9↑𝑀))) = ((9↑𝑁) · (((2 · 𝑁) + 1) · 𝐹))
9895, 97eqtri 2847 . . . . . . 7 ((9↑3) · (5 · 7)) = ((9↑𝑁) · (((2 · 𝑁) + 1) · 𝐹))
9998oveq2i 7160 . . . . . 6 (3 · ((9↑3) · (5 · 7))) = (3 · ((9↑𝑁) · (((2 · 𝑁) + 1) · 𝐹)))
100 df-7 11702 . . . . . . . . . 10 7 = (6 + 1)
101100oveq2i 7160 . . . . . . . . 9 (3↑7) = (3↑(6 + 1))
102 3cn 11715 . . . . . . . . . . 11 3 ∈ ℂ
103 6nn0 11915 . . . . . . . . . . 11 6 ∈ ℕ0
104 expp1 13441 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 6 ∈ ℕ0) → (3↑(6 + 1)) = ((3↑6) · 3))
105102, 103, 104mp2an 691 . . . . . . . . . 10 (3↑(6 + 1)) = ((3↑6) · 3)
106 expmul 13479 . . . . . . . . . . . . 13 ((3 ∈ ℂ ∧ 2 ∈ ℕ0 ∧ 3 ∈ ℕ0) → (3↑(2 · 3)) = ((3↑2)↑3))
107102, 7, 72, 106mp3an 1458 . . . . . . . . . . . 12 (3↑(2 · 3)) = ((3↑2)↑3)
10855, 102mulcomi 10647 . . . . . . . . . . . . . 14 (2 · 3) = (3 · 2)
109 3t2e6 11800 . . . . . . . . . . . . . 14 (3 · 2) = 6
110108, 109eqtri 2847 . . . . . . . . . . . . 13 (2 · 3) = 6
111110oveq2i 7160 . . . . . . . . . . . 12 (3↑(2 · 3)) = (3↑6)
112 sq3 13566 . . . . . . . . . . . . 13 (3↑2) = 9
113112oveq1i 7159 . . . . . . . . . . . 12 ((3↑2)↑3) = (9↑3)
114107, 111, 1133eqtr3i 2855 . . . . . . . . . . 11 (3↑6) = (9↑3)
115114oveq1i 7159 . . . . . . . . . 10 ((3↑6) · 3) = ((9↑3) · 3)
116105, 115eqtri 2847 . . . . . . . . 9 (3↑(6 + 1)) = ((9↑3) · 3)
11775, 102mulcomi 10647 . . . . . . . . 9 ((9↑3) · 3) = (3 · (9↑3))
118101, 116, 1173eqtri 2851 . . . . . . . 8 (3↑7) = (3 · (9↑3))
119118oveq1i 7159 . . . . . . 7 ((3↑7) · (5 · 7)) = ((3 · (9↑3)) · (5 · 7))
120102, 75, 76mulassi 10650 . . . . . . 7 ((3 · (9↑3)) · (5 · 7)) = (3 · ((9↑3) · (5 · 7)))
121119, 120eqtri 2847 . . . . . 6 ((3↑7) · (5 · 7)) = (3 · ((9↑3) · (5 · 7)))
12226nncni 11644 . . . . . . . . 9 ((2 · 𝑁) + 1) ∈ ℂ
123102, 122, 90mul32i 10834 . . . . . . . 8 ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) = ((3 · (9↑𝑁)) · ((2 · 𝑁) + 1))
124123oveq1i 7159 . . . . . . 7 (((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) · 𝐹) = (((3 · (9↑𝑁)) · ((2 · 𝑁) + 1)) · 𝐹)
125102, 90mulcli 10646 . . . . . . . 8 (3 · (9↑𝑁)) ∈ ℂ
126125, 122, 57mulassi 10650 . . . . . . 7 (((3 · (9↑𝑁)) · ((2 · 𝑁) + 1)) · 𝐹) = ((3 · (9↑𝑁)) · (((2 · 𝑁) + 1) · 𝐹))
127122, 57mulcli 10646 . . . . . . . 8 (((2 · 𝑁) + 1) · 𝐹) ∈ ℂ
128102, 90, 127mulassi 10650 . . . . . . 7 ((3 · (9↑𝑁)) · (((2 · 𝑁) + 1) · 𝐹)) = (3 · ((9↑𝑁) · (((2 · 𝑁) + 1) · 𝐹)))
129124, 126, 1283eqtri 2851 . . . . . 6 (((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) · 𝐹) = (3 · ((9↑𝑁) · (((2 · 𝑁) + 1) · 𝐹)))
13099, 121, 1293eqtr4i 2857 . . . . 5 ((3↑7) · (5 · 7)) = (((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) · 𝐹)
131130oveq2i 7160 . . . 4 (2 · ((3↑7) · (5 · 7))) = (2 · (((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) · 𝐹))
13265nncni 11644 . . . . . 6 (3↑7) ∈ ℂ
133132, 76mulcli 10646 . . . . 5 ((3↑7) · (5 · 7)) ∈ ℂ
134133, 55mulcomi 10647 . . . 4 (((3↑7) · (5 · 7)) · 2) = (2 · ((3↑7) · (5 · 7)))
13530nncni 11644 . . . . 5 ((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) ∈ ℂ
136135, 55, 57mul12i 10833 . . . 4 (((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) · (2 · 𝐹)) = (2 · (((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) · 𝐹))
137131, 134, 1363eqtr4i 2857 . . 3 (((3↑7) · (5 · 7)) · 2) = (((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) · (2 · 𝐹))
13871, 137breqtri 5077 . 2 (((3↑7) · (5 · 7)) · 2) ≤ (((3 · ((2 · 𝑁) + 1)) · (9↑𝑁)) · (2 · 𝐹))
1391, 22, 7, 30, 32, 34, 54, 61, 138log2ublem1 25539 1 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...𝑁)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 𝐺)
Colors of variables: wff setvar class
Syntax hints:  wa 399   = wceq 1538  wtru 1539  wcel 2115   class class class wbr 5052  cfv 6343  (class class class)co 7149  cc 10533  cr 10534  0cc0 10535  1c1 10536   + caddc 10538   · cmul 10540  cle 10674  cmin 10868   / cdiv 11295  cn 11634  2c2 11689  3c3 11690  5c5 11692  6c6 11693  7c7 11694  9c9 11696  0cn0 11894  cuz 12240  ...cfz 12894  cexp 13434  Σcsu 15042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5253  ax-pr 5317  ax-un 7455  ax-inf2 9101  ax-cnex 10591  ax-resscn 10592  ax-1cn 10593  ax-icn 10594  ax-addcl 10595  ax-addrcl 10596  ax-mulcl 10597  ax-mulrcl 10598  ax-mulcom 10599  ax-addass 10600  ax-mulass 10601  ax-distr 10602  ax-i2m1 10603  ax-1ne0 10604  ax-1rid 10605  ax-rnegex 10606  ax-rrecex 10607  ax-cnre 10608  ax-pre-lttri 10609  ax-pre-lttrn 10610  ax-pre-ltadd 10611  ax-pre-mulgt0 10612  ax-pre-sup 10613
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3015  df-nel 3119  df-ral 3138  df-rex 3139  df-reu 3140  df-rmo 3141  df-rab 3142  df-v 3482  df-sbc 3759  df-csb 3867  df-dif 3922  df-un 3924  df-in 3926  df-ss 3936  df-pss 3938  df-nul 4277  df-if 4451  df-pw 4524  df-sn 4551  df-pr 4553  df-tp 4555  df-op 4557  df-uni 4825  df-int 4863  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-tr 5159  df-id 5447  df-eprel 5452  df-po 5461  df-so 5462  df-fr 5501  df-se 5502  df-we 5503  df-xp 5548  df-rel 5549  df-cnv 5550  df-co 5551  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555  df-pred 6135  df-ord 6181  df-on 6182  df-lim 6183  df-suc 6184  df-iota 6302  df-fun 6345  df-fn 6346  df-f 6347  df-f1 6348  df-fo 6349  df-f1o 6350  df-fv 6351  df-isom 6352  df-riota 7107  df-ov 7152  df-oprab 7153  df-mpo 7154  df-om 7575  df-1st 7684  df-2nd 7685  df-wrecs 7943  df-recs 8004  df-rdg 8042  df-1o 8098  df-oadd 8102  df-er 8285  df-en 8506  df-dom 8507  df-sdom 8508  df-fin 8509  df-sup 8903  df-oi 8971  df-card 9365  df-pnf 10675  df-mnf 10676  df-xr 10677  df-ltxr 10678  df-le 10679  df-sub 10870  df-neg 10871  df-div 11296  df-nn 11635  df-2 11697  df-3 11698  df-4 11699  df-5 11700  df-6 11701  df-7 11702  df-8 11703  df-9 11704  df-n0 11895  df-z 11979  df-uz 12241  df-rp 12387  df-fz 12895  df-fzo 13038  df-seq 13374  df-exp 13435  df-hash 13696  df-cj 14458  df-re 14459  df-im 14460  df-sqrt 14594  df-abs 14595  df-clim 14845  df-sum 15043
This theorem is referenced by:  log2ublem3  25541
  Copyright terms: Public domain W3C validator