![]() |
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 8425 | . . . 4 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ ℝ) | |
2 | 1 | leidd 7671 | . . 3 ⊢ (𝑀 ∈ ℤ → 𝑀 ≤ 𝑀) |
3 | 2 | ancli 316 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀)) |
4 | eluz1 8693 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑀 ≤ 𝑀))) | |
5 | 3, 4 | mpbird 165 | 1 ⊢ (𝑀 ∈ ℤ → 𝑀 ∈ (ℤ≥‘𝑀)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ∈ wcel 1434 class class class wbr 3787 ‘cfv 4926 ≤ cle 7205 ℤcz 8421 ℤ≥cuz 8689 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in1 577 ax-in2 578 ax-io 663 ax-5 1377 ax-7 1378 ax-gen 1379 ax-ie1 1423 ax-ie2 1424 ax-8 1436 ax-10 1437 ax-11 1438 ax-i12 1439 ax-bndl 1440 ax-4 1441 ax-13 1445 ax-14 1446 ax-17 1460 ax-i9 1464 ax-ial 1468 ax-i5r 1469 ax-ext 2064 ax-sep 3898 ax-pow 3950 ax-pr 3966 ax-un 4190 ax-setind 4282 ax-cnex 7118 ax-resscn 7119 ax-pre-ltirr 7139 |
This theorem depends on definitions: df-bi 115 df-3or 921 df-3an 922 df-tru 1288 df-fal 1291 df-nf 1391 df-sb 1687 df-eu 1945 df-mo 1946 df-clab 2069 df-cleq 2075 df-clel 2078 df-nfc 2209 df-ne 2247 df-nel 2341 df-ral 2354 df-rex 2355 df-rab 2358 df-v 2604 df-sbc 2817 df-dif 2976 df-un 2978 df-in 2980 df-ss 2987 df-pw 3386 df-sn 3406 df-pr 3407 df-op 3409 df-uni 3604 df-br 3788 df-opab 3842 df-mpt 3843 df-id 4050 df-xp 4371 df-rel 4372 df-cnv 4373 df-co 4374 df-dm 4375 df-iota 4891 df-fun 4928 df-fv 4934 df-ov 5540 df-pnf 7206 df-mnf 7207 df-xr 7208 df-ltxr 7209 df-le 7210 df-neg 7338 df-z 8422 df-uz 8690 |
This theorem is referenced by: uzn0 8704 uz11 8711 eluzfz1 9115 eluzfz2 9116 elfz3 9118 elfz1end 9139 fzssp1 9150 fzpred 9152 fzp1ss 9155 fzpr 9159 fztp 9160 elfz0add 9200 fzolb 9228 zpnn0elfzo 9282 fzosplitsnm1 9284 fzofzp1 9302 fzosplitsn 9308 fzostep1 9312 frec2uzuzd 9473 frecuzrdgrrn 9479 frec2uzrdg 9480 frecuzrdgrcl 9481 frecuzrdgsuc 9485 frecuzrdgrclt 9486 frecuzrdgg 9487 frecuzrdgsuctlem 9494 uzsinds 9507 iseqvalt 9521 iseq1 9522 iseq1t 9523 iseqfcl 9524 iseqfclt 9525 iseqcl 9526 iseqp1 9527 iseqp1t 9528 iseqfveq 9535 iseq1p 9544 iseqcaopr3 9545 iseqhomo 9554 faclbnd3 9756 bcm1k 9773 bcn2 9777 rexuz3 10003 r19.2uz 10006 resqrexlemcvg 10032 resqrexlemgt0 10033 resqrexlemoverl 10034 cau3lem 10127 caubnd2 10130 climconst 10256 climuni 10259 climcau 10311 serif0 10316 zsupcllemstep 10474 zsupcllemex 10475 ialgr0 10559 eucialg 10574 pw2dvds 10677 |
Copyright terms: Public domain | W3C validator |