Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2104
≠ wne 2938 (class class class)co 7411
ℝcr 11111 0cc0 11112
/ cdiv 11875 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911
ax-6 1969 ax-7 2009 ax-8 2106
ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2701 ax-sep 5298 ax-nul 5305 ax-pow 5362 ax-pr 5426 ax-un 7727 ax-resscn 11169 ax-1cn 11170 ax-icn 11171 ax-addcl 11172 ax-addrcl 11173 ax-mulcl 11174 ax-mulrcl 11175 ax-mulcom 11176 ax-addass 11177 ax-mulass 11178 ax-distr 11179 ax-i2m1 11180 ax-1ne0 11181 ax-1rid 11182 ax-rnegex 11183 ax-rrecex 11184 ax-cnre 11185 ax-pre-lttri 11186 ax-pre-lttrn 11187 ax-pre-ltadd 11188 ax-pre-mulgt0 11189 |
This theorem depends on definitions:
df-bi 206 df-an 395
df-or 844 df-3or 1086 df-3an 1087 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2532 df-eu 2561 df-clab 2708 df-cleq 2722 df-clel 2808 df-nfc 2883 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3374 df-reu 3375 df-rab 3431 df-v 3474 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-pw 4603 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-mpt 5231 df-id 5573 df-po 5587 df-so 5588 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6494 df-fun 6544 df-fn 6545 df-f 6546 df-f1 6547 df-fo 6548 df-f1o 6549 df-fv 6550 df-riota 7367 df-ov 7414 df-oprab 7415 df-mpo 7416 df-er 8705 df-en 8942 df-dom 8943 df-sdom 8944 df-pnf 11254 df-mnf 11255 df-xr 11256 df-ltxr 11257 df-le 11258 df-sub 11450 df-neg 11451 df-div 11876 |
This theorem is referenced by: recp1lt1
12116 ledivp1
12120 supmul1
12187 rimul
12207 div4p1lem1div2
12471 divelunit
13475 fldiv4p1lem1div2
13804 fldiv4lem1div2uz2
13805 quoremz
13824 intfracq
13828 fldiv
13829 modmulnn
13858 modmuladd
13882 modmuladdnn0
13884 expnbnd
14199 discr1
14206 discr
14207 sqreulem
15310 fprodle
15944 fldivndvdslt
16361 flodddiv4t2lthalf
16363 iccpnfhmeo
24690 ipcau2
24982 mbfmulc2lem
25396 i1fmulc
25453 itg1mulc
25454 itg2monolem3
25502 dvferm2lem
25738 dvcvx
25772 radcnvlem1
26161 tanord1
26282 logf1o2
26394 relogbcl
26514 ang180lem2
26551 chordthmlem2
26574 jensenlem2
26728 regamcl
26801 gausslemma2dlem0d
27098 gausslemma2dlem3
27107 gausslemma2dlem4
27108 gausslemma2dlem5
27110 2lgslem1a2
27129 2lgslem1
27133 2lgslem2
27134 2lgsoddprmlem2
27148 selberg3lem1
27296 selberg4lem1
27299 ostth2
27376 ttgcontlem1
28409 colinearalg
28435 axsegconlem8
28449 axpaschlem
28465 axeuclidlem
28487 nmophmi
31551 unitdivcld
33179 dya2icoseg
33574 dya2iocucvr
33581 signsply0
33860 logdivsqrle
33960 hgt750lem
33961 hgt750leme
33968 tgoldbachgtde
33970 sinccvglem
34955 circum
34957 knoppndvlem1
35691 knoppndvlem14
35704 knoppndvlem15
35705 knoppndvlem17
35707 knoppndvlem18
35708 knoppndvlem19
35709 knoppndvlem21
35711 poimirlem31
36822 itg2addnclem
36842 itg2addnclem2
36843 areacirclem1
36879 areacirclem4
36882 lcmineqlem15
41214 3lexlogpow5ineq2
41226 3lexlogpow5ineq4
41227 3lexlogpow2ineq1
41229 3lexlogpow2ineq2
41230 3lexlogpow5ineq5
41231 dvrelog2
41235 dvrelog3
41236 dvrelog2b
41237 dvrelogpow2b
41239 aks4d1p1p4
41242 aks4d1p1p6
41244 aks4d1p1p7
41245 aks4d1p1p5
41246 aks4d1p5
41251 aks4d1p8
41258 2ap1caineq
41267 pellexlem1
41869 pellexlem6
41874 reglogcl
41930 modabsdifz
42027 areaquad
42267 imo72b2
43226 hashnzfzclim
43383 sineq0ALT
44000 suplesup
44347 reclt0d
44395 xrralrecnnge
44398 ltdiv23neg
44402 iooiinioc
44567 0ellimcdiv
44663 dvdivbd
44937 ioodvbdlimc1lem1
44945 ioodvbdlimc1lem2
44946 ioodvbdlimc2lem
44948 stoweidlem1
45015 stoweidlem13
45027 stoweidlem26
45040 stoweidlem34
45048 stoweidlem36
45050 stoweidlem51
45065 stoweidlem60
45074 wallispilem4
45082 wallispilem5
45083 stirlingr
45104 dirker2re
45106 dirkerval2
45108 dirkerre
45109 dirkertrigeq
45115 dirkeritg
45116 dirkercncflem1
45117 dirkercncflem4
45120 fourierdlem4
45125 fourierdlem7
45128 fourierdlem9
45130 fourierdlem16
45137 fourierdlem19
45140 fourierdlem21
45142 fourierdlem22
45143 fourierdlem24
45145 fourierdlem26
45147 fourierdlem30
45151 fourierdlem39
45160 fourierdlem41
45162 fourierdlem42
45163 fourierdlem43
45164 fourierdlem47
45167 fourierdlem48
45168 fourierdlem49
45169 fourierdlem51
45171 fourierdlem56
45176 fourierdlem57
45177 fourierdlem58
45178 fourierdlem59
45179 fourierdlem63
45183 fourierdlem64
45184 fourierdlem66
45186 fourierdlem71
45191 fourierdlem72
45192 fourierdlem78
45198 fourierdlem83
45203 fourierdlem87
45207 fourierdlem89
45209 fourierdlem90
45210 fourierdlem91
45211 fourierdlem95
45215 fourierdlem103
45223 fourierdlem104
45224 etransclem48
45296 qndenserrnbllem
45308 sge0rpcpnf
45435 sge0ad2en
45445 ovnsubaddlem1
45584 hoidmvlelem3
45611 ovolval5lem1
45666 ovolval5lem2
45667 vonioolem2
45695 vonicclem2
45698 pimrecltneg
45738 smfrec
45803 smfdiv
45811 sigardiv
45875 lighneallem2
46572 requad01
46587 requad1
46588 requad2
46589 modn0mul
47293 refdivmptf
47315 fldivexpfllog2
47338 dignnld
47376 dig2nn1st
47378 dig2bits
47387 dignn0flhalflem2
47389 affinecomb1
47475 eenglngeehlnmlem1
47510 eenglngeehlnmlem2
47511 rrx2vlinest
47514 line2ylem
47524 line2
47525 line2xlem
47526 itsclc0lem1
47529 itsclc0lem2
47530 itscnhlc0yqe
47532 itsclquadb
47549 |