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 6976 | . 2 ⊢ ℝ ⊆ ℂ | |
2 | 1 | sseli 2941 | 1 ⊢ (𝐴 ∈ ℝ → 𝐴 ∈ ℂ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1393 ℂcc 6887 ℝcr 6888 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-5 1336 ax-7 1337 ax-gen 1338 ax-ie1 1382 ax-ie2 1383 ax-8 1395 ax-11 1397 ax-4 1400 ax-17 1419 ax-i9 1423 ax-ial 1427 ax-i5r 1428 ax-ext 2022 ax-resscn 6976 |
This theorem depends on definitions: df-bi 110 df-nf 1350 df-sb 1646 df-clab 2027 df-cleq 2033 df-clel 2036 df-in 2924 df-ss 2931 |
This theorem is referenced by: mulid1 7024 recnd 7054 pnfnre 7067 mnfnre 7068 cnegexlem1 7186 cnegexlem2 7187 cnegexlem3 7188 cnegex 7189 renegcl 7272 resubcl 7275 mul02lem2 7385 ltaddsub2 7432 leaddsub2 7434 leltadd 7442 ltaddpos 7447 ltaddpos2 7448 posdif 7450 lenegcon1 7461 lenegcon2 7462 addge01 7467 addge02 7468 leaddle0 7472 mullt0 7475 recexre 7569 msqge0 7607 mulge0 7610 recexap 7634 ltm1 7812 prodgt02 7819 prodge02 7821 ltmul2 7822 lemul2 7823 lemul2a 7825 ltmulgt12 7831 lemulge12 7833 gt0div 7836 ge0div 7837 ltmuldiv2 7841 ltdivmul 7842 ltdivmul2 7844 ledivmul2 7846 lemuldiv2 7848 cju 7913 nnge1 7937 halfpos 8156 lt2halves 8160 addltmul 8161 avgle1 8165 avgle2 8166 div4p1lem1div2 8177 nnrecl 8179 elznn0 8260 elznn 8261 zmulcl 8297 elz2 8312 gtndiv 8335 zeo 8343 eqreznegel 8549 negm 8550 irradd 8580 irrmul 8581 divlt1lt 8650 divle1le 8651 xnegneg 8746 divelunit 8870 fzonmapblen 9043 expgt1 9293 mulexpzap 9295 leexp1a 9309 expubnd 9311 sqgt0ap 9322 lt2sq 9327 le2sq 9328 sqge0 9330 sumsqeq0 9332 bernneq 9369 bernneq2 9370 crre 9457 crim 9458 reim0 9461 mulreap 9464 rere 9465 remul2 9473 redivap 9474 immul2 9480 imdivap 9481 cjre 9482 cjreim 9503 rennim 9600 sqrt0rlem 9601 resqrexlemover 9608 absreimsq 9665 absreim 9666 absnid 9671 leabs 9672 absre 9673 absresq 9674 sqabs 9678 ltabs 9683 absdiflt 9688 absdifle 9689 lenegsq 9691 abssuble0 9699 |
Copyright terms: Public domain | W3C validator |