![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > qcn | GIF version |
Description: A rational number is a complex number. (Contributed by NM, 2-Aug-2004.) |
Ref | Expression |
---|---|
qcn | ⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | qsscn 8867 | . 2 ⊢ ℚ ⊆ ℂ | |
2 | 1 | sseli 3004 | 1 ⊢ (𝐴 ∈ ℚ → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1434 ℂcc 7111 ℚcq 8855 |
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 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2065 ax-sep 3916 ax-pow 3968 ax-pr 3992 ax-un 4216 ax-setind 4308 ax-cnex 7199 ax-resscn 7200 ax-1cn 7201 ax-1re 7202 ax-icn 7203 ax-addcl 7204 ax-addrcl 7205 ax-mulcl 7206 ax-mulrcl 7207 ax-addcom 7208 ax-mulcom 7209 ax-addass 7210 ax-mulass 7211 ax-distr 7212 ax-i2m1 7213 ax-0lt1 7214 ax-1rid 7215 ax-0id 7216 ax-rnegex 7217 ax-precex 7218 ax-cnre 7219 ax-pre-ltirr 7220 ax-pre-ltwlin 7221 ax-pre-lttrn 7222 ax-pre-apti 7223 ax-pre-ltadd 7224 ax-pre-mulgt0 7225 ax-pre-mulext 7226 |
This theorem depends on definitions: df-bi 115 df-3or 921 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1688 df-eu 1946 df-mo 1947 df-clab 2070 df-cleq 2076 df-clel 2079 df-nfc 2212 df-ne 2250 df-nel 2345 df-ral 2358 df-rex 2359 df-reu 2360 df-rmo 2361 df-rab 2362 df-v 2612 df-sbc 2825 df-csb 2918 df-dif 2984 df-un 2986 df-in 2988 df-ss 2995 df-pw 3402 df-sn 3422 df-pr 3423 df-op 3425 df-uni 3622 df-int 3657 df-iun 3700 df-br 3806 df-opab 3860 df-mpt 3861 df-id 4076 df-po 4079 df-iso 4080 df-xp 4397 df-rel 4398 df-cnv 4399 df-co 4400 df-dm 4401 df-rn 4402 df-res 4403 df-ima 4404 df-iota 4917 df-fun 4954 df-fn 4955 df-f 4956 df-fv 4960 df-riota 5520 df-ov 5567 df-oprab 5568 df-mpt2 5569 df-1st 5819 df-2nd 5820 df-pnf 7287 df-mnf 7288 df-xr 7289 df-ltxr 7290 df-le 7291 df-sub 7418 df-neg 7419 df-reap 7812 df-ap 7819 df-div 7898 df-inn 8177 df-z 8503 df-q 8856 |
This theorem is referenced by: qsubcl 8874 qapne 8875 qdivcl 8879 qrevaddcl 8880 irradd 8882 irrmul 8883 qavgle 9415 divfl0 9448 flqzadd 9450 intqfrac2 9471 flqdiv 9473 modqvalr 9477 flqpmodeq 9479 modq0 9481 mulqmod0 9482 negqmod0 9483 modqlt 9485 modqdiffl 9487 modqfrac 9489 flqmod 9490 intqfrac 9491 modqmulnn 9494 modqvalp1 9495 modqid 9501 modqcyc 9511 modqcyc2 9512 modqadd1 9513 modqaddabs 9514 modqmuladdnn0 9520 qnegmod 9521 modqadd2mod 9526 modqm1p1mod0 9527 modqmul1 9529 modqnegd 9531 modqadd12d 9532 modqsub12d 9533 q2txmodxeq0 9536 q2submod 9537 modqmulmodr 9542 modqaddmulmod 9543 modqdi 9544 modqsubdir 9545 modqeqmodmin 9546 qsqcl 9714 bezoutlemnewy 10610 sqrt2irraplemnn 10782 ex-ceil 10842 qdencn 11070 |
Copyright terms: Public domain | W3C validator |