Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > uzid | GIF version |
Description: Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
Ref | Expression |
---|---|
uzid | ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | zre 9186 | . . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ) | |
2 | 1 | leidd 8403 | . . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀) |
3 | 2 | ancli 321 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)) |
4 | eluz1 9461 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀))) | |
5 | 3, 4 | mpbird 166 | 1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 2135 class class class wbr 3976 ‘cfv 5182 ≤ cle 7925 ℤcz 9182 ℤ≥cuz 9457 |
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 604 ax-in2 605 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-13 2137 ax-14 2138 ax-ext 2146 ax-sep 4094 ax-pow 4147 ax-pr 4181 ax-un 4405 ax-setind 4508 ax-cnex 7835 ax-resscn 7836 ax-pre-ltirr 7856 |
This theorem depends on definitions: df-bi 116 df-3or 968 df-3an 969 df-tru 1345 df-fal 1348 df-nf 1448 df-sb 1750 df-eu 2016 df-mo 2017 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-ne 2335 df-nel 2430 df-ral 2447 df-rex 2448 df-rab 2451 df-v 2723 df-sbc 2947 df-dif 3113 df-un 3115 df-in 3117 df-ss 3124 df-pw 3555 df-sn 3576 df-pr 3577 df-op 3579 df-uni 3784 df-br 3977 df-opab 4038 df-mpt 4039 df-id 4265 df-xp 4604 df-rel 4605 df-cnv 4606 df-co 4607 df-dm 4608 df-iota 5147 df-fun 5184 df-fv 5190 df-ov 5839 df-pnf 7926 df-mnf 7927 df-xr 7928 df-ltxr 7929 df-le 7930 df-neg 8063 df-z 9183 df-uz 9458 |
This theorem is referenced by: uzn0 9472 uz11 9479 eluzfz1 9956 eluzfz2 9957 elfz3 9959 elfz1end 9980 fzssp1 9992 fzpred 9995 fzp1ss 9998 fzpr 10002 fztp 10003 elfz0add 10045 fzolb 10078 zpnn0elfzo 10132 fzosplitsnm1 10134 fzofzp1 10152 fzosplitsn 10158 fzostep1 10162 frec2uzuzd 10327 frecuzrdgrrn 10333 frec2uzrdg 10334 frecuzrdgrcl 10335 frecuzrdgsuc 10339 frecuzrdgrclt 10340 frecuzrdgg 10341 frecuzrdgsuctlem 10348 uzsinds 10367 seq3val 10383 seqvalcd 10384 seq3-1 10385 seqf 10386 seq3p1 10387 seq3fveq 10396 seq3-1p 10405 seq3caopr3 10406 iseqf1olemjpcl 10420 iseqf1olemqpcl 10421 seq3f1oleml 10428 seq3f1o 10429 seq3homo 10435 faclbnd3 10645 bcm1k 10662 bcn2 10666 seq3coll 10741 rexuz3 10918 r19.2uz 10921 resqrexlemcvg 10947 resqrexlemgt0 10948 resqrexlemoverl 10949 cau3lem 11042 caubnd2 11045 climconst 11217 climuni 11220 climcau 11274 serf0 11279 fsumparts 11397 isum1p 11419 isumrpcl 11421 cvgratz 11459 mertenslemi1 11462 ntrivcvgap0 11476 fprodabs 11543 eftlub 11617 zsupcllemstep 11863 zsupcllemex 11864 ialgr0 11955 eucalg 11970 pw2dvds 12075 eulerthlemrprm 12138 oddprm 12168 pcfac 12257 pcbc 12258 ennnfonelem1 12277 lmconst 12757 2logb9irr 13430 sqrt2cxp2logb9e3 13434 2logb9irrap 13436 cvgcmp2nlemabs 13745 trilpolemlt1 13754 |
Copyright terms: Public domain | W3C validator |