![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nncnd | Unicode version |
Description: A positive integer is a complex number. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnred.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nncnd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnsscn 8629 |
. 2
![]() ![]() ![]() ![]() | |
2 | nnred.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sseldi 3059 |
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 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1404 ax-7 1405 ax-gen 1406 ax-ie1 1450 ax-ie2 1451 ax-8 1463 ax-10 1464 ax-11 1465 ax-i12 1466 ax-bndl 1467 ax-4 1468 ax-17 1487 ax-i9 1491 ax-ial 1495 ax-i5r 1496 ax-ext 2095 ax-sep 4004 ax-cnex 7630 ax-resscn 7631 ax-1re 7633 ax-addrcl 7636 |
This theorem depends on definitions: df-bi 116 df-tru 1315 df-nf 1418 df-sb 1717 df-clab 2100 df-cleq 2106 df-clel 2109 df-nfc 2242 df-ral 2393 df-v 2657 df-in 3041 df-ss 3048 df-int 3736 df-inn 8625 |
This theorem is referenced by: peano5uzti 9057 qapne 9327 qtri3or 9907 exbtwnzlemstep 9912 intfracq 9980 flqdiv 9981 modqmulnn 10002 addmodid 10032 modaddmodup 10047 modsumfzodifsn 10056 addmodlteq 10058 facdiv 10371 facndiv 10372 faclbnd 10374 faclbnd6 10377 facubnd 10378 facavg 10379 bccmpl 10387 bcn0 10388 bcn1 10391 bcm1k 10393 bcp1n 10394 bcp1nk 10395 bcval5 10396 bcpasc 10399 permnn 10404 cvg1nlemcxze 10640 cvg1nlemcau 10642 resqrexlemcalc3 10674 binom11 11141 binom1dif 11142 divcnv 11152 arisum2 11154 trireciplem 11155 trirecip 11156 expcnvap0 11157 geo2sum 11169 geo2lim 11171 cvgratnnlembern 11178 cvgratnnlemnexp 11179 cvgratnnlemmn 11180 cvgratnnlemsumlt 11183 cvgratnnlemfm 11184 cvgratnnlemrate 11185 cvgratz 11187 eftcl 11205 eftabs 11207 efcllemp 11209 ege2le3 11222 efcj 11224 efaddlem 11225 eftlub 11241 eirraplem 11325 oexpneg 11416 divalglemnn 11457 bezoutlemnewy 11524 mulgcd 11544 rplpwr 11555 sqgcd 11557 lcmgcdlem 11598 3lcm2e6woprm 11607 cncongr1 11624 cncongr2 11625 prmind2 11641 divgcdodd 11661 prmdvdsexpr 11668 sqrt2irrlem 11679 oddpwdclemxy 11686 oddpwdclemodd 11689 oddpwdclemdc 11690 oddpwdc 11691 sqpweven 11692 2sqpwodd 11693 sqrt2irraplemnn 11696 sqrt2irrap 11697 qmuldeneqnum 11712 divnumden 11713 qnumgt0 11715 numdensq 11719 hashdvds 11736 phiprmpw 11737 oddennn 11744 evenennn 11745 trilpolemeq1 12914 trilpolemlt1 12915 |
Copyright terms: Public domain | W3C validator |