Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2104
(class class class)co 7411 1c1 11113
− cmin 11448 ℤcz 12562 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3966 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-iun 4998 df-br 5148 df-opab 5210 df-mpt 5231 df-tr 5265 df-id 5573 df-eprel 5579 df-po 5587 df-so 5588 df-fr 5630 df-we 5632 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-pred 6299 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7858 df-2nd 7978 df-frecs 8268 df-wrecs 8299 df-recs 8373 df-rdg 8412 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-nn 12217 df-n0 12477 df-z 12563 |
This theorem is referenced by: zlem1lt
12618 zltlem1
12619 zextlt
12640 zeo
12652 eluzp1m1
12852 uzm1
12864 zbtwnre
12934 fz01en
13533 fzsuc2
13563 elfzm11
13576 uzdisj
13578 preduz
13627 predfz
13630 elfzo
13638 fzon
13657 fzoss2
13664 fzossrbm1
13665 fzosplitsnm1
13711 ubmelm1fzo
13732 elfzom1b
13735 fzosplitprm1
13746 fzoshftral
13753 sermono
14004 seqf1olem1
14011 seqf1olem2
14012 bcm1k
14279 bcn2
14283 bcp1m1
14284 bcpasc
14285 bccl
14286 hashbclem
14415 seqcoll
14429 revccat
14720 revrev
14721 absrdbnd
15292 fsumm1
15701 binomlem
15779 isumsplit
15790 climcndslem1
15799 arisum2
15811 pwdif
15818 pwm1geoser
15819 mertenslem1
15834 fprodser
15897 fprodm1
15915 risefacval2
15958 fallfacval2
15959 fallfacval3
15960 fallfacfwd
15984 binomfallfaclem2
15988 3dvds
16278 oddm1even
16290 oddp1even
16291 mod2eq1n2dvds
16294 zob
16306 nno
16329 pwp1fsum
16338 isprm3
16624 ncoprmlnprm
16668 hashdvds
16712 pockthlem
16842 4sqlem11
16892 vdwapun
16911 vdwnnlem2
16933 efgsp1
19646 efgsres
19647 srgbinomlem4
20123 srgbinomlem
20124 znunit
21338 dvexp3
25730 dvfsumlem1
25778 degltlem1
25825 atantayl2
26679 wilthlem1
26808 basellem5
26825 mersenne
26966 perfectlem1
26968 lgslem1
27036 lgsval2lem
27046 lgseisenlem1
27114 lgseisenlem2
27115 lgseisenlem3
27116 lgsquadlem1
27119 lgsquadlem3
27121 lgsquad2lem1
27123 lgsquad3
27126 2sqlem8
27165 2sqblem
27170 dchrisumlem1
27228 logdivbnd
27295 pntrsumbnd2
27306 ostth2lem3
27374 axlowdim
28486 pthdlem1
29290 pthdlem2
29292 wwlksm1edg
29402 clwwlkccatlem
29509 clwlkclwwlklem2fv1
29515 clwlkclwwlklem2a4
29517 clwlkclwwlklem2a
29518 clwlkclwwlklem2
29520 clwlkclwwlk
29522 clwwisshclwwslem
29534 clwwlkf
29567 wwlksubclwwlk
29578 numclwwlk5
29908 numclwwlk7
29911 frgrreggt1
29913 0nn0m1nnn0
34400 erdszelem7
34486 elfzm12
34958 fz0n
35004 fwddifnp1
35441 knoppndvlem2
35692 ltflcei
36779 poimirlem1
36792 poimirlem2
36793 poimirlem6
36797 poimirlem7
36798 poimirlem8
36799 poimirlem9
36800 poimirlem15
36806 poimirlem16
36807 poimirlem17
36808 poimirlem18
36809 poimirlem19
36810 poimirlem20
36811 poimirlem24
36815 poimirlem27
36818 poimirlem31
36822 poimirlem32
36823 mettrifi
36928 rmxluc
41977 rmyluc
41978 jm2.24
42004 jm2.18
42029 jm2.22
42036 jm2.23
42037 jm2.26lem3
42042 jm2.15nn0
42044 jm2.16nn0
42045 jm2.27a
42046 jm2.27c
42048 jm3.1lem3
42060 hashnzfz
43381 monoords
44305 fzisoeu
44308 dvnmul
44957 stoweidlem11
45025 dirkercncflem1
45117 fourierdlem48
45168 fourierdlem49
45169 fourierdlem65
45185 fourierdlem79
45199 zm1nn
46308 iccpartipre
46387 sfprmdvdsmersenne
46569 lighneallem4a
46574 proththd
46580 dfodd6
46603 evenm1odd
46605 oddm1eveni
46608 onego
46612 m1expoddALTV
46614 dfodd4
46625 oddflALTV
46629 oddm1evenALTV
46641 nnoALTV
46661 perfectALTVlem1
46687 altgsumbcALT
47117 pw2m1lepw2m1
47288 m1modmmod
47294 difmodm1lt
47295 zofldiv2
47304 logbpw2m1
47340 nnolog2flm1
47363 dignn0flhalflem1
47388 |