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

Theorem log2ublem3 26442
Description: Lemma for log2ub 26443. 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 12309 . . . . . . 7 0 ≤ 0
2 risefall0lem 15966 . . . . . . . . . . 11 (0...(0 − 1)) = ∅
32sumeq1i 15640 . . . . . . . . . 10 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
4 sum0 15663 . . . . . . . . . 10 Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
53, 4eqtri 2760 . . . . . . . . 9 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
65oveq2i 7416 . . . . . . . 8 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = (((3↑7) · (5 · 7)) · 0)
7 3cn 12289 . . . . . . . . . . 11 3 ∈ ℂ
8 7nn0 12490 . . . . . . . . . . 11 7 ∈ ℕ0
9 expcl 14041 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 7 ∈ ℕ0) → (3↑7) ∈ ℂ)
107, 8, 9mp2an 690 . . . . . . . . . 10 (3↑7) ∈ ℂ
11 5cn 12296 . . . . . . . . . . 11 5 ∈ ℂ
12 7cn 12302 . . . . . . . . . . 11 7 ∈ ℂ
1311, 12mulcli 11217 . . . . . . . . . 10 (5 · 7) ∈ ℂ
1410, 13mulcli 11217 . . . . . . . . 9 ((3↑7) · (5 · 7)) ∈ ℂ
1514mul01i 11400 . . . . . . . 8 (((3↑7) · (5 · 7)) · 0) = 0
166, 15eqtri 2760 . . . . . . 7 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = 0
17 2cn 12283 . . . . . . . 8 2 ∈ ℂ
1817mul01i 11400 . . . . . . 7 (2 · 0) = 0
191, 16, 183brtr4i 5177 . . . . . 6 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 0)
20 0nn0 12483 . . . . . 6 0 ∈ ℕ0
21 2nn0 12485 . . . . . . . . . 10 2 ∈ ℕ0
22 5nn0 12488 . . . . . . . . . 10 5 ∈ ℕ0
2321, 22deccl 12688 . . . . . . . . 9 25 ∈ ℕ0
2423, 22deccl 12688 . . . . . . . 8 255 ∈ ℕ0
25 1nn0 12484 . . . . . . . 8 1 ∈ ℕ0
2624, 25deccl 12688 . . . . . . 7 2551 ∈ ℕ0
2726, 22deccl 12688 . . . . . 6 25515 ∈ ℕ0
28 eqid 2732 . . . . . 6 (0 − 1) = (0 − 1)
2927nn0cni 12480 . . . . . . 7 25515 ∈ ℂ
3029addlidi 11398 . . . . . 6 (0 + 25515) = 25515
31 3nn0 12486 . . . . . 6 3 ∈ ℕ0
327addridi 11397 . . . . . 6 (3 + 0) = 3
3329mullidi 11215 . . . . . . 7 (1 · 25515) = 25515
3418oveq1i 7415 . . . . . . . . 9 ((2 · 0) + 1) = (0 + 1)
35 0p1e1 12330 . . . . . . . . 9 (0 + 1) = 1
3634, 35eqtri 2760 . . . . . . . 8 ((2 · 0) + 1) = 1
3736oveq1i 7415 . . . . . . 7 (((2 · 0) + 1) · 25515) = (1 · 25515)
3822, 8nn0mulcli 12506 . . . . . . . 8 (5 · 7) ∈ ℕ0
398, 21deccl 12688 . . . . . . . 8 72 ∈ ℕ0
40 9nn0 12492 . . . . . . . 8 9 ∈ ℕ0
41 2p1e3 12350 . . . . . . . . 9 (2 + 1) = 3
42 8nn0 12491 . . . . . . . . . 10 8 ∈ ℕ0
43 1p1e2 12333 . . . . . . . . . . 11 (1 + 1) = 2
44 9cn 12308 . . . . . . . . . . . . . 14 9 ∈ ℂ
45 exp1 14029 . . . . . . . . . . . . . 14 (9 ∈ ℂ → (9↑1) = 9)
4644, 45ax-mp 5 . . . . . . . . . . . . 13 (9↑1) = 9
4746oveq1i 7415 . . . . . . . . . . . 12 ((9↑1) · 9) = (9 · 9)
48 9t9e81 12802 . . . . . . . . . . . 12 (9 · 9) = 81
4947, 48eqtri 2760 . . . . . . . . . . 11 ((9↑1) · 9) = 81
5040, 25, 43, 49numexpp1 17007 . . . . . . . . . 10 (9↑2) = 81
51 8cn 12305 . . . . . . . . . . 11 8 ∈ ℂ
52 9t8e72 12801 . . . . . . . . . . 11 (9 · 8) = 72
5344, 51, 52mulcomli 11219 . . . . . . . . . 10 (8 · 9) = 72
5444mullidi 11215 . . . . . . . . . 10 (1 · 9) = 9
5540, 42, 25, 50, 53, 54decmul1 12737 . . . . . . . . 9 ((9↑2) · 9) = 729
5640, 21, 41, 55numexpp1 17007 . . . . . . . 8 (9↑3) = 729
5731, 25deccl 12688 . . . . . . . 8 31 ∈ ℕ0
58 eqid 2732 . . . . . . . . 9 72 = 72
59 eqid 2732 . . . . . . . . 9 31 = 31
60 7t5e35 12785 . . . . . . . . . . 11 (7 · 5) = 35
6112, 11, 60mulcomli 11219 . . . . . . . . . 10 (5 · 7) = 35
62 7p3e10 12748 . . . . . . . . . . 11 (7 + 3) = 10
6312, 7, 62addcomli 11402 . . . . . . . . . 10 (3 + 7) = 10
64 ax-1cn 11164 . . . . . . . . . . . . 13 1 ∈ ℂ
65 3p1e4 12353 . . . . . . . . . . . . 13 (3 + 1) = 4
667, 64, 65addcomli 11402 . . . . . . . . . . . 12 (1 + 3) = 4
6766oveq2i 7416 . . . . . . . . . . 11 ((3 · 7) + (1 + 3)) = ((3 · 7) + 4)
68 4nn0 12487 . . . . . . . . . . . 12 4 ∈ ℕ0
69 7t3e21 12783 . . . . . . . . . . . . 13 (7 · 3) = 21
7012, 7, 69mulcomli 11219 . . . . . . . . . . . 12 (3 · 7) = 21
71 4cn 12293 . . . . . . . . . . . . 13 4 ∈ ℂ
72 4p1e5 12354 . . . . . . . . . . . . 13 (4 + 1) = 5
7371, 64, 72addcomli 11402 . . . . . . . . . . . 12 (1 + 4) = 5
7421, 25, 68, 70, 73decaddi 12733 . . . . . . . . . . 11 ((3 · 7) + 4) = 25
7567, 74eqtri 2760 . . . . . . . . . 10 ((3 · 7) + (1 + 3)) = 25
7661oveq1i 7415 . . . . . . . . . . 11 ((5 · 7) + 0) = (35 + 0)
7731, 22deccl 12688 . . . . . . . . . . . . 13 35 ∈ ℕ0
7877nn0cni 12480 . . . . . . . . . . . 12 35 ∈ ℂ
7978addridi 11397 . . . . . . . . . . 11 (35 + 0) = 35
8076, 79eqtri 2760 . . . . . . . . . 10 ((5 · 7) + 0) = 35
8131, 22, 25, 20, 61, 63, 8, 22, 31, 75, 80decmac 12725 . . . . . . . . 9 (((5 · 7) · 7) + (3 + 7)) = 255
8225dec0h 12695 . . . . . . . . . 10 1 = 01
83 3t2e6 12374 . . . . . . . . . . . 12 (3 · 2) = 6
8483, 35oveq12i 7417 . . . . . . . . . . 11 ((3 · 2) + (0 + 1)) = (6 + 1)
85 6p1e7 12356 . . . . . . . . . . 11 (6 + 1) = 7
8684, 85eqtri 2760 . . . . . . . . . 10 ((3 · 2) + (0 + 1)) = 7
87 5t2e10 12773 . . . . . . . . . . 11 (5 · 2) = 10
8825, 20, 35, 87decsuc 12704 . . . . . . . . . 10 ((5 · 2) + 1) = 11
8931, 22, 20, 25, 61, 82, 21, 25, 25, 86, 88decmac 12725 . . . . . . . . 9 (((5 · 7) · 2) + 1) = 71
908, 21, 31, 25, 58, 59, 38, 25, 8, 81, 89decma2c 12726 . . . . . . . 8 (((5 · 7) · 72) + 31) = 2551
91 9t3e27 12796 . . . . . . . . . . 11 (9 · 3) = 27
9244, 7, 91mulcomli 11219 . . . . . . . . . 10 (3 · 9) = 27
93 7p4e11 12749 . . . . . . . . . 10 (7 + 4) = 11
9421, 8, 68, 92, 41, 25, 93decaddci 12734 . . . . . . . . 9 ((3 · 9) + 4) = 31
95 9t5e45 12798 . . . . . . . . . 10 (9 · 5) = 45
9644, 11, 95mulcomli 11219 . . . . . . . . 9 (5 · 9) = 45
9740, 31, 22, 61, 22, 68, 94, 96decmul1c 12738 . . . . . . . 8 ((5 · 7) · 9) = 315
9838, 39, 40, 56, 22, 57, 90, 97decmul2c 12739 . . . . . . 7 ((5 · 7) · (9↑3)) = 25515
9933, 37, 983eqtr4ri 2771 . . . . . 6 ((5 · 7) · (9↑3)) = (((2 · 0) + 1) · 25515)
10019, 20, 27, 20, 28, 30, 31, 32, 99log2ublem2 26441 . . . . 5 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...0)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 25515)
10140, 68deccl 12688 . . . . . 6 94 ∈ ℕ0
102101, 22deccl 12688 . . . . 5 945 ∈ ℕ0
103 1m1e0 12280 . . . . 5 (1 − 1) = 0
104 eqid 2732 . . . . . 6 25515 = 25515
105 eqid 2732 . . . . . 6 945 = 945
106 6nn0 12489 . . . . . . . . 9 6 ∈ ℕ0
10721, 106deccl 12688 . . . . . . . 8 26 ∈ ℕ0
108107, 68deccl 12688 . . . . . . 7 264 ∈ ℕ0
109 5p1e6 12355 . . . . . . 7 (5 + 1) = 6
110 eqid 2732 . . . . . . . 8 2551 = 2551
111 eqid 2732 . . . . . . . 8 94 = 94
112 eqid 2732 . . . . . . . . 9 255 = 255
113 eqid 2732 . . . . . . . . . 10 25 = 25
11421, 22, 109, 113decsuc 12704 . . . . . . . . 9 (25 + 1) = 26
115 9p5e14 12763 . . . . . . . . . 10 (9 + 5) = 14
11644, 11, 115addcomli 11402 . . . . . . . . 9 (5 + 9) = 14
11723, 22, 40, 112, 114, 68, 116decaddci 12734 . . . . . . . 8 (255 + 9) = 264
11824, 25, 40, 68, 110, 111, 117, 73decadd 12727 . . . . . . 7 (2551 + 94) = 2645
119108, 22, 109, 118decsuc 12704 . . . . . 6 ((2551 + 94) + 1) = 2646
120 5p5e10 12744 . . . . . 6 (5 + 5) = 10
12126, 22, 101, 22, 104, 105, 119, 120decaddc2 12729 . . . . 5 (25515 + 945) = 26460
12244sqvali 14140 . . . . . . . 8 (9↑2) = (9 · 9)
123 3t3e9 12375 . . . . . . . . 9 (3 · 3) = 9
124123oveq1i 7415 . . . . . . . 8 ((3 · 3) · 9) = (9 · 9)
1257, 7, 44mulassi 11221 . . . . . . . 8 ((3 · 3) · 9) = (3 · (3 · 9))
126122, 124, 1253eqtr2i 2766 . . . . . . 7 (9↑2) = (3 · (3 · 9))
127126oveq2i 7416 . . . . . 6 ((5 · 7) · (9↑2)) = ((5 · 7) · (3 · (3 · 9)))
1287, 44mulcli 11217 . . . . . . . 8 (3 · 9) ∈ ℂ
12913, 7, 128mul12i 11405 . . . . . . 7 ((5 · 7) · (3 · (3 · 9))) = (3 · ((5 · 7) · (3 · 9)))
13021, 68deccl 12688 . . . . . . . . 9 24 ∈ ℕ0
131 eqid 2732 . . . . . . . . . 10 24 = 24
13283, 41oveq12i 7417 . . . . . . . . . . 11 ((3 · 2) + (2 + 1)) = (6 + 3)
133 6p3e9 12368 . . . . . . . . . . 11 (6 + 3) = 9
134132, 133eqtri 2760 . . . . . . . . . 10 ((3 · 2) + (2 + 1)) = 9
13571addlidi 11398 . . . . . . . . . . 11 (0 + 4) = 4
13625, 20, 68, 87, 135decaddi 12733 . . . . . . . . . 10 ((5 · 2) + 4) = 14
13731, 22, 21, 68, 61, 131, 21, 68, 25, 134, 136decmac 12725 . . . . . . . . 9 (((5 · 7) · 2) + 24) = 94
13821, 25, 31, 70, 66decaddi 12733 . . . . . . . . . 10 ((3 · 7) + 3) = 24
1398, 31, 22, 61, 22, 31, 138, 61decmul1c 12738 . . . . . . . . 9 ((5 · 7) · 7) = 245
14038, 21, 8, 92, 22, 130, 137, 139decmul2c 12739 . . . . . . . 8 ((5 · 7) · (3 · 9)) = 945
141140oveq2i 7416 . . . . . . 7 (3 · ((5 · 7) · (3 · 9))) = (3 · 945)
142129, 141eqtri 2760 . . . . . 6 ((5 · 7) · (3 · (3 · 9))) = (3 · 945)
143 df-3 12272 . . . . . . . 8 3 = (2 + 1)
14417mulridi 11214 . . . . . . . . 9 (2 · 1) = 2
145144oveq1i 7415 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
146143, 145eqtr4i 2763 . . . . . . 7 3 = ((2 · 1) + 1)
147146oveq1i 7415 . . . . . 6 (3 · 945) = (((2 · 1) + 1) · 945)
148127, 142, 1473eqtri 2764 . . . . 5 ((5 · 7) · (9↑2)) = (((2 · 1) + 1) · 945)
149100, 27, 102, 25, 103, 121, 21, 41, 148log2ublem2 26441 . . . 4 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...1)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26460)
150108, 106deccl 12688 . . . . 5 2646 ∈ ℕ0
151150, 20deccl 12688 . . . 4 26460 ∈ ℕ0
152106, 31deccl 12688 . . . 4 63 ∈ ℕ0
153 2m1e1 12334 . . . 4 (2 − 1) = 1
154 eqid 2732 . . . . 5 26460 = 26460
155 eqid 2732 . . . . 5 63 = 63
156 eqid 2732 . . . . . 6 2646 = 2646
157 eqid 2732 . . . . . . 7 264 = 264
158107, 68, 72, 157decsuc 12704 . . . . . 6 (264 + 1) = 265
159 6p6e12 12747 . . . . . 6 (6 + 6) = 12
160108, 106, 106, 156, 158, 21, 159decaddci 12734 . . . . 5 (2646 + 6) = 2652
1617addlidi 11398 . . . . 5 (0 + 3) = 3
162150, 20, 106, 31, 154, 155, 160, 161decadd 12727 . . . 4 (26460 + 63) = 26523
163 1p2e3 12351 . . . 4 (1 + 2) = 3
16446oveq2i 7416 . . . . 5 ((5 · 7) · (9↑1)) = ((5 · 7) · 9)
16511, 12, 44mulassi 11221 . . . . . 6 ((5 · 7) · 9) = (5 · (7 · 9))
166 9t7e63 12800 . . . . . . . 8 (9 · 7) = 63
16744, 12, 166mulcomli 11219 . . . . . . 7 (7 · 9) = 63
168167oveq2i 7416 . . . . . 6 (5 · (7 · 9)) = (5 · 63)
169165, 168eqtri 2760 . . . . 5 ((5 · 7) · 9) = (5 · 63)
170 df-5 12274 . . . . . . 7 5 = (4 + 1)
171 2t2e4 12372 . . . . . . . 8 (2 · 2) = 4
172171oveq1i 7415 . . . . . . 7 ((2 · 2) + 1) = (4 + 1)
173170, 172eqtr4i 2763 . . . . . 6 5 = ((2 · 2) + 1)
174173oveq1i 7415 . . . . 5 (5 · 63) = (((2 · 2) + 1) · 63)
175164, 169, 1743eqtri 2764 . . . 4 ((5 · 7) · (9↑1)) = (((2 · 2) + 1) · 63)
176149, 151, 152, 21, 153, 162, 25, 163, 175log2ublem2 26441 . . 3 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...2)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26523)
177107, 22deccl 12688 . . . . 5 265 ∈ ℕ0
178177, 21deccl 12688 . . . 4 2652 ∈ ℕ0
179178, 31deccl 12688 . . 3 26523 ∈ ℕ0
180 3m1e2 12336 . . 3 (3 − 1) = 2
181 eqid 2732 . . . 4 26523 = 26523
182 5p3e8 12365 . . . . 5 (5 + 3) = 8
18311, 7, 182addcomli 11402 . . . 4 (3 + 5) = 8
184178, 31, 22, 181, 183decaddi 12733 . . 3 (26523 + 5) = 26528
18512, 11mulcli 11217 . . . . 5 (7 · 5) ∈ ℂ
186185mulridi 11214 . . . 4 ((7 · 5) · 1) = (7 · 5)
18711, 12mulcomi 11218 . . . . 5 (5 · 7) = (7 · 5)
188 exp0 14027 . . . . . 6 (9 ∈ ℂ → (9↑0) = 1)
18944, 188ax-mp 5 . . . . 5 (9↑0) = 1
190187, 189oveq12i 7417 . . . 4 ((5 · 7) · (9↑0)) = ((7 · 5) · 1)
1917, 17, 83mulcomli 11219 . . . . . . 7 (2 · 3) = 6
192191oveq1i 7415 . . . . . 6 ((2 · 3) + 1) = (6 + 1)
193 df-7 12276 . . . . . 6 7 = (6 + 1)
194192, 193eqtr4i 2763 . . . . 5 ((2 · 3) + 1) = 7
195194oveq1i 7415 . . . 4 (((2 · 3) + 1) · 5) = (7 · 5)
196186, 190, 1953eqtr4i 2770 . . 3 ((5 · 7) · (9↑0)) = (((2 · 3) + 1) · 5)
197176, 179, 22, 31, 180, 184, 20, 161, 196log2ublem2 26441 . 2 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26528)
198 eqid 2732 . . 3 26528 = 26528
199 eqid 2732 . . . 4 2652 = 2652
200 eqid 2732 . . . . 5 265 = 265
201 00id 11385 . . . . . 6 (0 + 0) = 0
20220dec0h 12695 . . . . . 6 0 = 00
203201, 202eqtri 2760 . . . . 5 (0 + 0) = 00
204 eqid 2732 . . . . . 6 26 = 26
20535, 82eqtri 2760 . . . . . 6 (0 + 1) = 01
206171, 35oveq12i 7417 . . . . . . 7 ((2 · 2) + (0 + 1)) = (4 + 1)
207206, 72eqtri 2760 . . . . . 6 ((2 · 2) + (0 + 1)) = 5
208 6cn 12299 . . . . . . . 8 6 ∈ ℂ
209 6t2e12 12777 . . . . . . . 8 (6 · 2) = 12
210208, 17, 209mulcomli 11219 . . . . . . 7 (2 · 6) = 12
21125, 21, 41, 210decsuc 12704 . . . . . 6 ((2 · 6) + 1) = 13
21221, 106, 20, 25, 204, 205, 21, 31, 25, 207, 211decma2c 12726 . . . . 5 ((2 · 26) + (0 + 1)) = 53
21311, 17, 87mulcomli 11219 . . . . . . 7 (2 · 5) = 10
214213oveq1i 7415 . . . . . 6 ((2 · 5) + 0) = (10 + 0)
215 dec10p 12716 . . . . . 6 (10 + 0) = 10
216214, 215eqtri 2760 . . . . 5 ((2 · 5) + 0) = 10
217107, 22, 20, 20, 200, 203, 21, 20, 25, 212, 216decma2c 12726 . . . 4 ((2 · 265) + (0 + 0)) = 530
21822dec0h 12695 . . . . 5 5 = 05
219172, 72, 2183eqtri 2764 . . . 4 ((2 · 2) + 1) = 05
220177, 21, 20, 25, 199, 82, 21, 22, 20, 217, 219decma2c 12726 . . 3 ((2 · 2652) + 1) = 5305
221 8t2e16 12788 . . . 4 (8 · 2) = 16
22251, 17, 221mulcomli 11219 . . 3 (2 · 8) = 16
22321, 178, 42, 198, 106, 25, 220, 222decmul2c 12739 . 2 (2 · 26528) = 53056
224197, 223breqtri 5172 1 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ 53056
Colors of variables: wff setvar class
Syntax hints:   = wceq 1541  wcel 2106  c0 4321   class class class wbr 5147  (class class class)co 7405  cc 11104  0cc0 11106  1c1 11107   + caddc 11109   · cmul 11111  cle 11245  cmin 11440   / cdiv 11867  2c2 12263  3c3 12264  4c4 12265  5c5 12266  6c6 12267  7c7 12268  8c8 12269  9c9 12270  0cn0 12468  cdc 12673  ...cfz 13480  cexp 14023  Σcsu 15628
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721  ax-inf2 9632  ax-cnex 11162  ax-resscn 11163  ax-1cn 11164  ax-icn 11165  ax-addcl 11166  ax-addrcl 11167  ax-mulcl 11168  ax-mulrcl 11169  ax-mulcom 11170  ax-addass 11171  ax-mulass 11172  ax-distr 11173  ax-i2m1 11174  ax-1ne0 11175  ax-1rid 11176  ax-rnegex 11177  ax-rrecex 11178  ax-cnre 11179  ax-pre-lttri 11180  ax-pre-lttrn 11181  ax-pre-ltadd 11182  ax-pre-mulgt0 11183  ax-pre-sup 11184
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-isom 6549  df-riota 7361  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7852  df-1st 7971  df-2nd 7972  df-frecs 8262  df-wrecs 8293  df-recs 8367  df-rdg 8406  df-1o 8462  df-er 8699  df-en 8936  df-dom 8937  df-sdom 8938  df-fin 8939  df-sup 9433  df-oi 9501  df-card 9930  df-pnf 11246  df-mnf 11247  df-xr 11248  df-ltxr 11249  df-le 11250  df-sub 11442  df-neg 11443  df-div 11868  df-nn 12209  df-2 12271  df-3 12272  df-4 12273  df-5 12274  df-6 12275  df-7 12276  df-8 12277  df-9 12278  df-n0 12469  df-z 12555  df-dec 12674  df-uz 12819  df-rp 12971  df-fz 13481  df-fzo 13624  df-seq 13963  df-exp 14024  df-hash 14287  df-cj 15042  df-re 15043  df-im 15044  df-sqrt 15178  df-abs 15179  df-clim 15428  df-sum 15629
This theorem is referenced by:  log2ub  26443
  Copyright terms: Public domain W3C validator