Colors of
variables: wff
setvar class |
Syntax hints: class class
class wbr 5104 (class class class)co 7350
1c1 10986 + caddc 10988 < clt 11123
2c2 12142 |
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-10 2138 ax-11 2155 ax-12 2172 ax-ext 2709 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7663 ax-resscn 11042 ax-1cn 11043 ax-icn 11044 ax-addcl 11045 ax-addrcl 11046 ax-mulcl 11047 ax-mulrcl 11048 ax-mulcom 11049 ax-addass 11050 ax-mulass 11051 ax-distr 11052 ax-i2m1 11053 ax-1ne0 11054 ax-1rid 11055 ax-rnegex 11056 ax-rrecex 11057 ax-cnre 11058 ax-pre-lttri 11059 ax-pre-lttrn 11060 ax-pre-ltadd 11061 ax-pre-mulgt0 11062 |
This theorem depends on definitions:
df-bi 206 df-an 398
df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2888 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-reu 3353 df-rab 3407 df-v 3446 df-sbc 3739 df-csb 3855 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5529 df-po 5543 df-so 5544 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-iota 6444 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7306 df-ov 7353 df-oprab 7354 df-mpo 7355 df-er 8582 df-en 8818 df-dom 8819 df-sdom 8820 df-pnf 11125 df-mnf 11126 df-xr 11127 df-ltxr 11128 df-le 11129 df-sub 11321 df-neg 11322 df-2 12150 |
This theorem is referenced by: 1lt3
12260 1lt4
12263 1lt6
12272 1lt7
12278 1lt8
12285 1lt9
12293 1ne2
12295 1le2
12296 halflt1
12305 nn0n0n1ge2b
12415 nn0ge2m1nn
12416 halfnz
12512 1lt10
12690 fztpval
13432 ige2m2fzo
13564 faclbnd5
14126 hashgt23el
14252 hashfun
14265 hashge2el2dif
14307 wrdlenge2n0
14368 ccat2s1p2
14446 s3fv1
14713 pfx2
14768 wwlktovf
14779 sqrt2gt1lt2
15094 ege2le3
15907 ene1
16027 mod2eq1n2dvds
16164 bits0o
16245 bitsfzolem
16249 bitsfzo
16250 bitsfi
16252 2prm
16503 4nprm
16506 iserodd
16642 dec2dvds
16870 dec5nprm
16873 dec2nprm
16874 2expltfac
16900 5prm
16916 6nprm
16917 7prm
16918 8nprm
16919 10nprm
16921 11prm
16922 13prm
16923 17prm
16924 19prm
16925 37prm
16928 83prm
16930 317prm
16933 631prm
16934 basendxltplusgndx
17097 grpstr
17100 grpbaseOLD
17103 grpplusgOLD
17105 rngstr
17114 lmodstr
17141 topgrpstr
17177 psgnunilem2
19209 isnzr2hash
20657 dyadss
24880 opnmbllem
24887 lhop1lem
25299 aaliou3lem8
25627 zetacvg
26286 lgamgulmlem4
26303 ppi1
26435 cht1
26436 chtrpcl
26446 ppiltx
26448 chtub
26482 chpval2
26488 mersenne
26497 perfectlem1
26499 perfectlem2
26500 bpos1
26553 bposlem1
26554 bposlem6
26559 bposlem7
26560 bposlem8
26561 lgseisenlem1
26645 2sqblem
26701 chebbnd1lem1
26739 chebbnd1lem3
26741 chebbnd1
26742 chtppilimlem1
26743 chtppilimlem2
26744 chtppilim
26745 chto1ub
26746 chebbnd2
26747 chto1lb
26748 mulog2sumlem2
26805 pntrmax
26834 pntrlog2bndlem2
26848 pntrlog2bndlem4
26850 pntpbnd1a
26855 pntibndlem3
26862 pntibnd
26863 pntlemb
26867 pntlemk
26876 pnt
26884 axlowdim
27696 lfgrnloop
27862 lfuhgr1v0e
27988 nbusgrvtxm1
28113 cusgrsizeindb1
28184 lfgrwlkprop
28421 usgr2pthlem
28497 uspgrn2crct
28539 clwlkclwwlklem2fv2
28726 clwwlkext2edg
28786 eupth2lem3lem4
28961 ex-mod
29179 9p10ne21
29200 cshw1s2
31596 fib1
32761 ballotlem2
32849 chtvalz
33003 hgt750lemd
33022 hgt750lem
33025 hgt750leme
33032 lfuhgr2
33473 subfacp1lem1
33534 subfacp1lem5
33539 knoppndvlem12
34872 knoppndvlem18
34878 relowlpssretop
35721 tan2h
35956 opnmbllem0
36000 heiborlem7
36162 lcmineqlem22
40393 3lexlogpow5ineq2
40398 3lexlogpow5ineq4
40399 3lexlogpow5ineq3
40400 3lexlogpow2ineq1
40401 3lexlogpow2ineq2
40402 3lexlogpow5ineq5
40403 aks4d1lem1
40405 dvrelog2b
40409 dvrelogpow2b
40411 aks4d1p1p3
40412 aks4d1p1p2
40413 aks4d1p1p4
40414 aks4d1p1p6
40416 aks4d1p1p7
40417 aks4d1p1p5
40418 aks4d1p1
40419 aks4d1p2
40420 aks4d1p3
40421 aks4d1p5
40423 aks4d1p6
40424 aks4d1p7d1
40425 aks4d1p7
40426 aks4d1p8
40430 aks4d1p9
40431 flt4lem7
40831 pellfundgt1
41040 stoweidlem13
43976 stoweidlem26
43989 wallispilem4
44031 wallispi
44033 wallispi2lem1
44034 wallispi2lem2
44035 wallispi2
44036 stirlinglem1
44037 dirkertrigeqlem1
44061 dirkercncflem1
44066 fouriersw
44194 etransclem23
44220 salexct2
44302 fmtnoge3
45440 fmtnof1
45445 fmtno4prm
45485 2pwp1prm
45499 127prm
45509 sfprmdvdsmersenne
45513 lighneallem2
45516 dfodd4
45569 perfectALTVlem1
45631 perfectALTVlem2
45632 nnsum4primesevenALTV
45711 cznnring
45972 pw2m1lepw2m1
46319 difmodm1lt
46326 rege1logbzge0
46363 logbpw2m1
46371 fllog2
46372 blenpw2m1
46383 nnpw2blen
46384 dignn0flhalflem1
46419 |