![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 1zzd | GIF version |
Description: 1 is an integer, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Ref | Expression |
---|---|
1zzd | ⊢ (𝜑 → 1 ∈ ℤ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1z 8874 | . 2 ⊢ 1 ∈ ℤ | |
2 | 1 | a1i 9 | 1 ⊢ (𝜑 → 1 ∈ ℤ) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∈ wcel 1445 1c1 7448 ℤcz 8848 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 582 ax-in2 583 ax-io 668 ax-5 1388 ax-7 1389 ax-gen 1390 ax-ie1 1434 ax-ie2 1435 ax-8 1447 ax-10 1448 ax-11 1449 ax-i12 1450 ax-bndl 1451 ax-4 1452 ax-13 1456 ax-14 1457 ax-17 1471 ax-i9 1475 ax-ial 1479 ax-i5r 1480 ax-ext 2077 ax-sep 3978 ax-pow 4030 ax-pr 4060 ax-un 4284 ax-setind 4381 ax-cnex 7533 ax-resscn 7534 ax-1cn 7535 ax-1re 7536 ax-icn 7537 ax-addcl 7538 ax-addrcl 7539 ax-mulcl 7540 ax-addcom 7542 ax-addass 7544 ax-distr 7546 ax-i2m1 7547 ax-0lt1 7548 ax-0id 7550 ax-rnegex 7551 ax-cnre 7553 ax-pre-ltirr 7554 ax-pre-ltwlin 7555 ax-pre-lttrn 7556 ax-pre-ltadd 7558 |
This theorem depends on definitions: df-bi 116 df-3or 928 df-3an 929 df-tru 1299 df-fal 1302 df-nf 1402 df-sb 1700 df-eu 1958 df-mo 1959 df-clab 2082 df-cleq 2088 df-clel 2091 df-nfc 2224 df-ne 2263 df-nel 2358 df-ral 2375 df-rex 2376 df-reu 2377 df-rab 2379 df-v 2635 df-sbc 2855 df-dif 3015 df-un 3017 df-in 3019 df-ss 3026 df-pw 3451 df-sn 3472 df-pr 3473 df-op 3475 df-uni 3676 df-int 3711 df-br 3868 df-opab 3922 df-id 4144 df-xp 4473 df-rel 4474 df-cnv 4475 df-co 4476 df-dm 4477 df-iota 5014 df-fun 5051 df-fv 5057 df-riota 5646 df-ov 5693 df-oprab 5694 df-mpt2 5695 df-pnf 7621 df-mnf 7622 df-xr 7623 df-ltxr 7624 df-le 7625 df-sub 7752 df-neg 7753 df-inn 8521 df-z 8849 |
This theorem is referenced by: uzm1 9148 elfz1b 9653 fzm1 9663 fzoss2 9732 fzo1fzo0n0 9743 qnegmod 9925 addmodid 9928 q2submod 9941 ser3mono 10028 seq3f1olemqsumkj 10048 exp3vallem 10071 exp3val 10072 exp1 10076 facnn 10250 fac0 10251 fac1 10252 bcp1nk 10285 hashfiv01gt1 10305 fseq1hash 10324 hashfz 10344 zfz1isolemsplit 10358 seq3coll 10362 resqrexlemf 10555 resqrexlemf1 10556 resqrexlemnmsq 10565 resqrexlemcvg 10567 climuni 10836 climrecvg1n 10891 climcvg1nlem 10892 isummolemnm 10922 summodclem2a 10924 summodclem2 10925 summodc 10926 zsumdc 10927 fsum3 10930 sum0 10931 fisumss 10935 fsumcl2lem 10941 fsumadd 10949 sumsnf 10952 fsummulc2 10991 telfsumo 11009 fsumparts 11013 binomlem 11026 divcnv 11040 arisum 11041 arisum2 11042 trireciplem 11043 trirecip 11044 expcnvap0 11045 expcnv 11047 geo2sum 11057 geo2lim 11059 geoisum1 11062 geoisum1c 11063 cvgratnnlemseq 11069 cvgratnnlemsumlt 11071 cvgratnnlemrate 11073 cvgratnn 11074 cvgratz 11075 mertenslemub 11077 mertenslemi1 11078 mertenslem2 11079 ege2le3 11110 nn0o1gt2 11332 gcdsupex 11376 gcdsupcl 11377 gcdaddm 11402 lcmval 11472 lcmcllem 11476 lcmledvds 11479 isprm3 11527 isprm4 11528 prmind2 11529 dvdsnprmd 11534 rpexp 11559 pw2dvds 11571 phivalfi 11615 phicl2 11617 hashdvds 11624 phiprmpw 11625 phimullem 11628 hashgcdeq 11631 lmtopcnp 12101 |
Copyright terms: Public domain | W3C validator |