Colors of
variables: wff
setvar class |
Syntax hints: class class
class wbr 5139 (class class class)co 7402
0cc0 11107 1c1 11108
+ caddc 11110 ≤
cle 11247 2c2 12265 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905
ax-6 1963 ax-7 2003 ax-8 2100
ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2163 ax-ext 2695 ax-sep 5290 ax-nul 5297 ax-pow 5354 ax-pr 5418 ax-un 7719 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 845 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2526 df-eu 2555 df-clab 2702 df-cleq 2716 df-clel 2802 df-nfc 2877 df-ne 2933 df-nel 3039 df-ral 3054 df-rex 3063 df-reu 3369 df-rab 3425 df-v 3468 df-sbc 3771 df-csb 3887 df-dif 3944 df-un 3946 df-in 3948 df-ss 3958 df-nul 4316 df-if 4522 df-pw 4597 df-sn 4622 df-pr 4624 df-op 4628 df-uni 4901 df-br 5140 df-opab 5202 df-mpt 5223 df-id 5565 df-po 5579 df-so 5580 df-xp 5673 df-rel 5674 df-cnv 5675 df-co 5676 df-dm 5677 df-rn 5678 df-res 5679 df-ima 5680 df-iota 6486 df-fun 6536 df-fn 6537 df-f 6538 df-f1 6539 df-fo 6540 df-f1o 6541 df-fv 6542 df-riota 7358 df-ov 7405 df-oprab 7406 df-mpo 7407 df-er 8700 df-en 8937 df-dom 8938 df-sdom 8939 df-pnf 11248 df-mnf 11249 df-xr 11250 df-ltxr 11251 df-le 11252 df-sub 11444 df-neg 11445 df-2 12273 |
This theorem is referenced by: expubnd
14140 4bc2eq6
14287 sqrt4
15217 sqrt2gt1lt2
15219 sqreulem
15304 amgm2
15314 efcllem
16019 ege2le3
16032 cos2bnd
16130 evennn2n
16293 6gcd4e2
16479 isprm7
16644 efgredleme
19655 abvtrivd
20675 zringndrg
21325 iihalf1
24776 minveclem2
25278 sincos4thpi
26367 tan4thpi
26368 2irrexpq
26584 log2tlbnd
26796 ppisval
26955 bposlem1
27136 bposlem8
27143 bposlem9
27144 lgslem1
27149 m1lgs
27240 2lgslem1a1
27241 2lgslem4
27258 2sqlem11
27281 2sq2
27285 2sqreultlem
27299 2sqreunnltlem
27302 dchrisumlem3
27343 mulog2sumlem2
27387 log2sumbnd
27396 chpdifbndlem1
27405 usgr2pthlem
29492 pthdlem2
29497 ex-abs
30180 nrt2irr
30198 ipidsq
30435 minvecolem2
30600 normpar2i
30881 wrdt2ind
32587 sqsscirc1
33380 nexple
33499 eulerpartlemgc
33853 knoppndvlem10
35888 knoppndvlem11
35889 knoppndvlem14
35892 lcm2un
41376 aks4d1p1p7
41436 2ap1caineq
41458 pellexlem2
42082 sqrtcval
42906 imo72b2lem0
43431 sumnnodd
44856 0ellimcdiv
44875 stoweidlem26
45252 wallispilem4
45294 wallispi
45296 wallispi2lem1
45297 wallispi2
45299 stirlinglem1
45300 stirlinglem5
45304 stirlinglem6
45305 stirlinglem7
45306 stirlinglem11
45310 stirlinglem15
45314 fourierdlem68
45400 fouriersw
45457 smfmullem4
46020 lighneallem4a
46786 fpprel2
46919 |