Metamath Proof Explorer


Theorem coeeu

Description: Uniqueness of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Assertion coeeu ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†’ โˆƒ! ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )

Proof

Step Hyp Ref Expression
1 plyssc โŠข ( Poly โ€˜ ๐‘† ) โŠ† ( Poly โ€˜ โ„‚ )
2 1 sseli โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†’ ๐น โˆˆ ( Poly โ€˜ โ„‚ ) )
3 elply2 โŠข ( ๐น โˆˆ ( Poly โ€˜ โ„‚ ) โ†” ( โ„‚ โŠ† โ„‚ โˆง โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( โ„‚ โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
4 3 simprbi โŠข ( ๐น โˆˆ ( Poly โ€˜ โ„‚ ) โ†’ โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( โ„‚ โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
5 rexcom โŠข ( โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘Ž โˆˆ ( ( โ„‚ โˆช { 0 } ) โ†‘m โ„•0 ) ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” โˆƒ ๐‘Ž โˆˆ ( ( โ„‚ โˆช { 0 } ) โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
6 4 5 sylib โŠข ( ๐น โˆˆ ( Poly โ€˜ โ„‚ ) โ†’ โˆƒ ๐‘Ž โˆˆ ( ( โ„‚ โˆช { 0 } ) โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
7 2 6 syl โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†’ โˆƒ ๐‘Ž โˆˆ ( ( โ„‚ โˆช { 0 } ) โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
8 0cn โŠข 0 โˆˆ โ„‚
9 snssi โŠข ( 0 โˆˆ โ„‚ โ†’ { 0 } โŠ† โ„‚ )
10 8 9 ax-mp โŠข { 0 } โŠ† โ„‚
11 ssequn2 โŠข ( { 0 } โŠ† โ„‚ โ†” ( โ„‚ โˆช { 0 } ) = โ„‚ )
12 10 11 mpbi โŠข ( โ„‚ โˆช { 0 } ) = โ„‚
13 12 oveq1i โŠข ( ( โ„‚ โˆช { 0 } ) โ†‘m โ„•0 ) = ( โ„‚ โ†‘m โ„•0 )
14 13 rexeqi โŠข ( โˆƒ ๐‘Ž โˆˆ ( ( โ„‚ โˆช { 0 } ) โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” โˆƒ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
15 7 14 sylib โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†’ โˆƒ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
16 reeanv โŠข ( โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘š โˆˆ โ„•0 ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†” ( โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง โˆƒ ๐‘š โˆˆ โ„•0 ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
17 simp1l โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ๐น โˆˆ ( Poly โ€˜ ๐‘† ) )
18 simp1rl โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) )
19 simp1rr โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) )
20 simp2l โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ๐‘› โˆˆ โ„•0 )
21 simp2r โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ๐‘š โˆˆ โ„•0 )
22 simp3ll โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } )
23 simp3rl โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } )
24 simp3lr โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
25 oveq1 โŠข ( ๐‘ง = ๐‘ค โ†’ ( ๐‘ง โ†‘ ๐‘˜ ) = ( ๐‘ค โ†‘ ๐‘˜ ) )
26 25 oveq2d โŠข ( ๐‘ง = ๐‘ค โ†’ ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ค โ†‘ ๐‘˜ ) ) )
27 26 sumeq2sdv โŠข ( ๐‘ง = ๐‘ค โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ค โ†‘ ๐‘˜ ) ) )
28 fveq2 โŠข ( ๐‘˜ = ๐‘— โ†’ ( ๐‘Ž โ€˜ ๐‘˜ ) = ( ๐‘Ž โ€˜ ๐‘— ) )
29 oveq2 โŠข ( ๐‘˜ = ๐‘— โ†’ ( ๐‘ค โ†‘ ๐‘˜ ) = ( ๐‘ค โ†‘ ๐‘— ) )
30 28 29 oveq12d โŠข ( ๐‘˜ = ๐‘— โ†’ ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ค โ†‘ ๐‘˜ ) ) = ( ( ๐‘Ž โ€˜ ๐‘— ) ยท ( ๐‘ค โ†‘ ๐‘— ) ) )
31 30 cbvsumv โŠข ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ค โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘— ) ยท ( ๐‘ค โ†‘ ๐‘— ) )
32 27 31 eqtrdi โŠข ( ๐‘ง = ๐‘ค โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘— ) ยท ( ๐‘ค โ†‘ ๐‘— ) ) )
33 32 cbvmptv โŠข ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ค โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘— ) ยท ( ๐‘ค โ†‘ ๐‘— ) ) )
34 24 33 eqtrdi โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ๐น = ( ๐‘ค โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘— ) ยท ( ๐‘ค โ†‘ ๐‘— ) ) ) )
35 simp3rr โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
36 25 oveq2d โŠข ( ๐‘ง = ๐‘ค โ†’ ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ค โ†‘ ๐‘˜ ) ) )
37 36 sumeq2sdv โŠข ( ๐‘ง = ๐‘ค โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ค โ†‘ ๐‘˜ ) ) )
38 fveq2 โŠข ( ๐‘˜ = ๐‘— โ†’ ( ๐‘ โ€˜ ๐‘˜ ) = ( ๐‘ โ€˜ ๐‘— ) )
39 38 29 oveq12d โŠข ( ๐‘˜ = ๐‘— โ†’ ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ค โ†‘ ๐‘˜ ) ) = ( ( ๐‘ โ€˜ ๐‘— ) ยท ( ๐‘ค โ†‘ ๐‘— ) ) )
40 39 cbvsumv โŠข ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ค โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘— ) ยท ( ๐‘ค โ†‘ ๐‘— ) )
41 37 40 eqtrdi โŠข ( ๐‘ง = ๐‘ค โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘— ) ยท ( ๐‘ค โ†‘ ๐‘— ) ) )
42 41 cbvmptv โŠข ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ค โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘— ) ยท ( ๐‘ค โ†‘ ๐‘— ) ) )
43 35 42 eqtrdi โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ๐น = ( ๐‘ค โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘— โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘— ) ยท ( ๐‘ค โ†‘ ๐‘— ) ) ) )
44 17 18 19 20 21 22 23 34 43 coeeulem โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) โˆง ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) ) โ†’ ๐‘Ž = ๐‘ )
45 44 3expia โŠข ( ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โˆง ( ๐‘› โˆˆ โ„•0 โˆง ๐‘š โˆˆ โ„•0 ) ) โ†’ ( ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†’ ๐‘Ž = ๐‘ ) )
46 45 rexlimdvva โŠข ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โ†’ ( โˆƒ ๐‘› โˆˆ โ„•0 โˆƒ ๐‘š โˆˆ โ„•0 ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†’ ๐‘Ž = ๐‘ ) )
47 16 46 syl5bir โŠข ( ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โˆง ( ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆง ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ) ) โ†’ ( ( โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง โˆƒ ๐‘š โˆˆ โ„•0 ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†’ ๐‘Ž = ๐‘ ) )
48 47 ralrimivva โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†’ โˆ€ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆ€ ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ( ( โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง โˆƒ ๐‘š โˆˆ โ„•0 ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†’ ๐‘Ž = ๐‘ ) )
49 imaeq1 โŠข ( ๐‘Ž = ๐‘ โ†’ ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) )
50 49 eqeq1d โŠข ( ๐‘Ž = ๐‘ โ†’ ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โ†” ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } ) )
51 fveq1 โŠข ( ๐‘Ž = ๐‘ โ†’ ( ๐‘Ž โ€˜ ๐‘˜ ) = ( ๐‘ โ€˜ ๐‘˜ ) )
52 51 oveq1d โŠข ( ๐‘Ž = ๐‘ โ†’ ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) )
53 52 sumeq2sdv โŠข ( ๐‘Ž = ๐‘ โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) )
54 53 mpteq2dv โŠข ( ๐‘Ž = ๐‘ โ†’ ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
55 54 eqeq2d โŠข ( ๐‘Ž = ๐‘ โ†’ ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†” ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
56 50 55 anbi12d โŠข ( ๐‘Ž = ๐‘ โ†’ ( ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
57 56 rexbidv โŠข ( ๐‘Ž = ๐‘ โ†’ ( โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
58 fvoveq1 โŠข ( ๐‘› = ๐‘š โ†’ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) = ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) )
59 58 imaeq2d โŠข ( ๐‘› = ๐‘š โ†’ ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) )
60 59 eqeq1d โŠข ( ๐‘› = ๐‘š โ†’ ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โ†” ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } ) )
61 oveq2 โŠข ( ๐‘› = ๐‘š โ†’ ( 0 ... ๐‘› ) = ( 0 ... ๐‘š ) )
62 61 sumeq1d โŠข ( ๐‘› = ๐‘š โ†’ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) = ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) )
63 62 mpteq2dv โŠข ( ๐‘› = ๐‘š โ†’ ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) )
64 63 eqeq2d โŠข ( ๐‘› = ๐‘š โ†’ ( ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) โ†” ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
65 60 64 anbi12d โŠข ( ๐‘› = ๐‘š โ†’ ( ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
66 65 cbvrexvw โŠข ( โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” โˆƒ ๐‘š โˆˆ โ„•0 ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )
67 57 66 bitrdi โŠข ( ๐‘Ž = ๐‘ โ†’ ( โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” โˆƒ ๐‘š โˆˆ โ„•0 ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) )
68 67 reu4 โŠข ( โˆƒ! ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โ†” ( โˆƒ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง โˆ€ ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆ€ ๐‘ โˆˆ ( โ„‚ โ†‘m โ„•0 ) ( ( โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) โˆง โˆƒ ๐‘š โˆˆ โ„•0 ( ( ๐‘ โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘š + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘š ) ( ( ๐‘ โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) ) โ†’ ๐‘Ž = ๐‘ ) ) )
69 15 48 68 sylanbrc โŠข ( ๐น โˆˆ ( Poly โ€˜ ๐‘† ) โ†’ โˆƒ! ๐‘Ž โˆˆ ( โ„‚ โ†‘m โ„•0 ) โˆƒ ๐‘› โˆˆ โ„•0 ( ( ๐‘Ž โ€œ ( โ„คโ‰ฅ โ€˜ ( ๐‘› + 1 ) ) ) = { 0 } โˆง ๐น = ( ๐‘ง โˆˆ โ„‚ โ†ฆ ฮฃ ๐‘˜ โˆˆ ( 0 ... ๐‘› ) ( ( ๐‘Ž โ€˜ ๐‘˜ ) ยท ( ๐‘ง โ†‘ ๐‘˜ ) ) ) ) )