Colors of
variables: wff
setvar class |
Syntax hints:
= wceq 1541 (class class class)co 7405
0cc0 11106 1c1 11107
+ caddc 11109 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913
ax-6 1971 ax-7 2011 ax-8 2108
ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2703 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7721 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 |
This theorem depends on definitions:
df-bi 206 df-an 397
df-or 846 df-3or 1088 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2534 df-eu 2563 df-clab 2710 df-cleq 2724 df-clel 2810 df-nfc 2885 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rab 3433 df-v 3476 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-po 5587 df-so 5588 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-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-ov 7408 df-er 8699 df-en 8936 df-dom 8937 df-sdom 8938 df-pnf 11246 df-mnf 11247 df-ltxr 11249 |
This theorem is referenced by: 6p5e11
12746 7p4e11
12749 8p3e11
12754 9p2e11
12760 fz1ssfz0
13593 fz0to3un2pr
13599 fzo01
13710 bcp1nk
14273 pfx1
14649 arisum2
15803 ege2le3
16029 ef4p
16052 efgt1p2
16053 efgt1p
16054 bitsmod
16373 prmdiv
16714 prmreclem2
16846 vdwap1
16906 11prm
17044 631prm
17056 mulgnn0p1
18959 gsummptfzsplitl
19795 itgcnlem
25298 dveflem
25487 ply1rem
25672 vieta1lem2
25815 vieta1
25816 pserdvlem2
25931 pserdv2
25933 abelthlem6
25939 abelthlem9
25943 cosne0
26029 logf1o2
26149 logtayl
26159 ang180lem3
26305 birthdaylem2
26446 ftalem5
26570 ppi2
26663 ppiublem2
26695 ppiub
26696 bclbnd
26772 bposlem2
26777 lgsdir2lem3
26819 lgseisenlem1
26867 axlowdimlem13
28201 spthispth
28972 uhgrwkspthlem2
29000 upgr3v3e3cycl
29422 upgr4cycl4dv4e
29427 ballotlemii
33490 ballotlem1c
33494 subfacval2
34166 cvmliftlem5
34268 sticksstones11
40960 sticksstones12
40962 metakunt24
40996 3cubeslem1
41407 halffl
43992 sinaover2ne0
44570 stoweidlem11
44713 stoweidlem13
44715 stirlinglem7
44782 fourierdlem48
44856 fourierdlem49
44857 fourierdlem69
44877 fourierdlem79
44887 fourierdlem93
44901 etransclem7
44943 etransclem25
44961 etransclem26
44962 etransclem37
44973 tworepnotupword
45586 iccpartlt
46078 31prm
46251 1odd
46567 itcoval1
47302 ackval1
47320 ackval41a
47333 |