Colors of
variables: wff
setvar class |
Syntax hints:
∈ wcel 2107 (class class class)co 7358
ℝcr 11055 1c1 11057
+ caddc 11059 8c8 12219
9c9 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 11114 ax-icn 11115 ax-addcl 11116 ax-addrcl 11117 ax-mulcl 11118 ax-mulrcl 11119 ax-i2m1 11124 ax-1ne0 11125 ax-rrecex 11128 ax-cnre 11129 |
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 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-iota 6449 df-fv 6505 df-ov 7361 df-2 12221 df-3 12222
df-4 12223 df-5 12224
df-6 12225 df-7 12226
df-8 12227 df-9 12228 |
This theorem is referenced by: 7lt9
12358 6lt9
12359 5lt9
12360 4lt9
12361 3lt9
12362 2lt9
12363 1lt9
12364 10re
12642 9lt10
12754 8lt10
12755 0.999...
15771 cos2bnd
16075 sincos2sgn
16081 slotsdifplendx
17261 dsndxntsetndx
17279 unifndxntsetndx
17286 cnfldfunALTOLD
20826 tuslemOLD
23635 setsmsdsOLD
23847 tnglemOLD
24013 tngdsOLD
24028 2logb9irr
26161 sqrt2cxp2logb9e3
26165 log2tlbnd
26311 bposlem4
26651 bposlem5
26652 bposlem7
26654 bposlem8
26655 bposlem9
26656 ex-fv
29429 dp2lt10
31789 hgt750lem
33321 hgt750lem2
33322 hgt750leme
33328 problem5
34314 60gcd7e1
40508 lcmineqlem23
40554 3lexlogpow5ineq1
40557 3lexlogpow5ineq2
40558 3lexlogpow5ineq4
40559 3lexlogpow5ineq3
40560 3lexlogpow2ineq2
40562 3lexlogpow5ineq5
40563 aks4d1lem1
40565 aks4d1p1
40579 aks4d1p6
40584 aks4d1p7d1
40585 aks4d1p7
40586 aks4d1p8
40590 31prm
45875 2exp340mod341
46011 341fppr2
46012 9fppr8
46015 nfermltl8rev
46020 nfermltl2rev
46021 wtgoldbnnsum4prm
46080 bgoldbnnsum3prm
46082 bgoldbtbndlem1
46083 ackval42
46868 |