Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
≠ wne 2941 class class class wbr 5149
ℝcr 11109 0cc0 11110
< clt 11248 |
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 2704 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-resscn 11167 ax-1cn 11168 ax-addrcl 11171 ax-rnegex 11181 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 |
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 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-ltxr 11253 |
This theorem is referenced by: recextlem2
11845 prodgt0
12061 ltdiv1
12078 ltmuldiv
12087 ltrec
12096 lerec
12097 lediv12a
12107 recp1lt1
12112 ledivp1
12116 supmul1
12183 nnne0
12246 rpnnen1lem5
12965 ltexp2a
14131 leexp2
14136 leexp2a
14137 expnbnd
14195 expmulnbnd
14198 discr1
14202 eqsqrt2d
15315 bpoly4
16003 isabvd
20428 gzrngunit
21011 fvmptnn04ifa
22352 chfacffsupp
22358 chfacfscmul0
22360 chfacfpmmul0
22364 stdbdxmet
24024 evth
24475 itg2monolem3
25270 mvth
25509 dvlip
25510 dvcvx
25537 ftc1lem4
25556 dgradd2
25782 radcnvlem1
25925 pilem2
25964 coseq00topi
26012 tangtx
26015 tanabsge
26016 cos02pilt1
26035 tanord1
26046 logcnlem4
26153 cxplt
26202 atantan
26428 jensenlem2
26492 jensen
26493 lgamgulmlem2
26534 basellem3
26587 basellem4
26588 basellem8
26592 dchrmusumlema
26996 selberg3lem1
27060 abvcxp
27118 ostth2
27140 axsegconlem8
28213 axsegconlem9
28214 axsegconlem10
28215 axpaschlem
28229 axcontlem2
28254 axcontlem4
28256 axcontlem7
28259 iswwlksnx
29125 wspn0
29209 friendshipgt3
29682 his6
30383 eigrei
31118 cycpmco2lem4
32319 cycpmco2lem5
32320 finexttrb
32772 xrge0iifcv
32945 sgnmul
33572 sgn0bi
33577 sgnmulsgp
33580 signsvfpn
33627 tgoldbachgtde
33703 tgoldbachgtda
33704 lfuhgr2
34140 knoppndvlem18
35453 knoppndvlem19
35454 knoppndvlem21
35456 ftc1cnnclem
36607 areacirclem1
36624 3lexlogpow2ineq1
40971 3lexlogpow2ineq2
40972 3lexlogpow5ineq5
40973 aks4d1p1p6
40986 sn-nnne0
41369 3cubeslem2
41471 irrapxlem2
41609 irrapxlem5
41612 pellexlem2
41616 imo72b2
42972 binomcxplemnotnn0
43163 dvdivbd
44687 dvbdfbdioolem1
44692 ioodvbdlimc1lem1
44695 ioodvbdlimc1lem2
44696 ioodvbdlimc2lem
44698 stoweidlem7
44771 stoweidlem36
44800 wallispilem3
44831 wallispilem4
44832 wallispi2lem1
44835 wallispi2lem2
44836 stirlinglem3
44840 stirlinglem6
44843 stirlinglem7
44844 stirlinglem10
44847 stirlinglem11
44848 stirlinglem12
44849 stirlinglem13
44850 stirlinglem14
44851 stirlinglem15
44852 dirkerval2
44858 dirkeritg
44866 dirkercncflem2
44868 fourierdlem6
44877 fourierdlem7
44878 fourierdlem19
44890 fourierdlem26
44897 fourierdlem30
44901 fourierdlem48
44918 fourierdlem49
44919 fourierdlem51
44921 fourierdlem63
44933 fourierdlem64
44934 fourierdlem71
44941 fourierdlem89
44959 fourierdlem90
44960 fourierdlem91
44961 fourierdlem103
44973 fourierdlem104
44974 fourierdlem112
44982 sqwvfoura
44992 fourierswlem
44994 etransclem4
45002 etransclem31
45029 etransclem32
45030 iccpartgt
46143 rege1logbrege0
47292 itcovalsuc
47401 ackvalsuc1mpt
47412 eenglngeehlnmlem2
47472 itsclc0yqsol
47498 itscnhlc0xyqsol
47499 itsclc0xyqsolr
47503 itsclinecirc0in
47509 itscnhlinecirc02p
47519 inlinecirc02plem
47520 |