| Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > ILE Home > Th. List > 4z | GIF version | ||
| Description: 4 is an integer. (Contributed by BJ, 26-Mar-2020.) |
| Ref | Expression |
|---|---|
| 4z | ⊢ 4 ∈ ℤ |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 4nn 9159 | . 2 ⊢ 4 ∈ ℕ | |
| 2 | 1 | nnzi 9352 | 1 ⊢ 4 ∈ ℤ |
| Colors of variables: wff set class |
| Syntax hints: ∈ wcel 2167 4c4 9048 ℤcz 9331 |
| 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 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-sep 4152 ax-pow 4208 ax-pr 4243 ax-un 4469 ax-setind 4574 ax-cnex 7975 ax-resscn 7976 ax-1cn 7977 ax-1re 7978 ax-icn 7979 ax-addcl 7980 ax-addrcl 7981 ax-mulcl 7982 ax-addcom 7984 ax-addass 7986 ax-distr 7988 ax-i2m1 7989 ax-0lt1 7990 ax-0id 7992 ax-rnegex 7993 ax-cnre 7995 ax-pre-ltirr 7996 ax-pre-ltwlin 7997 ax-pre-lttrn 7998 ax-pre-ltadd 8000 |
| This theorem depends on definitions: df-bi 117 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rab 2484 df-v 2765 df-sbc 2990 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-pw 3608 df-sn 3629 df-pr 3630 df-op 3632 df-uni 3841 df-int 3876 df-br 4035 df-opab 4096 df-id 4329 df-xp 4670 df-rel 4671 df-cnv 4672 df-co 4673 df-dm 4674 df-iota 5220 df-fun 5261 df-fv 5267 df-riota 5880 df-ov 5928 df-oprab 5929 df-mpo 5930 df-pnf 8068 df-mnf 8069 df-xr 8070 df-ltxr 8071 df-le 8072 df-sub 8204 df-neg 8205 df-inn 8996 df-2 9054 df-3 9055 df-4 9056 df-z 9332 |
| This theorem is referenced by: fz0to4untppr 10204 fzo0to42pr 10301 iexpcyc 10741 sqoddm1div8 10790 4bc2eq6 10871 resqrexlemga 11193 ef01bndlem 11926 sin01bnd 11927 cos01bnd 11928 4dvdseven 12087 flodddiv4lt 12108 6gcd4e2 12175 6lcm4e12 12268 prm23lt5 12445 lgsdir2lem2 15317 m1lgs 15373 2lgsoddprmlem2 15394 |
| Copyright terms: Public domain | W3C validator |