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

Theorem log2ublem3 25831
Description: Lemma for log2ub 25832. 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 11931 . . . . . . 7 0 ≤ 0
2 risefall0lem 15588 . . . . . . . . . . 11 (0...(0 − 1)) = ∅
32sumeq1i 15262 . . . . . . . . . 10 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))
4 sum0 15285 . . . . . . . . . 10 Σ𝑛 ∈ ∅ (2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
53, 4eqtri 2765 . . . . . . . . 9 Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛))) = 0
65oveq2i 7224 . . . . . . . 8 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = (((3↑7) · (5 · 7)) · 0)
7 3cn 11911 . . . . . . . . . . 11 3 ∈ ℂ
8 7nn0 12112 . . . . . . . . . . 11 7 ∈ ℕ0
9 expcl 13653 . . . . . . . . . . 11 ((3 ∈ ℂ ∧ 7 ∈ ℕ0) → (3↑7) ∈ ℂ)
107, 8, 9mp2an 692 . . . . . . . . . 10 (3↑7) ∈ ℂ
11 5cn 11918 . . . . . . . . . . 11 5 ∈ ℂ
12 7cn 11924 . . . . . . . . . . 11 7 ∈ ℂ
1311, 12mulcli 10840 . . . . . . . . . 10 (5 · 7) ∈ ℂ
1410, 13mulcli 10840 . . . . . . . . 9 ((3↑7) · (5 · 7)) ∈ ℂ
1514mul01i 11022 . . . . . . . 8 (((3↑7) · (5 · 7)) · 0) = 0
166, 15eqtri 2765 . . . . . . 7 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) = 0
17 2cn 11905 . . . . . . . 8 2 ∈ ℂ
1817mul01i 11022 . . . . . . 7 (2 · 0) = 0
191, 16, 183brtr4i 5083 . . . . . 6 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...(0 − 1))(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 0)
20 0nn0 12105 . . . . . 6 0 ∈ ℕ0
21 2nn0 12107 . . . . . . . . . 10 2 ∈ ℕ0
22 5nn0 12110 . . . . . . . . . 10 5 ∈ ℕ0
2321, 22deccl 12308 . . . . . . . . 9 25 ∈ ℕ0
2423, 22deccl 12308 . . . . . . . 8 255 ∈ ℕ0
25 1nn0 12106 . . . . . . . 8 1 ∈ ℕ0
2624, 25deccl 12308 . . . . . . 7 2551 ∈ ℕ0
2726, 22deccl 12308 . . . . . 6 25515 ∈ ℕ0
28 eqid 2737 . . . . . 6 (0 − 1) = (0 − 1)
2927nn0cni 12102 . . . . . . 7 25515 ∈ ℂ
3029addid2i 11020 . . . . . 6 (0 + 25515) = 25515
31 3nn0 12108 . . . . . 6 3 ∈ ℕ0
327addid1i 11019 . . . . . 6 (3 + 0) = 3
3329mulid2i 10838 . . . . . . 7 (1 · 25515) = 25515
3418oveq1i 7223 . . . . . . . . 9 ((2 · 0) + 1) = (0 + 1)
35 0p1e1 11952 . . . . . . . . 9 (0 + 1) = 1
3634, 35eqtri 2765 . . . . . . . 8 ((2 · 0) + 1) = 1
3736oveq1i 7223 . . . . . . 7 (((2 · 0) + 1) · 25515) = (1 · 25515)
3822, 8nn0mulcli 12128 . . . . . . . 8 (5 · 7) ∈ ℕ0
398, 21deccl 12308 . . . . . . . 8 72 ∈ ℕ0
40 9nn0 12114 . . . . . . . 8 9 ∈ ℕ0
41 2p1e3 11972 . . . . . . . . 9 (2 + 1) = 3
42 8nn0 12113 . . . . . . . . . 10 8 ∈ ℕ0
43 1p1e2 11955 . . . . . . . . . . 11 (1 + 1) = 2
44 9cn 11930 . . . . . . . . . . . . . 14 9 ∈ ℂ
45 exp1 13641 . . . . . . . . . . . . . 14 (9 ∈ ℂ → (9↑1) = 9)
4644, 45ax-mp 5 . . . . . . . . . . . . 13 (9↑1) = 9
4746oveq1i 7223 . . . . . . . . . . . 12 ((9↑1) · 9) = (9 · 9)
48 9t9e81 12422 . . . . . . . . . . . 12 (9 · 9) = 81
4947, 48eqtri 2765 . . . . . . . . . . 11 ((9↑1) · 9) = 81
5040, 25, 43, 49numexpp1 16631 . . . . . . . . . 10 (9↑2) = 81
51 8cn 11927 . . . . . . . . . . 11 8 ∈ ℂ
52 9t8e72 12421 . . . . . . . . . . 11 (9 · 8) = 72
5344, 51, 52mulcomli 10842 . . . . . . . . . 10 (8 · 9) = 72
5444mulid2i 10838 . . . . . . . . . 10 (1 · 9) = 9
5540, 42, 25, 50, 53, 54decmul1 12357 . . . . . . . . 9 ((9↑2) · 9) = 729
5640, 21, 41, 55numexpp1 16631 . . . . . . . 8 (9↑3) = 729
5731, 25deccl 12308 . . . . . . . 8 31 ∈ ℕ0
58 eqid 2737 . . . . . . . . 9 72 = 72
59 eqid 2737 . . . . . . . . 9 31 = 31
60 7t5e35 12405 . . . . . . . . . . 11 (7 · 5) = 35
6112, 11, 60mulcomli 10842 . . . . . . . . . 10 (5 · 7) = 35
62 7p3e10 12368 . . . . . . . . . . 11 (7 + 3) = 10
6312, 7, 62addcomli 11024 . . . . . . . . . 10 (3 + 7) = 10
64 ax-1cn 10787 . . . . . . . . . . . . 13 1 ∈ ℂ
65 3p1e4 11975 . . . . . . . . . . . . 13 (3 + 1) = 4
667, 64, 65addcomli 11024 . . . . . . . . . . . 12 (1 + 3) = 4
6766oveq2i 7224 . . . . . . . . . . 11 ((3 · 7) + (1 + 3)) = ((3 · 7) + 4)
68 4nn0 12109 . . . . . . . . . . . 12 4 ∈ ℕ0
69 7t3e21 12403 . . . . . . . . . . . . 13 (7 · 3) = 21
7012, 7, 69mulcomli 10842 . . . . . . . . . . . 12 (3 · 7) = 21
71 4cn 11915 . . . . . . . . . . . . 13 4 ∈ ℂ
72 4p1e5 11976 . . . . . . . . . . . . 13 (4 + 1) = 5
7371, 64, 72addcomli 11024 . . . . . . . . . . . 12 (1 + 4) = 5
7421, 25, 68, 70, 73decaddi 12353 . . . . . . . . . . 11 ((3 · 7) + 4) = 25
7567, 74eqtri 2765 . . . . . . . . . 10 ((3 · 7) + (1 + 3)) = 25
7661oveq1i 7223 . . . . . . . . . . 11 ((5 · 7) + 0) = (35 + 0)
7731, 22deccl 12308 . . . . . . . . . . . . 13 35 ∈ ℕ0
7877nn0cni 12102 . . . . . . . . . . . 12 35 ∈ ℂ
7978addid1i 11019 . . . . . . . . . . 11 (35 + 0) = 35
8076, 79eqtri 2765 . . . . . . . . . 10 ((5 · 7) + 0) = 35
8131, 22, 25, 20, 61, 63, 8, 22, 31, 75, 80decmac 12345 . . . . . . . . 9 (((5 · 7) · 7) + (3 + 7)) = 255
8225dec0h 12315 . . . . . . . . . 10 1 = 01
83 3t2e6 11996 . . . . . . . . . . . 12 (3 · 2) = 6
8483, 35oveq12i 7225 . . . . . . . . . . 11 ((3 · 2) + (0 + 1)) = (6 + 1)
85 6p1e7 11978 . . . . . . . . . . 11 (6 + 1) = 7
8684, 85eqtri 2765 . . . . . . . . . 10 ((3 · 2) + (0 + 1)) = 7
87 5t2e10 12393 . . . . . . . . . . 11 (5 · 2) = 10
8825, 20, 35, 87decsuc 12324 . . . . . . . . . 10 ((5 · 2) + 1) = 11
8931, 22, 20, 25, 61, 82, 21, 25, 25, 86, 88decmac 12345 . . . . . . . . 9 (((5 · 7) · 2) + 1) = 71
908, 21, 31, 25, 58, 59, 38, 25, 8, 81, 89decma2c 12346 . . . . . . . 8 (((5 · 7) · 72) + 31) = 2551
91 9t3e27 12416 . . . . . . . . . . 11 (9 · 3) = 27
9244, 7, 91mulcomli 10842 . . . . . . . . . 10 (3 · 9) = 27
93 7p4e11 12369 . . . . . . . . . 10 (7 + 4) = 11
9421, 8, 68, 92, 41, 25, 93decaddci 12354 . . . . . . . . 9 ((3 · 9) + 4) = 31
95 9t5e45 12418 . . . . . . . . . 10 (9 · 5) = 45
9644, 11, 95mulcomli 10842 . . . . . . . . 9 (5 · 9) = 45
9740, 31, 22, 61, 22, 68, 94, 96decmul1c 12358 . . . . . . . 8 ((5 · 7) · 9) = 315
9838, 39, 40, 56, 22, 57, 90, 97decmul2c 12359 . . . . . . 7 ((5 · 7) · (9↑3)) = 25515
9933, 37, 983eqtr4ri 2776 . . . . . 6 ((5 · 7) · (9↑3)) = (((2 · 0) + 1) · 25515)
10019, 20, 27, 20, 28, 30, 31, 32, 99log2ublem2 25830 . . . . 5 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...0)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 25515)
10140, 68deccl 12308 . . . . . 6 94 ∈ ℕ0
102101, 22deccl 12308 . . . . 5 945 ∈ ℕ0
103 1m1e0 11902 . . . . 5 (1 − 1) = 0
104 eqid 2737 . . . . . 6 25515 = 25515
105 eqid 2737 . . . . . 6 945 = 945
106 6nn0 12111 . . . . . . . . 9 6 ∈ ℕ0
10721, 106deccl 12308 . . . . . . . 8 26 ∈ ℕ0
108107, 68deccl 12308 . . . . . . 7 264 ∈ ℕ0
109 5p1e6 11977 . . . . . . 7 (5 + 1) = 6
110 eqid 2737 . . . . . . . 8 2551 = 2551
111 eqid 2737 . . . . . . . 8 94 = 94
112 eqid 2737 . . . . . . . . 9 255 = 255
113 eqid 2737 . . . . . . . . . 10 25 = 25
11421, 22, 109, 113decsuc 12324 . . . . . . . . 9 (25 + 1) = 26
115 9p5e14 12383 . . . . . . . . . 10 (9 + 5) = 14
11644, 11, 115addcomli 11024 . . . . . . . . 9 (5 + 9) = 14
11723, 22, 40, 112, 114, 68, 116decaddci 12354 . . . . . . . 8 (255 + 9) = 264
11824, 25, 40, 68, 110, 111, 117, 73decadd 12347 . . . . . . 7 (2551 + 94) = 2645
119108, 22, 109, 118decsuc 12324 . . . . . 6 ((2551 + 94) + 1) = 2646
120 5p5e10 12364 . . . . . 6 (5 + 5) = 10
12126, 22, 101, 22, 104, 105, 119, 120decaddc2 12349 . . . . 5 (25515 + 945) = 26460
12244sqvali 13749 . . . . . . . 8 (9↑2) = (9 · 9)
123 3t3e9 11997 . . . . . . . . 9 (3 · 3) = 9
124123oveq1i 7223 . . . . . . . 8 ((3 · 3) · 9) = (9 · 9)
1257, 7, 44mulassi 10844 . . . . . . . 8 ((3 · 3) · 9) = (3 · (3 · 9))
126122, 124, 1253eqtr2i 2771 . . . . . . 7 (9↑2) = (3 · (3 · 9))
127126oveq2i 7224 . . . . . 6 ((5 · 7) · (9↑2)) = ((5 · 7) · (3 · (3 · 9)))
1287, 44mulcli 10840 . . . . . . . 8 (3 · 9) ∈ ℂ
12913, 7, 128mul12i 11027 . . . . . . 7 ((5 · 7) · (3 · (3 · 9))) = (3 · ((5 · 7) · (3 · 9)))
13021, 68deccl 12308 . . . . . . . . 9 24 ∈ ℕ0
131 eqid 2737 . . . . . . . . . 10 24 = 24
13283, 41oveq12i 7225 . . . . . . . . . . 11 ((3 · 2) + (2 + 1)) = (6 + 3)
133 6p3e9 11990 . . . . . . . . . . 11 (6 + 3) = 9
134132, 133eqtri 2765 . . . . . . . . . 10 ((3 · 2) + (2 + 1)) = 9
13571addid2i 11020 . . . . . . . . . . 11 (0 + 4) = 4
13625, 20, 68, 87, 135decaddi 12353 . . . . . . . . . 10 ((5 · 2) + 4) = 14
13731, 22, 21, 68, 61, 131, 21, 68, 25, 134, 136decmac 12345 . . . . . . . . 9 (((5 · 7) · 2) + 24) = 94
13821, 25, 31, 70, 66decaddi 12353 . . . . . . . . . 10 ((3 · 7) + 3) = 24
1398, 31, 22, 61, 22, 31, 138, 61decmul1c 12358 . . . . . . . . 9 ((5 · 7) · 7) = 245
14038, 21, 8, 92, 22, 130, 137, 139decmul2c 12359 . . . . . . . 8 ((5 · 7) · (3 · 9)) = 945
141140oveq2i 7224 . . . . . . 7 (3 · ((5 · 7) · (3 · 9))) = (3 · 945)
142129, 141eqtri 2765 . . . . . 6 ((5 · 7) · (3 · (3 · 9))) = (3 · 945)
143 df-3 11894 . . . . . . . 8 3 = (2 + 1)
14417mulid1i 10837 . . . . . . . . 9 (2 · 1) = 2
145144oveq1i 7223 . . . . . . . 8 ((2 · 1) + 1) = (2 + 1)
146143, 145eqtr4i 2768 . . . . . . 7 3 = ((2 · 1) + 1)
147146oveq1i 7223 . . . . . 6 (3 · 945) = (((2 · 1) + 1) · 945)
148127, 142, 1473eqtri 2769 . . . . 5 ((5 · 7) · (9↑2)) = (((2 · 1) + 1) · 945)
149100, 27, 102, 25, 103, 121, 21, 41, 148log2ublem2 25830 . . . 4 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...1)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26460)
150108, 106deccl 12308 . . . . 5 2646 ∈ ℕ0
151150, 20deccl 12308 . . . 4 26460 ∈ ℕ0
152106, 31deccl 12308 . . . 4 63 ∈ ℕ0
153 2m1e1 11956 . . . 4 (2 − 1) = 1
154 eqid 2737 . . . . 5 26460 = 26460
155 eqid 2737 . . . . 5 63 = 63
156 eqid 2737 . . . . . 6 2646 = 2646
157 eqid 2737 . . . . . . 7 264 = 264
158107, 68, 72, 157decsuc 12324 . . . . . 6 (264 + 1) = 265
159 6p6e12 12367 . . . . . 6 (6 + 6) = 12
160108, 106, 106, 156, 158, 21, 159decaddci 12354 . . . . 5 (2646 + 6) = 2652
1617addid2i 11020 . . . . 5 (0 + 3) = 3
162150, 20, 106, 31, 154, 155, 160, 161decadd 12347 . . . 4 (26460 + 63) = 26523
163 1p2e3 11973 . . . 4 (1 + 2) = 3
16446oveq2i 7224 . . . . 5 ((5 · 7) · (9↑1)) = ((5 · 7) · 9)
16511, 12, 44mulassi 10844 . . . . . 6 ((5 · 7) · 9) = (5 · (7 · 9))
166 9t7e63 12420 . . . . . . . 8 (9 · 7) = 63
16744, 12, 166mulcomli 10842 . . . . . . 7 (7 · 9) = 63
168167oveq2i 7224 . . . . . 6 (5 · (7 · 9)) = (5 · 63)
169165, 168eqtri 2765 . . . . 5 ((5 · 7) · 9) = (5 · 63)
170 df-5 11896 . . . . . . 7 5 = (4 + 1)
171 2t2e4 11994 . . . . . . . 8 (2 · 2) = 4
172171oveq1i 7223 . . . . . . 7 ((2 · 2) + 1) = (4 + 1)
173170, 172eqtr4i 2768 . . . . . 6 5 = ((2 · 2) + 1)
174173oveq1i 7223 . . . . 5 (5 · 63) = (((2 · 2) + 1) · 63)
175164, 169, 1743eqtri 2769 . . . 4 ((5 · 7) · (9↑1)) = (((2 · 2) + 1) · 63)
176149, 151, 152, 21, 153, 162, 25, 163, 175log2ublem2 25830 . . 3 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...2)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26523)
177107, 22deccl 12308 . . . . 5 265 ∈ ℕ0
178177, 21deccl 12308 . . . 4 2652 ∈ ℕ0
179178, 31deccl 12308 . . 3 26523 ∈ ℕ0
180 3m1e2 11958 . . 3 (3 − 1) = 2
181 eqid 2737 . . . 4 26523 = 26523
182 5p3e8 11987 . . . . 5 (5 + 3) = 8
18311, 7, 182addcomli 11024 . . . 4 (3 + 5) = 8
184178, 31, 22, 181, 183decaddi 12353 . . 3 (26523 + 5) = 26528
18512, 11mulcli 10840 . . . . 5 (7 · 5) ∈ ℂ
186185mulid1i 10837 . . . 4 ((7 · 5) · 1) = (7 · 5)
18711, 12mulcomi 10841 . . . . 5 (5 · 7) = (7 · 5)
188 exp0 13639 . . . . . 6 (9 ∈ ℂ → (9↑0) = 1)
18944, 188ax-mp 5 . . . . 5 (9↑0) = 1
190187, 189oveq12i 7225 . . . 4 ((5 · 7) · (9↑0)) = ((7 · 5) · 1)
1917, 17, 83mulcomli 10842 . . . . . . 7 (2 · 3) = 6
192191oveq1i 7223 . . . . . 6 ((2 · 3) + 1) = (6 + 1)
193 df-7 11898 . . . . . 6 7 = (6 + 1)
194192, 193eqtr4i 2768 . . . . 5 ((2 · 3) + 1) = 7
195194oveq1i 7223 . . . 4 (((2 · 3) + 1) · 5) = (7 · 5)
196186, 190, 1953eqtr4i 2775 . . 3 ((5 · 7) · (9↑0)) = (((2 · 3) + 1) · 5)
197176, 179, 22, 31, 180, 184, 20, 161, 196log2ublem2 25830 . 2 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ (2 · 26528)
198 eqid 2737 . . 3 26528 = 26528
199 eqid 2737 . . . 4 2652 = 2652
200 eqid 2737 . . . . 5 265 = 265
201 00id 11007 . . . . . 6 (0 + 0) = 0
20220dec0h 12315 . . . . . 6 0 = 00
203201, 202eqtri 2765 . . . . 5 (0 + 0) = 00
204 eqid 2737 . . . . . 6 26 = 26
20535, 82eqtri 2765 . . . . . 6 (0 + 1) = 01
206171, 35oveq12i 7225 . . . . . . 7 ((2 · 2) + (0 + 1)) = (4 + 1)
207206, 72eqtri 2765 . . . . . 6 ((2 · 2) + (0 + 1)) = 5
208 6cn 11921 . . . . . . . 8 6 ∈ ℂ
209 6t2e12 12397 . . . . . . . 8 (6 · 2) = 12
210208, 17, 209mulcomli 10842 . . . . . . 7 (2 · 6) = 12
21125, 21, 41, 210decsuc 12324 . . . . . 6 ((2 · 6) + 1) = 13
21221, 106, 20, 25, 204, 205, 21, 31, 25, 207, 211decma2c 12346 . . . . 5 ((2 · 26) + (0 + 1)) = 53
21311, 17, 87mulcomli 10842 . . . . . . 7 (2 · 5) = 10
214213oveq1i 7223 . . . . . 6 ((2 · 5) + 0) = (10 + 0)
215 dec10p 12336 . . . . . 6 (10 + 0) = 10
216214, 215eqtri 2765 . . . . 5 ((2 · 5) + 0) = 10
217107, 22, 20, 20, 200, 203, 21, 20, 25, 212, 216decma2c 12346 . . . 4 ((2 · 265) + (0 + 0)) = 530
21822dec0h 12315 . . . . 5 5 = 05
219172, 72, 2183eqtri 2769 . . . 4 ((2 · 2) + 1) = 05
220177, 21, 20, 25, 199, 82, 21, 22, 20, 217, 219decma2c 12346 . . 3 ((2 · 2652) + 1) = 5305
221 8t2e16 12408 . . . 4 (8 · 2) = 16
22251, 17, 221mulcomli 10842 . . 3 (2 · 8) = 16
22321, 178, 42, 198, 106, 25, 220, 222decmul2c 12359 . 2 (2 · 26528) = 53056
224197, 223breqtri 5078 1 (((3↑7) · (5 · 7)) · Σ𝑛 ∈ (0...3)(2 / ((3 · ((2 · 𝑛) + 1)) · (9↑𝑛)))) ≤ 53056
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  wcel 2110  c0 4237   class class class wbr 5053  (class class class)co 7213  cc 10727  0cc0 10729  1c1 10730   + caddc 10732   · cmul 10734  cle 10868  cmin 11062   / cdiv 11489  2c2 11885  3c3 11886  4c4 11887  5c5 11888  6c6 11889  7c7 11890  8c8 11891  9c9 11892  0cn0 12090  cdc 12293  ...cfz 13095  cexp 13635  Σcsu 15249
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5179  ax-sep 5192  ax-nul 5199  ax-pow 5258  ax-pr 5322  ax-un 7523  ax-inf2 9256  ax-cnex 10785  ax-resscn 10786  ax-1cn 10787  ax-icn 10788  ax-addcl 10789  ax-addrcl 10790  ax-mulcl 10791  ax-mulrcl 10792  ax-mulcom 10793  ax-addass 10794  ax-mulass 10795  ax-distr 10796  ax-i2m1 10797  ax-1ne0 10798  ax-1rid 10799  ax-rnegex 10800  ax-rrecex 10801  ax-cnre 10802  ax-pre-lttri 10803  ax-pre-lttrn 10804  ax-pre-ltadd 10805  ax-pre-mulgt0 10806  ax-pre-sup 10807
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3410  df-sbc 3695  df-csb 3812  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-pss 3885  df-nul 4238  df-if 4440  df-pw 4515  df-sn 4542  df-pr 4544  df-tp 4546  df-op 4548  df-uni 4820  df-int 4860  df-iun 4906  df-br 5054  df-opab 5116  df-mpt 5136  df-tr 5162  df-id 5455  df-eprel 5460  df-po 5468  df-so 5469  df-fr 5509  df-se 5510  df-we 5511  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-pred 6160  df-ord 6216  df-on 6217  df-lim 6218  df-suc 6219  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388  df-isom 6389  df-riota 7170  df-ov 7216  df-oprab 7217  df-mpo 7218  df-om 7645  df-1st 7761  df-2nd 7762  df-wrecs 8047  df-recs 8108  df-rdg 8146  df-1o 8202  df-er 8391  df-en 8627  df-dom 8628  df-sdom 8629  df-fin 8630  df-sup 9058  df-oi 9126  df-card 9555  df-pnf 10869  df-mnf 10870  df-xr 10871  df-ltxr 10872  df-le 10873  df-sub 11064  df-neg 11065  df-div 11490  df-nn 11831  df-2 11893  df-3 11894  df-4 11895  df-5 11896  df-6 11897  df-7 11898  df-8 11899  df-9 11900  df-n0 12091  df-z 12177  df-dec 12294  df-uz 12439  df-rp 12587  df-fz 13096  df-fzo 13239  df-seq 13575  df-exp 13636  df-hash 13897  df-cj 14662  df-re 14663  df-im 14664  df-sqrt 14798  df-abs 14799  df-clim 15049  df-sum 15250
This theorem is referenced by:  log2ub  25832
  Copyright terms: Public domain W3C validator