![]() |
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 7933 | . 2 ⊢ ℝ ⊆ ℂ | |
2 | 1 | sseli 3166 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 ℂcc 7839 ℝcr 7840 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 ax-resscn 7933 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-in 3150 df-ss 3157 |
This theorem is referenced by: mulrid 7984 recnd 8016 pnfnre 8029 mnfnre 8030 cnegexlem1 8162 cnegexlem2 8163 cnegexlem3 8164 cnegex 8165 renegcl 8248 resubcl 8251 negf1o 8369 mul02lem2 8375 ltaddneg 8411 ltaddnegr 8412 ltaddsub2 8424 leaddsub2 8426 leltadd 8434 ltaddpos 8439 ltaddpos2 8440 posdif 8442 lenegcon1 8453 lenegcon2 8454 addge01 8459 addge02 8460 leaddle0 8464 mullt0 8467 recexre 8565 msqge0 8603 mulge0 8606 aprcl 8633 recexap 8640 rerecapb 8830 ltm1 8833 prodgt02 8840 prodge02 8842 ltmul2 8843 lemul2 8844 lemul2a 8846 ltmulgt12 8852 lemulge12 8854 gt0div 8857 ge0div 8858 ltmuldiv2 8862 ltdivmul 8863 ltdivmul2 8865 ledivmul2 8867 lemuldiv2 8869 negiso 8942 cju 8948 nnge1 8972 halfpos 9180 lt2halves 9184 addltmul 9185 avgle1 9189 avgle2 9190 div4p1lem1div2 9202 nnrecl 9204 elznn0 9298 elznn 9299 nzadd 9335 zmulcl 9336 difgtsumgt 9352 elz2 9354 gtndiv 9378 zeo 9388 supminfex 9627 eqreznegel 9644 negm 9645 irradd 9676 irrmul 9677 divlt1lt 9754 divle1le 9755 xnegneg 9863 rexsub 9883 xnegid 9889 xaddcom 9891 xaddid1 9892 xnegdi 9898 xaddass 9899 xleaddadd 9917 divelunit 10032 fzonmapblen 10217 expgt1 10589 mulexpzap 10591 leexp1a 10606 expubnd 10608 sqgt0ap 10620 lt2sq 10625 le2sq 10626 sqge0 10628 sumsqeq0 10630 bernneq 10672 bernneq2 10673 nn0ltexp2 10721 crre 10898 crim 10899 reim0 10902 mulreap 10905 rere 10906 remul2 10914 redivap 10915 immul2 10921 imdivap 10922 cjre 10923 cjreim 10944 rennim 11043 sqrt0rlem 11044 resqrexlemover 11051 absreimsq 11108 absreim 11109 absnid 11114 leabs 11115 absre 11118 absresq 11119 sqabs 11123 ltabs 11128 absdiflt 11133 absdifle 11134 lenegsq 11136 abssuble0 11144 dfabsmax 11258 max0addsup 11260 negfi 11268 minclpr 11277 reefcl 11708 efgt0 11724 reeftlcl 11729 resinval 11755 recosval 11756 resin4p 11758 recos4p 11759 resincl 11760 recoscl 11761 retanclap 11762 efieq 11775 sinbnd 11792 cosbnd 11793 absefi 11808 odd2np1 11910 infssuzex 11982 remetdval 14496 bl2ioo 14499 ioo2bl 14500 sincosq1sgn 14704 sincosq2sgn 14705 sincosq3sgn 14706 sincosq4sgn 14707 sinq12gt0 14708 relogoprlem 14746 logcxp 14775 rpcxpcl 14781 cxpcom 14814 rprelogbdiv 14832 triap 15236 trirec0 15251 |
Copyright terms: Public domain | W3C validator |