Metamath Proof Explorer

Theorem itgeqa

Description: Approximate equality of integrals. If C ( x ) = D ( x ) for almost all x , then S. B C ( x )d x = S. B D ( x ) d x and one is integrable iff the other is. (Contributed by Mario Carneiro, 12-Aug-2014) (Revised by Mario Carneiro, 2-Sep-2014)

Ref Expression
Hypotheses itgeqa.1 โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐ถ โˆˆ โ„‚ )
itgeqa.2 โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐ท โˆˆ โ„‚ )
itgeqa.3 โŠข ( ๐œ‘ โ†’ ๐ด โŠ† โ„ )
itgeqa.4 โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ๐ด ) = 0 )
itgeqa.5 โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( ๐ต โˆ– ๐ด ) ) โ†’ ๐ถ = ๐ท )
Assertion itgeqa ( ๐œ‘ โ†’ ( ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ ๐ฟ1 โ†” ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ท ) โˆˆ ๐ฟ1 ) โˆง โˆซ ๐ต ๐ถ d ๐‘ฅ = โˆซ ๐ต ๐ท d ๐‘ฅ ) )

Proof

Step Hyp Ref Expression
1 itgeqa.1 โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐ถ โˆˆ โ„‚ )
2 itgeqa.2 โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐ท โˆˆ โ„‚ )
3 itgeqa.3 โŠข ( ๐œ‘ โ†’ ๐ด โŠ† โ„ )
4 itgeqa.4 โŠข ( ๐œ‘ โ†’ ( vol* โ€˜ ๐ด ) = 0 )
5 itgeqa.5 โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( ๐ต โˆ– ๐ด ) ) โ†’ ๐ถ = ๐ท )
6 3 4 5 1 2 mbfeqa โŠข ( ๐œ‘ โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ MblFn โ†” ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ท ) โˆˆ MblFn ) )
7 ifan โŠข if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ๐‘ฅ โˆˆ ๐ต , if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) , 0 )
8 1 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐ถ โˆˆ โ„‚ )
9 ax-icn โŠข i โˆˆ โ„‚
10 ine0 โŠข i โ‰  0
11 elfzelz โŠข ( ๐‘˜ โˆˆ ( 0 ... 3 ) โ†’ ๐‘˜ โˆˆ โ„ค )
12 11 ad2antlr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐‘˜ โˆˆ โ„ค )
13 expclz โŠข ( ( i โˆˆ โ„‚ โˆง i โ‰  0 โˆง ๐‘˜ โˆˆ โ„ค ) โ†’ ( i โ†‘ ๐‘˜ ) โˆˆ โ„‚ )
14 9 10 12 13 mp3an12i โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( i โ†‘ ๐‘˜ ) โˆˆ โ„‚ )
15 expne0i โŠข ( ( i โˆˆ โ„‚ โˆง i โ‰  0 โˆง ๐‘˜ โˆˆ โ„ค ) โ†’ ( i โ†‘ ๐‘˜ ) โ‰  0 )
16 9 10 12 15 mp3an12i โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( i โ†‘ ๐‘˜ ) โ‰  0 )
17 8 14 16 divcld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) โˆˆ โ„‚ )
18 17 recld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ โ„ )
19 0re โŠข 0 โˆˆ โ„
20 ifcl โŠข ( ( ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ โ„ โˆง 0 โˆˆ โ„ ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„ )
21 18 19 20 sylancl โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„ )
22 21 rexrd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„* )
23 max1 โŠข ( ( 0 โˆˆ โ„ โˆง ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ โ„ ) โ†’ 0 โ‰ค if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
24 19 18 23 sylancr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ 0 โ‰ค if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
25 elxrge0 โŠข ( if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ ( 0 [,] +โˆž ) โ†” ( if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„* โˆง 0 โ‰ค if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
26 22 24 25 sylanbrc โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ ( 0 [,] +โˆž ) )
27 0e0iccpnf โŠข 0 โˆˆ ( 0 [,] +โˆž )
28 27 a1i โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ยฌ ๐‘ฅ โˆˆ ๐ต ) โ†’ 0 โˆˆ ( 0 [,] +โˆž ) )
29 26 28 ifclda โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ if ( ๐‘ฅ โˆˆ ๐ต , if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) , 0 ) โˆˆ ( 0 [,] +โˆž ) )
30 7 29 eqeltrid โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ ( 0 [,] +โˆž ) )
31 30 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ โ„ ) โ†’ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ ( 0 [,] +โˆž ) )
32 31 fmpttd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) : โ„ โŸถ ( 0 [,] +โˆž ) )
33 ifan โŠข if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ๐‘ฅ โˆˆ ๐ต , if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) , 0 )
34 2 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐ท โˆˆ โ„‚ )
35 34 14 16 divcld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) โˆˆ โ„‚ )
36 35 recld โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ โ„ )
37 ifcl โŠข ( ( ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ โ„ โˆง 0 โˆˆ โ„ ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„ )
38 36 19 37 sylancl โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„ )
39 38 rexrd โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„* )
40 max1 โŠข ( ( 0 โˆˆ โ„ โˆง ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ โ„ ) โ†’ 0 โ‰ค if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
41 19 36 40 sylancr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ 0 โ‰ค if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
42 elxrge0 โŠข ( if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ ( 0 [,] +โˆž ) โ†” ( if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ โ„* โˆง 0 โ‰ค if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
43 39 41 42 sylanbrc โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ ( 0 [,] +โˆž ) )
44 43 28 ifclda โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ if ( ๐‘ฅ โˆˆ ๐ต , if ( 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) , 0 ) โˆˆ ( 0 [,] +โˆž ) )
45 33 44 eqeltrid โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ ( 0 [,] +โˆž ) )
46 45 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฅ โˆˆ โ„ ) โ†’ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ ( 0 [,] +โˆž ) )
47 46 fmpttd โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) : โ„ โŸถ ( 0 [,] +โˆž ) )
48 3 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ๐ด โŠ† โ„ )
49 4 adantr โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( vol* โ€˜ ๐ด ) = 0 )
50 simpll โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐œ‘ )
51 simpr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐‘ฅ โˆˆ ๐ต )
52 eldifn โŠข ( ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) โ†’ ยฌ ๐‘ฅ โˆˆ ๐ด )
53 52 ad2antlr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ยฌ ๐‘ฅ โˆˆ ๐ด )
54 51 53 eldifd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐‘ฅ โˆˆ ( ๐ต โˆ– ๐ด ) )
55 50 54 5 syl2anc โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ๐ถ = ๐ท )
56 55 fvoveq1d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) )
57 56 ibllem โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โ†’ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) = if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
58 eldifi โŠข ( ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) โ†’ ๐‘ฅ โˆˆ โ„ )
59 58 adantl โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โ†’ ๐‘ฅ โˆˆ โ„ )
60 fvex โŠข ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ V
61 c0ex โŠข 0 โˆˆ V
62 60 61 ifex โŠข if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ V
63 eqid โŠข ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
64 63 fvmpt2 โŠข ( ( ๐‘ฅ โˆˆ โ„ โˆง if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ V ) โ†’ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
65 59 62 64 sylancl โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โ†’ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
66 fvex โŠข ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) โˆˆ V
67 66 61 ifex โŠข if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ V
68 eqid โŠข ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
69 68 fvmpt2 โŠข ( ( ๐‘ฅ โˆˆ โ„ โˆง if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) โˆˆ V ) โ†’ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
70 59 67 69 sylancl โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โ†’ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) )
71 57 65 70 3eqtr4d โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ) โ†’ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) )
72 71 ralrimiva โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) )
73 nfv โŠข โ„ฒ ๐‘ฆ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ )
74 nffvmpt1 โŠข โ„ฒ ๐‘ฅ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ )
75 nffvmpt1 โŠข โ„ฒ ๐‘ฅ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ )
76 74 75 nfeq โŠข โ„ฒ ๐‘ฅ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ )
77 fveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) )
78 fveq2 โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) )
79 77 78 eqeq12d โŠข ( ๐‘ฅ = ๐‘ฆ โ†’ ( ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) โ†” ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) ) )
80 73 76 79 cbvralw โŠข ( โˆ€ ๐‘ฅ โˆˆ ( โ„ โˆ– ๐ด ) ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฅ ) โ†” โˆ€ ๐‘ฆ โˆˆ ( โ„ โˆ– ๐ด ) ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) )
81 72 80 sylib โŠข ( ๐œ‘ โ†’ โˆ€ ๐‘ฆ โˆˆ ( โ„ โˆ– ๐ด ) ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) )
82 81 r19.21bi โŠข ( ( ๐œ‘ โˆง ๐‘ฆ โˆˆ ( โ„ โˆ– ๐ด ) ) โ†’ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) )
83 82 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โˆง ๐‘ฆ โˆˆ ( โ„ โˆ– ๐ด ) ) โ†’ ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) = ( ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) โ€˜ ๐‘ฆ ) )
84 32 47 48 49 83 itg2eqa โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) = ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
85 84 eleq1d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ โ†” ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ ) )
86 85 ralbidva โŠข ( ๐œ‘ โ†’ ( โˆ€ ๐‘˜ โˆˆ ( 0 ... 3 ) ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ โ†” โˆ€ ๐‘˜ โˆˆ ( 0 ... 3 ) ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ ) )
87 6 86 anbi12d โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ MblFn โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... 3 ) ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ ) โ†” ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ท ) โˆˆ MblFn โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... 3 ) ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ ) ) )
88 eqidd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
89 eqidd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) )
90 88 89 1 isibl2 โŠข ( ๐œ‘ โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ ๐ฟ1 โ†” ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ MblFn โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... 3 ) ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ ) ) )
91 eqidd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) = ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) )
92 eqidd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐ต ) โ†’ ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) )
93 91 92 2 isibl2 โŠข ( ๐œ‘ โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ท ) โˆˆ ๐ฟ1 โ†” ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ท ) โˆˆ MblFn โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... 3 ) ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) โˆˆ โ„ ) ) )
94 87 90 93 3bitr4d โŠข ( ๐œ‘ โ†’ ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ ๐ฟ1 โ†” ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ท ) โˆˆ ๐ฟ1 ) )
95 84 oveq2d โŠข ( ( ๐œ‘ โˆง ๐‘˜ โˆˆ ( 0 ... 3 ) ) โ†’ ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) = ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) )
96 95 sumeq2dv โŠข ( ๐œ‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) ) )
97 eqid โŠข ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) )
98 97 dfitg โŠข โˆซ ๐ต ๐ถ d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ถ / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
99 eqid โŠข ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) = ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) )
100 99 dfitg โŠข โˆซ ๐ต ๐ท d ๐‘ฅ = ฮฃ ๐‘˜ โˆˆ ( 0 ... 3 ) ( ( i โ†‘ ๐‘˜ ) ยท ( โˆซ2 โ€˜ ( ๐‘ฅ โˆˆ โ„ โ†ฆ if ( ( ๐‘ฅ โˆˆ ๐ต โˆง 0 โ‰ค ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) ) , ( โ„œ โ€˜ ( ๐ท / ( i โ†‘ ๐‘˜ ) ) ) , 0 ) ) ) )
101 96 98 100 3eqtr4g โŠข ( ๐œ‘ โ†’ โˆซ ๐ต ๐ถ d ๐‘ฅ = โˆซ ๐ต ๐ท d ๐‘ฅ )
102 94 101 jca โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ถ ) โˆˆ ๐ฟ1 โ†” ( ๐‘ฅ โˆˆ ๐ต โ†ฆ ๐ท ) โˆˆ ๐ฟ1 ) โˆง โˆซ ๐ต ๐ถ d ๐‘ฅ = โˆซ ๐ต ๐ท d ๐‘ฅ ) )