![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eluz2nn | GIF version |
Description: An integer is greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.) |
Ref | Expression |
---|---|
eluz2nn | ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1z 9314 | . . 3 ⊢ 1 ∈ ℤ | |
2 | 1le2 9162 | . . 3 ⊢ 1 ≤ 2 | |
3 | eluzuzle 9571 | . . 3 ⊢ ((1 ∈ ℤ ∧ 1 ≤ 2) → (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ (ℤ≥‘1))) | |
4 | 1, 2, 3 | mp2an 426 | . 2 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ (ℤ≥‘1)) |
5 | nnuz 9599 | . 2 ⊢ ℕ = (ℤ≥‘1) | |
6 | 4, 5 | eleqtrrdi 2283 | 1 ⊢ (𝐴 ∈ (ℤ≥‘2) → 𝐴 ∈ ℕ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 2160 class class class wbr 4021 ‘cfv 5238 1c1 7847 ≤ cle 8028 ℕcn 8954 2c2 9005 ℤcz 9288 ℤ≥cuz 9563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-13 2162 ax-14 2163 ax-ext 2171 ax-sep 4139 ax-pow 4195 ax-pr 4230 ax-un 4454 ax-setind 4557 ax-cnex 7937 ax-resscn 7938 ax-1cn 7939 ax-1re 7940 ax-icn 7941 ax-addcl 7942 ax-addrcl 7943 ax-mulcl 7944 ax-addcom 7946 ax-addass 7948 ax-distr 7950 ax-i2m1 7951 ax-0lt1 7952 ax-0id 7954 ax-rnegex 7955 ax-cnre 7957 ax-pre-ltirr 7958 ax-pre-ltwlin 7959 ax-pre-lttrn 7960 ax-pre-ltadd 7962 |
This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1472 df-sb 1774 df-eu 2041 df-mo 2042 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-ne 2361 df-nel 2456 df-ral 2473 df-rex 2474 df-reu 2475 df-rab 2477 df-v 2754 df-sbc 2978 df-dif 3146 df-un 3148 df-in 3150 df-ss 3157 df-pw 3595 df-sn 3616 df-pr 3617 df-op 3619 df-uni 3828 df-int 3863 df-br 4022 df-opab 4083 df-mpt 4084 df-id 4314 df-xp 4653 df-rel 4654 df-cnv 4655 df-co 4656 df-dm 4657 df-rn 4658 df-res 4659 df-ima 4660 df-iota 5199 df-fun 5240 df-fn 5241 df-f 5242 df-fv 5246 df-riota 5855 df-ov 5903 df-oprab 5904 df-mpo 5905 df-pnf 8029 df-mnf 8030 df-xr 8031 df-ltxr 8032 df-le 8033 df-sub 8165 df-neg 8166 df-inn 8955 df-2 9013 df-z 9289 df-uz 9564 |
This theorem is referenced by: eluz4nn 9604 eluzge2nn0 9605 eluz2n0 9606 elnn1uz2 9643 zgt1rpn0n1 9731 modm1div 11848 isprm3 12161 isprm4 12162 prmind2 12163 nprm 12166 exprmfct 12181 prmdvdsfz 12182 isprm5lem 12184 isprm6 12190 phibndlem 12259 phibnd 12260 dfphi2 12263 pclemub 12330 pcprendvds2 12334 pcpre1 12335 dvdsprmpweqnn 12379 expnprm 12396 4sqlem15 12448 4sqlem16 12449 infpn2 12518 logbrec 14863 logbgcd1irr 14870 logbgcd1irraplemexp 14871 logbgcd1irraplemap 14872 2sqlem6 14953 |
Copyright terms: Public domain | W3C validator |