Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
≠ wne 2940 (class class class)co 7361
ℝcr 11058 0cc0 11059
/ cdiv 11820 |
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 2704 ax-sep 5260 ax-nul 5267 ax-pow 5324 ax-pr 5388 ax-un 7676 ax-resscn 11116 ax-1cn 11117 ax-icn 11118 ax-addcl 11119 ax-addrcl 11120 ax-mulcl 11121 ax-mulrcl 11122 ax-mulcom 11123 ax-addass 11124 ax-mulass 11125 ax-distr 11126 ax-i2m1 11127 ax-1ne0 11128 ax-1rid 11129 ax-rnegex 11130 ax-rrecex 11131 ax-cnre 11132 ax-pre-lttri 11133 ax-pre-lttrn 11134 ax-pre-ltadd 11135 ax-pre-mulgt0 11136 |
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 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3352 df-reu 3353 df-rab 3407 df-v 3449 df-sbc 3744 df-csb 3860 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-pw 4566 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-br 5110 df-opab 5172 df-mpt 5193 df-id 5535 df-po 5549 df-so 5550 df-xp 5643 df-rel 5644 df-cnv 5645 df-co 5646 df-dm 5647 df-rn 5648 df-res 5649 df-ima 5650 df-iota 6452 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7317 df-ov 7364 df-oprab 7365 df-mpo 7366 df-er 8654 df-en 8890 df-dom 8891 df-sdom 8892 df-pnf 11199 df-mnf 11200 df-xr 11201 df-ltxr 11202 df-le 11203 df-sub 11395 df-neg 11396 df-div 11821 |
This theorem is referenced by: recp1lt1
12061 ledivp1
12065 supmul1
12132 rimul
12152 div4p1lem1div2
12416 divelunit
13420 fldiv4p1lem1div2
13749 fldiv4lem1div2uz2
13750 quoremz
13769 intfracq
13773 fldiv
13774 modmulnn
13803 modmuladd
13827 modmuladdnn0
13829 expnbnd
14144 discr1
14151 discr
14152 sqreulem
15253 fprodle
15887 fldivndvdslt
16304 flodddiv4t2lthalf
16306 iccpnfhmeo
24331 ipcau2
24621 mbfmulc2lem
25034 i1fmulc
25091 itg1mulc
25092 itg2monolem3
25140 dvferm2lem
25373 dvcvx
25407 radcnvlem1
25795 tanord1
25916 logf1o2
26028 relogbcl
26146 ang180lem2
26183 chordthmlem2
26206 jensenlem2
26360 regamcl
26433 gausslemma2dlem0d
26730 gausslemma2dlem3
26739 gausslemma2dlem4
26740 gausslemma2dlem5
26742 2lgslem1a2
26761 2lgslem1
26765 2lgslem2
26766 2lgsoddprmlem2
26780 selberg3lem1
26928 selberg4lem1
26931 ostth2
27008 ttgcontlem1
27882 colinearalg
27908 axsegconlem8
27922 axpaschlem
27938 axeuclidlem
27960 nmophmi
31022 unitdivcld
32546 dya2icoseg
32941 dya2iocucvr
32948 signsply0
33227 logdivsqrle
33327 hgt750lem
33328 hgt750leme
33335 tgoldbachgtde
33337 sinccvglem
34324 circum
34326 knoppndvlem1
35028 knoppndvlem14
35041 knoppndvlem15
35042 knoppndvlem17
35044 knoppndvlem18
35045 knoppndvlem19
35046 knoppndvlem21
35048 poimirlem31
36159 itg2addnclem
36179 itg2addnclem2
36180 areacirclem1
36216 areacirclem4
36219 lcmineqlem15
40550 3lexlogpow5ineq2
40562 3lexlogpow5ineq4
40563 3lexlogpow2ineq1
40565 3lexlogpow2ineq2
40566 3lexlogpow5ineq5
40567 dvrelog2
40571 dvrelog3
40572 dvrelog2b
40573 dvrelogpow2b
40575 aks4d1p1p4
40578 aks4d1p1p6
40580 aks4d1p1p7
40581 aks4d1p1p5
40582 aks4d1p5
40587 aks4d1p8
40594 2ap1caineq
40603 pellexlem1
41199 pellexlem6
41204 reglogcl
41260 modabsdifz
41357 areaquad
41597 imo72b2
42537 hashnzfzclim
42694 sineq0ALT
43311 suplesup
43664 reclt0d
43712 xrralrecnnge
43715 ltdiv23neg
43719 iooiinioc
43884 0ellimcdiv
43980 dvdivbd
44254 ioodvbdlimc1lem1
44262 ioodvbdlimc1lem2
44263 ioodvbdlimc2lem
44265 stoweidlem1
44332 stoweidlem13
44344 stoweidlem26
44357 stoweidlem34
44365 stoweidlem36
44367 stoweidlem51
44382 stoweidlem60
44391 wallispilem4
44399 wallispilem5
44400 stirlingr
44421 dirker2re
44423 dirkerval2
44425 dirkerre
44426 dirkertrigeq
44432 dirkeritg
44433 dirkercncflem1
44434 dirkercncflem4
44437 fourierdlem4
44442 fourierdlem7
44445 fourierdlem9
44447 fourierdlem16
44454 fourierdlem19
44457 fourierdlem21
44459 fourierdlem22
44460 fourierdlem24
44462 fourierdlem26
44464 fourierdlem30
44468 fourierdlem39
44477 fourierdlem41
44479 fourierdlem42
44480 fourierdlem43
44481 fourierdlem47
44484 fourierdlem48
44485 fourierdlem49
44486 fourierdlem51
44488 fourierdlem56
44493 fourierdlem57
44494 fourierdlem58
44495 fourierdlem59
44496 fourierdlem63
44500 fourierdlem64
44501 fourierdlem66
44503 fourierdlem71
44508 fourierdlem72
44509 fourierdlem78
44515 fourierdlem83
44520 fourierdlem87
44524 fourierdlem89
44526 fourierdlem90
44527 fourierdlem91
44528 fourierdlem95
44532 fourierdlem103
44540 fourierdlem104
44541 etransclem48
44613 qndenserrnbllem
44625 sge0rpcpnf
44752 sge0ad2en
44762 ovnsubaddlem1
44901 hoidmvlelem3
44928 ovolval5lem1
44983 ovolval5lem2
44984 vonioolem2
45012 vonicclem2
45015 pimrecltneg
45055 smfrec
45120 smfdiv
45128 sigardiv
45192 lighneallem2
45888 requad01
45903 requad1
45904 requad2
45905 modn0mul
46696 refdivmptf
46718 fldivexpfllog2
46741 dignnld
46779 dig2nn1st
46781 dig2bits
46790 dignn0flhalflem2
46792 affinecomb1
46878 eenglngeehlnmlem1
46913 eenglngeehlnmlem2
46914 rrx2vlinest
46917 line2ylem
46927 line2
46928 line2xlem
46929 itsclc0lem1
46932 itsclc0lem2
46933 itscnhlc0yqe
46935 itsclquadb
46952 |