Metamath Proof Explorer

Theorem itgcl

Description: The integral of an integrable function is a complex number. This is Metamath 100 proof #86. (Contributed by Mario Carneiro, 29-Jun-2014)

Ref Expression
Hypotheses itgmpt.1 โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด ) โ†’ ๐ต โˆˆ ๐‘‰ )
itgcl.2 โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ๐ต ) โˆˆ ๐ฟ1 )
Assertion itgcl ( ๐œ‘ โ†’ โˆซ ๐ด ๐ต d ๐‘ฅ โˆˆ โ„‚ )

Proof

Step Hyp Ref Expression
1 itgmpt.1 โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด ) โ†’ ๐ต โˆˆ ๐‘‰ )
2 itgcl.2 โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐ด โ†ฆ ๐ต ) โˆˆ ๐ฟ1 )
3 eqid โŠข ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) )
4 3 dfitg โŠข โˆซ ๐ด ๐ต d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
5 fzfid โŠข ( ๐œ‘ โ†’ ( 0 ... 3 ) โˆˆ Fin )
6 ax-icn โŠข i โˆˆ โ„‚
7 elfznn0 โŠข ( ๐‘˜ โˆˆ ( 0 ... 3 ) โ†’ ๐‘˜ โˆˆ โ„•0 )
8 7 adantl โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ๐‘˜ โˆˆ โ„•0 )
9 expcl โŠข ( ( i โˆˆ โ„‚ โˆง ๐‘˜ โˆˆ โ„•0 ) โ†’ ( i โ†‘ ๐‘˜ ) โˆˆ โ„‚ )
10 6 8 9 sylancr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( i โ†‘ ๐‘˜ ) โˆˆ โ„‚ )
11 elfzelz โŠข ( ๐‘˜ โˆˆ ( 0 ... 3 ) โ†’ ๐‘˜ โˆˆ โ„ค )
12 eqidd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
13 eqidd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ด ) โ†’ ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) )
14 12 13 2 1 iblitg โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ โ„ค ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ )
15 11 14 sylan2 โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ )
16 15 recnd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„‚ )
17 10 16 mulcld โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) โˆˆ โ„‚ )
18 5 17 fsumcl โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ด โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ต / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) โˆˆ โ„‚ )
19 4 18 eqeltrid โŠข ( ๐œ‘ โ†’ โˆซ ๐ด ๐ต d ๐‘ฅ โˆˆ โ„‚ )