Theorem recnt 5325

Description: A real number is a complex number.

Assertion

Ref	Expression
recnt	⊢ (A ∈ ℝ → A ∈ ℂ)

Proof of Theorem recnt

Step	Hyp	Ref	Expression
1		axresscn 5280	. 2 ⊢ ℝ ⊆ ℂ
2	1	sseli 2068	1 ⊢ (A ∈ ℝ → A ∈ ℂ)

Syntax hints:   → wi 3   ∈ wcel 960  ℂcc 5244  ℝcr 5245

This theorem is referenced by:  recnd 5327  cnegextlem1 5357  cnegextlem2 5358  cnegextlem3 5359  cnegext 5360  renegcl 5428  resubclt 5450  pnfnre 5508  mnfnre 5509  ltadd2t 5636  leadd2t 5638  ltsubadd2t 5640  lesubadd2t 5642  ltaddsub2t 5644  leaddsub2t 5646  leltaddt 5658  addgtge0t 5661  ltaddpost 5663  ltaddpos2t 5664  posdift 5666  ltnegcon1t 5668  lenegcon1t 5670  lenegcon2t 5671  lesub1t 5672  lesub2t 5673  ltsub1t 5674  ltsub2t 5675  addge01t 5684  addge02t 5685  subge0t 5686  suble0t 5687  recext 5696  redivcl 5800  ltm1t 5817  prodgt02t 5829  prodge02t 5831  ltmul2t 5833  lemul1t 5834  lemul2t 5835  lemul1it 5839  lemul1itOLD 5840  lemul2it 5841  lemul2itOLD 5842  mulgt1t 5847  ltmulgt11t 5848  ltmulgt12t 5849  lemulge11t 5850  gt0divt 5855  ge0divt 5856  ltmuldiv2t 5867  ltmuldiv2tOLD 5868  ltdivmult 5869  ltdivmultOLD 5870  ledivmultOLD 5871  ltdivmul2t 5872  ltdivmul2tOLD 5873  lt2mul2divt 5874  ledivmul2tOLD 5875  lemuldiv2t 5878  lemuldiv2tOLD 5879  ltdiv2t 5889  ltrec1t 5890  lerec2t 5891  ledivdivt 5892  lediv2t 5893  ltdiv23t 5894  lediv23t 5895  lediv12it 5898  recp1lt1 5903  ledivp1t 5907  nnge1t 5945  nnleltp1t 5956  lt2halvest 6044  avglet 6046  infm3lem 6055  reuunineg 6068  infmrcl 6071  nnreclt 6074  elznn0 6151  elznn 6152  zaddclt 6167  elnn0nn 6173  zmulclt 6182  zltp1let 6183  gtndivt 6195  zeot 6201  dfuz 6204  uzindOLD 6210  rebtwnz 6224  intfrac 6254  zqt 6261  qbtwnre 6279  icoshftf1oi 6410  expgt0t 6590  expge0t 6592  expgt1t 6593  expge1t 6594  expordit 6601  expord2t 6605  expmwordit 6607  expubndt 6609  sqgt0t 6623  lt2sqt 6631  le2sqt 6632  sqlecant 6642  bernneq 6653  bernneq2 6654  expnbndt 6655  discrlem3 6659  rimul 6745  crret 6770  crimt 6771  reim0t 6775  reret 6799  cjret 6810  cjreimt 6828  cjreim2t 6829  absreimsqt 6856  absreimt 6857  absdivz 6859  absnidt 6863  leabst 6864  absret 6866  absresqt 6867  abssubne0t 6882  absdifltt 6883  absdiflet 6884  lenegsqt 6885  releabst 6886  abssuble0t 6896  absmaxt 6897  seq1ublem 6911  2climnn 7102  2climnn0 7103  climrecl 7110  climge0 7112  climaddlem3 7116  climmullem5 7124  climcmplem 7137  climcmpc1 7139  climsqueeze 7140  climsqueeze2 7141  climubi 7153  climsup 7155  climcau 7156  caucvg 7163  ser1f0 7170  iserzgt0 7211  cvgratlem1 7250  cvgratlem2 7251  cvgratlem5 7254  ivthlem1 7281  eftabs 7375  reeftlclt 7380  reeff1 7410  absefm1le 7412  reeff1o 7426  resinvalt 7433  recosvalt 7434  efi4pt 7435  resin4pt 7436  recos4pt 7437  resinclt 7438  recosclt 7439  efieq 7450  sinbndt 7466  cosbndt 7467  cos01bndlem3 7472  absefit 7483  abseft 7484  znnen 7503  bl2in 7840  remetdval 7905  bl2ioo 7908  ioo2bl 7909  tgioolem 7911  lmuni 7948  lmle 7957  lmcau 7993  readdsubg 8125  nvsge0 8287  nmoub3i 8432  nmlnoubi 8452  isblo3i 8457  blocnilem 8460  ipasslem3 8488  ipasslem9 8494  ipasslem11 8496  ubthlem9 8533  minveclem24 8564  minveclem26 8566  pilem1 8666  pilem3 8668  sincosq1sgn 8699  sincosq2sgn 8700  sincosq3sgn 8701  sincosq4sgn 8702  sinq12gt0t 8703  sineq0 8708  efif 8716  efifolem5 8721  efifolem6 8722  efifolem7 8723  efif1lem3 8727  efielcirc 8734  shftefif1olem 8736  resslogrn 8748  relogoprlem 8764  projlem24 9204  pjthlem7 9220  nmopub2tALT 9828  nmfnleub2t 9845  hmopmt 9941  lnopcon 9958  lnfncon 9985  riesz1t 9993  leopmulit 10061  leopmult 10062  leopmul2it 10063  leopnmidt 10066  nmopleidt 10067  cdj1 10355  cdj3lem1 10356  cdj3 10363  lediv2itALT 10366  nndivlub 10417  truni1 10485  dmse1 10594  mslb1 10600  2wsms 10601  msra3 10602  iintlem1 10603  trran 10607  trnij 10608  cnvtr 10609

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-nul 2715  ax-pow 2748  ax-pr 2785  ax-un 2872  ax-inf2 4634

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 778  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-reu 1654  df-rab 1655  df-v 1815  df-sbc 1945  df-csb 2005  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-pss 2058  df-nul 2284  df-if 2366  df-pw 2406  df-sn 2416  df-pr 2417  df-tp 2419  df-op 2420  df-uni 2508  df-int 2538  df-iun 2572  df-br 2625  df-opab 2672  df-tr 2686  df-eprel 2838  df-id 2841  df-po 2846  df-so 2856  df-fr 2923  df-we 2940  df-ord 2957  df-on 2958  df-lim 2959  df-suc 2960  df-om 3138  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-f 3200  df-fv 3204  df-rdg 3938  df-opr 3971  df-oprab 3972  df-1st 4085  df-2nd 4086  df-1o 4139  df-oadd 4141  df-omul 4142  df-er 4267  df-ec 4269  df-qs 4272  df-ni 5012  df-pli 5013  df-mi 5014  df-lti 5015  df-plpq 5047  df-mpq 5048  df-enq 5049  df-nq 5050  df-plq 5051  df-mq 5052  df-rq 5053  df-ltq 5054  df-1q 5055  df-np 5098  df-1p 5099  df-enr 5178  df-nr 5179  df-0r 5183  df-c 5252  df-r 5256

Copyright terms: Public domain