Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 (class class class)co 7361
ℝcr 11058 1c1 11060
+ caddc 11062 4c4 12218
5c5 12219 |
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 |
This theorem is referenced by: 6re
12251 6pos
12271 3lt5
12339 2lt5
12340 1lt5
12341 5lt6
12342 4lt6
12343 5lt7
12348 4lt7
12349 5lt8
12355 4lt8
12356 5lt9
12363 4lt9
12364 5lt10
12761 4lt10
12762 5recm6rec
12770 ef01bndlem
16074 prm23ge5
16695 prmlem1
16988 vscandxnscandx
17213 slotsdifipndx
17224 slotstnscsi
17249 plendxnscandx
17262 slotsdnscsi
17281 rmodislmodOLD
20435 sralemOLD
20684 srascaOLD
20692 zlmlemOLD
20941 ppiublem1
26573 ppiub
26575 bposlem3
26657 bposlem4
26658 bposlem5
26659 bposlem6
26660 bposlem8
26662 bposlem9
26663 lgsdir2lem1
26696 gausslemma2dlem4
26740 2lgslem3
26775 cchhllemOLD
27885 ex-id
29427 ex-sqrt
29447 threehalves
31827 cyc3conja
32062 resvvscaOLD
32183 zlmdsOLD
32608 zlmtsetOLD
32610 hgt750lem2
33329 hgt750leme
33335 problem2
34318 12gcd5e1
40510 lcmineqlem23
40558 3lexlogpow2ineq1
40565 3lexlogpow2ineq2
40566 aks4d1p1p4
40578 aks4d1p1p6
40580 aks4d1p1p7
40581 aks4d1p1p5
40582 stoweidlem13
44344 31prm
45879 gbegt5
46043 gbowgt5
46044 sbgoldbo
46069 nnsum3primesle9
46076 nnsum4primesodd
46078 evengpop3
46080 |