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

Theorem log2ublem3 26453
Description: Lemma for log2ub 26454. 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 12313 . . . . . . 7 0 ≤ 0
2 risefall0lem 15970 . . . . . . . . . . 11 (0...(0 − 1)) = ∅
32sumeq1i 15644 . . . . . . . . . 10 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
4 sum0 15667 . . . . . . . . . 10 Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
53, 4eqtri 2761 . . . . . . . . 9 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
65oveq2i 7420 . . . . . . . 8 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = (((3↑7) · (5 · 7)) · 0)
7 3cn 12293 . . . . . . . . . . 11 3 ∈ ℂ
8 7nn0 12494 . . . . . . . . . . 11 7 ∈ ℕ0
9 expcl 14045 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 7 ∈ ℕ0) → (3↑7) ∈ ℂ)
107, 8, 9mp2an 691 . . . . . . . . . 10 (3↑7) ∈ ℂ
11 5cn 12300 . . . . . . . . . . 11 5 ∈ ℂ
12 7cn 12306 . . . . . . . . . . 11 7 ∈ ℂ
1311, 12mulcli 11221 . . . . . . . . . 10 (5 · 7) ∈ ℂ
1410, 13mulcli 11221 . . . . . . . . 9 ((3↑7) · (5 · 7)) ∈ ℂ
1514mul01i 11404 . . . . . . . 8 (((3↑7) · (5 · 7)) · 0) = 0
166, 15eqtri 2761 . . . . . . 7 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = 0
17 2cn 12287 . . . . . . . 8 2 ∈ ℂ
1817mul01i 11404 . . . . . . 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 12487 . . . . . 6 0 ∈ ℕ0
21 2nn0 12489 . . . . . . . . . 10 2 ∈ ℕ0
22 5nn0 12492 . . . . . . . . . 10 5 ∈ ℕ0
2321, 22deccl 12692 . . . . . . . . 9 25 ∈ ℕ0
2423, 22deccl 12692 . . . . . . . 8 255 ∈ ℕ0
25 1nn0 12488 . . . . . . . 8 1 ∈ ℕ0
2624, 25deccl 12692 . . . . . . 7 2551 ∈ ℕ0
2726, 22deccl 12692 . . . . . 6 25515 ∈ ℕ0
28 eqid 2733 . . . . . 6 (0 − 1) = (0 − 1)
2927nn0cni 12484 . . . . . . 7 25515 ∈ ℂ
3029addlidi 11402 . . . . . 6 (0 + 25515) = 25515
31 3nn0 12490 . . . . . 6 3 ∈ ℕ0
327addridi 11401 . . . . . 6 (3 + 0) = 3
3329mullidi 11219 . . . . . . 7 (1 · 25515) = 25515
3418oveq1i 7419 . . . . . . . . 9 ((2 · 0) + 1) = (0 + 1)
35 0p1e1 12334 . . . . . . . . 9 (0 + 1) = 1
3634, 35eqtri 2761 . . . . . . . 8 ((2 · 0) + 1) = 1
3736oveq1i 7419 . . . . . . 7 (((2 · 0) + 1) · 25515) = (1 · 25515)
3822, 8nn0mulcli 12510 . . . . . . . 8 (5 · 7) ∈ ℕ0
398, 21deccl 12692 . . . . . . . 8 72 ∈ ℕ0
40 9nn0 12496 . . . . . . . 8 9 ∈ ℕ0
41 2p1e3 12354 . . . . . . . . 9 (2 + 1) = 3
42 8nn0 12495 . . . . . . . . . 10 8 ∈ ℕ0
43 1p1e2 12337 . . . . . . . . . . 11 (1 + 1) = 2
44 9cn 12312 . . . . . . . . . . . . . 14 9 ∈ ℂ
45 exp1 14033 . . . . . . . . . . . . . 14 (9 ∈ ℂ → (9↑1) = 9)
4644, 45ax-mp 5 . . . . . . . . . . . . 13 (9↑1) = 9
4746oveq1i 7419 . . . . . . . . . . . 12 ((9↑1) · 9) = (9 · 9)
48 9t9e81 12806 . . . . . . . . . . . 12 (9 · 9) = 81
4947, 48eqtri 2761 . . . . . . . . . . 11 ((9↑1) · 9) = 81
5040, 25, 43, 49numexpp1 17011 . . . . . . . . . 10 (9↑2) = 81
51 8cn 12309 . . . . . . . . . . 11 8 ∈ ℂ
52 9t8e72 12805 . . . . . . . . . . 11 (9 · 8) = 72
5344, 51, 52mulcomli 11223 . . . . . . . . . 10 (8 · 9) = 72
5444mullidi 11219 . . . . . . . . . 10 (1 · 9) = 9
5540, 42, 25, 50, 53, 54decmul1 12741 . . . . . . . . 9 ((9↑2) · 9) = 729
5640, 21, 41, 55numexpp1 17011 . . . . . . . 8 (9↑3) = 729
5731, 25deccl 12692 . . . . . . . 8 31 ∈ ℕ0
58 eqid 2733 . . . . . . . . 9 72 = 72
59 eqid 2733 . . . . . . . . 9 31 = 31
60 7t5e35 12789 . . . . . . . . . . 11 (7 · 5) = 35
6112, 11, 60mulcomli 11223 . . . . . . . . . 10 (5 · 7) = 35
62 7p3e10 12752 . . . . . . . . . . 11 (7 + 3) = 10
6312, 7, 62addcomli 11406 . . . . . . . . . 10 (3 + 7) = 10
64 ax-1cn 11168 . . . . . . . . . . . . 13 1 ∈ ℂ
65 3p1e4 12357 . . . . . . . . . . . . 13 (3 + 1) = 4
667, 64, 65addcomli 11406 . . . . . . . . . . . 12 (1 + 3) = 4
6766oveq2i 7420 . . . . . . . . . . 11 ((3 · 7) + (1 + 3)) = ((3 · 7) + 4)
68 4nn0 12491 . . . . . . . . . . . 12 4 ∈ ℕ0
69 7t3e21 12787 . . . . . . . . . . . . 13 (7 · 3) = 21
7012, 7, 69mulcomli 11223 . . . . . . . . . . . 12 (3 · 7) = 21
71 4cn 12297 . . . . . . . . . . . . 13 4 ∈ ℂ
72 4p1e5 12358 . . . . . . . . . . . . 13 (4 + 1) = 5
7371, 64, 72addcomli 11406 . . . . . . . . . . . 12 (1 + 4) = 5
7421, 25, 68, 70, 73decaddi 12737 . . . . . . . . . . 11 ((3 · 7) + 4) = 25
7567, 74eqtri 2761 . . . . . . . . . 10 ((3 · 7) + (1 + 3)) = 25
7661oveq1i 7419 . . . . . . . . . . 11 ((5 · 7) + 0) = (35 + 0)
7731, 22deccl 12692 . . . . . . . . . . . . 13 35 ∈ ℕ0
7877nn0cni 12484 . . . . . . . . . . . 12 35 ∈ ℂ
7978addridi 11401 . . . . . . . . . . 11 (35 + 0) = 35
8076, 79eqtri 2761 . . . . . . . . . 10 ((5 · 7) + 0) = 35
8131, 22, 25, 20, 61, 63, 8, 22, 31, 75, 80decmac 12729 . . . . . . . . 9 (((5 · 7) · 7) + (3 + 7)) = 255
8225dec0h 12699 . . . . . . . . . 10 1 = 01
83 3t2e6 12378 . . . . . . . . . . . 12 (3 · 2) = 6
8483, 35oveq12i 7421 . . . . . . . . . . 11 ((3 · 2) + (0 + 1)) = (6 + 1)
85 6p1e7 12360 . . . . . . . . . . 11 (6 + 1) = 7
8684, 85eqtri 2761 . . . . . . . . . 10 ((3 · 2) + (0 + 1)) = 7
87 5t2e10 12777 . . . . . . . . . . 11 (5 · 2) = 10
8825, 20, 35, 87decsuc 12708 . . . . . . . . . 10 ((5 · 2) + 1) = 11
8931, 22, 20, 25, 61, 82, 21, 25, 25, 86, 88decmac 12729 . . . . . . . . 9 (((5 · 7) · 2) + 1) = 71
908, 21, 31, 25, 58, 59, 38, 25, 8, 81, 89decma2c 12730 . . . . . . . 8 (((5 · 7) · 72) + 31) = 2551
91 9t3e27 12800 . . . . . . . . . . 11 (9 · 3) = 27
9244, 7, 91mulcomli 11223 . . . . . . . . . 10 (3 · 9) = 27
93 7p4e11 12753 . . . . . . . . . 10 (7 + 4) = 11
9421, 8, 68, 92, 41, 25, 93decaddci 12738 . . . . . . . . 9 ((3 · 9) + 4) = 31
95 9t5e45 12802 . . . . . . . . . 10 (9 · 5) = 45
9644, 11, 95mulcomli 11223 . . . . . . . . 9 (5 · 9) = 45
9740, 31, 22, 61, 22, 68, 94, 96decmul1c 12742 . . . . . . . 8 ((5 · 7) · 9) = 315
9838, 39, 40, 56, 22, 57, 90, 97decmul2c 12743 . . . . . . 7 ((5 · 7) · (9↑3)) = 25515
9933, 37, 983eqtr4ri 2772 . . . . . 6 ((5 · 7) · (9↑3)) = (((2 · 0) + 1) · 25515)
10019, 20, 27, 20, 28, 30, 31, 32, 99log2ublem2 26452 . . . . 5 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...0)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 25515)
10140, 68deccl 12692 . . . . . 6 94 ∈ ℕ0
102101, 22deccl 12692 . . . . 5 945 ∈ ℕ0
103 1m1e0 12284 . . . . 5 (1 − 1) = 0
104 eqid 2733 . . . . . 6 25515 = 25515
105 eqid 2733 . . . . . 6 945 = 945
106 6nn0 12493 . . . . . . . . 9 6 ∈ ℕ0
10721, 106deccl 12692 . . . . . . . 8 26 ∈ ℕ0
108107, 68deccl 12692 . . . . . . 7 264 ∈ ℕ0
109 5p1e6 12359 . . . . . . 7 (5 + 1) = 6
110 eqid 2733 . . . . . . . 8 2551 = 2551
111 eqid 2733 . . . . . . . 8 94 = 94
112 eqid 2733 . . . . . . . . 9 255 = 255
113 eqid 2733 . . . . . . . . . 10 25 = 25
11421, 22, 109, 113decsuc 12708 . . . . . . . . 9 (25 + 1) = 26
115 9p5e14 12767 . . . . . . . . . 10 (9 + 5) = 14
11644, 11, 115addcomli 11406 . . . . . . . . 9 (5 + 9) = 14
11723, 22, 40, 112, 114, 68, 116decaddci 12738 . . . . . . . 8 (255 + 9) = 264
11824, 25, 40, 68, 110, 111, 117, 73decadd 12731 . . . . . . 7 (2551 + 94) = 2645
119108, 22, 109, 118decsuc 12708 . . . . . 6 ((2551 + 94) + 1) = 2646
120 5p5e10 12748 . . . . . 6 (5 + 5) = 10
12126, 22, 101, 22, 104, 105, 119, 120decaddc2 12733 . . . . 5 (25515 + 945) = 26460
12244sqvali 14144 . . . . . . . 8 (9↑2) = (9 · 9)
123 3t3e9 12379 . . . . . . . . 9 (3 · 3) = 9
124123oveq1i 7419 . . . . . . . 8 ((3 · 3) · 9) = (9 · 9)
1257, 7, 44mulassi 11225 . . . . . . . 8 ((3 · 3) · 9) = (3 · (3 · 9))
126122, 124, 1253eqtr2i 2767 . . . . . . 7 (9↑2) = (3 · (3 · 9))
127126oveq2i 7420 . . . . . 6 ((5 · 7) · (9↑2)) = ((5 · 7) · (3 · (3 · 9)))
1287, 44mulcli 11221 . . . . . . . 8 (3 · 9) ∈ ℂ
12913, 7, 128mul12i 11409 . . . . . . 7 ((5 · 7) · (3 · (3 · 9))) = (3 · ((5 · 7) · (3 · 9)))
13021, 68deccl 12692 . . . . . . . . 9 24 ∈ ℕ0
131 eqid 2733 . . . . . . . . . 10 24 = 24
13283, 41oveq12i 7421 . . . . . . . . . . 11 ((3 · 2) + (2 + 1)) = (6 + 3)
133 6p3e9 12372 . . . . . . . . . . 11 (6 + 3) = 9
134132, 133eqtri 2761 . . . . . . . . . 10 ((3 · 2) + (2 + 1)) = 9
13571addlidi 11402 . . . . . . . . . . 11 (0 + 4) = 4
13625, 20, 68, 87, 135decaddi 12737 . . . . . . . . . 10 ((5 · 2) + 4) = 14
13731, 22, 21, 68, 61, 131, 21, 68, 25, 134, 136decmac 12729 . . . . . . . . 9 (((5 · 7) · 2) + 24) = 94
13821, 25, 31, 70, 66decaddi 12737 . . . . . . . . . 10 ((3 · 7) + 3) = 24
1398, 31, 22, 61, 22, 31, 138, 61decmul1c 12742 . . . . . . . . 9 ((5 · 7) · 7) = 245
14038, 21, 8, 92, 22, 130, 137, 139decmul2c 12743 . . . . . . . 8 ((5 · 7) · (3 · 9)) = 945
141140oveq2i 7420 . . . . . . 7 (3 · ((5 · 7) · (3 · 9))) = (3 · 945)
142129, 141eqtri 2761 . . . . . 6 ((5 · 7) · (3 · (3 · 9))) = (3 · 945)
143 df-3 12276 . . . . . . . 8 3 = (2 + 1)
14417mulridi 11218 . . . . . . . . 9 (2 · 1) = 2
145144oveq1i 7419 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
146143, 145eqtr4i 2764 . . . . . . 7 3 = ((2 · 1) + 1)
147146oveq1i 7419 . . . . . 6 (3 · 945) = (((2 · 1) + 1) · 945)
148127, 142, 1473eqtri 2765 . . . . 5 ((5 · 7) · (9↑2)) = (((2 · 1) + 1) · 945)
149100, 27, 102, 25, 103, 121, 21, 41, 148log2ublem2 26452 . . . 4 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...1)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26460)
150108, 106deccl 12692 . . . . 5 2646 ∈ ℕ0
151150, 20deccl 12692 . . . 4 26460 ∈ ℕ0
152106, 31deccl 12692 . . . 4 63 ∈ ℕ0
153 2m1e1 12338 . . . 4 (2 − 1) = 1
154 eqid 2733 . . . . 5 26460 = 26460
155 eqid 2733 . . . . 5 63 = 63
156 eqid 2733 . . . . . 6 2646 = 2646
157 eqid 2733 . . . . . . 7 264 = 264
158107, 68, 72, 157decsuc 12708 . . . . . 6 (264 + 1) = 265
159 6p6e12 12751 . . . . . 6 (6 + 6) = 12
160108, 106, 106, 156, 158, 21, 159decaddci 12738 . . . . 5 (2646 + 6) = 2652
1617addlidi 11402 . . . . 5 (0 + 3) = 3
162150, 20, 106, 31, 154, 155, 160, 161decadd 12731 . . . 4 (26460 + 63) = 26523
163 1p2e3 12355 . . . 4 (1 + 2) = 3
16446oveq2i 7420 . . . . 5 ((5 · 7) · (9↑1)) = ((5 · 7) · 9)
16511, 12, 44mulassi 11225 . . . . . 6 ((5 · 7) · 9) = (5 · (7 · 9))
166 9t7e63 12804 . . . . . . . 8 (9 · 7) = 63
16744, 12, 166mulcomli 11223 . . . . . . 7 (7 · 9) = 63
168167oveq2i 7420 . . . . . 6 (5 · (7 · 9)) = (5 · 63)
169165, 168eqtri 2761 . . . . 5 ((5 · 7) · 9) = (5 · 63)
170 df-5 12278 . . . . . . 7 5 = (4 + 1)
171 2t2e4 12376 . . . . . . . 8 (2 · 2) = 4
172171oveq1i 7419 . . . . . . 7 ((2 · 2) + 1) = (4 + 1)
173170, 172eqtr4i 2764 . . . . . 6 5 = ((2 · 2) + 1)
174173oveq1i 7419 . . . . 5 (5 · 63) = (((2 · 2) + 1) · 63)
175164, 169, 1743eqtri 2765 . . . 4 ((5 · 7) · (9↑1)) = (((2 · 2) + 1) · 63)
176149, 151, 152, 21, 153, 162, 25, 163, 175log2ublem2 26452 . . 3 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...2)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26523)
177107, 22deccl 12692 . . . . 5 265 ∈ ℕ0
178177, 21deccl 12692 . . . 4 2652 ∈ ℕ0
179178, 31deccl 12692 . . 3 26523 ∈ ℕ0
180 3m1e2 12340 . . 3 (3 − 1) = 2
181 eqid 2733 . . . 4 26523 = 26523
182 5p3e8 12369 . . . . 5 (5 + 3) = 8
18311, 7, 182addcomli 11406 . . . 4 (3 + 5) = 8
184178, 31, 22, 181, 183decaddi 12737 . . 3 (26523 + 5) = 26528
18512, 11mulcli 11221 . . . . 5 (7 · 5) ∈ ℂ
186185mulridi 11218 . . . 4 ((7 · 5) · 1) = (7 · 5)
18711, 12mulcomi 11222 . . . . 5 (5 · 7) = (7 · 5)
188 exp0 14031 . . . . . 6 (9 ∈ ℂ → (9↑0) = 1)
18944, 188ax-mp 5 . . . . 5 (9↑0) = 1
190187, 189oveq12i 7421 . . . 4 ((5 · 7) · (9↑0)) = ((7 · 5) · 1)
1917, 17, 83mulcomli 11223 . . . . . . 7 (2 · 3) = 6
192191oveq1i 7419 . . . . . 6 ((2 · 3) + 1) = (6 + 1)
193 df-7 12280 . . . . . 6 7 = (6 + 1)
194192, 193eqtr4i 2764 . . . . 5 ((2 · 3) + 1) = 7
195194oveq1i 7419 . . . 4 (((2 · 3) + 1) · 5) = (7 · 5)
196186, 190, 1953eqtr4i 2771 . . 3 ((5 · 7) · (9↑0)) = (((2 · 3) + 1) · 5)
197176, 179, 22, 31, 180, 184, 20, 161, 196log2ublem2 26452 . 2 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26528)
198 eqid 2733 . . 3 26528 = 26528
199 eqid 2733 . . . 4 2652 = 2652
200 eqid 2733 . . . . 5 265 = 265
201 00id 11389 . . . . . 6 (0 + 0) = 0
20220dec0h 12699 . . . . . 6 0 = 00
203201, 202eqtri 2761 . . . . 5 (0 + 0) = 00
204 eqid 2733 . . . . . 6 26 = 26
20535, 82eqtri 2761 . . . . . 6 (0 + 1) = 01
206171, 35oveq12i 7421 . . . . . . 7 ((2 · 2) + (0 + 1)) = (4 + 1)
207206, 72eqtri 2761 . . . . . 6 ((2 · 2) + (0 + 1)) = 5
208 6cn 12303 . . . . . . . 8 6 ∈ ℂ
209 6t2e12 12781 . . . . . . . 8 (6 · 2) = 12
210208, 17, 209mulcomli 11223 . . . . . . 7 (2 · 6) = 12
21125, 21, 41, 210decsuc 12708 . . . . . 6 ((2 · 6) + 1) = 13
21221, 106, 20, 25, 204, 205, 21, 31, 25, 207, 211decma2c 12730 . . . . 5 ((2 · 26) + (0 + 1)) = 53
21311, 17, 87mulcomli 11223 . . . . . . 7 (2 · 5) = 10
214213oveq1i 7419 . . . . . 6 ((2 · 5) + 0) = (10 + 0)
215 dec10p 12720 . . . . . 6 (10 + 0) = 10
216214, 215eqtri 2761 . . . . 5 ((2 · 5) + 0) = 10
217107, 22, 20, 20, 200, 203, 21, 20, 25, 212, 216decma2c 12730 . . . 4 ((2 · 265) + (0 + 0)) = 530
21822dec0h 12699 . . . . 5 5 = 05
219172, 72, 2183eqtri 2765 . . . 4 ((2 · 2) + 1) = 05
220177, 21, 20, 25, 199, 82, 21, 22, 20, 217, 219decma2c 12730 . . 3 ((2 · 2652) + 1) = 5305
221 8t2e16 12792 . . . 4 (8 · 2) = 16
22251, 17, 221mulcomli 11223 . . 3 (2 · 8) = 16
22321, 178, 42, 198, 106, 25, 220, 222decmul2c 12743 . 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 1542  wcel 2107  c0 4323   class class class wbr 5149  (class class class)co 7409  cc 11108  0cc0 11110  1c1 11111   + caddc 11113   · cmul 11115  cle 11249  cmin 11444   / cdiv 11871  2c2 12267  3c3 12268  4c4 12269  5c5 12270  6c6 12271  7c7 12272  8c8 12273  9c9 12274  0cn0 12472  cdc 12677  ...cfz 13484  cexp 14027  Σcsu 15632
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725  ax-inf2 9636  ax-cnex 11166  ax-resscn 11167  ax-1cn 11168  ax-icn 11169  ax-addcl 11170  ax-addrcl 11171  ax-mulcl 11172  ax-mulrcl 11173  ax-mulcom 11174  ax-addass 11175  ax-mulass 11176  ax-distr 11177  ax-i2m1 11178  ax-1ne0 11179  ax-1rid 11180  ax-rnegex 11181  ax-rrecex 11182  ax-cnre 11183  ax-pre-lttri 11184  ax-pre-lttrn 11185  ax-pre-ltadd 11186  ax-pre-mulgt0 11187  ax-pre-sup 11188
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  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 7365  df-ov 7412  df-oprab 7413  df-mpo 7414  df-om 7856  df-1st 7975  df-2nd 7976  df-frecs 8266  df-wrecs 8297  df-recs 8371  df-rdg 8410  df-1o 8466  df-er 8703  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9437  df-oi 9505  df-card 9934  df-pnf 11250  df-mnf 11251  df-xr 11252  df-ltxr 11253  df-le 11254  df-sub 11446  df-neg 11447  df-div 11872  df-nn 12213  df-2 12275  df-3 12276  df-4 12277  df-5 12278  df-6 12279  df-7 12280  df-8 12281  df-9 12282  df-n0 12473  df-z 12559  df-dec 12678  df-uz 12823  df-rp 12975  df-fz 13485  df-fzo 13628  df-seq 13967  df-exp 14028  df-hash 14291  df-cj 15046  df-re 15047  df-im 15048  df-sqrt 15182  df-abs 15183  df-clim 15432  df-sum 15633
This theorem is referenced by:  log2ub  26454
  Copyright terms: Public domain W3C validator