Mathbox for Scott Fenton |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > logi | Structured version Visualization version GIF version |
Description: Calculate the logarithm of i. (Contributed by Scott Fenton, 13-Apr-2020.) |
Ref | Expression |
---|---|
logi | ⊢ (log‘i) = (i · (π / 2)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | efhalfpi 25393 | . 2 ⊢ (exp‘(i · (π / 2))) = i | |
2 | ax-icn 10818 | . . 3 ⊢ i ∈ ℂ | |
3 | ine0 11297 | . . 3 ⊢ i ≠ 0 | |
4 | halfpire 25386 | . . . . . 6 ⊢ (π / 2) ∈ ℝ | |
5 | 4 | recni 10877 | . . . . 5 ⊢ (π / 2) ∈ ℂ |
6 | 2, 5 | mulcli 10870 | . . . 4 ⊢ (i · (π / 2)) ∈ ℂ |
7 | pipos 25382 | . . . . . . 7 ⊢ 0 < π | |
8 | pire 25380 | . . . . . . . 8 ⊢ π ∈ ℝ | |
9 | lt0neg2 11369 | . . . . . . . 8 ⊢ (π ∈ ℝ → (0 < π ↔ -π < 0)) | |
10 | 8, 9 | ax-mp 5 | . . . . . . 7 ⊢ (0 < π ↔ -π < 0) |
11 | 7, 10 | mpbi 233 | . . . . . 6 ⊢ -π < 0 |
12 | halfpos2 12089 | . . . . . . . 8 ⊢ (π ∈ ℝ → (0 < π ↔ 0 < (π / 2))) | |
13 | 8, 12 | ax-mp 5 | . . . . . . 7 ⊢ (0 < π ↔ 0 < (π / 2)) |
14 | 7, 13 | mpbi 233 | . . . . . 6 ⊢ 0 < (π / 2) |
15 | 8 | renegcli 11169 | . . . . . . 7 ⊢ -π ∈ ℝ |
16 | 0re 10865 | . . . . . . 7 ⊢ 0 ∈ ℝ | |
17 | 15, 16, 4 | lttri 10988 | . . . . . 6 ⊢ ((-π < 0 ∧ 0 < (π / 2)) → -π < (π / 2)) |
18 | 11, 14, 17 | mp2an 692 | . . . . 5 ⊢ -π < (π / 2) |
19 | reim 14705 | . . . . . . 7 ⊢ ((π / 2) ∈ ℂ → (ℜ‘(π / 2)) = (ℑ‘(i · (π / 2)))) | |
20 | 5, 19 | ax-mp 5 | . . . . . 6 ⊢ (ℜ‘(π / 2)) = (ℑ‘(i · (π / 2))) |
21 | rere 14718 | . . . . . . 7 ⊢ ((π / 2) ∈ ℝ → (ℜ‘(π / 2)) = (π / 2)) | |
22 | 4, 21 | ax-mp 5 | . . . . . 6 ⊢ (ℜ‘(π / 2)) = (π / 2) |
23 | 20, 22 | eqtr3i 2769 | . . . . 5 ⊢ (ℑ‘(i · (π / 2))) = (π / 2) |
24 | 18, 23 | breqtrri 5097 | . . . 4 ⊢ -π < (ℑ‘(i · (π / 2))) |
25 | 8 | a1i 11 | . . . . . . . . . . 11 ⊢ (⊤ → π ∈ ℝ) |
26 | 25, 25 | ltaddposd 11446 | . . . . . . . . . 10 ⊢ (⊤ → (0 < π ↔ π < (π + π))) |
27 | 7, 26 | mpbii 236 | . . . . . . . . 9 ⊢ (⊤ → π < (π + π)) |
28 | picn 25381 | . . . . . . . . . 10 ⊢ π ∈ ℂ | |
29 | 28 | times2i 11999 | . . . . . . . . 9 ⊢ (π · 2) = (π + π) |
30 | 27, 29 | breqtrrdi 5112 | . . . . . . . 8 ⊢ (⊤ → π < (π · 2)) |
31 | 2rp 12621 | . . . . . . . . . 10 ⊢ 2 ∈ ℝ+ | |
32 | 31 | a1i 11 | . . . . . . . . 9 ⊢ (⊤ → 2 ∈ ℝ+) |
33 | 25, 25, 32 | ltdivmul2d 12710 | . . . . . . . 8 ⊢ (⊤ → ((π / 2) < π ↔ π < (π · 2))) |
34 | 30, 33 | mpbird 260 | . . . . . . 7 ⊢ (⊤ → (π / 2) < π) |
35 | 34 | mptru 1550 | . . . . . 6 ⊢ (π / 2) < π |
36 | 4, 8, 35 | ltleii 10985 | . . . . 5 ⊢ (π / 2) ≤ π |
37 | 23, 36 | eqbrtri 5091 | . . . 4 ⊢ (ℑ‘(i · (π / 2))) ≤ π |
38 | ellogrn 25480 | . . . 4 ⊢ ((i · (π / 2)) ∈ ran log ↔ ((i · (π / 2)) ∈ ℂ ∧ -π < (ℑ‘(i · (π / 2))) ∧ (ℑ‘(i · (π / 2))) ≤ π)) | |
39 | 6, 24, 37, 38 | mpbir3an 1343 | . . 3 ⊢ (i · (π / 2)) ∈ ran log |
40 | logeftb 25504 | . . 3 ⊢ ((i ∈ ℂ ∧ i ≠ 0 ∧ (i · (π / 2)) ∈ ran log) → ((log‘i) = (i · (π / 2)) ↔ (exp‘(i · (π / 2))) = i)) | |
41 | 2, 3, 39, 40 | mp3an 1463 | . 2 ⊢ ((log‘i) = (i · (π / 2)) ↔ (exp‘(i · (π / 2))) = i) |
42 | 1, 41 | mpbir 234 | 1 ⊢ (log‘i) = (i · (π / 2)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 209 = wceq 1543 ⊤wtru 1544 ∈ wcel 2112 ≠ wne 2943 class class class wbr 5070 ran crn 5570 ‘cfv 6401 (class class class)co 7235 ℂcc 10757 ℝcr 10758 0cc0 10759 ici 10761 + caddc 10762 · cmul 10764 < clt 10897 ≤ cle 10898 -cneg 11093 / cdiv 11519 2c2 11915 ℝ+crp 12616 ℜcre 14693 ℑcim 14694 expce 15656 πcpi 15661 logclog 25475 |
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 2114 ax-9 2122 ax-10 2143 ax-11 2160 ax-12 2177 ax-ext 2710 ax-rep 5196 ax-sep 5209 ax-nul 5216 ax-pow 5275 ax-pr 5339 ax-un 7545 ax-inf2 9286 ax-cnex 10815 ax-resscn 10816 ax-1cn 10817 ax-icn 10818 ax-addcl 10819 ax-addrcl 10820 ax-mulcl 10821 ax-mulrcl 10822 ax-mulcom 10823 ax-addass 10824 ax-mulass 10825 ax-distr 10826 ax-i2m1 10827 ax-1ne0 10828 ax-1rid 10829 ax-rnegex 10830 ax-rrecex 10831 ax-cnre 10832 ax-pre-lttri 10833 ax-pre-lttrn 10834 ax-pre-ltadd 10835 ax-pre-mulgt0 10836 ax-pre-sup 10837 ax-addf 10838 ax-mulf 10839 |
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 2073 df-mo 2541 df-eu 2570 df-clab 2717 df-cleq 2731 df-clel 2818 df-nfc 2889 df-ne 2944 df-nel 3050 df-ral 3069 df-rex 3070 df-reu 3071 df-rmo 3072 df-rab 3073 df-v 3425 df-sbc 3712 df-csb 3829 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3902 df-nul 4255 df-if 4457 df-pw 4532 df-sn 4559 df-pr 4561 df-tp 4563 df-op 4565 df-uni 4837 df-int 4877 df-iun 4923 df-iin 4924 df-br 5071 df-opab 5133 df-mpt 5153 df-tr 5179 df-id 5472 df-eprel 5478 df-po 5486 df-so 5487 df-fr 5527 df-se 5528 df-we 5529 df-xp 5575 df-rel 5576 df-cnv 5577 df-co 5578 df-dm 5579 df-rn 5580 df-res 5581 df-ima 5582 df-pred 6179 df-ord 6237 df-on 6238 df-lim 6239 df-suc 6240 df-iota 6359 df-fun 6403 df-fn 6404 df-f 6405 df-f1 6406 df-fo 6407 df-f1o 6408 df-fv 6409 df-isom 6410 df-riota 7192 df-ov 7238 df-oprab 7239 df-mpo 7240 df-of 7491 df-om 7667 df-1st 7783 df-2nd 7784 df-supp 7928 df-wrecs 8071 df-recs 8132 df-rdg 8170 df-1o 8226 df-2o 8227 df-er 8415 df-map 8534 df-pm 8535 df-ixp 8603 df-en 8651 df-dom 8652 df-sdom 8653 df-fin 8654 df-fsupp 9016 df-fi 9057 df-sup 9088 df-inf 9089 df-oi 9156 df-card 9585 df-pnf 10899 df-mnf 10900 df-xr 10901 df-ltxr 10902 df-le 10903 df-sub 11094 df-neg 11095 df-div 11520 df-nn 11861 df-2 11923 df-3 11924 df-4 11925 df-5 11926 df-6 11927 df-7 11928 df-8 11929 df-9 11930 df-n0 12121 df-z 12207 df-dec 12324 df-uz 12469 df-q 12575 df-rp 12617 df-xneg 12734 df-xadd 12735 df-xmul 12736 df-ioo 12969 df-ioc 12970 df-ico 12971 df-icc 12972 df-fz 13126 df-fzo 13269 df-fl 13397 df-mod 13475 df-seq 13607 df-exp 13668 df-fac 13873 df-bc 13902 df-hash 13930 df-shft 14663 df-cj 14695 df-re 14696 df-im 14697 df-sqrt 14831 df-abs 14832 df-limsup 15065 df-clim 15082 df-rlim 15083 df-sum 15283 df-ef 15662 df-sin 15664 df-cos 15665 df-pi 15667 df-struct 16733 df-sets 16750 df-slot 16768 df-ndx 16778 df-base 16794 df-ress 16818 df-plusg 16848 df-mulr 16849 df-starv 16850 df-sca 16851 df-vsca 16852 df-ip 16853 df-tset 16854 df-ple 16855 df-ds 16857 df-unif 16858 df-hom 16859 df-cco 16860 df-rest 16960 df-topn 16961 df-0g 16979 df-gsum 16980 df-topgen 16981 df-pt 16982 df-prds 16985 df-xrs 17040 df-qtop 17045 df-imas 17046 df-xps 17048 df-mre 17122 df-mrc 17123 df-acs 17125 df-mgm 18147 df-sgrp 18196 df-mnd 18207 df-submnd 18252 df-mulg 18522 df-cntz 18744 df-cmn 19205 df-psmet 20388 df-xmet 20389 df-met 20390 df-bl 20391 df-mopn 20392 df-fbas 20393 df-fg 20394 df-cnfld 20397 df-top 21823 df-topon 21840 df-topsp 21862 df-bases 21875 df-cld 21948 df-ntr 21949 df-cls 21950 df-nei 22027 df-lp 22065 df-perf 22066 df-cn 22156 df-cnp 22157 df-haus 22244 df-tx 22491 df-hmeo 22684 df-fil 22775 df-fm 22867 df-flim 22868 df-flf 22869 df-xms 23250 df-ms 23251 df-tms 23252 df-cncf 23807 df-limc 24795 df-dv 24796 df-log 25477 |
This theorem is referenced by: iexpire 33451 |
Copyright terms: Public domain | W3C validator |