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

Theorem log2ublem3 26689
Description: Lemma for log2ub 26690. 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 12317 . . . . . . 7 0 ≤ 0
2 risefall0lem 15974 . . . . . . . . . . 11 (0...(0 − 1)) = ∅
32sumeq1i 15648 . . . . . . . . . 10 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
4 sum0 15671 . . . . . . . . . 10 Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
53, 4eqtri 2758 . . . . . . . . 9 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
65oveq2i 7422 . . . . . . . 8 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = (((3↑7) · (5 · 7)) · 0)
7 3cn 12297 . . . . . . . . . . 11 3 ∈ ℂ
8 7nn0 12498 . . . . . . . . . . 11 7 ∈ ℕ0
9 expcl 14049 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 7 ∈ ℕ0) → (3↑7) ∈ ℂ)
107, 8, 9mp2an 688 . . . . . . . . . 10 (3↑7) ∈ ℂ
11 5cn 12304 . . . . . . . . . . 11 5 ∈ ℂ
12 7cn 12310 . . . . . . . . . . 11 7 ∈ ℂ
1311, 12mulcli 11225 . . . . . . . . . 10 (5 · 7) ∈ ℂ
1410, 13mulcli 11225 . . . . . . . . 9 ((3↑7) · (5 · 7)) ∈ ℂ
1514mul01i 11408 . . . . . . . 8 (((3↑7) · (5 · 7)) · 0) = 0
166, 15eqtri 2758 . . . . . . 7 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = 0
17 2cn 12291 . . . . . . . 8 2 ∈ ℂ
1817mul01i 11408 . . . . . . 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 12491 . . . . . 6 0 ∈ ℕ0
21 2nn0 12493 . . . . . . . . . 10 2 ∈ ℕ0
22 5nn0 12496 . . . . . . . . . 10 5 ∈ ℕ0
2321, 22deccl 12696 . . . . . . . . 9 25 ∈ ℕ0
2423, 22deccl 12696 . . . . . . . 8 255 ∈ ℕ0
25 1nn0 12492 . . . . . . . 8 1 ∈ ℕ0
2624, 25deccl 12696 . . . . . . 7 2551 ∈ ℕ0
2726, 22deccl 12696 . . . . . 6 25515 ∈ ℕ0
28 eqid 2730 . . . . . 6 (0 − 1) = (0 − 1)
2927nn0cni 12488 . . . . . . 7 25515 ∈ ℂ
3029addlidi 11406 . . . . . 6 (0 + 25515) = 25515
31 3nn0 12494 . . . . . 6 3 ∈ ℕ0
327addridi 11405 . . . . . 6 (3 + 0) = 3
3329mullidi 11223 . . . . . . 7 (1 · 25515) = 25515
3418oveq1i 7421 . . . . . . . . 9 ((2 · 0) + 1) = (0 + 1)
35 0p1e1 12338 . . . . . . . . 9 (0 + 1) = 1
3634, 35eqtri 2758 . . . . . . . 8 ((2 · 0) + 1) = 1
3736oveq1i 7421 . . . . . . 7 (((2 · 0) + 1) · 25515) = (1 · 25515)
3822, 8nn0mulcli 12514 . . . . . . . 8 (5 · 7) ∈ ℕ0
398, 21deccl 12696 . . . . . . . 8 72 ∈ ℕ0
40 9nn0 12500 . . . . . . . 8 9 ∈ ℕ0
41 2p1e3 12358 . . . . . . . . 9 (2 + 1) = 3
42 8nn0 12499 . . . . . . . . . 10 8 ∈ ℕ0
43 1p1e2 12341 . . . . . . . . . . 11 (1 + 1) = 2
44 9cn 12316 . . . . . . . . . . . . . 14 9 ∈ ℂ
45 exp1 14037 . . . . . . . . . . . . . 14 (9 ∈ ℂ → (9↑1) = 9)
4644, 45ax-mp 5 . . . . . . . . . . . . 13 (9↑1) = 9
4746oveq1i 7421 . . . . . . . . . . . 12 ((9↑1) · 9) = (9 · 9)
48 9t9e81 12810 . . . . . . . . . . . 12 (9 · 9) = 81
4947, 48eqtri 2758 . . . . . . . . . . 11 ((9↑1) · 9) = 81
5040, 25, 43, 49numexpp1 17015 . . . . . . . . . 10 (9↑2) = 81
51 8cn 12313 . . . . . . . . . . 11 8 ∈ ℂ
52 9t8e72 12809 . . . . . . . . . . 11 (9 · 8) = 72
5344, 51, 52mulcomli 11227 . . . . . . . . . 10 (8 · 9) = 72
5444mullidi 11223 . . . . . . . . . 10 (1 · 9) = 9
5540, 42, 25, 50, 53, 54decmul1 12745 . . . . . . . . 9 ((9↑2) · 9) = 729
5640, 21, 41, 55numexpp1 17015 . . . . . . . 8 (9↑3) = 729
5731, 25deccl 12696 . . . . . . . 8 31 ∈ ℕ0
58 eqid 2730 . . . . . . . . 9 72 = 72
59 eqid 2730 . . . . . . . . 9 31 = 31
60 7t5e35 12793 . . . . . . . . . . 11 (7 · 5) = 35
6112, 11, 60mulcomli 11227 . . . . . . . . . 10 (5 · 7) = 35
62 7p3e10 12756 . . . . . . . . . . 11 (7 + 3) = 10
6312, 7, 62addcomli 11410 . . . . . . . . . 10 (3 + 7) = 10
64 ax-1cn 11170 . . . . . . . . . . . . 13 1 ∈ ℂ
65 3p1e4 12361 . . . . . . . . . . . . 13 (3 + 1) = 4
667, 64, 65addcomli 11410 . . . . . . . . . . . 12 (1 + 3) = 4
6766oveq2i 7422 . . . . . . . . . . 11 ((3 · 7) + (1 + 3)) = ((3 · 7) + 4)
68 4nn0 12495 . . . . . . . . . . . 12 4 ∈ ℕ0
69 7t3e21 12791 . . . . . . . . . . . . 13 (7 · 3) = 21
7012, 7, 69mulcomli 11227 . . . . . . . . . . . 12 (3 · 7) = 21
71 4cn 12301 . . . . . . . . . . . . 13 4 ∈ ℂ
72 4p1e5 12362 . . . . . . . . . . . . 13 (4 + 1) = 5
7371, 64, 72addcomli 11410 . . . . . . . . . . . 12 (1 + 4) = 5
7421, 25, 68, 70, 73decaddi 12741 . . . . . . . . . . 11 ((3 · 7) + 4) = 25
7567, 74eqtri 2758 . . . . . . . . . 10 ((3 · 7) + (1 + 3)) = 25
7661oveq1i 7421 . . . . . . . . . . 11 ((5 · 7) + 0) = (35 + 0)
7731, 22deccl 12696 . . . . . . . . . . . . 13 35 ∈ ℕ0
7877nn0cni 12488 . . . . . . . . . . . 12 35 ∈ ℂ
7978addridi 11405 . . . . . . . . . . 11 (35 + 0) = 35
8076, 79eqtri 2758 . . . . . . . . . 10 ((5 · 7) + 0) = 35
8131, 22, 25, 20, 61, 63, 8, 22, 31, 75, 80decmac 12733 . . . . . . . . 9 (((5 · 7) · 7) + (3 + 7)) = 255
8225dec0h 12703 . . . . . . . . . 10 1 = 01
83 3t2e6 12382 . . . . . . . . . . . 12 (3 · 2) = 6
8483, 35oveq12i 7423 . . . . . . . . . . 11 ((3 · 2) + (0 + 1)) = (6 + 1)
85 6p1e7 12364 . . . . . . . . . . 11 (6 + 1) = 7
8684, 85eqtri 2758 . . . . . . . . . 10 ((3 · 2) + (0 + 1)) = 7
87 5t2e10 12781 . . . . . . . . . . 11 (5 · 2) = 10
8825, 20, 35, 87decsuc 12712 . . . . . . . . . 10 ((5 · 2) + 1) = 11
8931, 22, 20, 25, 61, 82, 21, 25, 25, 86, 88decmac 12733 . . . . . . . . 9 (((5 · 7) · 2) + 1) = 71
908, 21, 31, 25, 58, 59, 38, 25, 8, 81, 89decma2c 12734 . . . . . . . 8 (((5 · 7) · 72) + 31) = 2551
91 9t3e27 12804 . . . . . . . . . . 11 (9 · 3) = 27
9244, 7, 91mulcomli 11227 . . . . . . . . . 10 (3 · 9) = 27
93 7p4e11 12757 . . . . . . . . . 10 (7 + 4) = 11
9421, 8, 68, 92, 41, 25, 93decaddci 12742 . . . . . . . . 9 ((3 · 9) + 4) = 31
95 9t5e45 12806 . . . . . . . . . 10 (9 · 5) = 45
9644, 11, 95mulcomli 11227 . . . . . . . . 9 (5 · 9) = 45
9740, 31, 22, 61, 22, 68, 94, 96decmul1c 12746 . . . . . . . 8 ((5 · 7) · 9) = 315
9838, 39, 40, 56, 22, 57, 90, 97decmul2c 12747 . . . . . . 7 ((5 · 7) · (9↑3)) = 25515
9933, 37, 983eqtr4ri 2769 . . . . . 6 ((5 · 7) · (9↑3)) = (((2 · 0) + 1) · 25515)
10019, 20, 27, 20, 28, 30, 31, 32, 99log2ublem2 26688 . . . . 5 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...0)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 25515)
10140, 68deccl 12696 . . . . . 6 94 ∈ ℕ0
102101, 22deccl 12696 . . . . 5 945 ∈ ℕ0
103 1m1e0 12288 . . . . 5 (1 − 1) = 0
104 eqid 2730 . . . . . 6 25515 = 25515
105 eqid 2730 . . . . . 6 945 = 945
106 6nn0 12497 . . . . . . . . 9 6 ∈ ℕ0
10721, 106deccl 12696 . . . . . . . 8 26 ∈ ℕ0
108107, 68deccl 12696 . . . . . . 7 264 ∈ ℕ0
109 5p1e6 12363 . . . . . . 7 (5 + 1) = 6
110 eqid 2730 . . . . . . . 8 2551 = 2551
111 eqid 2730 . . . . . . . 8 94 = 94
112 eqid 2730 . . . . . . . . 9 255 = 255
113 eqid 2730 . . . . . . . . . 10 25 = 25
11421, 22, 109, 113decsuc 12712 . . . . . . . . 9 (25 + 1) = 26
115 9p5e14 12771 . . . . . . . . . 10 (9 + 5) = 14
11644, 11, 115addcomli 11410 . . . . . . . . 9 (5 + 9) = 14
11723, 22, 40, 112, 114, 68, 116decaddci 12742 . . . . . . . 8 (255 + 9) = 264
11824, 25, 40, 68, 110, 111, 117, 73decadd 12735 . . . . . . 7 (2551 + 94) = 2645
119108, 22, 109, 118decsuc 12712 . . . . . 6 ((2551 + 94) + 1) = 2646
120 5p5e10 12752 . . . . . 6 (5 + 5) = 10
12126, 22, 101, 22, 104, 105, 119, 120decaddc2 12737 . . . . 5 (25515 + 945) = 26460
12244sqvali 14148 . . . . . . . 8 (9↑2) = (9 · 9)
123 3t3e9 12383 . . . . . . . . 9 (3 · 3) = 9
124123oveq1i 7421 . . . . . . . 8 ((3 · 3) · 9) = (9 · 9)
1257, 7, 44mulassi 11229 . . . . . . . 8 ((3 · 3) · 9) = (3 · (3 · 9))
126122, 124, 1253eqtr2i 2764 . . . . . . 7 (9↑2) = (3 · (3 · 9))
127126oveq2i 7422 . . . . . 6 ((5 · 7) · (9↑2)) = ((5 · 7) · (3 · (3 · 9)))
1287, 44mulcli 11225 . . . . . . . 8 (3 · 9) ∈ ℂ
12913, 7, 128mul12i 11413 . . . . . . 7 ((5 · 7) · (3 · (3 · 9))) = (3 · ((5 · 7) · (3 · 9)))
13021, 68deccl 12696 . . . . . . . . 9 24 ∈ ℕ0
131 eqid 2730 . . . . . . . . . 10 24 = 24
13283, 41oveq12i 7423 . . . . . . . . . . 11 ((3 · 2) + (2 + 1)) = (6 + 3)
133 6p3e9 12376 . . . . . . . . . . 11 (6 + 3) = 9
134132, 133eqtri 2758 . . . . . . . . . 10 ((3 · 2) + (2 + 1)) = 9
13571addlidi 11406 . . . . . . . . . . 11 (0 + 4) = 4
13625, 20, 68, 87, 135decaddi 12741 . . . . . . . . . 10 ((5 · 2) + 4) = 14
13731, 22, 21, 68, 61, 131, 21, 68, 25, 134, 136decmac 12733 . . . . . . . . 9 (((5 · 7) · 2) + 24) = 94
13821, 25, 31, 70, 66decaddi 12741 . . . . . . . . . 10 ((3 · 7) + 3) = 24
1398, 31, 22, 61, 22, 31, 138, 61decmul1c 12746 . . . . . . . . 9 ((5 · 7) · 7) = 245
14038, 21, 8, 92, 22, 130, 137, 139decmul2c 12747 . . . . . . . 8 ((5 · 7) · (3 · 9)) = 945
141140oveq2i 7422 . . . . . . 7 (3 · ((5 · 7) · (3 · 9))) = (3 · 945)
142129, 141eqtri 2758 . . . . . 6 ((5 · 7) · (3 · (3 · 9))) = (3 · 945)
143 df-3 12280 . . . . . . . 8 3 = (2 + 1)
14417mulridi 11222 . . . . . . . . 9 (2 · 1) = 2
145144oveq1i 7421 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
146143, 145eqtr4i 2761 . . . . . . 7 3 = ((2 · 1) + 1)
147146oveq1i 7421 . . . . . 6 (3 · 945) = (((2 · 1) + 1) · 945)
148127, 142, 1473eqtri 2762 . . . . 5 ((5 · 7) · (9↑2)) = (((2 · 1) + 1) · 945)
149100, 27, 102, 25, 103, 121, 21, 41, 148log2ublem2 26688 . . . 4 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...1)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26460)
150108, 106deccl 12696 . . . . 5 2646 ∈ ℕ0
151150, 20deccl 12696 . . . 4 26460 ∈ ℕ0
152106, 31deccl 12696 . . . 4 63 ∈ ℕ0
153 2m1e1 12342 . . . 4 (2 − 1) = 1
154 eqid 2730 . . . . 5 26460 = 26460
155 eqid 2730 . . . . 5 63 = 63
156 eqid 2730 . . . . . 6 2646 = 2646
157 eqid 2730 . . . . . . 7 264 = 264
158107, 68, 72, 157decsuc 12712 . . . . . 6 (264 + 1) = 265
159 6p6e12 12755 . . . . . 6 (6 + 6) = 12
160108, 106, 106, 156, 158, 21, 159decaddci 12742 . . . . 5 (2646 + 6) = 2652
1617addlidi 11406 . . . . 5 (0 + 3) = 3
162150, 20, 106, 31, 154, 155, 160, 161decadd 12735 . . . 4 (26460 + 63) = 26523
163 1p2e3 12359 . . . 4 (1 + 2) = 3
16446oveq2i 7422 . . . . 5 ((5 · 7) · (9↑1)) = ((5 · 7) · 9)
16511, 12, 44mulassi 11229 . . . . . 6 ((5 · 7) · 9) = (5 · (7 · 9))
166 9t7e63 12808 . . . . . . . 8 (9 · 7) = 63
16744, 12, 166mulcomli 11227 . . . . . . 7 (7 · 9) = 63
168167oveq2i 7422 . . . . . 6 (5 · (7 · 9)) = (5 · 63)
169165, 168eqtri 2758 . . . . 5 ((5 · 7) · 9) = (5 · 63)
170 df-5 12282 . . . . . . 7 5 = (4 + 1)
171 2t2e4 12380 . . . . . . . 8 (2 · 2) = 4
172171oveq1i 7421 . . . . . . 7 ((2 · 2) + 1) = (4 + 1)
173170, 172eqtr4i 2761 . . . . . 6 5 = ((2 · 2) + 1)
174173oveq1i 7421 . . . . 5 (5 · 63) = (((2 · 2) + 1) · 63)
175164, 169, 1743eqtri 2762 . . . 4 ((5 · 7) · (9↑1)) = (((2 · 2) + 1) · 63)
176149, 151, 152, 21, 153, 162, 25, 163, 175log2ublem2 26688 . . 3 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...2)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26523)
177107, 22deccl 12696 . . . . 5 265 ∈ ℕ0
178177, 21deccl 12696 . . . 4 2652 ∈ ℕ0
179178, 31deccl 12696 . . 3 26523 ∈ ℕ0
180 3m1e2 12344 . . 3 (3 − 1) = 2
181 eqid 2730 . . . 4 26523 = 26523
182 5p3e8 12373 . . . . 5 (5 + 3) = 8
18311, 7, 182addcomli 11410 . . . 4 (3 + 5) = 8
184178, 31, 22, 181, 183decaddi 12741 . . 3 (26523 + 5) = 26528
18512, 11mulcli 11225 . . . . 5 (7 · 5) ∈ ℂ
186185mulridi 11222 . . . 4 ((7 · 5) · 1) = (7 · 5)
18711, 12mulcomi 11226 . . . . 5 (5 · 7) = (7 · 5)
188 exp0 14035 . . . . . 6 (9 ∈ ℂ → (9↑0) = 1)
18944, 188ax-mp 5 . . . . 5 (9↑0) = 1
190187, 189oveq12i 7423 . . . 4 ((5 · 7) · (9↑0)) = ((7 · 5) · 1)
1917, 17, 83mulcomli 11227 . . . . . . 7 (2 · 3) = 6
192191oveq1i 7421 . . . . . 6 ((2 · 3) + 1) = (6 + 1)
193 df-7 12284 . . . . . 6 7 = (6 + 1)
194192, 193eqtr4i 2761 . . . . 5 ((2 · 3) + 1) = 7
195194oveq1i 7421 . . . 4 (((2 · 3) + 1) · 5) = (7 · 5)
196186, 190, 1953eqtr4i 2768 . . 3 ((5 · 7) · (9↑0)) = (((2 · 3) + 1) · 5)
197176, 179, 22, 31, 180, 184, 20, 161, 196log2ublem2 26688 . 2 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26528)
198 eqid 2730 . . 3 26528 = 26528
199 eqid 2730 . . . 4 2652 = 2652
200 eqid 2730 . . . . 5 265 = 265
201 00id 11393 . . . . . 6 (0 + 0) = 0
20220dec0h 12703 . . . . . 6 0 = 00
203201, 202eqtri 2758 . . . . 5 (0 + 0) = 00
204 eqid 2730 . . . . . 6 26 = 26
20535, 82eqtri 2758 . . . . . 6 (0 + 1) = 01
206171, 35oveq12i 7423 . . . . . . 7 ((2 · 2) + (0 + 1)) = (4 + 1)
207206, 72eqtri 2758 . . . . . 6 ((2 · 2) + (0 + 1)) = 5
208 6cn 12307 . . . . . . . 8 6 ∈ ℂ
209 6t2e12 12785 . . . . . . . 8 (6 · 2) = 12
210208, 17, 209mulcomli 11227 . . . . . . 7 (2 · 6) = 12
21125, 21, 41, 210decsuc 12712 . . . . . 6 ((2 · 6) + 1) = 13
21221, 106, 20, 25, 204, 205, 21, 31, 25, 207, 211decma2c 12734 . . . . 5 ((2 · 26) + (0 + 1)) = 53
21311, 17, 87mulcomli 11227 . . . . . . 7 (2 · 5) = 10
214213oveq1i 7421 . . . . . 6 ((2 · 5) + 0) = (10 + 0)
215 dec10p 12724 . . . . . 6 (10 + 0) = 10
216214, 215eqtri 2758 . . . . 5 ((2 · 5) + 0) = 10
217107, 22, 20, 20, 200, 203, 21, 20, 25, 212, 216decma2c 12734 . . . 4 ((2 · 265) + (0 + 0)) = 530
21822dec0h 12703 . . . . 5 5 = 05
219172, 72, 2183eqtri 2762 . . . 4 ((2 · 2) + 1) = 05
220177, 21, 20, 25, 199, 82, 21, 22, 20, 217, 219decma2c 12734 . . 3 ((2 · 2652) + 1) = 5305
221 8t2e16 12796 . . . 4 (8 · 2) = 16
22251, 17, 221mulcomli 11227 . . 3 (2 · 8) = 16
22321, 178, 42, 198, 106, 25, 220, 222decmul2c 12747 . 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 1539  wcel 2104  c0 4321   class class class wbr 5147  (class class class)co 7411  cc 11110  0cc0 11112  1c1 11113   + caddc 11115   · cmul 11117  cle 11253  cmin 11448   / cdiv 11875  2c2 12271  3c3 12272  4c4 12273  5c5 12274  6c6 12275  7c7 12276  8c8 12277  9c9 12278  0cn0 12476  cdc 12681  ...cfz 13488  cexp 14031  Σcsu 15636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-inf2 9638  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189  ax-pre-sup 11190
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  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 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-om 7858  df-1st 7977  df-2nd 7978  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-sup 9439  df-oi 9507  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-div 11876  df-nn 12217  df-2 12279  df-3 12280  df-4 12281  df-5 12282  df-6 12283  df-7 12284  df-8 12285  df-9 12286  df-n0 12477  df-z 12563  df-dec 12682  df-uz 12827  df-rp 12979  df-fz 13489  df-fzo 13632  df-seq 13971  df-exp 14032  df-hash 14295  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-clim 15436  df-sum 15637
This theorem is referenced by:  log2ub  26690
  Copyright terms: Public domain W3C validator