Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1539 (class class class)co 7413
1c1 11115 + caddc 11117 · cmul 11119
2c2 12273 3c3 12274
6c6 12277 9c9 12280 |
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-ext 2701 ax-resscn 11171 ax-1cn 11172 ax-icn 11173 ax-addcl 11174 ax-mulcl 11176 ax-mulcom 11178 ax-addass 11179 ax-mulass 11180 ax-distr 11181 ax-1rid 11184 ax-cnre 11187 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-or 844 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-sb 2066 df-clab 2708 df-cleq 2722 df-clel 2808 df-rex 3069 df-rab 3431 df-v 3474 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-iota 6496 df-fv 6552 df-ov 7416 df-2 12281 df-3 12282
df-4 12283 df-5 12284
df-6 12285 df-7 12286
df-8 12287 df-9 12288 |
This theorem is referenced by: sq3
14168 3dvds
16280 3dvdsdec
16281 3dvds2dec
16282 9nprm
17052 11prm
17054 43prm
17061 83prm
17062 317prm
17065 1259lem2
17071 1259lem4
17073 1259prm
17075 2503lem2
17077 mcubic
26586 log2tlbnd
26684 log2ublem3
26687 log2ub
26688 bposlem9
27029 lgsdir2lem5
27066 ex-lcm
29976 hgt750lem
33959 hgt750lem2
33960 3lexlogpow2ineq2
41232 3lexlogpow5ineq5
41233 3cubeslem3l
41728 3cubeslem3r
41729 inductionexd
43210 fmtno5lem3
46523 fmtno4prmfac193
46541 fmtno4nprmfac193
46542 127prm
46567 2exp340mod341
46701 9fppr8
46705 |