Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 (class class class)co 7358
1c1 11053 + caddc 11055 · cmul 11057
2c2 12209 3c3 12210
6c6 12213 9c9 12216 |
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-ext 2708 ax-resscn 11109 ax-1cn 11110 ax-icn 11111 ax-addcl 11112 ax-mulcl 11114 ax-mulcom 11116 ax-addass 11117 ax-mulass 11118 ax-distr 11119 ax-1rid 11122 ax-cnre 11125 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-clel 2815 df-rex 3075 df-rab 3409 df-v 3448 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-iota 6449 df-fv 6505 df-ov 7361 df-2 12217 df-3 12218
df-4 12219 df-5 12220
df-6 12221 df-7 12222
df-8 12223 df-9 12224 |
This theorem is referenced by: sq3
14103 3dvds
16214 3dvdsdec
16215 3dvds2dec
16216 9nprm
16986 11prm
16988 43prm
16995 83prm
16996 317prm
16999 1259lem2
17005 1259lem4
17007 1259prm
17009 2503lem2
17011 mcubic
26200 log2tlbnd
26298 log2ublem3
26301 log2ub
26302 bposlem9
26643 lgsdir2lem5
26680 ex-lcm
29405 hgt750lem
33267 hgt750lem2
33268 3lexlogpow2ineq2
40519 3lexlogpow5ineq5
40520 3cubeslem3l
41012 3cubeslem3r
41013 inductionexd
42434 fmtno5lem3
45754 fmtno4prmfac193
45772 fmtno4nprmfac193
45773 127prm
45798 2exp340mod341
45932 9fppr8
45936 |