![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 4z | Structured version Visualization version GIF version |
Description: 4 is an integer. (Contributed by BJ, 26-Mar-2020.) |
Ref | Expression |
---|---|
4z | ⊢ 4 ∈ ℤ |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 4nn 12372 | . 2 ⊢ 4 ∈ ℕ | |
2 | 1 | nnzi 12663 | 1 ⊢ 4 ∈ ℤ |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2103 4c4 12346 ℤcz 12635 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2105 ax-9 2113 ax-10 2136 ax-11 2153 ax-12 2173 ax-ext 2705 ax-sep 5320 ax-nul 5327 ax-pr 5450 ax-un 7766 ax-1cn 11238 ax-icn 11239 ax-addcl 11240 ax-addrcl 11241 ax-mulcl 11242 ax-mulrcl 11243 ax-i2m1 11248 ax-1ne0 11249 ax-rrecex 11252 ax-cnre 11253 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2890 df-ne 2943 df-ral 3064 df-rex 3073 df-reu 3384 df-rab 3439 df-v 3484 df-sbc 3799 df-csb 3916 df-dif 3973 df-un 3975 df-in 3977 df-ss 3987 df-pss 3990 df-nul 4348 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-iun 5021 df-br 5170 df-opab 5232 df-mpt 5253 df-tr 5287 df-id 5597 df-eprel 5603 df-po 5611 df-so 5612 df-fr 5654 df-we 5656 df-xp 5705 df-rel 5706 df-cnv 5707 df-co 5708 df-dm 5709 df-rn 5710 df-res 5711 df-ima 5712 df-pred 6331 df-ord 6397 df-on 6398 df-lim 6399 df-suc 6400 df-iota 6524 df-fun 6574 df-fn 6575 df-f 6576 df-f1 6577 df-fo 6578 df-f1o 6579 df-fv 6580 df-ov 7448 df-om 7900 df-2nd 8027 df-frecs 8318 df-wrecs 8349 df-recs 8423 df-rdg 8462 df-neg 11519 df-nn 12290 df-2 12352 df-3 12353 df-4 12354 df-z 12636 |
This theorem is referenced by: fz0to4untppr 13683 fzo0to42pr 13799 fzo1to4tp 13800 iexpcyc 14252 sqoddm1div8 14288 4bc2eq6 14374 ef01bndlem 16226 sin01bnd 16227 cos01bnd 16228 4dvdseven 16415 flodddiv4lt 16457 6gcd4e2 16579 6lcm4e12 16657 lcmf2a3a4e12 16688 ge2nprmge4 16742 prm23lt5 16856 1259lem3 17175 ppiub 27257 bclbnd 27333 bposlem6 27342 bposlem9 27345 lgsdir2lem2 27379 m1lgs 27441 2lgsoddprmlem2 27462 chebbnd1lem2 27523 chebbnd1lem3 27524 pntlema 27649 pntlemb 27650 ex-ind-dvds 30484 hgt750lemd 34617 3lexlogpow5ineq5 41965 aks4d1p1p7 41979 aks4d1p1p5 41980 aks4d1p1 41981 flt4lem7 42547 inductionexd 44057 wallispi2lem1 45926 fmtno4prmfac 47378 31prm 47403 mod42tp1mod8 47408 8even 47519 341fppr2 47540 4fppr1 47541 9fppr8 47543 fpprel2 47547 sbgoldbo 47593 nnsum3primesle9 47600 nnsum4primeseven 47606 nnsum4primesevenALTV 47607 tgblthelfgott 47621 zlmodzxzequa 48143 zlmodzxznm 48144 zlmodzxzequap 48146 zlmodzxzldeplem3 48149 zlmodzxzldep 48151 ldepsnlinclem1 48152 ldepsnlinc 48155 |
Copyright terms: Public domain | W3C validator |