Metamath Proof Explorer

Theorem eulerpartlemb

Description: Lemma for eulerpart . The set of all partitions of N is finite. (Contributed by Mario Carneiro, 26-Jan-2015)

Ref Expression
Hypotheses eulerpart.p โŠข ๐‘ƒ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) }
eulerpart.o โŠข ๐‘‚ = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› }
eulerpart.d โŠข ๐ท = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ โ„• ( ๐‘” โ€˜ ๐‘› ) โ‰ค 1 }
eulerpart.j โŠข ๐ฝ = { ๐‘ง โˆˆ โ„• โˆฃ ยฌ 2 โˆฅ ๐‘ง }
eulerpart.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐ฝ , ๐‘ฆ โˆˆ โ„•0 โ†ฆ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
eulerpart.h โŠข ๐ป = { ๐‘Ÿ โˆˆ ( ( ๐’ซ โ„•0 โˆฉ Fin ) โ†‘m ๐ฝ ) โˆฃ ( ๐‘Ÿ supp โˆ… ) โˆˆ Fin }
eulerpart.m โŠข ๐‘€ = ( ๐‘Ÿ โˆˆ ๐ป โ†ฆ { โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ โˆฃ ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ) } )
Assertion eulerpartlemb ๐‘ƒ โˆˆ Fin

Proof

Step Hyp Ref Expression
1 eulerpart.p โŠข ๐‘ƒ = { ๐‘“ โˆˆ ( โ„•0 โ†‘m โ„• ) โˆฃ ( ( โ—ก ๐‘“ โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘“ โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) }
2 eulerpart.o โŠข ๐‘‚ = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ยฌ 2 โˆฅ ๐‘› }
3 eulerpart.d โŠข ๐ท = { ๐‘” โˆˆ ๐‘ƒ โˆฃ โˆ€ ๐‘› โˆˆ โ„• ( ๐‘” โ€˜ ๐‘› ) โ‰ค 1 }
4 eulerpart.j โŠข ๐ฝ = { ๐‘ง โˆˆ โ„• โˆฃ ยฌ 2 โˆฅ ๐‘ง }
5 eulerpart.f โŠข ๐น = ( ๐‘ฅ โˆˆ ๐ฝ , ๐‘ฆ โˆˆ โ„•0 โ†ฆ ( ( 2 โ†‘ ๐‘ฆ ) ยท ๐‘ฅ ) )
6 eulerpart.h โŠข ๐ป = { ๐‘Ÿ โˆˆ ( ( ๐’ซ โ„•0 โˆฉ Fin ) โ†‘m ๐ฝ ) โˆฃ ( ๐‘Ÿ supp โˆ… ) โˆˆ Fin }
7 eulerpart.m โŠข ๐‘€ = ( ๐‘Ÿ โˆˆ ๐ป โ†ฆ { โŸจ ๐‘ฅ , ๐‘ฆ โŸฉ โˆฃ ( ๐‘ฅ โˆˆ ๐ฝ โˆง ๐‘ฆ โˆˆ ( ๐‘Ÿ โ€˜ ๐‘ฅ ) ) } )
8 fzfid โŠข ( โŠค โ†’ ( 1 ... ๐‘ ) โˆˆ Fin )
9 fzfi โŠข ( 0 ... ๐‘ ) โˆˆ Fin
10 snfi โŠข { 0 } โˆˆ Fin
11 9 10 ifcli โŠข if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) โˆˆ Fin
12 11 a1i โŠข ( ( โŠค โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) โˆˆ Fin )
13 eldifn โŠข ( ๐‘ฅ โˆˆ ( โ„• โˆ– ( 1 ... ๐‘ ) ) โ†’ ยฌ ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) )
14 13 adantl โŠข ( ( โŠค โˆง ๐‘ฅ โˆˆ ( โ„• โˆ– ( 1 ... ๐‘ ) ) ) โ†’ ยฌ ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) )
15 iffalse โŠข ( ยฌ ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) โ†’ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) = { 0 } )
16 eqimss โŠข ( if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) = { 0 } โ†’ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) โŠ† { 0 } )
17 14 15 16 3syl โŠข ( ( โŠค โˆง ๐‘ฅ โˆˆ ( โ„• โˆ– ( 1 ... ๐‘ ) ) ) โ†’ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) โŠ† { 0 } )
18 8 12 17 ixpfi2 โŠข ( โŠค โ†’ X ๐‘ฅ โˆˆ โ„• if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) โˆˆ Fin )
19 18 mptru โŠข X ๐‘ฅ โˆˆ โ„• if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) โˆˆ Fin
20 1 eulerpartleme โŠข ( ๐‘” โˆˆ ๐‘ƒ โ†” ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) )
21 ffn โŠข ( ๐‘” : โ„• โŸถ โ„•0 โ†’ ๐‘” Fn โ„• )
22 21 3ad2ant1 โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โ†’ ๐‘” Fn โ„• )
23 ffvelcdm โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„•0 )
24 23 3ad2antl1 โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„•0 )
25 24 nn0red โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„ )
26 nnre โŠข ( ๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ โ„ )
27 26 adantl โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ๐‘ฅ โˆˆ โ„ )
28 25 27 remulcld โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โˆˆ โ„ )
29 cnvimass โŠข ( โ—ก ๐‘” โ€œ โ„• ) โŠ† dom ๐‘”
30 fdm โŠข ( ๐‘” : โ„• โŸถ โ„•0 โ†’ dom ๐‘” = โ„• )
31 30 adantr โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ dom ๐‘” = โ„• )
32 29 31 sseqtrid โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ ( โ—ก ๐‘” โ€œ โ„• ) โŠ† โ„• )
33 32 sselda โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ ๐‘˜ โˆˆ โ„• )
34 ffvelcdm โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ๐‘” โ€˜ ๐‘˜ ) โˆˆ โ„•0 )
35 34 adantlr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ โ„• ) โ†’ ( ๐‘” โ€˜ ๐‘˜ ) โˆˆ โ„•0 )
36 33 35 syldan โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ ( ๐‘” โ€˜ ๐‘˜ ) โˆˆ โ„•0 )
37 33 nnnn0d โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ ๐‘˜ โˆˆ โ„•0 )
38 36 37 nn0mulcld โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) โˆˆ โ„•0 )
39 38 nn0cnd โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) โˆˆ โ„‚ )
40 simpl โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ ๐‘” : โ„• โŸถ โ„•0 )
41 nnex โŠข โ„• โˆˆ V
42 fcdmnn0supp โŠข ( ( โ„• โˆˆ V โˆง ๐‘” : โ„• โŸถ โ„•0 ) โ†’ ( ๐‘” supp 0 ) = ( โ—ก ๐‘” โ€œ โ„• ) )
43 41 42 mpan โŠข ( ๐‘” : โ„• โŸถ โ„•0 โ†’ ( ๐‘” supp 0 ) = ( โ—ก ๐‘” โ€œ โ„• ) )
44 43 adantr โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ ( ๐‘” supp 0 ) = ( โ—ก ๐‘” โ€œ โ„• ) )
45 eqimss โŠข ( ( ๐‘” supp 0 ) = ( โ—ก ๐‘” โ€œ โ„• ) โ†’ ( ๐‘” supp 0 ) โŠ† ( โ—ก ๐‘” โ€œ โ„• ) )
46 44 45 syl โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ ( ๐‘” supp 0 ) โŠ† ( โ—ก ๐‘” โ€œ โ„• ) )
47 41 a1i โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ โ„• โˆˆ V )
48 0nn0 โŠข 0 โˆˆ โ„•0
49 48 a1i โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ 0 โˆˆ โ„•0 )
50 40 46 47 49 suppssr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ( ๐‘” โ€˜ ๐‘˜ ) = 0 )
51 50 oveq1d โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ( 0 ยท ๐‘˜ ) )
52 eldifi โŠข ( ๐‘˜ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ ๐‘˜ โˆˆ โ„• )
53 52 adantl โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ๐‘˜ โˆˆ โ„• )
54 nncn โŠข ( ๐‘˜ โˆˆ โ„• โ†’ ๐‘˜ โˆˆ โ„‚ )
55 mul02 โŠข ( ๐‘˜ โˆˆ โ„‚ โ†’ ( 0 ยท ๐‘˜ ) = 0 )
56 53 54 55 3syl โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ( 0 ยท ๐‘˜ ) = 0 )
57 51 56 eqtrd โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = 0 )
58 nnuz โŠข โ„• = ( โ„คโ‰ฅ โ€˜ 1 )
59 58 eqimssi โŠข โ„• โŠ† ( โ„คโ‰ฅ โ€˜ 1 )
60 59 a1i โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ โ„• โŠ† ( โ„คโ‰ฅ โ€˜ 1 ) )
61 32 39 57 60 sumss โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ ฮฃ ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
62 simpr โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin )
63 62 38 fsumnn0cl โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ ฮฃ ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) โˆˆ โ„•0 )
64 61 63 eqeltrrd โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) โˆˆ โ„•0 )
65 eleq1 โŠข ( ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ โ†’ ( ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) โˆˆ โ„•0 โ†” ๐‘ โˆˆ โ„•0 ) )
66 64 65 syl5ibcom โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ ( ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ โ†’ ๐‘ โˆˆ โ„•0 ) )
67 66 3impia โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โ†’ ๐‘ โˆˆ โ„•0 )
68 67 adantr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ๐‘ โˆˆ โ„•0 )
69 68 nn0red โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ๐‘ โˆˆ โ„ )
70 24 nn0ge0d โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ 0 โ‰ค ( ๐‘” โ€˜ ๐‘ฅ ) )
71 nnge1 โŠข ( ๐‘ฅ โˆˆ โ„• โ†’ 1 โ‰ค ๐‘ฅ )
72 71 adantl โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ 1 โ‰ค ๐‘ฅ )
73 25 27 70 72 lemulge11d โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โ‰ค ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) )
74 62 adantr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ( ๐‘ฅ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin )
75 38 nn0red โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) โˆˆ โ„ )
76 75 adantlr โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ( ๐‘ฅ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) โˆˆ โ„ )
77 38 nn0ge0d โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ 0 โ‰ค ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
78 77 adantlr โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ( ๐‘ฅ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ 0 โ‰ค ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
79 fveq2 โŠข ( ๐‘˜ = ๐‘ฅ โ†’ ( ๐‘” โ€˜ ๐‘˜ ) = ( ๐‘” โ€˜ ๐‘ฅ ) )
80 id โŠข ( ๐‘˜ = ๐‘ฅ โ†’ ๐‘˜ = ๐‘ฅ )
81 79 80 oveq12d โŠข ( ๐‘˜ = ๐‘ฅ โ†’ ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) )
82 simprr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ( ๐‘ฅ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) )
83 74 76 78 81 82 fsumge1 โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ( ๐‘ฅ โˆˆ โ„• โˆง ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ‰ค ฮฃ ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
84 83 expr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ‰ค ฮฃ ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) ) )
85 eldif โŠข ( ๐‘ฅ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) โ†” ( ๐‘ฅ โˆˆ โ„• โˆง ยฌ ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) )
86 57 ralrimiva โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โ†’ โˆ€ ๐‘˜ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = 0 )
87 81 eqeq1d โŠข ( ๐‘˜ = ๐‘ฅ โ†’ ( ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = 0 โ†” ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) = 0 ) )
88 87 rspccva โŠข ( ( โˆ€ ๐‘˜ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = 0 โˆง ๐‘ฅ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) = 0 )
89 86 88 sylan โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ ( โ„• โˆ– ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) = 0 )
90 85 89 sylan2br โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ( ๐‘ฅ โˆˆ โ„• โˆง ยฌ ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) = 0 )
91 62 adantr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin )
92 38 adantlr โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) โˆˆ โ„•0 )
93 92 nn0red โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) โˆˆ โ„ )
94 92 nn0ge0d โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) โ†’ 0 โ‰ค ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
95 91 93 94 fsumge0 โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ 0 โ‰ค ฮฃ ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
96 95 adantrr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ( ๐‘ฅ โˆˆ โ„• โˆง ยฌ ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ 0 โ‰ค ฮฃ ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
97 90 96 eqbrtrd โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ( ๐‘ฅ โˆˆ โ„• โˆง ยฌ ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ) ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ‰ค ฮฃ ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
98 97 expr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ยฌ ๐‘ฅ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ‰ค ฮฃ ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) ) )
99 84 98 pm2.61d โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ‰ค ฮฃ ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
100 61 adantr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ฮฃ ๐‘˜ โˆˆ ( โ—ก ๐‘” โ€œ โ„• ) ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
101 99 100 breqtrd โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ‰ค ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
102 101 3adantl3 โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ‰ค ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) )
103 simpl3 โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ )
104 102 103 breqtrd โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ‰ค ๐‘ )
105 25 28 69 73 104 letrd โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โ‰ค ๐‘ )
106 nn0uz โŠข โ„•0 = ( โ„คโ‰ฅ โ€˜ 0 )
107 24 106 eleqtrdi โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ ( โ„คโ‰ฅ โ€˜ 0 ) )
108 68 nn0zd โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ๐‘ โˆˆ โ„ค )
109 elfz5 โŠข ( ( ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ ( โ„คโ‰ฅ โ€˜ 0 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ ( 0 ... ๐‘ ) โ†” ( ๐‘” โ€˜ ๐‘ฅ ) โ‰ค ๐‘ ) )
110 107 108 109 syl2anc โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ ( 0 ... ๐‘ ) โ†” ( ๐‘” โ€˜ ๐‘ฅ ) โ‰ค ๐‘ ) )
111 105 110 mpbird โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ ( 0 ... ๐‘ ) )
112 111 adantr โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ ( 0 ... ๐‘ ) )
113 iftrue โŠข ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) โ†’ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) = ( 0 ... ๐‘ ) )
114 113 adantl โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) ) โ†’ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) = ( 0 ... ๐‘ ) )
115 112 114 eleqtrrd โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) )
116 nnge1 โŠข ( ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„• โ†’ 1 โ‰ค ( ๐‘” โ€˜ ๐‘ฅ ) )
117 nnnn0 โŠข ( ๐‘ฅ โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ โ„•0 )
118 117 adantl โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ๐‘ฅ โˆˆ โ„•0 )
119 118 nn0ge0d โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ 0 โ‰ค ๐‘ฅ )
120 lemulge12 โŠข ( ( ( ๐‘ฅ โˆˆ โ„ โˆง ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„ ) โˆง ( 0 โ‰ค ๐‘ฅ โˆง 1 โ‰ค ( ๐‘” โ€˜ ๐‘ฅ ) ) ) โ†’ ๐‘ฅ โ‰ค ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) )
121 120 expr โŠข ( ( ( ๐‘ฅ โˆˆ โ„ โˆง ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„ ) โˆง 0 โ‰ค ๐‘ฅ ) โ†’ ( 1 โ‰ค ( ๐‘” โ€˜ ๐‘ฅ ) โ†’ ๐‘ฅ โ‰ค ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) ) )
122 27 25 119 121 syl21anc โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( 1 โ‰ค ( ๐‘” โ€˜ ๐‘ฅ ) โ†’ ๐‘ฅ โ‰ค ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) ) )
123 letr โŠข ( ( ๐‘ฅ โˆˆ โ„ โˆง ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โˆˆ โ„ โˆง ๐‘ โˆˆ โ„ ) โ†’ ( ( ๐‘ฅ โ‰ค ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โˆง ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ‰ค ๐‘ ) โ†’ ๐‘ฅ โ‰ค ๐‘ ) )
124 27 28 69 123 syl3anc โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ( ๐‘ฅ โ‰ค ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โˆง ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ‰ค ๐‘ ) โ†’ ๐‘ฅ โ‰ค ๐‘ ) )
125 104 124 mpan2d โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘ฅ โ‰ค ( ( ๐‘” โ€˜ ๐‘ฅ ) ยท ๐‘ฅ ) โ†’ ๐‘ฅ โ‰ค ๐‘ ) )
126 122 125 syld โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( 1 โ‰ค ( ๐‘” โ€˜ ๐‘ฅ ) โ†’ ๐‘ฅ โ‰ค ๐‘ ) )
127 116 126 syl5 โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„• โ†’ ๐‘ฅ โ‰ค ๐‘ ) )
128 simpr โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ๐‘ฅ โˆˆ โ„• )
129 128 58 eleqtrdi โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) )
130 elfz5 โŠข ( ( ๐‘ฅ โˆˆ ( โ„คโ‰ฅ โ€˜ 1 ) โˆง ๐‘ โˆˆ โ„ค ) โ†’ ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) โ†” ๐‘ฅ โ‰ค ๐‘ ) )
131 129 108 130 syl2anc โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) โ†” ๐‘ฅ โ‰ค ๐‘ ) )
132 127 131 sylibrd โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„• โ†’ ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) ) )
133 132 con3d โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ยฌ ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) โ†’ ยฌ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„• ) )
134 elnn0 โŠข ( ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„•0 โ†” ( ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„• โˆจ ( ๐‘” โ€˜ ๐‘ฅ ) = 0 ) )
135 24 134 sylib โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„• โˆจ ( ๐‘” โ€˜ ๐‘ฅ ) = 0 ) )
136 135 ord โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ยฌ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ โ„• โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) = 0 ) )
137 133 136 syld โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ยฌ ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) = 0 ) )
138 137 imp โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ยฌ ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) = 0 )
139 fvex โŠข ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ V
140 139 elsn โŠข ( ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ { 0 } โ†” ( ๐‘” โ€˜ ๐‘ฅ ) = 0 )
141 138 140 sylibr โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ยฌ ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ { 0 } )
142 15 adantl โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ยฌ ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) ) โ†’ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) = { 0 } )
143 141 142 eleqtrrd โŠข ( ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โˆง ยฌ ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) )
144 115 143 pm2.61dan โŠข ( ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โˆง ๐‘ฅ โˆˆ โ„• ) โ†’ ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) )
145 144 ralrimiva โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โ†’ โˆ€ ๐‘ฅ โˆˆ โ„• ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) )
146 vex โŠข ๐‘” โˆˆ V
147 146 elixp โŠข ( ๐‘” โˆˆ X ๐‘ฅ โˆˆ โ„• if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) โ†” ( ๐‘” Fn โ„• โˆง โˆ€ ๐‘ฅ โˆˆ โ„• ( ๐‘” โ€˜ ๐‘ฅ ) โˆˆ if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) ) )
148 22 145 147 sylanbrc โŠข ( ( ๐‘” : โ„• โŸถ โ„•0 โˆง ( โ—ก ๐‘” โ€œ โ„• ) โˆˆ Fin โˆง ฮฃ ๐‘˜ โˆˆ โ„• ( ( ๐‘” โ€˜ ๐‘˜ ) ยท ๐‘˜ ) = ๐‘ ) โ†’ ๐‘” โˆˆ X ๐‘ฅ โˆˆ โ„• if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) )
149 20 148 sylbi โŠข ( ๐‘” โˆˆ ๐‘ƒ โ†’ ๐‘” โˆˆ X ๐‘ฅ โˆˆ โ„• if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) )
150 149 ssriv โŠข ๐‘ƒ โŠ† X ๐‘ฅ โˆˆ โ„• if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } )
151 ssfi โŠข ( ( X ๐‘ฅ โˆˆ โ„• if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) โˆˆ Fin โˆง ๐‘ƒ โŠ† X ๐‘ฅ โˆˆ โ„• if ( ๐‘ฅ โˆˆ ( 1 ... ๐‘ ) , ( 0 ... ๐‘ ) , { 0 } ) ) โ†’ ๐‘ƒ โˆˆ Fin )
152 19 150 151 mp2an โŠข ๐‘ƒ โˆˆ Fin