Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 (class class class)co 7361
ℝcr 11058 1c1 11060
+ caddc 11062 5c5 12219
6c6 12220 |
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 2704 ax-1cn 11117 ax-icn 11118 ax-addcl 11119 ax-addrcl 11120 ax-mulcl 11121 ax-mulrcl 11122 ax-i2m1 11127 ax-1ne0 11128 ax-rrecex 11131 ax-cnre 11132 |
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 2711 df-cleq 2725 df-clel 2811 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-br 5110 df-iota 6452 df-fv 6508 df-ov 7364 df-2 12224 df-3 12225
df-4 12226 df-5 12227
df-6 12228 |
This theorem is referenced by: 7re
12254 7pos
12272 4lt6
12343 3lt6
12344 2lt6
12345 1lt6
12346 6lt7
12347 5lt7
12348 6lt8
12354 5lt8
12355 6lt9
12362 5lt9
12363 8th4div3
12381 halfpm6th
12382 div4p1lem1div2
12416 6lt10
12760 5lt10
12761 5recm6rec
12770 bpoly2
15948 bpoly3
15949 efi4p
16027 resin4p
16028 recos4p
16029 ef01bndlem
16074 sin01bnd
16075 cos01bnd
16076 slotsdifipndx
17224 slotstnscsi
17249 plendxnvscandx
17263 slotsdnscsi
17281 lt6abl
19680 sralemOLD
20684 sravscaOLD
20694 zlmlemOLD
20941 sincos6thpi
25895 pigt3
25897 basellem5
26457 basellem8
26460 basellem9
26461 ppiublem1
26573 ppiublem2
26574 ppiub
26575 chtub
26583 bposlem6
26660 bposlem8
26662 slotsinbpsd
27432 slotslnbpsd
27433 ex-res
29434 zlmdsOLD
32608 zlmtsetOLD
32610 hgt750lemd
33325 hgt750lem2
33329 hgt750leme
33335 problem4
34320 problem5
34321 gbegt5
46043 gbowgt5
46044 gbowge7
46045 gboge9
46046 sbgoldbwt
46059 sgoldbeven3prm
46065 mogoldbb
46067 sbgoldbo
46069 nnsum3primesle9
46076 nnsum4primesodd
46078 wtgoldbnnsum4prm
46084 bgoldbnnsum3prm
46086 pgrple2abl
46531 |