Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > nn0ge0d | GIF version |
Description: A nonnegative integer is greater than or equal to zero. (Contributed by Mario Carneiro, 27-May-2016.) |
Ref | Expression |
---|---|
nn0red.1 | ⊢ (𝜑 → 𝐴 ∈ ℕ0) |
Ref | Expression |
---|---|
nn0ge0d | ⊢ (𝜑 → 0 ≤ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nn0red.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ ℕ0) | |
2 | nn0ge0 9160 | . 2 ⊢ (𝐴 ∈ ℕ0 → 0 ≤ 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → 0 ≤ 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2141 class class class wbr 3989 0cc0 7774 ≤ cle 7955 ℕ0cn0 9135 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-sep 4107 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-i2m1 7879 ax-0lt1 7880 ax-0id 7882 ax-rnegex 7883 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-ltadd 7890 |
This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-rab 2457 df-v 2732 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-br 3990 df-opab 4051 df-xp 4617 df-cnv 4619 df-iota 5160 df-fv 5206 df-ov 5856 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-inn 8879 df-n0 9136 |
This theorem is referenced by: flqmulnn0 10255 zmodfz 10302 addmodid 10328 modifeq2int 10342 modaddmodlo 10344 modsumfzodifsn 10352 addmodlteq 10354 expnnval 10479 nn0le2msqd 10653 facwordi 10674 faclbnd 10675 faclbnd6 10678 facavg 10680 geolim2 11475 mertenslemi1 11498 eftabs 11619 efcllemp 11621 efaddlem 11637 eftlub 11653 oexpneg 11836 divalglemnn 11877 divalglemnqt 11879 divalglemeunn 11880 divalg2 11885 dfgcd2 11969 gcdmultiple 11975 gcdmultiplez 11976 dvdssqlem 11985 nn0seqcvgd 11995 mulgcddvds 12048 isprm5lem 12095 nn0sqrtelqelz 12160 nonsq 12161 phibndlem 12170 dfphi2 12174 modprm0 12208 pythagtriplem3 12221 pythagtriplem10 12223 pythagtriplem6 12224 pythagtriplem7 12225 pythagtriplem12 12229 pythagtriplem14 12231 pcge0 12266 pcprmpw2 12286 pcmptdvds 12297 fldivp1 12300 pcbc 12303 qexpz 12304 pockthlem 12308 pockthg 12309 mul4sqlem 12345 ennnfoneleminc 12366 logbgcd1irraplemexp 13680 lgsval2lem 13705 lgsval4a 13717 2sqlem3 13747 2sqlem7 13751 2sqlem8 13753 |
Copyright terms: Public domain | W3C validator |