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

Theorem log2ublem3 26686
Description: Lemma for log2ub 26687. In decimal, this is a proof that the first four terms of the series for log2 is less than 53056 / 76545. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 15-Sep-2021.)
Assertion
Ref Expression
log2ublem3 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ 53056

Proof of Theorem log2ublem3
StepHypRef Expression
1 0le0 12318 . . . . . . 7 0 ≤ 0
2 risefall0lem 15975 . . . . . . . . . . 11 (0...(0 − 1)) = ∅
32sumeq1i 15649 . . . . . . . . . 10 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
4 sum0 15672 . . . . . . . . . 10 Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
53, 4eqtri 2759 . . . . . . . . 9 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
65oveq2i 7423 . . . . . . . 8 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = (((3↑7) · (5 · 7)) · 0)
7 3cn 12298 . . . . . . . . . . 11 3 ∈ ℂ
8 7nn0 12499 . . . . . . . . . . 11 7 ∈ ℕ0
9 expcl 14050 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 7 ∈ ℕ0) → (3↑7) ∈ ℂ)
107, 8, 9mp2an 689 . . . . . . . . . 10 (3↑7) ∈ ℂ
11 5cn 12305 . . . . . . . . . . 11 5 ∈ ℂ
12 7cn 12311 . . . . . . . . . . 11 7 ∈ ℂ
1311, 12mulcli 11226 . . . . . . . . . 10 (5 · 7) ∈ ℂ
1410, 13mulcli 11226 . . . . . . . . 9 ((3↑7) · (5 · 7)) ∈ ℂ
1514mul01i 11409 . . . . . . . 8 (((3↑7) · (5 · 7)) · 0) = 0
166, 15eqtri 2759 . . . . . . 7 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = 0
17 2cn 12292 . . . . . . . 8 2 ∈ ℂ
1817mul01i 11409 . . . . . . 7 (2 · 0) = 0
191, 16, 183brtr4i 5179 . . . . . 6 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 0)
20 0nn0 12492 . . . . . 6 0 ∈ ℕ0
21 2nn0 12494 . . . . . . . . . 10 2 ∈ ℕ0
22 5nn0 12497 . . . . . . . . . 10 5 ∈ ℕ0
2321, 22deccl 12697 . . . . . . . . 9 25 ∈ ℕ0
2423, 22deccl 12697 . . . . . . . 8 255 ∈ ℕ0
25 1nn0 12493 . . . . . . . 8 1 ∈ ℕ0
2624, 25deccl 12697 . . . . . . 7 2551 ∈ ℕ0
2726, 22deccl 12697 . . . . . 6 25515 ∈ ℕ0
28 eqid 2731 . . . . . 6 (0 − 1) = (0 − 1)
2927nn0cni 12489 . . . . . . 7 25515 ∈ ℂ
3029addlidi 11407 . . . . . 6 (0 + 25515) = 25515
31 3nn0 12495 . . . . . 6 3 ∈ ℕ0
327addridi 11406 . . . . . 6 (3 + 0) = 3
3329mullidi 11224 . . . . . . 7 (1 · 25515) = 25515
3418oveq1i 7422 . . . . . . . . 9 ((2 · 0) + 1) = (0 + 1)
35 0p1e1 12339 . . . . . . . . 9 (0 + 1) = 1
3634, 35eqtri 2759 . . . . . . . 8 ((2 · 0) + 1) = 1
3736oveq1i 7422 . . . . . . 7 (((2 · 0) + 1) · 25515) = (1 · 25515)
3822, 8nn0mulcli 12515 . . . . . . . 8 (5 · 7) ∈ ℕ0
398, 21deccl 12697 . . . . . . . 8 72 ∈ ℕ0
40 9nn0 12501 . . . . . . . 8 9 ∈ ℕ0
41 2p1e3 12359 . . . . . . . . 9 (2 + 1) = 3
42 8nn0 12500 . . . . . . . . . 10 8 ∈ ℕ0
43 1p1e2 12342 . . . . . . . . . . 11 (1 + 1) = 2
44 9cn 12317 . . . . . . . . . . . . . 14 9 ∈ ℂ
45 exp1 14038 . . . . . . . . . . . . . 14 (9 ∈ ℂ → (9↑1) = 9)
4644, 45ax-mp 5 . . . . . . . . . . . . 13 (9↑1) = 9
4746oveq1i 7422 . . . . . . . . . . . 12 ((9↑1) · 9) = (9 · 9)
48 9t9e81 12811 . . . . . . . . . . . 12 (9 · 9) = 81
4947, 48eqtri 2759 . . . . . . . . . . 11 ((9↑1) · 9) = 81
5040, 25, 43, 49numexpp1 17016 . . . . . . . . . 10 (9↑2) = 81
51 8cn 12314 . . . . . . . . . . 11 8 ∈ ℂ
52 9t8e72 12810 . . . . . . . . . . 11 (9 · 8) = 72
5344, 51, 52mulcomli 11228 . . . . . . . . . 10 (8 · 9) = 72
5444mullidi 11224 . . . . . . . . . 10 (1 · 9) = 9
5540, 42, 25, 50, 53, 54decmul1 12746 . . . . . . . . 9 ((9↑2) · 9) = 729
5640, 21, 41, 55numexpp1 17016 . . . . . . . 8 (9↑3) = 729
5731, 25deccl 12697 . . . . . . . 8 31 ∈ ℕ0
58 eqid 2731 . . . . . . . . 9 72 = 72
59 eqid 2731 . . . . . . . . 9 31 = 31
60 7t5e35 12794 . . . . . . . . . . 11 (7 · 5) = 35
6112, 11, 60mulcomli 11228 . . . . . . . . . 10 (5 · 7) = 35
62 7p3e10 12757 . . . . . . . . . . 11 (7 + 3) = 10
6312, 7, 62addcomli 11411 . . . . . . . . . 10 (3 + 7) = 10
64 ax-1cn 11171 . . . . . . . . . . . . 13 1 ∈ ℂ
65 3p1e4 12362 . . . . . . . . . . . . 13 (3 + 1) = 4
667, 64, 65addcomli 11411 . . . . . . . . . . . 12 (1 + 3) = 4
6766oveq2i 7423 . . . . . . . . . . 11 ((3 · 7) + (1 + 3)) = ((3 · 7) + 4)
68 4nn0 12496 . . . . . . . . . . . 12 4 ∈ ℕ0
69 7t3e21 12792 . . . . . . . . . . . . 13 (7 · 3) = 21
7012, 7, 69mulcomli 11228 . . . . . . . . . . . 12 (3 · 7) = 21
71 4cn 12302 . . . . . . . . . . . . 13 4 ∈ ℂ
72 4p1e5 12363 . . . . . . . . . . . . 13 (4 + 1) = 5
7371, 64, 72addcomli 11411 . . . . . . . . . . . 12 (1 + 4) = 5
7421, 25, 68, 70, 73decaddi 12742 . . . . . . . . . . 11 ((3 · 7) + 4) = 25
7567, 74eqtri 2759 . . . . . . . . . 10 ((3 · 7) + (1 + 3)) = 25
7661oveq1i 7422 . . . . . . . . . . 11 ((5 · 7) + 0) = (35 + 0)
7731, 22deccl 12697 . . . . . . . . . . . . 13 35 ∈ ℕ0
7877nn0cni 12489 . . . . . . . . . . . 12 35 ∈ ℂ
7978addridi 11406 . . . . . . . . . . 11 (35 + 0) = 35
8076, 79eqtri 2759 . . . . . . . . . 10 ((5 · 7) + 0) = 35
8131, 22, 25, 20, 61, 63, 8, 22, 31, 75, 80decmac 12734 . . . . . . . . 9 (((5 · 7) · 7) + (3 + 7)) = 255
8225dec0h 12704 . . . . . . . . . 10 1 = 01
83 3t2e6 12383 . . . . . . . . . . . 12 (3 · 2) = 6
8483, 35oveq12i 7424 . . . . . . . . . . 11 ((3 · 2) + (0 + 1)) = (6 + 1)
85 6p1e7 12365 . . . . . . . . . . 11 (6 + 1) = 7
8684, 85eqtri 2759 . . . . . . . . . 10 ((3 · 2) + (0 + 1)) = 7
87 5t2e10 12782 . . . . . . . . . . 11 (5 · 2) = 10
8825, 20, 35, 87decsuc 12713 . . . . . . . . . 10 ((5 · 2) + 1) = 11
8931, 22, 20, 25, 61, 82, 21, 25, 25, 86, 88decmac 12734 . . . . . . . . 9 (((5 · 7) · 2) + 1) = 71
908, 21, 31, 25, 58, 59, 38, 25, 8, 81, 89decma2c 12735 . . . . . . . 8 (((5 · 7) · 72) + 31) = 2551
91 9t3e27 12805 . . . . . . . . . . 11 (9 · 3) = 27
9244, 7, 91mulcomli 11228 . . . . . . . . . 10 (3 · 9) = 27
93 7p4e11 12758 . . . . . . . . . 10 (7 + 4) = 11
9421, 8, 68, 92, 41, 25, 93decaddci 12743 . . . . . . . . 9 ((3 · 9) + 4) = 31
95 9t5e45 12807 . . . . . . . . . 10 (9 · 5) = 45
9644, 11, 95mulcomli 11228 . . . . . . . . 9 (5 · 9) = 45
9740, 31, 22, 61, 22, 68, 94, 96decmul1c 12747 . . . . . . . 8 ((5 · 7) · 9) = 315
9838, 39, 40, 56, 22, 57, 90, 97decmul2c 12748 . . . . . . 7 ((5 · 7) · (9↑3)) = 25515
9933, 37, 983eqtr4ri 2770 . . . . . 6 ((5 · 7) · (9↑3)) = (((2 · 0) + 1) · 25515)
10019, 20, 27, 20, 28, 30, 31, 32, 99log2ublem2 26685 . . . . 5 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...0)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 25515)
10140, 68deccl 12697 . . . . . 6 94 ∈ ℕ0
102101, 22deccl 12697 . . . . 5 945 ∈ ℕ0
103 1m1e0 12289 . . . . 5 (1 − 1) = 0
104 eqid 2731 . . . . . 6 25515 = 25515
105 eqid 2731 . . . . . 6 945 = 945
106 6nn0 12498 . . . . . . . . 9 6 ∈ ℕ0
10721, 106deccl 12697 . . . . . . . 8 26 ∈ ℕ0
108107, 68deccl 12697 . . . . . . 7 264 ∈ ℕ0
109 5p1e6 12364 . . . . . . 7 (5 + 1) = 6
110 eqid 2731 . . . . . . . 8 2551 = 2551
111 eqid 2731 . . . . . . . 8 94 = 94
112 eqid 2731 . . . . . . . . 9 255 = 255
113 eqid 2731 . . . . . . . . . 10 25 = 25
11421, 22, 109, 113decsuc 12713 . . . . . . . . 9 (25 + 1) = 26
115 9p5e14 12772 . . . . . . . . . 10 (9 + 5) = 14
11644, 11, 115addcomli 11411 . . . . . . . . 9 (5 + 9) = 14
11723, 22, 40, 112, 114, 68, 116decaddci 12743 . . . . . . . 8 (255 + 9) = 264
11824, 25, 40, 68, 110, 111, 117, 73decadd 12736 . . . . . . 7 (2551 + 94) = 2645
119108, 22, 109, 118decsuc 12713 . . . . . 6 ((2551 + 94) + 1) = 2646
120 5p5e10 12753 . . . . . 6 (5 + 5) = 10
12126, 22, 101, 22, 104, 105, 119, 120decaddc2 12738 . . . . 5 (25515 + 945) = 26460
12244sqvali 14149 . . . . . . . 8 (9↑2) = (9 · 9)
123 3t3e9 12384 . . . . . . . . 9 (3 · 3) = 9
124123oveq1i 7422 . . . . . . . 8 ((3 · 3) · 9) = (9 · 9)
1257, 7, 44mulassi 11230 . . . . . . . 8 ((3 · 3) · 9) = (3 · (3 · 9))
126122, 124, 1253eqtr2i 2765 . . . . . . 7 (9↑2) = (3 · (3 · 9))
127126oveq2i 7423 . . . . . 6 ((5 · 7) · (9↑2)) = ((5 · 7) · (3 · (3 · 9)))
1287, 44mulcli 11226 . . . . . . . 8 (3 · 9) ∈ ℂ
12913, 7, 128mul12i 11414 . . . . . . 7 ((5 · 7) · (3 · (3 · 9))) = (3 · ((5 · 7) · (3 · 9)))
13021, 68deccl 12697 . . . . . . . . 9 24 ∈ ℕ0
131 eqid 2731 . . . . . . . . . 10 24 = 24
13283, 41oveq12i 7424 . . . . . . . . . . 11 ((3 · 2) + (2 + 1)) = (6 + 3)
133 6p3e9 12377 . . . . . . . . . . 11 (6 + 3) = 9
134132, 133eqtri 2759 . . . . . . . . . 10 ((3 · 2) + (2 + 1)) = 9
13571addlidi 11407 . . . . . . . . . . 11 (0 + 4) = 4
13625, 20, 68, 87, 135decaddi 12742 . . . . . . . . . 10 ((5 · 2) + 4) = 14
13731, 22, 21, 68, 61, 131, 21, 68, 25, 134, 136decmac 12734 . . . . . . . . 9 (((5 · 7) · 2) + 24) = 94
13821, 25, 31, 70, 66decaddi 12742 . . . . . . . . . 10 ((3 · 7) + 3) = 24
1398, 31, 22, 61, 22, 31, 138, 61decmul1c 12747 . . . . . . . . 9 ((5 · 7) · 7) = 245
14038, 21, 8, 92, 22, 130, 137, 139decmul2c 12748 . . . . . . . 8 ((5 · 7) · (3 · 9)) = 945
141140oveq2i 7423 . . . . . . 7 (3 · ((5 · 7) · (3 · 9))) = (3 · 945)
142129, 141eqtri 2759 . . . . . 6 ((5 · 7) · (3 · (3 · 9))) = (3 · 945)
143 df-3 12281 . . . . . . . 8 3 = (2 + 1)
14417mulridi 11223 . . . . . . . . 9 (2 · 1) = 2
145144oveq1i 7422 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
146143, 145eqtr4i 2762 . . . . . . 7 3 = ((2 · 1) + 1)
147146oveq1i 7422 . . . . . 6 (3 · 945) = (((2 · 1) + 1) · 945)
148127, 142, 1473eqtri 2763 . . . . 5 ((5 · 7) · (9↑2)) = (((2 · 1) + 1) · 945)
149100, 27, 102, 25, 103, 121, 21, 41, 148log2ublem2 26685 . . . 4 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...1)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26460)
150108, 106deccl 12697 . . . . 5 2646 ∈ ℕ0
151150, 20deccl 12697 . . . 4 26460 ∈ ℕ0
152106, 31deccl 12697 . . . 4 63 ∈ ℕ0
153 2m1e1 12343 . . . 4 (2 − 1) = 1
154 eqid 2731 . . . . 5 26460 = 26460
155 eqid 2731 . . . . 5 63 = 63
156 eqid 2731 . . . . . 6 2646 = 2646
157 eqid 2731 . . . . . . 7 264 = 264
158107, 68, 72, 157decsuc 12713 . . . . . 6 (264 + 1) = 265
159 6p6e12 12756 . . . . . 6 (6 + 6) = 12
160108, 106, 106, 156, 158, 21, 159decaddci 12743 . . . . 5 (2646 + 6) = 2652
1617addlidi 11407 . . . . 5 (0 + 3) = 3
162150, 20, 106, 31, 154, 155, 160, 161decadd 12736 . . . 4 (26460 + 63) = 26523
163 1p2e3 12360 . . . 4 (1 + 2) = 3
16446oveq2i 7423 . . . . 5 ((5 · 7) · (9↑1)) = ((5 · 7) · 9)
16511, 12, 44mulassi 11230 . . . . . 6 ((5 · 7) · 9) = (5 · (7 · 9))
166 9t7e63 12809 . . . . . . . 8 (9 · 7) = 63
16744, 12, 166mulcomli 11228 . . . . . . 7 (7 · 9) = 63
168167oveq2i 7423 . . . . . 6 (5 · (7 · 9)) = (5 · 63)
169165, 168eqtri 2759 . . . . 5 ((5 · 7) · 9) = (5 · 63)
170 df-5 12283 . . . . . . 7 5 = (4 + 1)
171 2t2e4 12381 . . . . . . . 8 (2 · 2) = 4
172171oveq1i 7422 . . . . . . 7 ((2 · 2) + 1) = (4 + 1)
173170, 172eqtr4i 2762 . . . . . 6 5 = ((2 · 2) + 1)
174173oveq1i 7422 . . . . 5 (5 · 63) = (((2 · 2) + 1) · 63)
175164, 169, 1743eqtri 2763 . . . 4 ((5 · 7) · (9↑1)) = (((2 · 2) + 1) · 63)
176149, 151, 152, 21, 153, 162, 25, 163, 175log2ublem2 26685 . . 3 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...2)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26523)
177107, 22deccl 12697 . . . . 5 265 ∈ ℕ0
178177, 21deccl 12697 . . . 4 2652 ∈ ℕ0
179178, 31deccl 12697 . . 3 26523 ∈ ℕ0
180 3m1e2 12345 . . 3 (3 − 1) = 2
181 eqid 2731 . . . 4 26523 = 26523
182 5p3e8 12374 . . . . 5 (5 + 3) = 8
18311, 7, 182addcomli 11411 . . . 4 (3 + 5) = 8
184178, 31, 22, 181, 183decaddi 12742 . . 3 (26523 + 5) = 26528
18512, 11mulcli 11226 . . . . 5 (7 · 5) ∈ ℂ
186185mulridi 11223 . . . 4 ((7 · 5) · 1) = (7 · 5)
18711, 12mulcomi 11227 . . . . 5 (5 · 7) = (7 · 5)
188 exp0 14036 . . . . . 6 (9 ∈ ℂ → (9↑0) = 1)
18944, 188ax-mp 5 . . . . 5 (9↑0) = 1
190187, 189oveq12i 7424 . . . 4 ((5 · 7) · (9↑0)) = ((7 · 5) · 1)
1917, 17, 83mulcomli 11228 . . . . . . 7 (2 · 3) = 6
192191oveq1i 7422 . . . . . 6 ((2 · 3) + 1) = (6 + 1)
193 df-7 12285 . . . . . 6 7 = (6 + 1)
194192, 193eqtr4i 2762 . . . . 5 ((2 · 3) + 1) = 7
195194oveq1i 7422 . . . 4 (((2 · 3) + 1) · 5) = (7 · 5)
196186, 190, 1953eqtr4i 2769 . . 3 ((5 · 7) · (9↑0)) = (((2 · 3) + 1) · 5)
197176, 179, 22, 31, 180, 184, 20, 161, 196log2ublem2 26685 . 2 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26528)
198 eqid 2731 . . 3 26528 = 26528
199 eqid 2731 . . . 4 2652 = 2652
200 eqid 2731 . . . . 5 265 = 265
201 00id 11394 . . . . . 6 (0 + 0) = 0
20220dec0h 12704 . . . . . 6 0 = 00
203201, 202eqtri 2759 . . . . 5 (0 + 0) = 00
204 eqid 2731 . . . . . 6 26 = 26
20535, 82eqtri 2759 . . . . . 6 (0 + 1) = 01
206171, 35oveq12i 7424 . . . . . . 7 ((2 · 2) + (0 + 1)) = (4 + 1)
207206, 72eqtri 2759 . . . . . 6 ((2 · 2) + (0 + 1)) = 5
208 6cn 12308 . . . . . . . 8 6 ∈ ℂ
209 6t2e12 12786 . . . . . . . 8 (6 · 2) = 12
210208, 17, 209mulcomli 11228 . . . . . . 7 (2 · 6) = 12
21125, 21, 41, 210decsuc 12713 . . . . . 6 ((2 · 6) + 1) = 13
21221, 106, 20, 25, 204, 205, 21, 31, 25, 207, 211decma2c 12735 . . . . 5 ((2 · 26) + (0 + 1)) = 53
21311, 17, 87mulcomli 11228 . . . . . . 7 (2 · 5) = 10
214213oveq1i 7422 . . . . . 6 ((2 · 5) + 0) = (10 + 0)
215 dec10p 12725 . . . . . 6 (10 + 0) = 10
216214, 215eqtri 2759 . . . . 5 ((2 · 5) + 0) = 10
217107, 22, 20, 20, 200, 203, 21, 20, 25, 212, 216decma2c 12735 . . . 4 ((2 · 265) + (0 + 0)) = 530
21822dec0h 12704 . . . . 5 5 = 05
219172, 72, 2183eqtri 2763 . . . 4 ((2 · 2) + 1) = 05
220177, 21, 20, 25, 199, 82, 21, 22, 20, 217, 219decma2c 12735 . . 3 ((2 · 2652) + 1) = 5305
221 8t2e16 12797 . . . 4 (8 · 2) = 16
22251, 17, 221mulcomli 11228 . . 3 (2 · 8) = 16
22321, 178, 42, 198, 106, 25, 220, 222decmul2c 12748 . 2 (2 · 26528) = 53056
224197, 223breqtri 5174 1 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ 53056
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2105  c0 4323   class class class wbr 5149  (class class class)co 7412  cc 11111  0cc0 11113  1c1 11114   + caddc 11116   · cmul 11118  cle 11254  cmin 11449   / cdiv 11876  2c2 12272  3c3 12273  4c4 12274  5c5 12275  6c6 12276  7c7 12277  8c8 12278  9c9 12279  0cn0 12477  cdc 12682  ...cfz 13489  cexp 14032  Σcsu 15637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7728  ax-inf2 9639  ax-cnex 11169  ax-resscn 11170  ax-1cn 11171  ax-icn 11172  ax-addcl 11173  ax-addrcl 11174  ax-mulcl 11175  ax-mulrcl 11176  ax-mulcom 11177  ax-addass 11178  ax-mulass 11179  ax-distr 11180  ax-i2m1 11181  ax-1ne0 11182  ax-1rid 11183  ax-rnegex 11184  ax-rrecex 11185  ax-cnre 11186  ax-pre-lttri 11187  ax-pre-lttrn 11188  ax-pre-ltadd 11189  ax-pre-mulgt0 11190  ax-pre-sup 11191
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-int 4952  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-se 5633  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-isom 6553  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-om 7859  df-1st 7978  df-2nd 7979  df-frecs 8269  df-wrecs 8300  df-recs 8374  df-rdg 8413  df-1o 8469  df-er 8706  df-en 8943  df-dom 8944  df-sdom 8945  df-fin 8946  df-sup 9440  df-oi 9508  df-card 9937  df-pnf 11255  df-mnf 11256  df-xr 11257  df-ltxr 11258  df-le 11259  df-sub 11451  df-neg 11452  df-div 11877  df-nn 12218  df-2 12280  df-3 12281  df-4 12282  df-5 12283  df-6 12284  df-7 12285  df-8 12286  df-9 12287  df-n0 12478  df-z 12564  df-dec 12683  df-uz 12828  df-rp 12980  df-fz 13490  df-fzo 13633  df-seq 13972  df-exp 14033  df-hash 14296  df-cj 15051  df-re 15052  df-im 15053  df-sqrt 15187  df-abs 15188  df-clim 15437  df-sum 15638
This theorem is referenced by:  log2ub  26687
  Copyright terms: Public domain W3C validator