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 9485 | . 2 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) → 𝑀 ∈ ℤ) | |
2 | simp1 992 | . 2 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) → 𝑀 ∈ ℤ) | |
3 | eluz1 9484 | . . . 4 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | |
4 | ibar 299 | . . . 4 ⊢ (𝑀 ∈ ℤ → ((𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))) | |
5 | 3, 4 | bitrd 187 | . . 3 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)))) |
6 | 3anass 977 | . . 3 ⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁) ↔ (𝑀 ∈ ℤ ∧ (𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) | |
7 | 5, 6 | bitr4di 197 | . 2 ⊢ (𝑀 ∈ ℤ → (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁))) |
8 | 1, 2, 7 | pm5.21nii 699 | 1 ⊢ (𝑁 ∈ (ℤ≥‘𝑀) ↔ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑀 ≤ 𝑁)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 103 ↔ wb 104 ∧ w3a 973 ∈ wcel 2141 class class class wbr 3987 ‘cfv 5196 ≤ cle 7948 ℤcz 9205 ℤ≥cuz 9480 |
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-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-14 2144 ax-ext 2152 ax-sep 4105 ax-pow 4158 ax-pr 4192 ax-cnex 7858 ax-resscn 7859 |
This theorem depends on definitions: df-bi 116 df-3or 974 df-3an 975 df-tru 1351 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-ral 2453 df-rex 2454 df-rab 2457 df-v 2732 df-sbc 2956 df-un 3125 df-in 3127 df-ss 3134 df-pw 3566 df-sn 3587 df-pr 3588 df-op 3590 df-uni 3795 df-br 3988 df-opab 4049 df-mpt 4050 df-id 4276 df-xp 4615 df-rel 4616 df-cnv 4617 df-co 4618 df-dm 4619 df-rn 4620 df-res 4621 df-ima 4622 df-iota 5158 df-fun 5198 df-fn 5199 df-f 5200 df-fv 5204 df-ov 5854 df-neg 8086 df-z 9206 df-uz 9481 |
This theorem is referenced by: eluzuzle 9488 eluzelz 9489 eluzle 9492 uztrn 9496 eluzp1p1 9505 uznn0sub 9511 uz3m2nn 9525 1eluzge0 9526 2eluzge1 9528 raluz2 9531 rexuz2 9533 peano2uz 9535 nn0pzuz 9539 uzind4 9540 nn0ge2m1nnALT 9570 elfzuzb 9968 uzsubsubfz 9996 ige2m1fz 10059 4fvwrd4 10089 elfzo2 10099 elfzouz2 10110 fzossrbm1 10122 fzossfzop1 10161 ssfzo12bi 10174 elfzonelfzo 10179 elfzomelpfzo 10180 fzosplitprm1 10183 fzostep1 10186 fzind2 10188 flqword2 10238 fldiv4p1lem1div2 10254 uzennn 10385 seq3split 10428 iseqf1olemqk 10443 seq3f1olemqsumkj 10447 seq3f1olemqsumk 10448 seq3f1olemqsum 10449 bcval5 10690 seq3coll 10770 seq3shft 10795 resqrexlemoverl 10978 resqrexlemga 10980 fsum3cvg3 11352 fisumrev2 11402 isumshft 11446 cvgratnnlemseq 11482 cvgratnnlemabsle 11483 cvgratnnlemsumlt 11484 cvgratz 11488 oddge22np1 11833 nn0o 11859 suprzubdc 11900 zsupssdc 11902 uzwodc 11985 dvdsnprmd 12072 prmgt1 12079 oddprmgt2 12081 oddprmge3 12082 prm23ge5 12211 nninfdclemcl 12396 nninfdclemp1 12398 nninfdclemlt 12399 strleund 12499 strleun 12500 2logb9irr 13648 2logb9irrap 13654 lgsdilem2 13696 |
Copyright terms: Public domain | W3C validator |