MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  log2cnv Structured version   Visualization version   GIF version
Theorem log2cnv 26673
Description: Using the Taylor series for arctan(i / 3), produce a rapidly convergent series for log2. (Contributed by Mario Carneiro, 7-Apr-2015.)
Hypothesis
Ref Expression
log2cnv.1 𝐹 = (𝑛 ∈ β„•0 ↦ (2 / ((3 Β· ((2 Β· 𝑛) + 1)) Β· (9↑𝑛))))
Assertion
Ref Expression
log2cnv seq0( + , 𝐹) ⇝ (logβ€˜2)
Proof of Theorem log2cnv
Dummy variable π‘˜ is distinct from all other variables.
StepHypRef Expression
1 nn0uz 12868 . . . 4 β„•0 = (β„€β‰₯β€˜0)
2 0zd 12574 . . . 4 (⊀ β†’ 0 ∈ β„€)
3 2cn 12291 . . . . . 6 2 ∈ β„‚
4 ax-icn 11171 . . . . . 6 i ∈ β„‚
5 ine0 11653 . . . . . 6 i β‰  0
63, 4, 5divcli 11960 . . . . 5 (2 / i) ∈ β„‚
76a1i 11 . . . 4 (⊀ β†’ (2 / i) ∈ β„‚)
8 3cn 12297 . . . . . . 7 3 ∈ β„‚
9 3ne0 12322 . . . . . . 7 3 β‰  0
104, 8, 9divcli 11960 . . . . . 6 (i / 3) ∈ β„‚
11 absdiv 15246 . . . . . . . . 9 ((i ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ (absβ€˜(i / 3)) = ((absβ€˜i) / (absβ€˜3)))
124, 8, 9, 11mp3an 1461 . . . . . . . 8 (absβ€˜(i / 3)) = ((absβ€˜i) / (absβ€˜3))
13 absi 15237 . . . . . . . . 9 (absβ€˜i) = 1
14 3re 12296 . . . . . . . . . 10 3 ∈ ℝ
15 0re 11220 . . . . . . . . . . 11 0 ∈ ℝ
16 3pos 12321 . . . . . . . . . . 11 0 < 3
1715, 14, 16ltleii 11341 . . . . . . . . . 10 0 ≀ 3
18 absid 15247 . . . . . . . . . 10 ((3 ∈ ℝ ∧ 0 ≀ 3) β†’ (absβ€˜3) = 3)
1914, 17, 18mp2an 690 . . . . . . . . 9 (absβ€˜3) = 3
2013, 19oveq12i 7423 . . . . . . . 8 ((absβ€˜i) / (absβ€˜3)) = (1 / 3)
2112, 20eqtri 2760 . . . . . . 7 (absβ€˜(i / 3)) = (1 / 3)
22 1lt3 12389 . . . . . . . 8 1 < 3
23 recgt1 12114 . . . . . . . . 9 ((3 ∈ ℝ ∧ 0 < 3) β†’ (1 < 3 ↔ (1 / 3) < 1))
2414, 16, 23mp2an 690 . . . . . . . 8 (1 < 3 ↔ (1 / 3) < 1)
2522, 24mpbi 229 . . . . . . 7 (1 / 3) < 1
2621, 25eqbrtri 5169 . . . . . 6 (absβ€˜(i / 3)) < 1
27 eqid 2732 . . . . . . 7 (𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1)))) = (𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))
2827atantayl3 26668 . . . . . 6 (((i / 3) ∈ β„‚ ∧ (absβ€˜(i / 3)) < 1) β†’ seq0( + , (𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))) ⇝ (arctanβ€˜(i / 3)))
2910, 26, 28mp2an 690 . . . . 5 seq0( + , (𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))) ⇝ (arctanβ€˜(i / 3))
3029a1i 11 . . . 4 (⊀ β†’ seq0( + , (𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))) ⇝ (arctanβ€˜(i / 3)))
31 oveq2 7419 . . . . . . . . 9 (𝑛 = π‘˜ β†’ (-1↑𝑛) = (-1β†‘π‘˜))
32 oveq2 7419 . . . . . . . . . . . 12 (𝑛 = π‘˜ β†’ (2 Β· 𝑛) = (2 Β· π‘˜))
3332oveq1d 7426 . . . . . . . . . . 11 (𝑛 = π‘˜ β†’ ((2 Β· 𝑛) + 1) = ((2 Β· π‘˜) + 1))
3433oveq2d 7427 . . . . . . . . . 10 (𝑛 = π‘˜ β†’ ((i / 3)↑((2 Β· 𝑛) + 1)) = ((i / 3)↑((2 Β· π‘˜) + 1)))
3534, 33oveq12d 7429 . . . . . . . . 9 (𝑛 = π‘˜ β†’ (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1)) = (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1)))
3631, 35oveq12d 7429 . . . . . . . 8 (𝑛 = π‘˜ β†’ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))) = ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
37 ovex 7444 . . . . . . . 8 ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) ∈ V
3836, 27, 37fvmpt 6998 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜) = ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
394a1i 11 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ i ∈ β„‚)
408a1i 11 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ 3 ∈ β„‚)
419a1i 11 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ 3 β‰  0)
42 2nn0 12493 . . . . . . . . . . . . . 14 2 ∈ β„•0
43 nn0mulcl 12512 . . . . . . . . . . . . . 14 ((2 ∈ β„•0 ∧ π‘˜ ∈ β„•0) β†’ (2 Β· π‘˜) ∈ β„•0)
4442, 43mpan 688 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) ∈ β„•0)
45 peano2nn0 12516 . . . . . . . . . . . . 13 ((2 Β· π‘˜) ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
4644, 45syl 17 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•0)
4739, 40, 41, 46expdivd 14129 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ ((i / 3)↑((2 Β· π‘˜) + 1)) = ((i↑((2 Β· π‘˜) + 1)) / (3↑((2 Β· π‘˜) + 1))))
4847oveq2d 7427 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) = ((-1β†‘π‘˜) Β· ((i↑((2 Β· π‘˜) + 1)) / (3↑((2 Β· π‘˜) + 1)))))
49 neg1cn 12330 . . . . . . . . . . . 12 -1 ∈ β„‚
50 expcl 14049 . . . . . . . . . . . 12 ((-1 ∈ β„‚ ∧ π‘˜ ∈ β„•0) β†’ (-1β†‘π‘˜) ∈ β„‚)
5149, 50mpan 688 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (-1β†‘π‘˜) ∈ β„‚)
52 expcl 14049 . . . . . . . . . . . 12 ((i ∈ β„‚ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (i↑((2 Β· π‘˜) + 1)) ∈ β„‚)
534, 46, 52sylancr 587 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (i↑((2 Β· π‘˜) + 1)) ∈ β„‚)
54 3nn 12295 . . . . . . . . . . . . 13 3 ∈ β„•
55 nnexpcl 14044 . . . . . . . . . . . . 13 ((3 ∈ β„• ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ (3↑((2 Β· π‘˜) + 1)) ∈ β„•)
5654, 46, 55sylancr 587 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (3↑((2 Β· π‘˜) + 1)) ∈ β„•)
5756nncnd 12232 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (3↑((2 Β· π‘˜) + 1)) ∈ β„‚)
5856nnne0d 12266 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (3↑((2 Β· π‘˜) + 1)) β‰  0)
5951, 53, 57, 58divassd 12029 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (i↑((2 Β· π‘˜) + 1))) / (3↑((2 Β· π‘˜) + 1))) = ((-1β†‘π‘˜) Β· ((i↑((2 Β· π‘˜) + 1)) / (3↑((2 Β· π‘˜) + 1)))))
60 expp1 14038 . . . . . . . . . . . . . . 15 ((i ∈ β„‚ ∧ (2 Β· π‘˜) ∈ β„•0) β†’ (i↑((2 Β· π‘˜) + 1)) = ((i↑(2 Β· π‘˜)) Β· i))
614, 44, 60sylancr 587 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ (i↑((2 Β· π‘˜) + 1)) = ((i↑(2 Β· π‘˜)) Β· i))
62 expmul 14077 . . . . . . . . . . . . . . . . 17 ((i ∈ β„‚ ∧ 2 ∈ β„•0 ∧ π‘˜ ∈ β„•0) β†’ (i↑(2 Β· π‘˜)) = ((i↑2)β†‘π‘˜))
634, 42, 62mp3an12 1451 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (i↑(2 Β· π‘˜)) = ((i↑2)β†‘π‘˜))
64 i2 14170 . . . . . . . . . . . . . . . . 17 (i↑2) = -1
6564oveq1i 7421 . . . . . . . . . . . . . . . 16 ((i↑2)β†‘π‘˜) = (-1β†‘π‘˜)
6663, 65eqtrdi 2788 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ (i↑(2 Β· π‘˜)) = (-1β†‘π‘˜))
6766oveq1d 7426 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ ((i↑(2 Β· π‘˜)) Β· i) = ((-1β†‘π‘˜) Β· i))
6861, 67eqtrd 2772 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ (i↑((2 Β· π‘˜) + 1)) = ((-1β†‘π‘˜) Β· i))
6968oveq2d 7427 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· (i↑((2 Β· π‘˜) + 1))) = ((-1β†‘π‘˜) Β· ((-1β†‘π‘˜) Β· i)))
7051, 51, 39mulassd 11241 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (-1β†‘π‘˜)) Β· i) = ((-1β†‘π‘˜) Β· ((-1β†‘π‘˜) Β· i)))
7149a1i 11 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ -1 ∈ β„‚)
72 id 22 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„•0)
7371, 72, 72expaddd 14117 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ (-1↑(π‘˜ + π‘˜)) = ((-1β†‘π‘˜) Β· (-1β†‘π‘˜)))
74 expmul 14077 . . . . . . . . . . . . . . . . . 18 ((-1 ∈ β„‚ ∧ 2 ∈ β„•0 ∧ π‘˜ ∈ β„•0) β†’ (-1↑(2 Β· π‘˜)) = ((-1↑2)β†‘π‘˜))
7549, 42, 74mp3an12 1451 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„•0 β†’ (-1↑(2 Β· π‘˜)) = ((-1↑2)β†‘π‘˜))
76 neg1sqe1 14164 . . . . . . . . . . . . . . . . . 18 (-1↑2) = 1
7776oveq1i 7421 . . . . . . . . . . . . . . . . 17 ((-1↑2)β†‘π‘˜) = (1β†‘π‘˜)
7875, 77eqtrdi 2788 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (-1↑(2 Β· π‘˜)) = (1β†‘π‘˜))
79 nn0cn 12486 . . . . . . . . . . . . . . . . . 18 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„‚)
80792timesd 12459 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„•0 β†’ (2 Β· π‘˜) = (π‘˜ + π‘˜))
8180oveq2d 7427 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (-1↑(2 Β· π‘˜)) = (-1↑(π‘˜ + π‘˜)))
82 nn0z 12587 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„•0 β†’ π‘˜ ∈ β„€)
83 1exp 14061 . . . . . . . . . . . . . . . . 17 (π‘˜ ∈ β„€ β†’ (1β†‘π‘˜) = 1)
8482, 83syl 17 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (1β†‘π‘˜) = 1)
8578, 81, 843eqtr3d 2780 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ (-1↑(π‘˜ + π‘˜)) = 1)
8673, 85eqtr3d 2774 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· (-1β†‘π‘˜)) = 1)
8786oveq1d 7426 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (-1β†‘π‘˜)) Β· i) = (1 Β· i))
884mullidi 11223 . . . . . . . . . . . . 13 (1 Β· i) = i
8987, 88eqtrdi 2788 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (-1β†‘π‘˜)) Β· i) = i)
9069, 70, 893eqtr2d 2778 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· (i↑((2 Β· π‘˜) + 1))) = i)
9190oveq1d 7426 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (i↑((2 Β· π‘˜) + 1))) / (3↑((2 Β· π‘˜) + 1))) = (i / (3↑((2 Β· π‘˜) + 1))))
9248, 59, 913eqtr2d 2778 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) = (i / (3↑((2 Β· π‘˜) + 1))))
9392oveq1d 7426 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) / ((2 Β· π‘˜) + 1)) = ((i / (3↑((2 Β· π‘˜) + 1))) / ((2 Β· π‘˜) + 1)))
94 expcl 14049 . . . . . . . . . 10 (((i / 3) ∈ β„‚ ∧ ((2 Β· π‘˜) + 1) ∈ β„•0) β†’ ((i / 3)↑((2 Β· π‘˜) + 1)) ∈ β„‚)
9510, 46, 94sylancr 587 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((i / 3)↑((2 Β· π‘˜) + 1)) ∈ β„‚)
96 nn0p1nn 12515 . . . . . . . . . . 11 ((2 Β· π‘˜) ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
9744, 96syl 17 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„•)
9897nncnd 12232 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) ∈ β„‚)
9997nnne0d 12266 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((2 Β· π‘˜) + 1) β‰  0)
10051, 95, 98, 99divassd 12029 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) / ((2 Β· π‘˜) + 1)) = ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))))
10139, 57, 98, 58, 99divdiv1d 12025 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((i / (3↑((2 Β· π‘˜) + 1))) / ((2 Β· π‘˜) + 1)) = (i / ((3↑((2 Β· π‘˜) + 1)) Β· ((2 Β· π‘˜) + 1))))
10293, 100, 1013eqtr3d 2780 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (i / ((3↑((2 Β· π‘˜) + 1)) Β· ((2 Β· π‘˜) + 1))))
10357, 98mulcomd 11239 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((3↑((2 Β· π‘˜) + 1)) Β· ((2 Β· π‘˜) + 1)) = (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1))))
104103oveq2d 7427 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (i / ((3↑((2 Β· π‘˜) + 1)) Β· ((2 Β· π‘˜) + 1))) = (i / (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1)))))
10538, 102, 1043eqtrd 2776 . . . . . 6 (π‘˜ ∈ β„•0 β†’ ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜) = (i / (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1)))))
10697, 56nnmulcld 12269 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1))) ∈ β„•)
107106nncnd 12232 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1))) ∈ β„‚)
108106nnne0d 12266 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1))) β‰  0)
10939, 107, 108divcld 11994 . . . . . 6 (π‘˜ ∈ β„•0 β†’ (i / (((2 Β· π‘˜) + 1) Β· (3↑((2 Β· π‘˜) + 1)))) ∈ β„‚)
110105, 109eqeltrd 2833 . . . . 5 (π‘˜ ∈ β„•0 β†’ ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜) ∈ β„‚)
111110adantl 482 . . . 4 ((⊀ ∧ π‘˜ ∈ β„•0) β†’ ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜) ∈ β„‚)
11233oveq2d 7427 . . . . . . . . 9 (𝑛 = π‘˜ β†’ (3 Β· ((2 Β· 𝑛) + 1)) = (3 Β· ((2 Β· π‘˜) + 1)))
113 oveq2 7419 . . . . . . . . 9 (𝑛 = π‘˜ β†’ (9↑𝑛) = (9β†‘π‘˜))
114112, 113oveq12d 7429 . . . . . . . 8 (𝑛 = π‘˜ β†’ ((3 Β· ((2 Β· 𝑛) + 1)) Β· (9↑𝑛)) = ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)))
115114oveq2d 7427 . . . . . . 7 (𝑛 = π‘˜ β†’ (2 / ((3 Β· ((2 Β· 𝑛) + 1)) Β· (9↑𝑛))) = (2 / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
116 log2cnv.1 . . . . . . 7 𝐹 = (𝑛 ∈ β„•0 ↦ (2 / ((3 Β· ((2 Β· 𝑛) + 1)) Β· (9↑𝑛))))
117 ovex 7444 . . . . . . 7 (2 / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) ∈ V
118115, 116, 117fvmpt 6998 . . . . . 6 (π‘˜ ∈ β„•0 β†’ (πΉβ€˜π‘˜) = (2 / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
119 expp1 14038 . . . . . . . . . . . . . . 15 ((3 ∈ β„‚ ∧ (2 Β· π‘˜) ∈ β„•0) β†’ (3↑((2 Β· π‘˜) + 1)) = ((3↑(2 Β· π‘˜)) Β· 3))
1208, 44, 119sylancr 587 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ (3↑((2 Β· π‘˜) + 1)) = ((3↑(2 Β· π‘˜)) Β· 3))
121 expmul 14077 . . . . . . . . . . . . . . . . 17 ((3 ∈ β„‚ ∧ 2 ∈ β„•0 ∧ π‘˜ ∈ β„•0) β†’ (3↑(2 Β· π‘˜)) = ((3↑2)β†‘π‘˜))
1228, 42, 121mp3an12 1451 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (3↑(2 Β· π‘˜)) = ((3↑2)β†‘π‘˜))
123 sq3 14166 . . . . . . . . . . . . . . . . 17 (3↑2) = 9
124123oveq1i 7421 . . . . . . . . . . . . . . . 16 ((3↑2)β†‘π‘˜) = (9β†‘π‘˜)
125122, 124eqtrdi 2788 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ (3↑(2 Β· π‘˜)) = (9β†‘π‘˜))
126125oveq1d 7426 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ ((3↑(2 Β· π‘˜)) Β· 3) = ((9β†‘π‘˜) Β· 3))
127 9nn 12314 . . . . . . . . . . . . . . . . 17 9 ∈ β„•
128 nnexpcl 14044 . . . . . . . . . . . . . . . . 17 ((9 ∈ β„• ∧ π‘˜ ∈ β„•0) β†’ (9β†‘π‘˜) ∈ β„•)
129127, 128mpan 688 . . . . . . . . . . . . . . . 16 (π‘˜ ∈ β„•0 β†’ (9β†‘π‘˜) ∈ β„•)
130129nncnd 12232 . . . . . . . . . . . . . . 15 (π‘˜ ∈ β„•0 β†’ (9β†‘π‘˜) ∈ β„‚)
131 mulcom 11198 . . . . . . . . . . . . . . 15 (((9β†‘π‘˜) ∈ β„‚ ∧ 3 ∈ β„‚) β†’ ((9β†‘π‘˜) Β· 3) = (3 Β· (9β†‘π‘˜)))
132130, 8, 131sylancl 586 . . . . . . . . . . . . . 14 (π‘˜ ∈ β„•0 β†’ ((9β†‘π‘˜) Β· 3) = (3 Β· (9β†‘π‘˜)))
133120, 126, 1323eqtrd 2776 . . . . . . . . . . . . 13 (π‘˜ ∈ β„•0 β†’ (3↑((2 Β· π‘˜) + 1)) = (3 Β· (9β†‘π‘˜)))
13490, 133oveq12d 7429 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· (i↑((2 Β· π‘˜) + 1))) / (3↑((2 Β· π‘˜) + 1))) = (i / (3 Β· (9β†‘π‘˜))))
13548, 59, 1343eqtr2d 2778 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) = (i / (3 Β· (9β†‘π‘˜))))
136135oveq1d 7426 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ (((-1β†‘π‘˜) Β· ((i / 3)↑((2 Β· π‘˜) + 1))) / ((2 Β· π‘˜) + 1)) = ((i / (3 Β· (9β†‘π‘˜))) / ((2 Β· π‘˜) + 1)))
137 nnmulcl 12240 . . . . . . . . . . . . 13 ((3 ∈ β„• ∧ (9β†‘π‘˜) ∈ β„•) β†’ (3 Β· (9β†‘π‘˜)) ∈ β„•)
13854, 129, 137sylancr 587 . . . . . . . . . . . 12 (π‘˜ ∈ β„•0 β†’ (3 Β· (9β†‘π‘˜)) ∈ β„•)
139138nncnd 12232 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (3 Β· (9β†‘π‘˜)) ∈ β„‚)
140138nnne0d 12266 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (3 Β· (9β†‘π‘˜)) β‰  0)
14139, 139, 98, 140, 99divdiv1d 12025 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((i / (3 Β· (9β†‘π‘˜))) / ((2 Β· π‘˜) + 1)) = (i / ((3 Β· (9β†‘π‘˜)) Β· ((2 Β· π‘˜) + 1))))
142136, 100, 1413eqtr3d 2780 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((-1β†‘π‘˜) Β· (((i / 3)↑((2 Β· π‘˜) + 1)) / ((2 Β· π‘˜) + 1))) = (i / ((3 Β· (9β†‘π‘˜)) Β· ((2 Β· π‘˜) + 1))))
14340, 130, 98mul32d 11428 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((3 Β· (9β†‘π‘˜)) Β· ((2 Β· π‘˜) + 1)) = ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)))
144143oveq2d 7427 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ (i / ((3 Β· (9β†‘π‘˜)) Β· ((2 Β· π‘˜) + 1))) = (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
14538, 142, 1443eqtrd 2776 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜) = (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
146145oveq2d 7427 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((2 / i) Β· ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜)) = ((2 / i) Β· (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)))))
147 nnmulcl 12240 . . . . . . . . . . . 12 ((3 ∈ β„• ∧ ((2 Β· π‘˜) + 1) ∈ β„•) β†’ (3 Β· ((2 Β· π‘˜) + 1)) ∈ β„•)
14854, 97, 147sylancr 587 . . . . . . . . . . 11 (π‘˜ ∈ β„•0 β†’ (3 Β· ((2 Β· π‘˜) + 1)) ∈ β„•)
149148, 129nnmulcld 12269 . . . . . . . . . 10 (π‘˜ ∈ β„•0 β†’ ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)) ∈ β„•)
150149nncnd 12232 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)) ∈ β„‚)
151149nnne0d 12266 . . . . . . . . 9 (π‘˜ ∈ β„•0 β†’ ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)) β‰  0)
15239, 150, 151divcld 11994 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) ∈ β„‚)
153 mulcom 11198 . . . . . . . 8 (((i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) ∈ β„‚ ∧ (2 / i) ∈ β„‚) β†’ ((i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) Β· (2 / i)) = ((2 / i) Β· (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)))))
154152, 6, 153sylancl 586 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) Β· (2 / i)) = ((2 / i) Β· (i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜)))))
1553a1i 11 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ 2 ∈ β„‚)
1565a1i 11 . . . . . . . 8 (π‘˜ ∈ β„•0 β†’ i β‰  0)
157155, 39, 150, 156, 151dmdcand 12023 . . . . . . 7 (π‘˜ ∈ β„•0 β†’ ((i / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))) Β· (2 / i)) = (2 / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
158146, 154, 1573eqtr2d 2778 . . . . . 6 (π‘˜ ∈ β„•0 β†’ ((2 / i) Β· ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜)) = (2 / ((3 Β· ((2 Β· π‘˜) + 1)) Β· (9β†‘π‘˜))))
159118, 158eqtr4d 2775 . . . . 5 (π‘˜ ∈ β„•0 β†’ (πΉβ€˜π‘˜) = ((2 / i) Β· ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜)))
160159adantl 482 . . . 4 ((⊀ ∧ π‘˜ ∈ β„•0) β†’ (πΉβ€˜π‘˜) = ((2 / i) Β· ((𝑛 ∈ β„•0 ↦ ((-1↑𝑛) Β· (((i / 3)↑((2 Β· 𝑛) + 1)) / ((2 Β· 𝑛) + 1))))β€˜π‘˜)))
1611, 2, 7, 30, 111, 160isermulc2 15608 . . 3 (⊀ β†’ seq0( + , 𝐹) ⇝ ((2 / i) Β· (arctanβ€˜(i / 3))))
162161mptru 1548 . 2 seq0( + , 𝐹) ⇝ ((2 / i) Β· (arctanβ€˜(i / 3)))
163 bndatandm 26658 . . . . . . . 8 (((i / 3) ∈ β„‚ ∧ (absβ€˜(i / 3)) < 1) β†’ (i / 3) ∈ dom arctan)
16410, 26, 163mp2an 690 . . . . . . 7 (i / 3) ∈ dom arctan
165 atanval 26613 . . . . . . 7 ((i / 3) ∈ dom arctan β†’ (arctanβ€˜(i / 3)) = ((i / 2) Β· ((logβ€˜(1 βˆ’ (i Β· (i / 3)))) βˆ’ (logβ€˜(1 + (i Β· (i / 3)))))))
166164, 165ax-mp 5 . . . . . 6 (arctanβ€˜(i / 3)) = ((i / 2) Β· ((logβ€˜(1 βˆ’ (i Β· (i / 3)))) βˆ’ (logβ€˜(1 + (i Β· (i / 3))))))
167 df-4 12281 . . . . . . . . . . . . 13 4 = (3 + 1)
168167oveq1i 7421 . . . . . . . . . . . 12 (4 / 3) = ((3 + 1) / 3)
169 ax-1cn 11170 . . . . . . . . . . . . 13 1 ∈ β„‚
1708, 169, 8, 9divdiri 11975 . . . . . . . . . . . 12 ((3 + 1) / 3) = ((3 / 3) + (1 / 3))
1718, 9dividi 11951 . . . . . . . . . . . . 13 (3 / 3) = 1
172171oveq1i 7421 . . . . . . . . . . . 12 ((3 / 3) + (1 / 3)) = (1 + (1 / 3))
173168, 170, 1723eqtri 2764 . . . . . . . . . . 11 (4 / 3) = (1 + (1 / 3))
174169, 8, 9divcli 11960 . . . . . . . . . . . 12 (1 / 3) ∈ β„‚
175169, 174subnegi 11543 . . . . . . . . . . 11 (1 βˆ’ -(1 / 3)) = (1 + (1 / 3))
176 divneg 11910 . . . . . . . . . . . . . 14 ((1 ∈ β„‚ ∧ 3 ∈ β„‚ ∧ 3 β‰  0) β†’ -(1 / 3) = (-1 / 3))
177169, 8, 9, 176mp3an 1461 . . . . . . . . . . . . 13 -(1 / 3) = (-1 / 3)
178 ixi 11847 . . . . . . . . . . . . . 14 (i Β· i) = -1
179178oveq1i 7421 . . . . . . . . . . . . 13 ((i Β· i) / 3) = (-1 / 3)
1804, 4, 8, 9divassi 11974 . . . . . . . . . . . . 13 ((i Β· i) / 3) = (i Β· (i / 3))
181177, 179, 1803eqtr2i 2766 . . . . . . . . . . . 12 -(1 / 3) = (i Β· (i / 3))
182181oveq2i 7422 . . . . . . . . . . 11 (1 βˆ’ -(1 / 3)) = (1 βˆ’ (i Β· (i / 3)))
183173, 175, 1823eqtr2ri 2767 . . . . . . . . . 10 (1 βˆ’ (i Β· (i / 3))) = (4 / 3)
184183fveq2i 6894 . . . . . . . . 9 (logβ€˜(1 βˆ’ (i Β· (i / 3)))) = (logβ€˜(4 / 3))
1858, 9pm3.2i 471 . . . . . . . . . . . . 13 (3 ∈ β„‚ ∧ 3 β‰  0)
186 divsubdir 11912 . . . . . . . . . . . . 13 ((3 ∈ β„‚ ∧ 1 ∈ β„‚ ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((3 βˆ’ 1) / 3) = ((3 / 3) βˆ’ (1 / 3)))
1878, 169, 185, 186mp3an 1461 . . . . . . . . . . . 12 ((3 βˆ’ 1) / 3) = ((3 / 3) βˆ’ (1 / 3))
188 3m1e2 12344 . . . . . . . . . . . . 13 (3 βˆ’ 1) = 2
189188oveq1i 7421 . . . . . . . . . . . 12 ((3 βˆ’ 1) / 3) = (2 / 3)
190171oveq1i 7421 . . . . . . . . . . . 12 ((3 / 3) βˆ’ (1 / 3)) = (1 βˆ’ (1 / 3))
191187, 189, 1903eqtr3i 2768 . . . . . . . . . . 11 (2 / 3) = (1 βˆ’ (1 / 3))
192169, 174negsubi 11542 . . . . . . . . . . 11 (1 + -(1 / 3)) = (1 βˆ’ (1 / 3))
193181oveq2i 7422 . . . . . . . . . . 11 (1 + -(1 / 3)) = (1 + (i Β· (i / 3)))
194191, 192, 1933eqtr2ri 2767 . . . . . . . . . 10 (1 + (i Β· (i / 3))) = (2 / 3)
195194fveq2i 6894 . . . . . . . . 9 (logβ€˜(1 + (i Β· (i / 3)))) = (logβ€˜(2 / 3))
196184, 195oveq12i 7423 . . . . . . . 8 ((logβ€˜(1 βˆ’ (i Β· (i / 3)))) βˆ’ (logβ€˜(1 + (i Β· (i / 3))))) = ((logβ€˜(4 / 3)) βˆ’ (logβ€˜(2 / 3)))
197 4re 12300 . . . . . . . . . . 11 4 ∈ ℝ
198 4pos 12323 . . . . . . . . . . 11 0 < 4
199197, 198elrpii 12981 . . . . . . . . . 10 4 ∈ ℝ+
200 3rp 12984 . . . . . . . . . 10 3 ∈ ℝ+
201 rpdivcl 13003 . . . . . . . . . 10 ((4 ∈ ℝ+ ∧ 3 ∈ ℝ+) β†’ (4 / 3) ∈ ℝ+)
202199, 200, 201mp2an 690 . . . . . . . . 9 (4 / 3) ∈ ℝ+
203 2rp 12983 . . . . . . . . . 10 2 ∈ ℝ+
204 rpdivcl 13003 . . . . . . . . . 10 ((2 ∈ ℝ+ ∧ 3 ∈ ℝ+) β†’ (2 / 3) ∈ ℝ+)
205203, 200, 204mp2an 690 . . . . . . . . 9 (2 / 3) ∈ ℝ+
206 relogdiv 26325 . . . . . . . . 9 (((4 / 3) ∈ ℝ+ ∧ (2 / 3) ∈ ℝ+) β†’ (logβ€˜((4 / 3) / (2 / 3))) = ((logβ€˜(4 / 3)) βˆ’ (logβ€˜(2 / 3))))
207202, 205, 206mp2an 690 . . . . . . . 8 (logβ€˜((4 / 3) / (2 / 3))) = ((logβ€˜(4 / 3)) βˆ’ (logβ€˜(2 / 3)))
208 4cn 12301 . . . . . . . . . . 11 4 ∈ β„‚
209 2cnne0 12426 . . . . . . . . . . 11 (2 ∈ β„‚ ∧ 2 β‰  0)
210 divcan7 11927 . . . . . . . . . . 11 ((4 ∈ β„‚ ∧ (2 ∈ β„‚ ∧ 2 β‰  0) ∧ (3 ∈ β„‚ ∧ 3 β‰  0)) β†’ ((4 / 3) / (2 / 3)) = (4 / 2))
211208, 209, 185, 210mp3an 1461 . . . . . . . . . 10 ((4 / 3) / (2 / 3)) = (4 / 2)
212 4d2e2 12386 . . . . . . . . . 10 (4 / 2) = 2
213211, 212eqtri 2760 . . . . . . . . 9 ((4 / 3) / (2 / 3)) = 2
214213fveq2i 6894 . . . . . . . 8 (logβ€˜((4 / 3) / (2 / 3))) = (logβ€˜2)
215196, 207, 2143eqtr2i 2766 . . . . . . 7 ((logβ€˜(1 βˆ’ (i Β· (i / 3)))) βˆ’ (logβ€˜(1 + (i Β· (i / 3))))) = (logβ€˜2)
216215oveq2i 7422 . . . . . 6 ((i / 2) Β· ((logβ€˜(1 βˆ’ (i Β· (i / 3)))) βˆ’ (logβ€˜(1 + (i Β· (i / 3)))))) = ((i / 2) Β· (logβ€˜2))
217166, 216eqtri 2760 . . . . 5 (arctanβ€˜(i / 3)) = ((i / 2) Β· (logβ€˜2))
218217oveq2i 7422 . . . 4 ((2 / i) Β· (arctanβ€˜(i / 3))) = ((2 / i) Β· ((i / 2) Β· (logβ€˜2)))
219 2ne0 12320 . . . . . 6 2 β‰  0
2204, 3, 219divcli 11960 . . . . 5 (i / 2) ∈ β„‚
221 logcl 26301 . . . . . 6 ((2 ∈ β„‚ ∧ 2 β‰  0) β†’ (logβ€˜2) ∈ β„‚)
2223, 219, 221mp2an 690 . . . . 5 (logβ€˜2) ∈ β„‚
2236, 220, 222mulassi 11229 . . . 4 (((2 / i) Β· (i / 2)) Β· (logβ€˜2)) = ((2 / i) Β· ((i / 2) Β· (logβ€˜2)))
224218, 223eqtr4i 2763 . . 3 ((2 / i) Β· (arctanβ€˜(i / 3))) = (((2 / i) Β· (i / 2)) Β· (logβ€˜2))
225 divcan6 11925 . . . . 5 (((2 ∈ β„‚ ∧ 2 β‰  0) ∧ (i ∈ β„‚ ∧ i β‰  0)) β†’ ((2 / i) Β· (i / 2)) = 1)
2263, 219, 4, 5, 225mp4an 691 . . . 4 ((2 / i) Β· (i / 2)) = 1
227226oveq1i 7421 . . 3 (((2 / i) Β· (i / 2)) Β· (logβ€˜2)) = (1 Β· (logβ€˜2))
228222mullidi 11223 . . 3 (1 Β· (logβ€˜2)) = (logβ€˜2)
229224, 227, 2283eqtri 2764 . 2 ((2 / i) Β· (arctanβ€˜(i / 3))) = (logβ€˜2)
230162, 229breqtri 5173 1 seq0( + , 𝐹) ⇝ (logβ€˜2)
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1541  βŠ€wtru 1542   ∈ wcel 2106   β‰  wne 2940   class class class wbr 5148   ↦ cmpt 5231  dom cdm 5676  β€˜cfv 6543  (class class class)co 7411  β„‚cc 11110  β„cr 11111  0cc0 11112  1c1 11113  ici 11114   + caddc 11115   Β· cmul 11117   < clt 11252   ≀ cle 11253   βˆ’ cmin 11448  -cneg 11449   / cdiv 11875  β„•cn 12216  2c2 12271  3c3 12272  4c4 12273  9c9 12278  β„•0cn0 12476  β„€cz 12562  β„+crp 12978  seqcseq 13970  β†‘cexp 14031  abscabs 15185   ⇝ cli 15432  logclog 26287  arctancatan 26593
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 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  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  ax-addf 11191  ax-mulf 11192
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 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-iin 5000  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-se 5632  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7672  df-om 7858  df-1st 7977  df-2nd 7978  df-supp 8149  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-2o 8469  df-oadd 8472  df-er 8705  df-map 8824  df-pm 8825  df-ixp 8894  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-fsupp 9364  df-fi 9408  df-sup 9439  df-inf 9440  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-xnn0 12549  df-z 12563  df-dec 12682  df-uz 12827  df-q 12937  df-rp 12979  df-xneg 13096  df-xadd 13097  df-xmul 13098  df-ioo 13332  df-ioc 13333  df-ico 13334  df-icc 13335  df-fz 13489  df-fzo 13632  df-fl 13761  df-mod 13839  df-seq 13971  df-exp 14032  df-fac 14238  df-bc 14267  df-hash 14295  df-shft 15018  df-cj 15050  df-re 15051  df-im 15052  df-sqrt 15186  df-abs 15187  df-limsup 15419  df-clim 15436  df-rlim 15437  df-sum 15637  df-ef 16015  df-sin 16017  df-cos 16018  df-tan 16019  df-pi 16020  df-dvds 16202  df-struct 17084  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-starv 17216  df-sca 17217  df-vsca 17218  df-ip 17219  df-tset 17220  df-ple 17221  df-ds 17223  df-unif 17224  df-hom 17225  df-cco 17226  df-rest 17372  df-topn 17373  df-0g 17391  df-gsum 17392  df-topgen 17393  df-pt 17394  df-prds 17397  df-xrs 17452  df-qtop 17457  df-imas 17458  df-xps 17460  df-mre 17534  df-mrc 17535  df-acs 17537  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-submnd 18706  df-mulg 18987  df-cntz 19222  df-cmn 19691  df-psmet 21136  df-xmet 21137  df-met 21138  df-bl 21139  df-mopn 21140  df-fbas 21141  df-fg 21142  df-cnfld 21145  df-top 22616  df-topon 22633  df-topsp 22655  df-bases 22669  df-cld 22743  df-ntr 22744  df-cls 22745  df-nei 22822  df-lp 22860  df-perf 22861  df-cn 22951  df-cnp 22952  df-haus 23039  df-cmp 23111  df-tx 23286  df-hmeo 23479  df-fil 23570  df-fm 23662  df-flim 23663  df-flf 23664  df-xms 24046  df-ms 24047  df-tms 24048  df-cncf 24618  df-limc 25607  df-dv 25608  df-ulm 26113  df-log 26289  df-atan 26596
This theorem is referenced by:  log2tlbnd  26674
  Copyright terms: Public domain W3C validator