Colors of
variables: wff
setvar class |
Syntax hints:
→ wi 4 ∈ wcel 2107
‘cfv 6497 ℝcr 11055 ⌊cfl 13701 |
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 5257 ax-nul 5264 ax-pow 5321 ax-pr 5385 ax-un 7673 ax-cnex 11112 ax-resscn 11113 ax-1cn 11114 ax-icn 11115 ax-addcl 11116 ax-addrcl 11117 ax-mulcl 11118 ax-mulrcl 11119 ax-mulcom 11120 ax-addass 11121 ax-mulass 11122 ax-distr 11123 ax-i2m1 11124 ax-1ne0 11125 ax-1rid 11126 ax-rnegex 11127 ax-rrecex 11128 ax-cnre 11129 ax-pre-lttri 11130 ax-pre-lttrn 11131 ax-pre-ltadd 11132 ax-pre-mulgt0 11133 ax-pre-sup 11134 |
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 3446 df-sbc 3741 df-csb 3857 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-pss 3930 df-nul 4284 df-if 4488 df-pw 4563 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-iun 4957 df-br 5107 df-opab 5169 df-mpt 5190 df-tr 5224 df-id 5532 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5589 df-we 5591 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-pred 6254 df-ord 6321 df-on 6322 df-lim 6323 df-suc 6324 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-fv 6505 df-riota 7314 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7804 df-2nd 7923 df-frecs 8213 df-wrecs 8244 df-recs 8318 df-rdg 8357 df-er 8651 df-en 8887 df-dom 8888 df-sdom 8889 df-sup 9383 df-inf 9384 df-pnf 11196 df-mnf 11197 df-xr 11198 df-ltxr 11199 df-le 11200 df-sub 11392 df-neg 11393 df-nn 12159 df-n0 12419 df-z 12505
df-uz 12769 df-fl 13703 |
This theorem is referenced by: fllep1
13712 fraclt1
13713 fracle1
13714 fracge0
13715 fllt
13717 flflp1
13718 flid
13719 flltnz
13722 flval3
13726 refldivcl
13734 fladdz
13736 flzadd
13737 flmulnn0
13738 flltdivnn0lt
13744 ceige
13755 ceim1l
13758 flleceil
13764 fleqceilz
13765 intfracq
13770 fldiv
13771 uzsup
13774 modvalr
13783 modfrac
13795 flmod
13796 intfrac
13797 modmulnn
13800 modcyc
13817 modadd1
13819 moddi
13850 modirr
13853 digit2
14145 digit1
14146 facavg
14207 rddif
15231 absrdbnd
15232 rexuzre
15243 o1fsum
15703 flo1
15744 isprm7
16589 opnmbllem
24981 mbfi1fseqlem1
25096 mbfi1fseqlem3
25098 mbfi1fseqlem4
25099 mbfi1fseqlem5
25100 mbfi1fseqlem6
25101 dvfsumlem1
25406 dvfsumlem2
25407 dvfsumlem3
25408 dvfsumlem4
25409 dvfsum2
25414 harmonicbnd4
26376 chtfl
26514 chpfl
26515 ppieq0
26541 ppiltx
26542 ppiub
26568 chpeq0
26572 chtub
26576 logfac2
26581 chpub
26584 logfacubnd
26585 logfaclbnd
26586 lgsquadlem1
26744 chtppilimlem1
26837 vmadivsum
26846 dchrisumlema
26852 dchrisumlem1
26853 dchrisumlem3
26855 dchrmusum2
26858 dchrisum0lem1b
26879 dchrisum0lem1
26880 dchrisum0lem2a
26881 dchrisum0lem3
26883 mudivsum
26894 mulogsumlem
26895 selberglem2
26910 pntrlog2bndlem6
26947 pntpbnd2
26951 pntlemg
26962 pntlemr
26966 pntlemj
26967 pntlemf
26969 pntlemk
26970 minvecolem4
29864 dnicld1
34981 dnibndlem2
34988 dnibndlem3
34989 dnibndlem4
34990 dnibndlem5
34991 dnibndlem7
34993 dnibndlem8
34994 dnibndlem9
34995 dnibndlem10
34996 dnibndlem11
34997 dnibndlem13
34999 dnibnd
35000 knoppcnlem4
35005 ltflcei
36112 leceifl
36113 opnmbllem0
36160 itg2addnclem2
36176 itg2addnclem3
36177 aks4d1p1p2
40573 hashnzfzclim
42690 lefldiveq
43613 fourierdlem4
44438 fourierdlem26
44460 fourierdlem47
44480 fourierdlem65
44498 flsubz
46689 dignn0flhalflem2
46788 |