Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 (class class class)co 7358
1c1 11053 + caddc 11055 ℕcn 12154
5c5 12212 6c6 12213 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914
ax-6 1972 ax-7 2012 ax-8 2109
ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2708 ax-sep 5257 ax-nul 5264 ax-pr 5385 ax-un 7673 ax-1cn 11110 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2890 df-ne 2945 df-ral 3066 df-rex 3075 df-reu 3355 df-rab 3409 df-v 3448 df-sbc 3741 df-csb 3857 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3930 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-iun 4957 df-br 5107 df-opab 5169 df-mpt 5190 df-tr 5224 df-id 5532 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5589 df-we 5591 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6254 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-fv 6505 df-ov 7361 df-om 7804 df-2nd 7923 df-frecs 8213 df-wrecs 8244 df-recs 8318 df-rdg 8357 df-nn 12155 df-2 12217
df-3 12218 df-4 12219
df-5 12220 df-6 12221 |
This theorem is referenced by: 7nn
12246 6nn0
12435 ef01bndlem
16067 sin01bnd
16068 cos01bnd
16069 6gcd4e2
16420 6lcm4e12
16493 83prm
16996 139prm
16997 163prm
16998 prmo6
17003 vscandx
17201 vscaid
17202 lmodstr
17207 ipsstr
17218 lt6abl
19673 psrvalstr
21321 opsrvscaOLD
21462 tngvscaOLD
24011 sincos3rdpi
25876 1cubrlem
26194 quart1cl
26207 quart1lem
26208 quart1
26209 log2ub
26302 log2le1
26303 basellem5
26437 basellem8
26440 basellem9
26441 ppiublem1
26553 ppiublem2
26554 ppiub
26555 bpos1
26634 bposlem9
26643 itvndx
27382 itvid
27384 slotsinbpsd
27386 lngndxnitvndx
27388 trkgstr
27389 ttgvalOLD
27821 ttglemOLD
27823 ttgvscaOLD
27830 ttgdsOLD
27832 eengstr
27932 ex-cnv
29384 ex-dm
29386 ex-dvds
29403 ex-gcd
29404 ex-lcm
29405 resvvscaOLD
32132 hgt750lem
33267 60gcd6e6
40464 60gcd7e1
40465 12lcm5e60
40468 60lcm6e60
40469 60lcm7e420
40470 lcm6un
40478 lcmineqlem
40512 3lexlogpow5ineq1
40514 aks4d1p1p5
40535 aks4d1p1
40536 rmydioph
41341 expdiophlem2
41349 algstr
41507 mnringvscadOLD
42512 139prmALT
45795 31prm
45796 127prm
45798 6even
45910 gbowge7
45962 stgoldbwt
45975 sbgoldbwt
45976 mogoldbb
45984 sbgoldbo
45986 nnsum3primesle9
45993 nnsum4primeseven
45999 wtgoldbnnsum4prm
46001 bgoldbnnsum3prm
46003 zlmodzxzequa
46584 zlmodzxznm
46585 zlmodzxzequap
46587 zlmodzxzldeplem3
46590 zlmodzxzldep
46592 ldepsnlinclem2
46594 ldepsnlinc
46596 |