![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > recn | GIF version |
Description: A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
Ref | Expression |
---|---|
recn | ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ax-resscn 7534 | . 2 ⊢ ℝ ⊆ ℂ | |
2 | 1 | sseli 3035 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1445 ℂcc 7445 ℝcr 7446 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-11 1449 ax-4 1452 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-resscn 7534 |
This theorem depends on definitions: df-bi 116 df-nf 1402 df-sb 1700 df-clab 2082 df-cleq 2088 df-clel 2091 df-in 3019 df-ss 3026 |
This theorem is referenced by: mulid1 7582 recnd 7613 pnfnre 7626 mnfnre 7627 cnegexlem1 7754 cnegexlem2 7755 cnegexlem3 7756 cnegex 7757 renegcl 7840 resubcl 7843 negf1o 7957 mul02lem2 7963 ltaddneg 7999 ltaddnegr 8000 ltaddsub2 8012 leaddsub2 8014 leltadd 8022 ltaddpos 8027 ltaddpos2 8028 posdif 8030 lenegcon1 8041 lenegcon2 8042 addge01 8047 addge02 8048 leaddle0 8052 mullt0 8055 recexre 8152 msqge0 8190 mulge0 8193 recexap 8219 ltm1 8404 prodgt02 8411 prodge02 8413 ltmul2 8414 lemul2 8415 lemul2a 8417 ltmulgt12 8423 lemulge12 8425 gt0div 8428 ge0div 8429 ltmuldiv2 8433 ltdivmul 8434 ltdivmul2 8436 ledivmul2 8438 lemuldiv2 8440 negiso 8513 cju 8519 nnge1 8543 halfpos 8745 lt2halves 8749 addltmul 8750 avgle1 8754 avgle2 8755 div4p1lem1div2 8767 nnrecl 8769 elznn0 8863 elznn 8864 nzadd 8900 zmulcl 8901 elz2 8916 gtndiv 8940 zeo 8950 supminfex 9184 eqreznegel 9198 negm 9199 irradd 9230 irrmul 9231 divlt1lt 9300 divle1le 9301 xnegneg 9399 rexsub 9419 xnegid 9425 xaddcom 9427 xaddid1 9428 xnegdi 9434 xaddass 9435 xleaddadd 9453 divelunit 9568 fzonmapblen 9747 expgt1 10124 mulexpzap 10126 leexp1a 10141 expubnd 10143 sqgt0ap 10154 lt2sq 10159 le2sq 10160 sqge0 10162 sumsqeq0 10164 bernneq 10205 bernneq2 10206 crre 10422 crim 10423 reim0 10426 mulreap 10429 rere 10430 remul2 10438 redivap 10439 immul2 10445 imdivap 10446 cjre 10447 cjreim 10468 rennim 10566 sqrt0rlem 10567 resqrexlemover 10574 absreimsq 10631 absreim 10632 absnid 10637 leabs 10638 absre 10641 absresq 10642 sqabs 10646 ltabs 10651 absdiflt 10656 absdifle 10657 lenegsq 10659 abssuble0 10667 dfabsmax 10781 max0addsup 10783 negfi 10790 minclpr 10799 reefcl 11123 efgt0 11139 reeftlcl 11144 resinval 11171 recosval 11172 resin4p 11174 recos4p 11175 resincl 11176 recoscl 11177 retanclap 11178 efieq 11191 sinbnd 11208 cosbnd 11209 absefi 11223 odd2np1 11316 infssuzex 11388 remetdval 12329 bl2ioo 12332 ioo2bl 12333 |
Copyright terms: Public domain | W3C validator |