axicn - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem axicn 5257

Description: i is a complex number. Axiom 4 of 25 for real and complex numbers, derived from ZF set theory.

**Assertion**
Ref	Expression
axicn	⊢ i ∈ ℂ

**Proof of Theorem axicn**
Step	Hyp	Ref	Expression
1		df-i 5230	. . . 4 ⊢ i = ⟨0_R, 1_R⟩
2	1	eleq1i 1536	. . 3 ⊢ (i ∈ ℂ ↔ ⟨0_R, 1_R⟩ ∈ ℂ)
3		1r 5177	. . . . 5 ⊢ 1_R ∈ R
4	3	elisseti 1816	. . . 4 ⊢ 1_R ∈ V
5	4	opelcn 5235	. . 3 ⊢ (⟨0_R, 1_R⟩ ∈ ℂ ↔ (0_R ∈ R ⋀ 1_R ∈ R))
6	2, 5	bitr 173	. 2 ⊢ (i ∈ ℂ ↔ (0_R ∈ R ⋀ 1_R ∈ R))
7		0r 5176	. 2 ⊢ 0_R ∈ R
8	6, 7, 3	mpbir2an 729	1 ⊢ i ∈ ℂ

Colors of variables: wff set class

Syntax hints: ⋀ wa 223 ∈ wcel 957 ⟨cop 2409 Rcnr 4980 0_Rc0r 4981 1_Rc1r 4982 ℂcc 5219 ici 5223

This theorem is referenced by: 0cn 5315 cnegextlem2 5333 cnegext 5335 0cnALT 5337 ine0 5421 1re 5422 ixi 5668 recextlem1 5669 recextlem2 5670 recext 5671 irec 6682 i2 6683 i3 6684 i4 6685 crulem 6687 cru 6688 crutOLD 6690 crne0 6691 crmul 6692 crrecz 6693 rimul 6696 nthruc 6697 replimtOLD 6714 cjclt 6717 crret 6723 crretOLD 6724 crimt 6725 crimtOLD 6726 imret 6731 imretOLD 6732 reim0t 6733 reim0bt 6734 reim0btOLD 6735 cjcj 6736 rereb 6738 rerebOLD 6739 cjreb 6740 recj 6741 imcj 6742 readd 6743 imadd 6744 cjadd 6747 cjmul 6748 reneg 6753 renegOLD 6754 imneg 6756 imnegOLD 6757 cjneg 6758 addcj 6759 recjt 6779 imcjt 6780 rei 6785 imi 6786 cji 6788 cjreimt 6789 cjreim2t 6790 cj11t 6791 abs00 6803 abs00OLD 6804 absreimsqt 6818 absreimt 6819 absi 6842 recant 6870 recantOLD 6871 caucvg3a 7133 caucvg3aOLD 7134 caucvg3lem 7136 caucvg3lemOLD 7137 abspef01tlub 7372 sinclt 7409 cosclt 7410 resinvalt 7411 recosvalt 7412 efi4pt 7413 resin4pt 7414 recos4pt 7415 resinclt 7416 recosclt 7417 sinnegt 7420 cosnegt 7421 sin0 7422 cos0 7424 efivalt 7425 efmivalt 7426 efeult 7427 sinadd 7429 cosadd 7430 sin01bndlem2 7446 sin01bndlem3 7447 cos01bndlem2 7448 cos01bndlem3 7449 abseft 7461 demoivre 7462 demoivreALT 7463 nvpi 8279 ipval2 8343 4ipval2 8344 ipval3 8345 4ipval3 8348 ipid 8349 ipcl 8351 ipcj 8353 ip0r 8356 ip1cnilem1 8359 ip1cnilem2 8360 ip1cnilem3 8361 ip1cnilem4 8362 ip1cnilem5 8363 ip1cnilem6 8364 sspival 8383 ip1ilem 8469 ipasslem10 8483 ipasslem11 8484 sincolem 8648 sincnlem 8649 sinco 8650 sincn 8652 eulerid 8666 sinperlem1 8669 efimpi 8679 efif 8700 efif1lem4 8712 efielcircOLD 8719 efielcirc 8723 circgrp 8724 shftefif1olem 8725 eff1lem 8727 eff1i 8728 effoi 8729 efper 8731 pilog 8752 polid2 9008 polid 9009 lnopeq0lem1 9921 lnopeq0 9923 lnophmlem2 9933

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 961 ax-gen 962 ax-8 963 ax-9 964 ax-10 965 ax-11 966 ax-12 967 ax-13 968 ax-14 969 ax-17 970 ax-4 972 ax-5o 974 ax-6o 977 ax-9o 1122 ax-10o 1139 ax-16 1210 ax-11o 1218 ax-ext 1459 ax-rep 2690 ax-sep 2700 ax-nul 2707 ax-pow 2739 ax-pr 2776 ax-un 2863 ax-inf2 4612

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 775 df-3an 776 df-ex 980 df-sb 1172 df-eu 1382 df-mo 1383 df-clab 1464 df-cleq 1469 df-clel 1472 df-ne 1586 df-ral 1648 df-rex 1649 df-reu 1650 df-rab 1651 df-v 1810 df-sbc 1940 df-csb 2000 df-dif 2047 df-un 2048 df-in 2049 df-ss 2051 df-pss 2053 df-nul 2279 df-if 2360 df-pw 2400 df-sn 2410 df-pr 2411 df-tp 2413 df-op 2414 df-uni 2501 df-int 2531 df-iun 2565 df-br 2617 df-opab 2664 df-tr 2678 df-eprel 2829 df-id 2832 df-po 2837 df-so 2847 df-fr 2914 df-we 2931 df-ord 2948 df-on 2949 df-lim 2950 df-suc 2951 df-om 3129 df-xp 3181 df-rel 3182 df-cnv 3183 df-co 3184 df-dm 3185 df-rn 3186 df-res 3187 df-ima 3188 df-fun 3189 df-fn 3190 df-f 3191 df-fv 3195 df-rdg 3929 df-opr 3962 df-oprab 3963 df-1st 4076 df-2nd 4077 df-1o 4130 df-oadd 4132 df-omul 4133 df-er 4258 df-ec 4260 df-qs 4263 df-ni 4987 df-pli 4988 df-mi 4989 df-lti 4990 df-plpq 5022 df-mpq 5023 df-enq 5024 df-nq 5025 df-plq 5026 df-mq 5027 df-rq 5028 df-ltq 5029 df-1q 5030 df-np 5073 df-1p 5074 df-plp 5075 df-enr 5153 df-nr 5154 df-0r 5158 df-1r 5159 df-c 5227 df-i 5230