cniccibl - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cniccibl		Structured version Visualization version GIF version

Theorem cniccibl 23330

Description: A continuous function on a closed bounded interval is integrable. (Contributed by Mario Carneiro, 12-Aug-2014.)

**Assertion**
Ref	Expression
cniccibl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿¹)

Proof of Theorem cniccibl Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iccmbl 23058	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴[,]𝐵) ∈ dom vol)
2		cnmbf 23149	. . 3 ⊢ (((𝐴[,]𝐵) ∈ dom vol ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ MblFn)
3	1, 2	stoic3 1691	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ MblFn)
4		simp3 1055	. . . . 5 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ))
5		cncff 22435	. . . . 5 ⊢ (𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ) → 𝐹:(𝐴[,]𝐵)⟶ℂ)
6		fdm 5950	. . . . 5 ⊢ (𝐹:(𝐴[,]𝐵)⟶ℂ → dom 𝐹 = (𝐴[,]𝐵))
7	4, 5, 6	3syl 18	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → dom 𝐹 = (𝐴[,]𝐵))
8	7	fveq2d 6092	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (vol‘dom 𝐹) = (vol‘(𝐴[,]𝐵)))
9		iccvolcl 23059	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (vol‘(𝐴[,]𝐵)) ∈ ℝ)
10	9	3adant3 1073	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (vol‘(𝐴[,]𝐵)) ∈ ℝ)
11	8, 10	eqeltrd 2687	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (vol‘dom 𝐹) ∈ ℝ)
12		cniccbdd 22954	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥)
13	7	raleqdv 3120	. . . 4 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ↔ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥))
14	13	rexbidv 3033	. . 3 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → (∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥 ↔ ∃𝑥 ∈ ℝ ∀𝑦 ∈ (𝐴[,]𝐵)(abs‘(𝐹‘𝑦)) ≤ 𝑥))
15	12, 14	mpbird 245	. 2 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥)
16		bddibl 23329	. 2 ⊢ ((𝐹 ∈ MblFn ∧ (vol‘dom 𝐹) ∈ ℝ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ dom 𝐹(abs‘(𝐹‘𝑦)) ≤ 𝑥) → 𝐹 ∈ 𝐿¹)
17	3, 11, 15, 16	syl3anc 1317	1 ⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐹 ∈ ((𝐴[,]𝐵)–cn→ℂ)) → 𝐹 ∈ 𝐿¹)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1030 = wceq 1474 ∈ wcel 1976 ∀wral 2895 ∃wrex 2896 class class class wbr 4577 dom cdm 5028 ⟶wf 5786 ‘cfv 5790 (class class class)co 6527 ℂcc 9790 ℝcr 9791 ≤ cle 9931 [,]cicc 12005 abscabs 13768 –cn→ccncf 22418 volcvol 22956 MblFncmbf 23106 𝐿¹cibl 23109

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1712 ax-4 1727 ax-5 1826 ax-6 1874 ax-7 1921 ax-8 1978 ax-9 1985 ax-10 2005 ax-11 2020 ax-12 2033 ax-13 2233 ax-ext 2589 ax-rep 4693 ax-sep 4703 ax-nul 4712 ax-pow 4764 ax-pr 4828 ax-un 6824 ax-inf2 8398 ax-cc 9117 ax-cnex 9848 ax-resscn 9849 ax-1cn 9850 ax-icn 9851 ax-addcl 9852 ax-addrcl 9853 ax-mulcl 9854 ax-mulrcl 9855 ax-mulcom 9856 ax-addass 9857 ax-mulass 9858 ax-distr 9859 ax-i2m1 9860 ax-1ne0 9861 ax-1rid 9862 ax-rnegex 9863 ax-rrecex 9864 ax-cnre 9865 ax-pre-lttri 9866 ax-pre-lttrn 9867 ax-pre-ltadd 9868 ax-pre-mulgt0 9869 ax-pre-sup 9870 ax-addf 9871 ax-mulf 9872

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-fal 1480 df-ex 1695 df-nf 1700 df-sb 1867 df-eu 2461 df-mo 2462 df-clab 2596 df-cleq 2602 df-clel 2605 df-nfc 2739 df-ne 2781 df-nel 2782 df-ral 2900 df-rex 2901 df-reu 2902 df-rmo 2903 df-rab 2904 df-v 3174 df-sbc 3402 df-csb 3499 df-dif 3542 df-un 3544 df-in 3546 df-ss 3553 df-pss 3555 df-nul 3874 df-if 4036 df-pw 4109 df-sn 4125 df-pr 4127 df-tp 4129 df-op 4131 df-uni 4367 df-int 4405 df-iun 4451 df-iin 4452 df-disj 4548 df-br 4578 df-opab 4638 df-mpt 4639 df-tr 4675 df-eprel 4939 df-id 4943 df-po 4949 df-so 4950 df-fr 4987 df-se 4988 df-we 4989 df-xp 5034 df-rel 5035 df-cnv 5036 df-co 5037 df-dm 5038 df-rn 5039 df-res 5040 df-ima 5041 df-pred 5583 df-ord 5629 df-on 5630 df-lim 5631 df-suc 5632 df-iota 5754 df-fun 5792 df-fn 5793 df-f 5794 df-f1 5795 df-fo 5796 df-f1o 5797 df-fv 5798 df-isom 5799 df-riota 6489 df-ov 6530 df-oprab 6531 df-mpt2 6532 df-of 6772 df-ofr 6773 df-om 6935 df-1st 7036 df-2nd 7037 df-supp 7160 df-wrecs 7271 df-recs 7332 df-rdg 7370 df-1o 7424 df-2o 7425 df-oadd 7428 df-omul 7429 df-er 7606 df-map 7723 df-pm 7724 df-ixp 7772 df-en 7819 df-dom 7820 df-sdom 7821 df-fin 7822 df-fsupp 8136 df-fi 8177 df-sup 8208 df-inf 8209 df-oi 8275 df-card 8625 df-acn 8628 df-cda 8850 df-pnf 9932 df-mnf 9933 df-xr 9934 df-ltxr 9935 df-le 9936 df-sub 10119 df-neg 10120 df-div 10534 df-nn 10868 df-2 10926 df-3 10927 df-4 10928 df-5 10929 df-6 10930 df-7 10931 df-8 10932 df-9 10933 df-n0 11140 df-z 11211 df-dec 11326 df-uz 11520 df-q 11621 df-rp 11665 df-xneg 11778 df-xadd 11779 df-xmul 11780 df-ioo 12006 df-ioc 12007 df-ico 12008 df-icc 12009 df-fz 12153 df-fzo 12290 df-fl 12410 df-mod 12486 df-seq 12619 df-exp 12678 df-hash 12935 df-cj 13633 df-re 13634 df-im 13635 df-sqrt 13769 df-abs 13770 df-limsup 13996 df-clim 14013 df-rlim 14014 df-sum 14211 df-struct 15643 df-ndx 15644 df-slot 15645 df-base 15646 df-sets 15647 df-ress 15648 df-plusg 15727 df-mulr 15728 df-starv 15729 df-sca 15730 df-vsca 15731 df-ip 15732 df-tset 15733 df-ple 15734 df-ds 15737 df-unif 15738 df-hom 15739 df-cco 15740 df-rest 15852 df-topn 15853 df-0g 15871 df-gsum 15872 df-topgen 15873 df-pt 15874 df-prds 15877 df-xrs 15931 df-qtop 15936 df-imas 15937 df-xps 15939 df-mre 16015 df-mrc 16016 df-acs 16018 df-mgm 17011 df-sgrp 17053 df-mnd 17064 df-submnd 17105 df-mulg 17310 df-cntz 17519 df-cmn 17964 df-psmet 19505 df-xmet 19506 df-met 19507 df-bl 19508 df-mopn 19509 df-cnfld 19514 df-top 20463 df-bases 20464 df-topon 20465 df-topsp 20466 df-cn 20783 df-cnp 20784 df-cmp 20942 df-tx 21117 df-hmeo 21310 df-xms 21876 df-ms 21877 df-tms 21878 df-cncf 22420 df-ovol 22957 df-vol 22958 df-mbf 23111 df-itg1 23112 df-itg2 23113 df-ibl 23114 df-0p 23160

This theorem is referenced by: itgsubstlem 23532 itgpowd 36615 arearect 36616 areaquad 36617 lhe4.4ex1a 37346 itgsin0pilem1 38638 ibliccsinexp 38639 itgsinexplem1 38642 itgsinexp 38643 itgcoscmulx 38658 itgsincmulx 38663 itgioocnicc 38666 iblcncfioo 38667 dirkeritg 38792 fourierdlem95 38891 sqwvfoura 38918 sqwvfourb 38919 etransclem18 38942

W3C validator