Theorem axicn 5290

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 5263	. . . 4 ⊢ i = ⟨0R, 1R⟩
2	1	eleq1i 1544	. . 3 ⊢ (i ∈ ℂ ↔ ⟨0R, 1R⟩ ∈ ℂ)
3		1r 5210	. . . . 5 ⊢ 1R ∈ R
4	3	elisseti 1825	. . . 4 ⊢ 1R ∈ V
5	4	opelcn 5268	. . 3 ⊢ (⟨0R, 1R⟩ ∈ ℂ ↔ (0R ∈ R ⋀ 1R ∈ R))
6	2, 5	bitri 173	. 2 ⊢ (i ∈ ℂ ↔ (0R ∈ R ⋀ 1R ∈ R))
7		0r 5209	. 2 ⊢ 0R ∈ R
8	6, 7, 3	mpbir2an 734	1 ⊢ i ∈ ℂ

Syntax hints:   ⋀ wa 223   ∈ wcel 962  ⟨cop 2423  Rcnr 5013  0_Rc0r 5014  1_Rc1r 5015  ℂcc 5252  ici 5256

This theorem is referenced by:  0cn 5348  cnegexlem2 5366  cnegex 5368  0cnALT 5370  ine0 5454  1re 5455  ixi 5701  recextlem1 5702  recextlem2 5703  recex 5704  irec 6763  i2 6764  i3 6765  i4 6766  crulem 6768  crui 6769  crne0i 6771  crmuli 6772  crreczi 6773  rimul 6776  nthruc 6777  cjcl 6796  crre 6801  crim 6802  imre 6805  reim0 6806  reim0b 6807  rereb 6808  mulre 6809  cjcji 6810  cjrebi 6813  recji 6814  imcji 6815  readdi 6816  imaddi 6817  cjaddi 6820  cjmuli 6821  renegi 6826  imnegi 6828  cjnegi 6829  addcji 6830  recj 6850  imcj 6851  rei 6856  imi 6857  cji 6859  cjreim 6860  cjreim2 6861  cj11 6862  abs00i 6874  absreimsq 6888  absreim 6889  absi 6910  recan 6937  caucvg3ai 7196  caucvg3lem 7198  abspef01tlubi 7427  sincl 7463  coscl 7464  resinval 7465  recosval 7466  efi4p 7467  resin4p 7468  recos4p 7469  resincl 7470  recoscl 7471  sinneg 7474  cosneg 7475  sin0 7476  cos0 7478  efival 7479  efmival 7480  efeul 7481  sinaddi 7483  cosaddi 7484  sin01bndlem2 7501  sin01bndlem3 7502  cos01bndlem2 7503  cos01bndlem3 7504  absef 7516  demoivre 7517  demoivreALT 7518  nvpi 8319  ipval2 8382  4ipval2 8383  ipval3 8384  4ipval3 8387  ipid 8388  ipcl 8390  ipcj 8392  ip0r 8395  ip1cnilem1 8398  ip1cnilem2 8399  ip1cnilem3 8400  ip1cnilem4 8401  ip1cnilem5 8402  ip1cnilem6 8403  sspival 8422  ip1ilem 8510  ipasslem10 8524  ipasslem11 8525  sincolem 8689  sincnlem 8690  sinco 8691  sincn 8693  eulerid 8707  sinperlem1 8710  efimpi 8722  efif 8745  efif1lem4 8757  efielcirc 8763  circgrp 8764  shftefif1olem 8765  eff1lem 8767  eff1i 8768  effoi 8769  efper 8771  pilog 8792  polid2i 9048  polidi 9049  lnopeq0lem1 9954  lnopeq0i 9956  lnophmlem2 9966

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 966  ax-gen 967  ax-8 968  ax-9 969  ax-10 970  ax-11 971  ax-12 972  ax-13 973  ax-14 974  ax-17 975  ax-4 977  ax-5o 979  ax-6o 982  ax-9o 1127  ax-10o 1144  ax-16 1214  ax-11o 1222  ax-ext 1464  ax-rep 2708  ax-sep 2718  ax-nul 2725  ax-pow 2758  ax-pr 2795  ax-un 2882  ax-inf2 4642

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 780  df-3an 781  df-ex 985  df-sb 1176  df-eu 1386  df-mo 1387  df-clab 1470  df-cleq 1475  df-clel 1478  df-ne 1594  df-ral 1656  df-rex 1657  df-reu 1658  df-rab 1659  df-v 1819  df-sbc 1949  df-csb 2012  df-dif 2060  df-un 2061  df-in 2062  df-ss 2064  df-pss 2066  df-nul 2292  df-if 2374  df-pw 2414  df-sn 2424  df-pr 2425  df-tp 2427  df-op 2428  df-uni 2518  df-int 2548  df-iun 2582  df-br 2635  df-opab 2682  df-tr 2696  df-eprel 2848  df-id 2851  df-po 2856  df-so 2866  df-fr 2933  df-we 2950  df-ord 2967  df-on 2968  df-lim 2969  df-suc 2970  df-om 3148  df-xp 3200  df-rel 3201  df-cnv 3202  df-co 3203  df-dm 3204  df-rn 3205  df-res 3206  df-ima 3207  df-fun 3208  df-fn 3209  df-f 3210  df-fv 3214  df-rdg 3948  df-opr 3981  df-oprab 3982  df-1st 4095  df-2nd 4096  df-1o 4149  df-oadd 4151  df-omul 4152  df-er 4277  df-ec 4279  df-qs 4282  df-ni 5020  df-pli 5021  df-mi 5022  df-lti 5023  df-plpq 5055  df-mpq 5056  df-enq 5057  df-nq 5058  df-plq 5059  df-mq 5060  df-rq 5061  df-ltq 5062  df-1q 5063  df-np 5106  df-1p 5107  df-plp 5108  df-enr 5186  df-nr 5187  df-0r 5191  df-1r 5192  df-c 5260  df-i 5263

Copyright terms: Public domain