HomeRelated theorems
GIF version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems GIF version |
| Description: i is a complex number. Axiom 4 of 25 for real and complex numbers, derived from ZF set theory. |
| Ref | Expression |
|---|---|
| axicn | ⊢ i ∈ ℂ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | df-i 5215 | . . . 4 ⊢ i = ⟨0R, 1R⟩ | |
| 2 | 1 | eleq1i 1529 | . . 3 ⊢ (i ∈ ℂ ↔ ⟨0R, 1R⟩ ∈ ℂ) |
| 3 | 1r 5162 | . . . . 5 ⊢ 1R ∈ R | |
| 4 | 3 | elisseti 1809 | . . . 4 ⊢ 1R ∈ V |
| 5 | 4 | opelcn 5220 | . . 3 ⊢ (⟨0R, 1R⟩ ∈ ℂ ↔ (0R ∈ R ⋀ 1R ∈ R)) |
| 6 | 2, 5 | bitr 173 | . 2 ⊢ (i ∈ ℂ ↔ (0R ∈ R ⋀ 1R ∈ R)) |
| 7 | 0r 5161 | . 2 ⊢ 0R ∈ R | |
| 8 | 6, 7, 3 | mpbir2an 728 | 1 ⊢ i ∈ ℂ |
| Colors of variables: wff set class |
| Syntax hints: ⋀ wa 223 ∈ wcel 955 ⟨cop 2401 Rcnr 4965 0Rc0r 4966 1Rc1r 4967 ℂcc 5204 ici 5208 |
| This theorem is referenced by: 0cn 5300 cnegextlem2 5318 cnegext 5320 0cnALT 5322 ine0 5406 1re 5407 ixi 5654 recextlem1 5655 recextlem2 5656 recext 5657 irec 6661 i2 6662 i3 6663 i4 6664 crulem 6666 cru 6667 crutOLD 6669 crne0 6670 crmul 6671 crrecz 6672 rimul 6675 nthruc 6676 replimtOLD 6693 cjclt 6696 crret 6702 crretOLD 6703 crimt 6704 crimtOLD 6705 imret 6710 reim0t 6711 reim0bt 6712 cjcj 6713 rereb 6715 cjreb 6716 recj 6717 imcj 6718 readd 6719 imadd 6720 cjadd 6723 cjmul 6724 reneg 6729 imneg 6731 cjneg 6732 addcj 6733 recjt 6753 imcjt 6754 rei 6759 imi 6760 cji 6762 cjreimt 6763 cjreim2t 6764 cj11t 6765 abs00 6777 absreimsqt 6791 absreimt 6792 absi 6815 recant 6842 caucvg3a 7100 caucvg3lem 7102 abspef01tlub 7336 sinclt 7373 cosclt 7374 resinvalt 7375 recosvalt 7376 efi4pt 7377 resin4pt 7378 recos4pt 7379 resinclt 7380 recosclt 7381 sinnegt 7384 cosnegt 7385 sin0 7386 cos0 7388 efivalt 7389 efmivalt 7390 efeult 7391 sinadd 7393 cosadd 7394 sin01bndlem2 7410 sin01bndlem3 7411 cos01bndlem2 7412 cos01bndlem3 7413 abseft 7425 demoivre 7426 demoivreALT 7427 nvpi 8233 ipval2 8291 4ipval2 8292 ipval3 8293 4ipval3 8296 ipid 8297 ipcl 8299 ipcj 8301 ip0r 8304 ip1cnilem1 8307 ip1cnilem2 8308 ip1cnilem3 8309 ip1cnilem4 8310 ip1cnilem5 8311 ip1cnilem6 8312 sspival 8331 ip1ilem 8416 ipasslem10 8430 ipasslem11 8431 sincolem 8584 sincnlem 8585 sinco 8586 sincn 8588 eulerid 8602 sinperlem1 8605 efimpi 8615 efif 8636 efif1lem4 8648 efielcircOLD 8655 efielcirc 8659 circgrp 8660 shftefif1olem 8661 shftefif1olemOLD 8662 eff1lem 8664 eff1i 8665 effoi 8666 effoiOLD 8667 efper 8669 pilog 8690 polid2 8945 polid 8946 lnopeq0lem1 9845 lnopeq0 9847 lnophmlem2 9857 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-9 962 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-rep 2683 ax-sep 2693 ax-nul 2700 ax-pow 2732 ax-pr 2769 ax-un 2857 ax-inf2 4597 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 774 df-3an 775 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-ral 1641 df-rex 1642 df-reu 1643 df-rab 1644 df-v 1803 df-sbc 1932 df-csb 1992 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-pss 2045 df-nul 2271 df-if 2352 df-pw 2392 df-sn 2402 df-pr 2403 df-tp 2405 df-op 2406 df-uni 2494 df-int 2524 df-iun 2558 df-br 2610 df-opab 2657 df-tr 2671 df-eprel 2821 df-id 2824 df-po 2831 df-so 2841 df-fr 2907 df-we 2924 df-ord 2941 df-on 2942 df-lim 2943 df-suc 2944 df-om 3122 df-xp 3174 df-rel 3175 df-cnv 3176 df-co 3177 df-dm 3178 df-rn 3179 df-res 3180 df-ima 3181 df-fun 3182 df-fn 3183 df-f 3184 df-fv 3188 df-rdg 3917 df-opr 3950 df-oprab 3951 df-1st 4063 df-2nd 4064 df-1o 4117 df-oadd 4119 df-omul 4120 df-er 4245 df-ec 4247 df-qs 4250 df-ni 4972 df-pli 4973 df-mi 4974 df-lti 4975 df-plpq 5007 df-mpq 5008 df-enq 5009 df-nq 5010 df-plq 5011 df-mq 5012 df-rq 5013 df-ltq 5014 df-1q 5015 df-np 5058 df-1p 5059 df-plp 5060 df-enr 5138 df-nr 5139 df-0r 5143 df-1r 5144 df-c 5212 df-i 5215 |