Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2105
class class class wbr 5149 (class class class)co 7412
ℝcr 11112 + caddc 11116 < clt 11253 |
This theorem was proved from axioms:
ax-mp 5 ax-1 6 ax-2 7
ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912
ax-6 1970 ax-7 2010 ax-8 2107
ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7728 ax-resscn 11170 ax-addrcl 11174 ax-pre-lttri 11187 ax-pre-ltadd 11189 |
This theorem depends on definitions:
df-bi 206 df-an 396
df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 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-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-ov 7415 df-er 8706 df-en 8943 df-dom 8944 df-sdom 8945 df-pnf 11255 df-mnf 11256 df-ltxr 11258 |
This theorem is referenced by: zltaddlt1le
13487 2tnp1ge0ge0
13799 ccatrn
14544 eirrlem
16152 prmreclem5
16858 iccntr
24558 icccmplem2
24560 ivthlem2
25202 uniioombllem3
25335 opnmbllem
25351 dvcnvre
25769 cosordlem
26272 efif1olem2
26285 atanlogaddlem
26651 pntibndlem2
27327 pntlemr
27338 dya2icoseg
33571 opnmbllem0
36828 fltnltalem
41707 binomcxplemdvbinom
43415 zltlesub
44295 supxrge
44348 ltadd12dd
44353 xrralrecnnle
44393 0ellimcdiv
44665 climleltrp
44692 ioodvbdlimc1lem2
44948 stoweidlem11
45027 stoweidlem14
45030 stoweidlem26
45042 stoweidlem44
45060 dirkertrigeqlem3
45116 dirkercncflem1
45119 dirkercncflem2
45120 fourierdlem4
45127 fourierdlem10
45133 fourierdlem28
45151 fourierdlem40
45163 fourierdlem50
45172 fourierdlem57
45179 fourierdlem59
45181 fourierdlem60
45182 fourierdlem61
45183 fourierdlem68
45190 fourierdlem74
45196 fourierdlem75
45197 fourierdlem76
45198 fourierdlem78
45200 fourierdlem79
45201 fourierdlem84
45206 fourierdlem93
45215 fourierdlem111
45233 fouriersw
45247 smfaddlem1
45779 smflimlem3
45789 |