Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
≠ wne 2941 (class class class)co 7409
ℝcr 11109 0cc0 11110
/ cdiv 11871 |
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 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 ax-resscn 11167 ax-1cn 11168 ax-icn 11169 ax-addcl 11170 ax-addrcl 11171 ax-mulcl 11172 ax-mulrcl 11173 ax-mulcom 11174 ax-addass 11175 ax-mulass 11176 ax-distr 11177 ax-i2m1 11178 ax-1ne0 11179 ax-1rid 11180 ax-rnegex 11181 ax-rrecex 11182 ax-cnre 11183 ax-pre-lttri 11184 ax-pre-lttrn 11185 ax-pre-ltadd 11186 ax-pre-mulgt0 11187 |
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 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-po 5589 df-so 5590 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7365 df-ov 7412 df-oprab 7413 df-mpo 7414 df-er 8703 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11250 df-mnf 11251 df-xr 11252 df-ltxr 11253 df-le 11254 df-sub 11446 df-neg 11447 df-div 11872 |
This theorem is referenced by: recp1lt1
12112 ledivp1
12116 supmul1
12183 rimul
12203 div4p1lem1div2
12467 divelunit
13471 fldiv4p1lem1div2
13800 fldiv4lem1div2uz2
13801 quoremz
13820 intfracq
13824 fldiv
13825 modmulnn
13854 modmuladd
13878 modmuladdnn0
13880 expnbnd
14195 discr1
14202 discr
14203 sqreulem
15306 fprodle
15940 fldivndvdslt
16357 flodddiv4t2lthalf
16359 iccpnfhmeo
24461 ipcau2
24751 mbfmulc2lem
25164 i1fmulc
25221 itg1mulc
25222 itg2monolem3
25270 dvferm2lem
25503 dvcvx
25537 radcnvlem1
25925 tanord1
26046 logf1o2
26158 relogbcl
26278 ang180lem2
26315 chordthmlem2
26338 jensenlem2
26492 regamcl
26565 gausslemma2dlem0d
26862 gausslemma2dlem3
26871 gausslemma2dlem4
26872 gausslemma2dlem5
26874 2lgslem1a2
26893 2lgslem1
26897 2lgslem2
26898 2lgsoddprmlem2
26912 selberg3lem1
27060 selberg4lem1
27063 ostth2
27140 ttgcontlem1
28142 colinearalg
28168 axsegconlem8
28182 axpaschlem
28198 axeuclidlem
28220 nmophmi
31284 unitdivcld
32881 dya2icoseg
33276 dya2iocucvr
33283 signsply0
33562 logdivsqrle
33662 hgt750lem
33663 hgt750leme
33670 tgoldbachgtde
33672 sinccvglem
34657 circum
34659 knoppndvlem1
35388 knoppndvlem14
35401 knoppndvlem15
35402 knoppndvlem17
35404 knoppndvlem18
35405 knoppndvlem19
35406 knoppndvlem21
35408 poimirlem31
36519 itg2addnclem
36539 itg2addnclem2
36540 areacirclem1
36576 areacirclem4
36579 lcmineqlem15
40908 3lexlogpow5ineq2
40920 3lexlogpow5ineq4
40921 3lexlogpow2ineq1
40923 3lexlogpow2ineq2
40924 3lexlogpow5ineq5
40925 dvrelog2
40929 dvrelog3
40930 dvrelog2b
40931 dvrelogpow2b
40933 aks4d1p1p4
40936 aks4d1p1p6
40938 aks4d1p1p7
40939 aks4d1p1p5
40940 aks4d1p5
40945 aks4d1p8
40952 2ap1caineq
40961 pellexlem1
41567 pellexlem6
41572 reglogcl
41628 modabsdifz
41725 areaquad
41965 imo72b2
42924 hashnzfzclim
43081 sineq0ALT
43698 suplesup
44049 reclt0d
44097 xrralrecnnge
44100 ltdiv23neg
44104 iooiinioc
44269 0ellimcdiv
44365 dvdivbd
44639 ioodvbdlimc1lem1
44647 ioodvbdlimc1lem2
44648 ioodvbdlimc2lem
44650 stoweidlem1
44717 stoweidlem13
44729 stoweidlem26
44742 stoweidlem34
44750 stoweidlem36
44752 stoweidlem51
44767 stoweidlem60
44776 wallispilem4
44784 wallispilem5
44785 stirlingr
44806 dirker2re
44808 dirkerval2
44810 dirkerre
44811 dirkertrigeq
44817 dirkeritg
44818 dirkercncflem1
44819 dirkercncflem4
44822 fourierdlem4
44827 fourierdlem7
44830 fourierdlem9
44832 fourierdlem16
44839 fourierdlem19
44842 fourierdlem21
44844 fourierdlem22
44845 fourierdlem24
44847 fourierdlem26
44849 fourierdlem30
44853 fourierdlem39
44862 fourierdlem41
44864 fourierdlem42
44865 fourierdlem43
44866 fourierdlem47
44869 fourierdlem48
44870 fourierdlem49
44871 fourierdlem51
44873 fourierdlem56
44878 fourierdlem57
44879 fourierdlem58
44880 fourierdlem59
44881 fourierdlem63
44885 fourierdlem64
44886 fourierdlem66
44888 fourierdlem71
44893 fourierdlem72
44894 fourierdlem78
44900 fourierdlem83
44905 fourierdlem87
44909 fourierdlem89
44911 fourierdlem90
44912 fourierdlem91
44913 fourierdlem95
44917 fourierdlem103
44925 fourierdlem104
44926 etransclem48
44998 qndenserrnbllem
45010 sge0rpcpnf
45137 sge0ad2en
45147 ovnsubaddlem1
45286 hoidmvlelem3
45313 ovolval5lem1
45368 ovolval5lem2
45369 vonioolem2
45397 vonicclem2
45400 pimrecltneg
45440 smfrec
45505 smfdiv
45513 sigardiv
45577 lighneallem2
46274 requad01
46289 requad1
46290 requad2
46291 modn0mul
47206 refdivmptf
47228 fldivexpfllog2
47251 dignnld
47289 dig2nn1st
47291 dig2bits
47300 dignn0flhalflem2
47302 affinecomb1
47388 eenglngeehlnmlem1
47423 eenglngeehlnmlem2
47424 rrx2vlinest
47427 line2ylem
47437 line2
47438 line2xlem
47439 itsclc0lem1
47442 itsclc0lem2
47443 itscnhlc0yqe
47445 itsclquadb
47462 |