Theorem recn 5294

Description: A real number is a complex number.

Hypothesis

Ref	Expression
recn.1	|- A e. RR

Assertion

Ref	Expression
recn	|- A e. CC

Proof of Theorem recn

Step	Hyp	Ref	Expression
1		axresscn 5248	. 2 |- RR (_ CC
2		recn.1	. 2 |- A e. RR
3	1, 2	sselii 2062	1 |- A e. CC

Syntax hints:   e. wcel 956  CCcc 5212  RRcr 5213

This theorem is referenced by:  renegcl 5396  ltadd1 5573  leadd2 5575  ltsubadd 5576  lesubadd 5577  addgt0 5580  addge0 5581  addgegt0 5582  add20 5584  ltneg 5585  leneg 5586  ltnegcon2 5587  mulge0 5589  lesub0 5594  msqgt0 5595  msqge0 5596  ltmullem 5622  redivcl 5762  eqneg 5768  recgt0i 5778  prodgt0lem 5782  prodgt0 5783  prodge0 5784  ltdiv1i 5787  ltmuldiv 5789  ltreci 5834  lerec 5836  lt2msq 5837  halfpos 5860  ledivp1 5862  ltdivp1 5863  nncn 5888  2cn 5935  3p2e5 5962  3p3e6 5963  4p2e6 5964  4p3e7 5965  4p4e8 5966  5p2e7 5967  5p3e8 5968  5p4e9 5969  5p5e10 5970  6p2e8 5971  6p3e9 5972  6p4e10 5973  7p2e9 5974  7p3e10 5975  8p2e10 5976  3t2e6 5978  3t3e9 5979  4t2e8 5980  5t2e10 5981  4d2e2 5982  8th4div3 5986  halfpm6th 5987  nn0cn 6066  nneo 6152  dfuz 6158  icoshftf1oi 6350  lt2sq 6563  le2sq 6564  sq11 6565  sqge0 6567  sq3 6578  discrlem1 6594  discrlem3 6596  nnesq 6600  nn0opth 6604  sqrlem1 6611  sqrlem2 6612  sqrlem10 6620  sqrlem11 6621  sqrlem15 6625  sqrlem16 6626  sqrlem19 6629  sqrlem20 6630  sqrmuli 6642  sqrsq 6658  sqr2irrlem1 6662  sqr2irrlem4 6665  crulem 6674  cru 6675  crrecz 6680  cjcj 6721  rereb 6723  cjreb 6724  recj 6725  imcj 6726  readd 6727  imadd 6728  remul 6729  immul 6730  cjadd 6731  cjmul 6732  ipcn 6733  cjmulval 6735  reneg 6737  negreb 6738  imneg 6739  cjneg 6740  addcj 6741  reret 6742  abs00 6785  absdivz 6802  absid 6804  leabs 6815  abslt 6818  absle 6819  absltOLD 6820  absleOLD 6821  recvalz 6833  cjdiv 6834  abstri 6837  abs3lem 6846  abs1m 6849  abslem2i 6853  fac3 6883  faclbnd4lem1 6893  climshft 7049  climshft2 7051  iserzshft2 7052  climsup 7099  caucvg 7107  cvgcmp2lem 7124  cvgcmp2clem 7126  infcvglem1 7164  infcvglem2 7165  fnsmnt 7169  expcnvlem2 7171  0.999... 7189  cvgratlem1ALT 7190  cvgratlem2ALT 7191  ivthlem1 7224  ivthlem6 7229  ivthlem7 7230  dsupivthlem 7234  ivthlem6OLD 7238  ivthlem7OLD 7239  efcltlem1 7254  reefcl 7267  erelem2 7270  efaddlem8 7295  efaddlem12 7299  efaddlem16 7303  efaddlem20 7307  efaddlem22 7309  ef01tllem1 7333  ef01tllem2 7334  absef01tllem 7336  eirrlem1 7338  eirrlem3 7340  eirrlem5 7342  effsumle 7346  efge1 7350  efge1p 7351  efgt0 7353  eflt 7355  absefm1le 7360  eflegeolem2 7362  efm1legeo 7365  efcnlem1 7367  reeff1olem1 7372  reeff1olem1OLD 7374  efi4pt 7385  sin01bndlem1 7417  sin01bndlem2 7418  sin01bndlem3 7419  cos01bndlem2 7420  cos01bndlem3 7421  cos2bnd 7425  cos01gt0 7427  sin4lt0 7431  ruclem1 7461  ruclem2 7462  ruclem3 7463  ipval2 8304  4ipval2 8305  4ipval3 8309  ipid 8310  ipcl 8312  ipcj 8314  ip0r 8317  ip1cnilem4 8323  ip1cnilem5 8324  ip1cnilem6 8325  nmblolbii 8403  ip0i 8428  ip1ilem 8429  ipasslem10 8443  siilem1 8455  siii 8457  minveclem26 8514  minveclem27 8515  minveclem30 8518  minveclem36 8524  minveclem38 8526  pilem1 8609  pilem3 8611  sinhalfpilem 8617  cospi 8620  eulerid 8621  sin2pi 8622  cos2pi 8623  sinperlem1 8624  sinperlem2 8625  sinper 8628  cosper 8629  sin2pim 8630  cos2pim 8631  sinmpi 8632  cosmpi 8633  efimpi 8634  sinhalfpip 8635  sinhalfpim 8636  coshalfpip 8637  coshalfpim 8638  sincosq1sgn 8640  sincosq2sgn 8641  sincosq3sgn 8642  sincosq4sgn 8643  sinq12gt0t 8644  sincosq1eq 8645  sincos4thpi 8646  sincos6thpi 8647  cosh111lem1 8648  efifolem2 8657  efifolem3 8658  efifolem4 8659  efifolem6 8661  efif1lem1 8664  efif1lem2 8665  efif1lem4 8667  efif1lem5 8668  shftefif1olem 8680  efper 8686  eff1o 8687  pilog 8707  normlem1 8915  normlem3 8917  normlem5 8919  normlem6 8920  norm-ii 8943  normsub 8947  norm3adif 8954  norm3lem 8955  normpar2 8962  polid2 8963  bcsALT 8985  projlem3 9127  projlem4 9128  projlem5 9129  projlem7 9131  projlem12 9136  projlem13 9137  projlem18 9142  projlem26 9150  pjthlem5 9161  pjthlem8 9164  pjthlem11 9167  pjnel 9608  lnopeq0 9870  lnophmlem2 9880  nmbdoplb 9887  nmcoplb 9896  nmophm 9899  nmbdfnlb 9916  nmcfnlb 9925  cnlnadjlem2 9939  cnlnadjlem7 9944  nmopadjlem 9960  nmopco 9966  nmopcoadj 9972  nmopcoadj0 9974  unierr 9975

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-inf2 4605

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-csb 1998  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-int 2529  df-iun 2563  df-br 2615  df-opab 2662  df-tr 2676  df-eprel 2827  df-id 2830  df-po 2835  df-so 2845  df-fr 2912  df-we 2929  df-ord 2946  df-on 2947  df-lim 2948  df-suc 2949  df-om 3127  df-xp 3179  df-rel 3180  df-cnv 3181  df-co 3182  df-dm 3183  df-rn 3184  df-res 3185  df-ima 3186  df-fun 3187  df-fn 3188  df-f 3189  df-fv 3193  df-rdg 3923  df-opr 3956  df-oprab 3957  df-1st 4069  df-2nd 4070  df-1o 4123  df-oadd 4125  df-omul 4126  df-er 4251  df-ec 4253  df-qs 4256  df-ni 4980  df-pli 4981  df-mi 4982  df-lti 4983  df-plpq 5015  df-mpq 5016  df-enq 5017  df-nq 5018  df-plq 5019  df-mq 5020  df-rq 5021  df-ltq 5022  df-1q 5023  df-np 5066  df-1p 5067  df-enr 5146  df-nr 5147  df-0r 5151  df-c 5220  df-r 5224

Copyright terms: Public domain