Metamath Proof Explorer


Theorem etransclem32

Description: This is the proof for the last equation in the proof of the derivative calculated in Juillerat p. 12, just after equation *(6) . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses etransclem32.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
etransclem32.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( ( TopOpen โ€˜ โ„‚fld ) โ†พt ๐‘† ) )
etransclem32.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„• )
etransclem32.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0 )
etransclem32.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฅ โ†‘ ( ๐‘ƒ โˆ’ 1 ) ) ยท โˆ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ( ๐‘ฅ โˆ’ ๐‘— ) โ†‘ ๐‘ƒ ) ) )
etransclem32.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
etransclem32.ngt โŠข ( ๐œ‘ โ†’ ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) < ๐‘ )
etransclem32.h โŠข ๐ป = ( ๐‘— โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฅ โˆ’ ๐‘— ) โ†‘ if ( ๐‘— = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) ) )
Assertion etransclem32 ( ๐œ‘ โ†’ ( ( ๐‘† D๐‘› ๐น ) โ€˜ ๐‘ ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ 0 ) )

Proof

Step Hyp Ref Expression
1 etransclem32.s โŠข ( ๐œ‘ โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
2 etransclem32.x โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ( ( TopOpen โ€˜ โ„‚fld ) โ†พt ๐‘† ) )
3 etransclem32.p โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„• )
4 etransclem32.m โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ โ„•0 )
5 etransclem32.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฅ โ†‘ ( ๐‘ƒ โˆ’ 1 ) ) ยท โˆ ๐‘— โˆˆ ( 1 ... ๐‘€ ) ( ( ๐‘ฅ โˆ’ ๐‘— ) โ†‘ ๐‘ƒ ) ) )
6 etransclem32.n โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„•0 )
7 etransclem32.ngt โŠข ( ๐œ‘ โ†’ ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) < ๐‘ )
8 etransclem32.h โŠข ๐ป = ( ๐‘— โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฅ โˆ’ ๐‘— ) โ†‘ if ( ๐‘— = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) ) )
9 etransclem11 โŠข ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) = ( ๐‘› โˆˆ โ„•0 โ†ฆ { ๐‘ โˆˆ ( ( 0 ... ๐‘› ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘› } )
10 1 2 3 4 5 6 8 9 etransclem30 โŠข ( ๐œ‘ โ†’ ( ( ๐‘† D๐‘› ๐น ) โ€˜ ๐‘ ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ฮฃ ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) ) ) )
11 simpr โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) )
12 9 6 etransclem12 โŠข ( ๐œ‘ โ†’ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) = { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } )
13 12 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) = { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } )
14 11 13 eleqtrd โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } )
15 14 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } )
16 nfv โŠข โ„ฒ ๐‘˜ ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } )
17 nfre1 โŠข โ„ฒ ๐‘˜ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ )
18 17 nfn โŠข โ„ฒ ๐‘˜ ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ )
19 16 18 nfan โŠข โ„ฒ ๐‘˜ ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) )
20 fzssre โŠข ( 0 ... ๐‘ ) โІ โ„
21 rabid โŠข ( ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } โ†” ( ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆง ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ ) )
22 21 simplbi โŠข ( ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } โ†’ ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) )
23 elmapi โŠข ( ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โ†’ ๐‘ : ( 0 ... ๐‘€ ) โŸถ ( 0 ... ๐‘ ) )
24 22 23 syl โŠข ( ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } โ†’ ๐‘ : ( 0 ... ๐‘€ ) โŸถ ( 0 ... ๐‘ ) )
25 24 adantl โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โ†’ ๐‘ : ( 0 ... ๐‘€ ) โŸถ ( 0 ... ๐‘ ) )
26 25 ffvelcdmda โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘˜ ) โˆˆ ( 0 ... ๐‘ ) )
27 20 26 sselid โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘˜ ) โˆˆ โ„ )
28 27 adantlr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘˜ ) โˆˆ โ„ )
29 nnm1nn0 โŠข ( ๐‘ƒ โˆˆ โ„• โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„•0 )
30 3 29 syl โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„•0 )
31 30 nn0red โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„ )
32 3 nnred โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„ )
33 31 32 ifcld โŠข ( ๐œ‘ โ†’ if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) โˆˆ โ„ )
34 33 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ) โ†’ if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) โˆˆ โ„ )
35 ralnex โŠข ( โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ยฌ if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) โ†” ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) )
36 35 biimpri โŠข ( ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) โ†’ โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ยฌ if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) )
37 36 r19.21bi โŠข ( ( ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ยฌ if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) )
38 37 adantll โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ยฌ if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) )
39 28 34 38 nltled โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) )
40 39 ex โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ( ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โ†’ ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) )
41 19 40 ralrimi โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) )
42 21 simprbi โŠข ( ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } โ†’ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ )
43 fveq2 โŠข ( ๐‘— = ๐‘˜ โ†’ ( ๐‘ โ€˜ ๐‘— ) = ( ๐‘ โ€˜ ๐‘˜ ) )
44 43 cbvsumv โŠข ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ )
45 42 44 eqtr3di โŠข ( ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } โ†’ ๐‘ = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) )
46 45 ad2antlr โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) โ†’ ๐‘ = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) )
47 fveq2 โŠข ( ๐‘˜ = โ„Ž โ†’ ( ๐‘ โ€˜ ๐‘˜ ) = ( ๐‘ โ€˜ โ„Ž ) )
48 47 cbvsumv โŠข ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) = ฮฃ โ„Ž โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ โ„Ž )
49 fzfid โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) โ†’ ( 0 ... ๐‘€ ) โˆˆ Fin )
50 25 ffvelcdmda โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โ„Ž โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ โ„Ž ) โˆˆ ( 0 ... ๐‘ ) )
51 20 50 sselid โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โ„Ž โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ โ„Ž ) โˆˆ โ„ )
52 51 adantlr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) โˆง โ„Ž โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ โ„Ž ) โˆˆ โ„ )
53 31 32 ifcld โŠข ( ๐œ‘ โ†’ if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) โˆˆ โ„ )
54 53 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) โˆง โ„Ž โˆˆ ( 0 ... ๐‘€ ) ) โ†’ if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) โˆˆ โ„ )
55 eqeq1 โŠข ( ๐‘˜ = โ„Ž โ†’ ( ๐‘˜ = 0 โ†” โ„Ž = 0 ) )
56 55 ifbid โŠข ( ๐‘˜ = โ„Ž โ†’ if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) = if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) )
57 47 56 breq12d โŠข ( ๐‘˜ = โ„Ž โ†’ ( ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) โ†” ( ๐‘ โ€˜ โ„Ž ) โ‰ค if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) )
58 57 rspccva โŠข ( ( โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) โˆง โ„Ž โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ โ„Ž ) โ‰ค if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) )
59 58 adantll โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) โˆง โ„Ž โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ โ„Ž ) โ‰ค if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) )
60 49 52 54 59 fsumle โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) โ†’ ฮฃ โ„Ž โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ โ„Ž ) โ‰ค ฮฃ โ„Ž โˆˆ ( 0 ... ๐‘€ ) if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) )
61 nn0uz โŠข โ„•0 = ( โ„คโ‰ฅ โ€˜ 0 )
62 4 61 eleqtrdi โŠข ( ๐œ‘ โ†’ ๐‘€ โˆˆ ( โ„คโ‰ฅ โ€˜ 0 ) )
63 3 nnnn0d โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„•0 )
64 30 63 ifcld โŠข ( ๐œ‘ โ†’ if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) โˆˆ โ„•0 )
65 64 adantr โŠข ( ( ๐œ‘ โˆง โ„Ž โˆˆ ( 0 ... ๐‘€ ) ) โ†’ if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) โˆˆ โ„•0 )
66 65 nn0cnd โŠข ( ( ๐œ‘ โˆง โ„Ž โˆˆ ( 0 ... ๐‘€ ) ) โ†’ if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) โˆˆ โ„‚ )
67 iftrue โŠข ( โ„Ž = 0 โ†’ if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) = ( ๐‘ƒ โˆ’ 1 ) )
68 62 66 67 fsum1p โŠข ( ๐œ‘ โ†’ ฮฃ โ„Ž โˆˆ ( 0 ... ๐‘€ ) if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) = ( ( ๐‘ƒ โˆ’ 1 ) + ฮฃ โ„Ž โˆˆ ( ( 0 + 1 ) ... ๐‘€ ) if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) )
69 0p1e1 โŠข ( 0 + 1 ) = 1
70 69 oveq1i โŠข ( ( 0 + 1 ) ... ๐‘€ ) = ( 1 ... ๐‘€ )
71 70 a1i โŠข ( ๐œ‘ โ†’ ( ( 0 + 1 ) ... ๐‘€ ) = ( 1 ... ๐‘€ ) )
72 71 sumeq1d โŠข ( ๐œ‘ โ†’ ฮฃ โ„Ž โˆˆ ( ( 0 + 1 ) ... ๐‘€ ) if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) = ฮฃ โ„Ž โˆˆ ( 1 ... ๐‘€ ) if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) )
73 0red โŠข ( โ„Ž โˆˆ ( 1 ... ๐‘€ ) โ†’ 0 โˆˆ โ„ )
74 1red โŠข ( โ„Ž โˆˆ ( 1 ... ๐‘€ ) โ†’ 1 โˆˆ โ„ )
75 elfzelz โŠข ( โ„Ž โˆˆ ( 1 ... ๐‘€ ) โ†’ โ„Ž โˆˆ โ„ค )
76 75 zred โŠข ( โ„Ž โˆˆ ( 1 ... ๐‘€ ) โ†’ โ„Ž โˆˆ โ„ )
77 0lt1 โŠข 0 < 1
78 77 a1i โŠข ( โ„Ž โˆˆ ( 1 ... ๐‘€ ) โ†’ 0 < 1 )
79 elfzle1 โŠข ( โ„Ž โˆˆ ( 1 ... ๐‘€ ) โ†’ 1 โ‰ค โ„Ž )
80 73 74 76 78 79 ltletrd โŠข ( โ„Ž โˆˆ ( 1 ... ๐‘€ ) โ†’ 0 < โ„Ž )
81 80 gt0ne0d โŠข ( โ„Ž โˆˆ ( 1 ... ๐‘€ ) โ†’ โ„Ž โ‰  0 )
82 81 neneqd โŠข ( โ„Ž โˆˆ ( 1 ... ๐‘€ ) โ†’ ยฌ โ„Ž = 0 )
83 82 iffalsed โŠข ( โ„Ž โˆˆ ( 1 ... ๐‘€ ) โ†’ if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) = ๐‘ƒ )
84 83 adantl โŠข ( ( ๐œ‘ โˆง โ„Ž โˆˆ ( 1 ... ๐‘€ ) ) โ†’ if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) = ๐‘ƒ )
85 84 sumeq2dv โŠข ( ๐œ‘ โ†’ ฮฃ โ„Ž โˆˆ ( 1 ... ๐‘€ ) if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) = ฮฃ โ„Ž โˆˆ ( 1 ... ๐‘€ ) ๐‘ƒ )
86 fzfid โŠข ( ๐œ‘ โ†’ ( 1 ... ๐‘€ ) โˆˆ Fin )
87 3 nncnd โŠข ( ๐œ‘ โ†’ ๐‘ƒ โˆˆ โ„‚ )
88 fsumconst โŠข ( ( ( 1 ... ๐‘€ ) โˆˆ Fin โˆง ๐‘ƒ โˆˆ โ„‚ ) โ†’ ฮฃ โ„Ž โˆˆ ( 1 ... ๐‘€ ) ๐‘ƒ = ( ( โ™ฏ โ€˜ ( 1 ... ๐‘€ ) ) ยท ๐‘ƒ ) )
89 86 87 88 syl2anc โŠข ( ๐œ‘ โ†’ ฮฃ โ„Ž โˆˆ ( 1 ... ๐‘€ ) ๐‘ƒ = ( ( โ™ฏ โ€˜ ( 1 ... ๐‘€ ) ) ยท ๐‘ƒ ) )
90 hashfz1 โŠข ( ๐‘€ โˆˆ โ„•0 โ†’ ( โ™ฏ โ€˜ ( 1 ... ๐‘€ ) ) = ๐‘€ )
91 4 90 syl โŠข ( ๐œ‘ โ†’ ( โ™ฏ โ€˜ ( 1 ... ๐‘€ ) ) = ๐‘€ )
92 91 oveq1d โŠข ( ๐œ‘ โ†’ ( ( โ™ฏ โ€˜ ( 1 ... ๐‘€ ) ) ยท ๐‘ƒ ) = ( ๐‘€ ยท ๐‘ƒ ) )
93 89 92 eqtrd โŠข ( ๐œ‘ โ†’ ฮฃ โ„Ž โˆˆ ( 1 ... ๐‘€ ) ๐‘ƒ = ( ๐‘€ ยท ๐‘ƒ ) )
94 72 85 93 3eqtrd โŠข ( ๐œ‘ โ†’ ฮฃ โ„Ž โˆˆ ( ( 0 + 1 ) ... ๐‘€ ) if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) = ( ๐‘€ ยท ๐‘ƒ ) )
95 94 oveq2d โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ โˆ’ 1 ) + ฮฃ โ„Ž โˆˆ ( ( 0 + 1 ) ... ๐‘€ ) if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) = ( ( ๐‘ƒ โˆ’ 1 ) + ( ๐‘€ ยท ๐‘ƒ ) ) )
96 30 nn0cnd โŠข ( ๐œ‘ โ†’ ( ๐‘ƒ โˆ’ 1 ) โˆˆ โ„‚ )
97 4 63 nn0mulcld โŠข ( ๐œ‘ โ†’ ( ๐‘€ ยท ๐‘ƒ ) โˆˆ โ„•0 )
98 97 nn0cnd โŠข ( ๐œ‘ โ†’ ( ๐‘€ ยท ๐‘ƒ ) โˆˆ โ„‚ )
99 96 98 addcomd โŠข ( ๐œ‘ โ†’ ( ( ๐‘ƒ โˆ’ 1 ) + ( ๐‘€ ยท ๐‘ƒ ) ) = ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) )
100 68 95 99 3eqtrd โŠข ( ๐œ‘ โ†’ ฮฃ โ„Ž โˆˆ ( 0 ... ๐‘€ ) if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) = ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) )
101 100 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) โ†’ ฮฃ โ„Ž โˆˆ ( 0 ... ๐‘€ ) if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) = ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) )
102 60 101 breqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) โ†’ ฮฃ โ„Ž โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ โ„Ž ) โ‰ค ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) )
103 48 102 eqbrtrid โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) )
104 46 103 eqbrtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง โˆ€ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘˜ ) โ‰ค if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) โ†’ ๐‘ โ‰ค ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) )
105 41 104 syldan โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ๐‘ โ‰ค ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) )
106 97 30 nn0addcld โŠข ( ๐œ‘ โ†’ ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) โˆˆ โ„•0 )
107 106 nn0red โŠข ( ๐œ‘ โ†’ ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) โˆˆ โ„ )
108 6 nn0red โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„ )
109 107 108 ltnled โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) < ๐‘ โ†” ยฌ ๐‘ โ‰ค ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) ) )
110 7 109 mpbid โŠข ( ๐œ‘ โ†’ ยฌ ๐‘ โ‰ค ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) )
111 110 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ยฌ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ยฌ ๐‘ โ‰ค ( ( ๐‘€ ยท ๐‘ƒ ) + ( ๐‘ƒ โˆ’ 1 ) ) )
112 105 111 condan โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โ†’ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) )
113 112 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โ†’ โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) )
114 nfv โŠข โ„ฒ ๐‘— ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ )
115 nfcv โŠข โ„ฒ ๐‘— ( 0 ... ๐‘€ )
116 115 nfsum1 โŠข โ„ฒ ๐‘— ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— )
117 116 nfeq1 โŠข โ„ฒ ๐‘— ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘
118 nfcv โŠข โ„ฒ ๐‘— ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) )
119 117 118 nfrabw โŠข โ„ฒ ๐‘— { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ }
120 119 nfcri โŠข โ„ฒ ๐‘— ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ }
121 114 120 nfan โŠข โ„ฒ ๐‘— ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } )
122 nfv โŠข โ„ฒ ๐‘— ๐‘˜ โˆˆ ( 0 ... ๐‘€ )
123 nfv โŠข โ„ฒ ๐‘— if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ )
124 121 122 123 nf3an โŠข โ„ฒ ๐‘— ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) )
125 nfcv โŠข โ„ฒ ๐‘— ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘˜ ) ) โ€˜ ( ๐‘ โ€˜ ๐‘˜ ) ) โ€˜ ๐‘ฅ )
126 fzfid โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ( 0 ... ๐‘€ ) โˆˆ Fin )
127 1 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
128 2 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ๐‘‹ โˆˆ ( ( TopOpen โ€˜ โ„‚fld ) โ†พt ๐‘† ) )
129 3 ad3antrrr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ๐‘ƒ โˆˆ โ„• )
130 etransclem5 โŠข ( ๐‘— โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฅ โˆ’ ๐‘— ) โ†‘ if ( ๐‘— = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) ) ) = ( ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ๐‘ฆ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฆ โˆ’ ๐‘˜ ) โ†‘ if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) ) )
131 8 130 eqtri โŠข ๐ป = ( ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ๐‘ฆ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฆ โˆ’ ๐‘˜ ) โ†‘ if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) ) )
132 simpr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ๐‘— โˆˆ ( 0 ... ๐‘€ ) )
133 24 ad2antlr โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ๐‘ : ( 0 ... ๐‘€ ) โŸถ ( 0 ... ๐‘ ) )
134 simpr โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ๐‘— โˆˆ ( 0 ... ๐‘€ ) )
135 133 134 ffvelcdmd โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘— ) โˆˆ ( 0 ... ๐‘ ) )
136 135 adantllr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘— ) โˆˆ ( 0 ... ๐‘ ) )
137 elfznn0 โŠข ( ( ๐‘ โ€˜ ๐‘— ) โˆˆ ( 0 ... ๐‘ ) โ†’ ( ๐‘ โ€˜ ๐‘— ) โˆˆ โ„•0 )
138 136 137 syl โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘— ) โˆˆ โ„•0 )
139 127 128 129 131 132 138 etransclem20 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) : ๐‘‹ โŸถ โ„‚ )
140 simpllr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ๐‘ฅ โˆˆ ๐‘‹ )
141 139 140 ffvelcdmd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) โˆˆ โ„‚ )
142 141 3ad2antl1 โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) โˆˆ โ„‚ )
143 fveq2 โŠข ( ๐‘— = ๐‘˜ โ†’ ( ๐ป โ€˜ ๐‘— ) = ( ๐ป โ€˜ ๐‘˜ ) )
144 143 oveq2d โŠข ( ๐‘— = ๐‘˜ โ†’ ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) = ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘˜ ) ) )
145 144 43 fveq12d โŠข ( ๐‘— = ๐‘˜ โ†’ ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) = ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘˜ ) ) โ€˜ ( ๐‘ โ€˜ ๐‘˜ ) ) )
146 145 fveq1d โŠข ( ๐‘— = ๐‘˜ โ†’ ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) = ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘˜ ) ) โ€˜ ( ๐‘ โ€˜ ๐‘˜ ) ) โ€˜ ๐‘ฅ ) )
147 simp2 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) )
148 1 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
149 148 3ad2ant1 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ๐‘† โˆˆ { โ„ , โ„‚ } )
150 2 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โ†’ ๐‘‹ โˆˆ ( ( TopOpen โ€˜ โ„‚fld ) โ†พt ๐‘† ) )
151 150 3ad2ant1 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ๐‘‹ โˆˆ ( ( TopOpen โ€˜ โ„‚fld ) โ†พt ๐‘† ) )
152 3 ad2antrr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โ†’ ๐‘ƒ โˆˆ โ„• )
153 152 3ad2ant1 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ๐‘ƒ โˆˆ โ„• )
154 etransclem5 โŠข ( ๐‘— โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฅ โˆ’ ๐‘— ) โ†‘ if ( ๐‘— = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) ) ) = ( โ„Ž โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ๐‘ฆ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฆ โˆ’ โ„Ž ) โ†‘ if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) ) )
155 8 154 eqtri โŠข ๐ป = ( โ„Ž โˆˆ ( 0 ... ๐‘€ ) โ†ฆ ( ๐‘ฆ โˆˆ ๐‘‹ โ†ฆ ( ( ๐‘ฆ โˆ’ โ„Ž ) โ†‘ if ( โ„Ž = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) ) ) )
156 26 elfzelzd โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘˜ ) โˆˆ โ„ค )
157 156 adantllr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘˜ ) โˆˆ โ„ค )
158 157 3adant3 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ( ๐‘ โ€˜ ๐‘˜ ) โˆˆ โ„ค )
159 simp3 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) )
160 149 151 153 155 147 158 159 etransclem19 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘˜ ) ) โ€˜ ( ๐‘ โ€˜ ๐‘˜ ) ) = ( ๐‘ฆ โˆˆ ๐‘‹ โ†ฆ 0 ) )
161 eqidd โŠข ( ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โˆง ๐‘ฆ = ๐‘ฅ ) โ†’ 0 = 0 )
162 simp1lr โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ๐‘ฅ โˆˆ ๐‘‹ )
163 0red โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ 0 โˆˆ โ„ )
164 160 161 162 163 fvmptd โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘˜ ) ) โ€˜ ( ๐‘ โ€˜ ๐‘˜ ) ) โ€˜ ๐‘ฅ ) = 0 )
165 124 125 126 142 146 147 164 fprod0 โŠข ( ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โˆง ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) โˆง if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) ) โ†’ โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) = 0 )
166 165 rexlimdv3a โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โ†’ ( โˆƒ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) if ( ๐‘˜ = 0 , ( ๐‘ƒ โˆ’ 1 ) , ๐‘ƒ ) < ( ๐‘ โ€˜ ๐‘˜ ) โ†’ โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) = 0 ) )
167 113 166 mpd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } ) โ†’ โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) = 0 )
168 15 167 syldan โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) = 0 )
169 168 oveq2d โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) ) = ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท 0 ) )
170 6 faccld โŠข ( ๐œ‘ โ†’ ( ! โ€˜ ๐‘ ) โˆˆ โ„• )
171 170 nncnd โŠข ( ๐œ‘ โ†’ ( ! โ€˜ ๐‘ ) โˆˆ โ„‚ )
172 171 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ( ! โ€˜ ๐‘ ) โˆˆ โ„‚ )
173 fzfid โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ( 0 ... ๐‘€ ) โˆˆ Fin )
174 simpll โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ๐œ‘ )
175 14 adantr โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ๐‘ โˆˆ { ๐‘ โˆˆ ( ( 0 ... ๐‘ ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ๐‘ โ€˜ ๐‘— ) = ๐‘ } )
176 simpr โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ๐‘— โˆˆ ( 0 ... ๐‘€ ) )
177 174 175 176 135 syl21anc โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘— ) โˆˆ ( 0 ... ๐‘ ) )
178 177 137 syl โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ๐‘ โ€˜ ๐‘— ) โˆˆ โ„•0 )
179 178 faccld โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โˆˆ โ„• )
180 179 nncnd โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โˆˆ โ„‚ )
181 173 180 fprodcl โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โˆˆ โ„‚ )
182 179 nnne0d โŠข ( ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โˆง ๐‘— โˆˆ ( 0 ... ๐‘€ ) ) โ†’ ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ‰  0 )
183 173 180 182 fprodn0 โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ‰  0 )
184 172 181 183 divcld โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) โˆˆ โ„‚ )
185 184 mul01d โŠข ( ( ๐œ‘ โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท 0 ) = 0 )
186 185 adantlr โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท 0 ) = 0 )
187 169 186 eqtrd โŠข ( ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โˆง ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ) โ†’ ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) ) = 0 )
188 187 sumeq2dv โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ฮฃ ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) ) = ฮฃ ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) 0 )
189 eqid โŠข ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) = ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } )
190 189 6 etransclem16 โŠข ( ๐œ‘ โ†’ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) โˆˆ Fin )
191 190 olcd โŠข ( ๐œ‘ โ†’ ( ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) โІ ( โ„คโ‰ฅ โ€˜ ๐ด ) โˆจ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) โˆˆ Fin ) )
192 191 adantr โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ( ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) โІ ( โ„คโ‰ฅ โ€˜ ๐ด ) โˆจ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) โˆˆ Fin ) )
193 sumz โŠข ( ( ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) โІ ( โ„คโ‰ฅ โ€˜ ๐ด ) โˆจ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) โˆˆ Fin ) โ†’ ฮฃ ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) 0 = 0 )
194 192 193 syl โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ฮฃ ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) 0 = 0 )
195 188 194 eqtrd โŠข ( ( ๐œ‘ โˆง ๐‘ฅ โˆˆ ๐‘‹ ) โ†’ ฮฃ ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) ) = 0 )
196 195 mpteq2dva โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ ฮฃ ๐‘ โˆˆ ( ( ๐‘š โˆˆ โ„•0 โ†ฆ { ๐‘‘ โˆˆ ( ( 0 ... ๐‘š ) โ†‘m ( 0 ... ๐‘€ ) ) โˆฃ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘€ ) ( ๐‘‘ โ€˜ ๐‘˜ ) = ๐‘š } ) โ€˜ ๐‘ ) ( ( ( ! โ€˜ ๐‘ ) / โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ! โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) ) ยท โˆ ๐‘— โˆˆ ( 0 ... ๐‘€ ) ( ( ( ๐‘† D๐‘› ( ๐ป โ€˜ ๐‘— ) ) โ€˜ ( ๐‘ โ€˜ ๐‘— ) ) โ€˜ ๐‘ฅ ) ) ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ 0 ) )
197 10 196 eqtrd โŠข ( ๐œ‘ โ†’ ( ( ๐‘† D๐‘› ๐น ) โ€˜ ๐‘ ) = ( ๐‘ฅ โˆˆ ๐‘‹ โ†ฆ 0 ) )