Colors of
variables: wff set class |
Syntax hints:
∈ wcel 2148 (class class class)co 5875
ℝcr 7810 1c1 7812
+ caddc 7814 2c2 8970 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1447 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-4 1510 ax-17 1526 ax-ial 1534 ax-ext 2159 ax-1re 7905 ax-addrcl 7908 |
This theorem depends on definitions:
df-bi 117 df-cleq 2170 df-clel 2173 df-2 8978 |
This theorem is referenced by: 2cn
8990 3re
8993 2ne0
9011 2ap0
9012 3pos
9013 2lt3
9089 1lt3
9090 2lt4
9092 1lt4
9093 2lt5
9096 2lt6
9101 1lt6
9102 2lt7
9107 1lt7
9108 2lt8
9114 1lt8
9115 2lt9
9122 1lt9
9123 1ap2
9126 1le2
9127 2rene0
9129 halfre
9132 halfgt0
9134 halflt1
9136 rehalfcl
9146 halfpos2
9149 halfnneg2
9151 addltmul
9155 nominpos
9156 avglt1
9157 avglt2
9158 div4p1lem1div2
9172 nn0lele2xi
9227 nn0ge2m1nn
9236 halfnz
9349 3halfnz
9350 2lt10
9521 1lt10
9522 eluz4eluz2
9567 uzuzle23
9571 uz3m2nn
9573 2rp
9658 xleaddadd
9887 fztpval
10083 fz0to4untppr
10124 fzo0to42pr
10220 qbtwnrelemcalc
10256 qbtwnre
10257 2tnp1ge0ge0
10301 flhalf
10302 fldiv4p1lem1div2
10305 mulp1mod1
10365 expubnd
10577 nn0opthlem2d
10701 faclbnd2
10722 4bc2eq6
10754 cvg1nlemres
10994 resqrexlemover
11019 resqrexlemga
11032 sqrt4
11056 sqrt2gt1lt2
11058 abstri
11113 amgm2
11127 maxabslemlub
11216 maxltsup
11227 bdtrilem
11247 efcllemp
11666 efcllem
11667 ege2le3
11679 ef01bndlem
11764 cos01bnd
11766 cos2bnd
11768 cos01gt0
11770 sin02gt0
11771 sincos2sgn
11773 sin4lt0
11774 cos12dec
11775 eirraplem
11784 egt2lt3
11787 epos
11788 ene1
11792 eap1
11793 oexpneg
11882 oddge22np1
11886 evennn02n
11887 evennn2n
11888 nn0ehalf
11908 nno
11911 nn0o
11912 nn0oddm1d2
11914 nnoddm1d2
11915 flodddiv4t2lthalf
11942 6gcd4e2
11996 ncoprmgcdne1b
12089 prmdc
12130 3lcm2e6
12160 sqrt2irrlem
12161 sqrt2re
12163 sqrt2irraplemnn
12179 sqrt2irrap
12180 plusgndxnmulrndx
12591 starvndxnplusgndx
12601 scandxnplusgndx
12613 vscandxnplusgndx
12618 ipndxnplusgndx
12631 tsetndxnplusgndx
12647 plendxnplusgndx
12661 dsndxnplusgndx
12672 slotsdifunifndx
12683 bl2in
13906 reeff1o
14197 cosz12
14204 sin0pilem1
14205 sin0pilem2
14206 pilem3
14207 pipos
14212 sinhalfpilem
14215 sincosq1lem
14249 sincosq4sgn
14253 sinq12gt0
14254 cosq23lt0
14257 coseq00topi
14259 coseq0negpitopi
14260 tangtx
14262 sincos4thpi
14264 tan4thpi
14265 sincos6thpi
14266 cosordlem
14273 cosq34lt1
14274 cos02pilt1
14275 cos0pilt1
14276 2logb9irr
14392 2logb3irr
14394 2logb9irrALT
14395 sqrt2cxp2logb9e3
14396 2logb9irrap
14398 lgslem1
14404 lgsdirprm
14438 lgseisenlem1
14453 lgseisenlem2
14454 ex-fl
14480 taupi
14823 |