![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > eluz2 | GIF version |
Description: Membership in an upper set of integers. We use the fact that a function's value (under our function value definition) is empty outside of its domain to show 𝑀 ∈ ℤ. (Contributed by NM, 5-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Ref | Expression |
---|---|
eluz2 | ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eluzel2 9014 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | |
2 | simp1 943 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ) | |
3 | eluz1 9013 | . . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | |
4 | ibar 295 | . . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))) | |
5 | 3, 4 | bitrd 186 | . . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))) |
6 | 3anass 928 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | |
7 | 5, 6 | syl6bbr 196 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
8 | 1, 2, 7 | pm5.21nii 655 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 102 ↔ wb 103 ∧ w3a 924 ∈ wcel 1438 class class class wbr 3843 ‘cfv 5010 ≤ cle 7513 ℤcz 8740 ℤ≥cuz 9009 |
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-io 665 ax-5 1381 ax-7 1382 ax-gen 1383 ax-ie1 1427 ax-ie2 1428 ax-8 1440 ax-10 1441 ax-11 1442 ax-i12 1443 ax-bndl 1444 ax-4 1445 ax-14 1450 ax-17 1464 ax-i9 1468 ax-ial 1472 ax-i5r 1473 ax-ext 2070 ax-sep 3955 ax-pow 4007 ax-pr 4034 ax-cnex 7426 ax-resscn 7427 |
This theorem depends on definitions: df-bi 115 df-3or 925 df-3an 926 df-tru 1292 df-nf 1395 df-sb 1693 df-eu 1951 df-mo 1952 df-clab 2075 df-cleq 2081 df-clel 2084 df-nfc 2217 df-ral 2364 df-rex 2365 df-rab 2368 df-v 2621 df-sbc 2841 df-un 3003 df-in 3005 df-ss 3012 df-pw 3429 df-sn 3450 df-pr 3451 df-op 3453 df-uni 3652 df-br 3844 df-opab 3898 df-mpt 3899 df-id 4118 df-xp 4442 df-rel 4443 df-cnv 4444 df-co 4445 df-dm 4446 df-rn 4447 df-res 4448 df-ima 4449 df-iota 4975 df-fun 5012 df-fn 5013 df-f 5014 df-fv 5018 df-ov 5647 df-neg 7646 df-z 8741 df-uz 9010 |
This theorem is referenced by: eluzuzle 9017 eluzelz 9018 eluzle 9021 uztrn 9025 eluzp1p1 9034 uznn0sub 9040 uz3m2nn 9051 1eluzge0 9052 2eluzge1 9054 raluz2 9057 rexuz2 9059 peano2uz 9061 nn0pzuz 9065 uzind4 9066 nn0ge2m1nnALT 9093 elfzuzb 9424 uzsubsubfz 9451 ige2m1fz 9512 4fvwrd4 9539 elfzo2 9549 elfzouz2 9560 fzossrbm1 9572 fzossfzop1 9611 ssfzo12bi 9624 elfzonelfzo 9629 elfzomelpfzo 9630 fzosplitprm1 9633 fzostep1 9636 fzind2 9638 flqword2 9684 fldiv4p1lem1div2 9700 seq3split 9895 iseqf1olemqk 9911 seq3f1olemqsumkj 9915 seq3f1olemqsumk 9916 seq3f1olemqsum 9917 ibcval5 10159 iseqcoll 10235 seq3shft 10260 resqrexlemoverl 10442 resqrexlemga 10444 fsum3cvg3 10776 fisumrev2 10827 isumshft 10871 cvgratnnlemseq 10907 cvgratnnlemabsle 10908 cvgratnnlemsumlt 10909 cvgratz 10913 oddge22np1 11146 nn0o 11172 dvdsnprmd 11372 prmgt1 11378 oddprmgt2 11380 oddprmge3 11381 |
Copyright terms: Public domain | W3C validator |