Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1542 (class class class)co 7362
+ caddc 11061 ·
cmul 11063 2c2 12215
4c4 12217 8c8 12221 |
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 11115 ax-1cn 11116 ax-icn 11117 ax-addcl 11118 ax-mulcl 11120 ax-mulcom 11122 ax-addass 11123 ax-mulass 11124 ax-distr 11125 ax-1rid 11128 ax-cnre 11131 |
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 3411 df-v 3450 df-dif 3918 df-un 3920 df-in 3922 df-ss 3932 df-nul 4288 df-if 4492 df-sn 4592 df-pr 4594 df-op 4598 df-uni 4871 df-br 5111 df-iota 6453 df-fv 6509 df-ov 7365 df-2 12223 df-3 12224
df-4 12225 df-5 12226
df-6 12227 df-7 12228
df-8 12229 |
This theorem is referenced by: 8th4div3
12380 4t3e12
12723 sq4e2t8
14110 cu2
14111 sqoddm1div8
14153 cos2bnd
16077 2exp7
16967 2exp8
16968 8nprm
16991 19prm
16997 139prm
17003 1259lem2
17011 1259lem3
17012 1259lem4
17013 1259lem5
17014 2503lem1
17016 2503lem2
17017 4001lem1
17020 4001lem2
17021 4001lem3
17022 4001lem4
17023 quart1lem
26221 quart1
26222 quartlem1
26223 log2tlbnd
26311 log2ub
26315 bpos1
26647 bposlem8
26655 lgsdir2lem2
26690 2lgslem3a
26760 2lgslem3b
26761 2lgslem3c
26762 2lgslem3d
26763 2lgsoddprmlem2
26773 2lgsoddprmlem3c
26776 2lgsoddprmlem3d
26777 chebbnd1lem2
26834 chebbnd1lem3
26835 pntlemr
26966 ex-exp
29436 420gcd8e4
40492 420lcm8e840
40497 lcmineqlem23
40537 3lexlogpow2ineq2
40545 fmtno4prmfac
45838 139prmALT
45862 mod42tp1mod8
45868 3exp4mod41
45882 41prothprm
45885 8even
45979 2exp340mod341
45999 8exp8mod9
46002 |