![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > recnd | Unicode version |
Description: Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
Ref | Expression |
---|---|
recnd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
recnd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | recnd.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | recn 6812 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
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 1333 ax-7 1334 ax-gen 1335 ax-ie1 1379 ax-ie2 1380 ax-8 1392 ax-11 1394 ax-4 1397 ax-17 1416 ax-i9 1420 ax-ial 1424 ax-i5r 1425 ax-ext 2019 ax-resscn 6775 |
This theorem depends on definitions: df-bi 110 df-nf 1347 df-sb 1643 df-clab 2024 df-cleq 2030 df-clel 2033 df-in 2918 df-ss 2925 |
This theorem is referenced by: readdcan 6950 ltadd2 7212 ltadd1 7219 leadd2 7221 ltsubadd 7222 ltsubadd2 7223 lesubadd 7224 lesubadd2 7225 ltaddsub 7226 leaddsub 7228 lesub1 7246 lesub2 7247 ltsub1 7248 ltsub2 7249 ltnegcon1 7253 ltnegcon2 7254 add20 7264 subge0 7265 suble0 7266 lesub0 7269 rimul 7369 rereim 7370 apreap 7371 ltmul1a 7375 ltmul1 7376 reapmul1 7379 remulext2 7384 cru 7386 apreim 7387 mulreim 7388 apadd1 7392 apneg 7395 mulext1 7396 rerecclap 7488 redivclap 7489 recgt0 7597 prodgt0gt0 7598 prodgt0 7599 prodge0 7601 lemul1a 7605 ltdiv1 7615 ltmuldiv 7621 ledivmul 7624 lt2mul2div 7626 ltrec 7630 lt2msq 7633 ltdiv2 7634 ltrec1 7635 lerec2 7636 ledivdiv 7637 lediv2 7638 ltdiv23 7639 lediv23 7640 lediv12a 7641 recp1lt1 7646 recreclt 7647 ledivp1 7650 avglt1 7940 avglt2 7941 nn0cnd 8013 zcn 8026 peano2z 8057 zaddcllemneg 8060 ztri3or 8064 zeo 8119 zcnd 8137 eluzelcn 8260 cnref1o 8357 rpcn 8366 rpcnd 8399 ltaddrp2d 8427 icoshftf1o 8629 lincmb01cmp 8641 iccf1o 8642 expcl2lemap 8921 expnegzap 8943 expaddzaplem 8952 expaddzap 8953 expmulzap 8955 ltexp2a 8960 leexp2a 8961 leexp2r 8962 exple1 8964 expubnd 8965 sq11 8979 bernneq2 9023 expnbnd 9025 remim 9088 reim0b 9090 rereb 9091 mulreap 9092 cjreb 9094 recj 9095 reneg 9096 readd 9097 resub 9098 remullem 9099 remul2 9101 redivap 9102 imcj 9103 imneg 9104 imadd 9105 imsub 9106 immul2 9108 imdivap 9109 cjcj 9111 cjadd 9112 ipcnval 9114 cjmulval 9116 cjneg 9118 imval2 9122 cjreim2 9132 cjap 9134 cnrecnv 9138 sqrtmsq 9215 absid 9225 |
Copyright terms: Public domain | W3C validator |