ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  qcn GIF version

Theorem qcn 9043
Description: A rational number is a complex number. (Contributed by NM, 2-Aug-2004.)
Assertion
Ref Expression
qcn (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)

Proof of Theorem qcn
StepHypRef Expression
1 qsscn 9040 . 2 ℚ ⊆ ℂ
21sseli 3010 1 (𝐴 ∈ ℚ → 𝐴 ∈ ℂ)
Colors of variables: wff set class
Syntax hints:  wi 4  wcel 1436  cc 7284  cq 9028
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-13 1447  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3930  ax-pow 3982  ax-pr 4008  ax-un 4232  ax-setind 4324  ax-cnex 7372  ax-resscn 7373  ax-1cn 7374  ax-1re 7375  ax-icn 7376  ax-addcl 7377  ax-addrcl 7378  ax-mulcl 7379  ax-mulrcl 7380  ax-addcom 7381  ax-mulcom 7382  ax-addass 7383  ax-mulass 7384  ax-distr 7385  ax-i2m1 7386  ax-0lt1 7387  ax-1rid 7388  ax-0id 7389  ax-rnegex 7390  ax-precex 7391  ax-cnre 7392  ax-pre-ltirr 7393  ax-pre-ltwlin 7394  ax-pre-lttrn 7395  ax-pre-apti 7396  ax-pre-ltadd 7397  ax-pre-mulgt0 7398  ax-pre-mulext 7399
This theorem depends on definitions:  df-bi 115  df-3or 923  df-3an 924  df-tru 1290  df-fal 1293  df-nf 1393  df-sb 1690  df-eu 1948  df-mo 1949  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-nel 2347  df-ral 2360  df-rex 2361  df-reu 2362  df-rmo 2363  df-rab 2364  df-v 2617  df-sbc 2830  df-csb 2923  df-dif 2990  df-un 2992  df-in 2994  df-ss 3001  df-pw 3416  df-sn 3436  df-pr 3437  df-op 3439  df-uni 3636  df-int 3671  df-iun 3714  df-br 3820  df-opab 3874  df-mpt 3875  df-id 4092  df-po 4095  df-iso 4096  df-xp 4415  df-rel 4416  df-cnv 4417  df-co 4418  df-dm 4419  df-rn 4420  df-res 4421  df-ima 4422  df-iota 4942  df-fun 4979  df-fn 4980  df-f 4981  df-fv 4985  df-riota 5562  df-ov 5609  df-oprab 5610  df-mpt2 5611  df-1st 5861  df-2nd 5862  df-pnf 7460  df-mnf 7461  df-xr 7462  df-ltxr 7463  df-le 7464  df-sub 7591  df-neg 7592  df-reap 7985  df-ap 7992  df-div 8071  df-inn 8350  df-z 8676  df-q 9029
This theorem is referenced by:  qsubcl  9047  qapne  9048  qdivcl  9052  qrevaddcl  9053  irradd  9055  irrmul  9056  qavgle  9590  divfl0  9623  flqzadd  9625  intqfrac2  9646  flqdiv  9648  modqvalr  9652  flqpmodeq  9654  modq0  9656  mulqmod0  9657  negqmod0  9658  modqlt  9660  modqdiffl  9662  modqfrac  9664  flqmod  9665  intqfrac  9666  modqmulnn  9669  modqvalp1  9670  modqid  9676  modqcyc  9686  modqcyc2  9687  modqadd1  9688  modqaddabs  9689  modqmuladdnn0  9695  qnegmod  9696  modqadd2mod  9701  modqm1p1mod0  9702  modqmul1  9704  modqnegd  9706  modqadd12d  9707  modqsub12d  9708  q2txmodxeq0  9711  q2submod  9712  modqmulmodr  9717  modqaddmulmod  9718  modqdi  9719  modqsubdir  9720  modqeqmodmin  9721  qsqcl  9916  bezoutlemnewy  10851  sqrt2irraplemnn  11023  ex-ceil  11083  qdencn  11344
  Copyright terms: Public domain W3C validator