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 7680 | . 2 ⊢ ℝ ⊆ ℂ | |
2 | 1 | sseli 3063 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1465 ℂcc 7586 ℝcr 7587 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-resscn 7680 |
This theorem depends on definitions: df-bi 116 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-clel 2113 df-in 3047 df-ss 3054 |
This theorem is referenced by: mulid1 7731 recnd 7762 pnfnre 7775 mnfnre 7776 cnegexlem1 7905 cnegexlem2 7906 cnegexlem3 7907 cnegex 7908 renegcl 7991 resubcl 7994 negf1o 8112 mul02lem2 8118 ltaddneg 8154 ltaddnegr 8155 ltaddsub2 8167 leaddsub2 8169 leltadd 8177 ltaddpos 8182 ltaddpos2 8183 posdif 8185 lenegcon1 8196 lenegcon2 8197 addge01 8202 addge02 8203 leaddle0 8207 mullt0 8210 recexre 8307 msqge0 8345 mulge0 8348 aprcl 8375 recexap 8381 ltm1 8568 prodgt02 8575 prodge02 8577 ltmul2 8578 lemul2 8579 lemul2a 8581 ltmulgt12 8587 lemulge12 8589 gt0div 8592 ge0div 8593 ltmuldiv2 8597 ltdivmul 8598 ltdivmul2 8600 ledivmul2 8602 lemuldiv2 8604 negiso 8677 cju 8683 nnge1 8707 halfpos 8909 lt2halves 8913 addltmul 8914 avgle1 8918 avgle2 8919 div4p1lem1div2 8931 nnrecl 8933 elznn0 9027 elznn 9028 nzadd 9064 zmulcl 9065 elz2 9080 gtndiv 9104 zeo 9114 supminfex 9348 eqreznegel 9362 negm 9363 irradd 9394 irrmul 9395 divlt1lt 9466 divle1le 9467 xnegneg 9571 rexsub 9591 xnegid 9597 xaddcom 9599 xaddid1 9600 xnegdi 9606 xaddass 9607 xleaddadd 9625 divelunit 9740 fzonmapblen 9919 expgt1 10286 mulexpzap 10288 leexp1a 10303 expubnd 10305 sqgt0ap 10316 lt2sq 10321 le2sq 10322 sqge0 10324 sumsqeq0 10326 bernneq 10367 bernneq2 10368 crre 10584 crim 10585 reim0 10588 mulreap 10591 rere 10592 remul2 10600 redivap 10601 immul2 10607 imdivap 10608 cjre 10609 cjreim 10630 rennim 10729 sqrt0rlem 10730 resqrexlemover 10737 absreimsq 10794 absreim 10795 absnid 10800 leabs 10801 absre 10804 absresq 10805 sqabs 10809 ltabs 10814 absdiflt 10819 absdifle 10820 lenegsq 10822 abssuble0 10830 dfabsmax 10944 max0addsup 10946 negfi 10954 minclpr 10963 reefcl 11288 efgt0 11304 reeftlcl 11309 resinval 11336 recosval 11337 resin4p 11339 recos4p 11340 resincl 11341 recoscl 11342 retanclap 11343 efieq 11356 sinbnd 11373 cosbnd 11374 absefi 11389 odd2np1 11482 infssuzex 11554 remetdval 12619 bl2ioo 12622 ioo2bl 12623 sincosq1sgn 12818 sincosq2sgn 12819 sincosq3sgn 12820 sincosq4sgn 12821 sinq12gt0 12822 triap 13120 |
Copyright terms: Public domain | W3C validator |