![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > nnred | GIF version |
Description: A positive integer is a real number. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nnred.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ) |
Ref | Expression |
---|---|
nnred | ⊢ (𝜑 → 𝐴 ∈ ℝ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nnssre 8487 | . 2 ⊢ ℕ ⊆ ℝ | |
2 | nnred.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ) | |
3 | 1, 2 | sseldi 3024 | 1 ⊢ (𝜑 → 𝐴 ∈ ℝ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1439 ℝcr 7410 ℕcn 8483 |
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 666 ax-5 1382 ax-7 1383 ax-gen 1384 ax-ie1 1428 ax-ie2 1429 ax-8 1441 ax-10 1442 ax-11 1443 ax-i12 1444 ax-bndl 1445 ax-4 1446 ax-17 1465 ax-i9 1469 ax-ial 1473 ax-i5r 1474 ax-ext 2071 ax-sep 3963 ax-cnex 7497 ax-resscn 7498 ax-1re 7500 ax-addrcl 7503 |
This theorem depends on definitions: df-bi 116 df-tru 1293 df-nf 1396 df-sb 1694 df-clab 2076 df-cleq 2082 df-clel 2085 df-nfc 2218 df-ral 2365 df-v 2622 df-in 3006 df-ss 3013 df-int 3695 df-inn 8484 |
This theorem is referenced by: exbtwnzlemstep 9720 qbtwnrelemcalc 9728 qbtwnre 9729 flqdiv 9789 modqmulnn 9810 modifeq2int 9854 modaddmodup 9855 modaddmodlo 9856 modsumfzodifsn 9864 addmodlteq 9866 bernneq3 10137 expnbnd 10138 facwordi 10209 faclbnd 10210 faclbnd2 10211 faclbnd3 10212 faclbnd6 10213 facubnd 10214 facavg 10215 bcp1nk 10231 ibcval5 10232 caucvgrelemcau 10474 caucvgre 10475 cvg1nlemcxze 10476 cvg1nlemcau 10478 cvg1nlemres 10479 resqrexlemdecn 10506 resqrexlemga 10517 fsum3cvg3 10850 divcnv 10952 cvgratnnlembern 10978 cvgratnnlemseq 10981 cvgratnnlemabsle 10982 cvgratnnlemsumlt 10983 cvgratnnlemrate 10985 cvgratz 10987 eftabs 11007 efcllemp 11009 ege2le3 11022 efcj 11024 eftlub 11041 eflegeo 11053 eirraplem 11125 dvdslelemd 11183 nno 11245 nnoddm1d2 11249 divalglemnqt 11259 divalglemeunn 11260 dvdsbnd 11287 sqgcd 11357 lcmgcdlem 11398 ncoprmgcdne1b 11410 prmind2 11441 coprm 11462 prmfac1 11470 sqrt2irraplemnn 11496 divdenle 11514 qnumgt0 11515 nn0sqrtelqelz 11523 hashdvds 11536 znnen 11550 strleund 11643 |
Copyright terms: Public domain | W3C validator |