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 
|- P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
eulerpart.o 
|- O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
eulerpart.d 
|- D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
eulerpart.j 
|- J = { z e. NN | -. 2 || z }
eulerpart.f 
|- F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
eulerpart.h 
|- H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
eulerpart.m 
|- M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
Assertion eulerpartlemb 
|- P e. Fin

Proof

Step Hyp Ref Expression
1 eulerpart.p 
 |-  P = { f e. ( NN0 ^m NN ) | ( ( `' f " NN ) e. Fin /\ sum_ k e. NN ( ( f ` k ) x. k ) = N ) }
2 eulerpart.o 
 |-  O = { g e. P | A. n e. ( `' g " NN ) -. 2 || n }
3 eulerpart.d 
 |-  D = { g e. P | A. n e. NN ( g ` n ) <_ 1 }
4 eulerpart.j 
 |-  J = { z e. NN | -. 2 || z }
5 eulerpart.f 
 |-  F = ( x e. J , y e. NN0 |-> ( ( 2 ^ y ) x. x ) )
6 eulerpart.h 
 |-  H = { r e. ( ( ~P NN0 i^i Fin ) ^m J ) | ( r supp (/) ) e. Fin }
7 eulerpart.m 
 |-  M = ( r e. H |-> { <. x , y >. | ( x e. J /\ y e. ( r ` x ) ) } )
8 fzfid 
 |-  ( T. -> ( 1 ... N ) e. Fin )
9 fzfi 
 |-  ( 0 ... N ) e. Fin
10 snfi 
 |-  { 0 } e. Fin
11 9 10 ifcli 
 |-  if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) e. Fin
12 11 a1i 
 |-  ( ( T. /\ x e. NN ) -> if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) e. Fin )
13 eldifn 
 |-  ( x e. ( NN \ ( 1 ... N ) ) -> -. x e. ( 1 ... N ) )
14 13 adantl 
 |-  ( ( T. /\ x e. ( NN \ ( 1 ... N ) ) ) -> -. x e. ( 1 ... N ) )
15 iffalse 
 |-  ( -. x e. ( 1 ... N ) -> if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) = { 0 } )
16 eqimss 
 |-  ( if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) = { 0 } -> if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) C_ { 0 } )
17 14 15 16 3syl 
 |-  ( ( T. /\ x e. ( NN \ ( 1 ... N ) ) ) -> if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) C_ { 0 } )
18 8 12 17 ixpfi2 
 |-  ( T. -> X_ x e. NN if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) e. Fin )
19 18 mptru 
 |-  X_ x e. NN if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) e. Fin
20 1 eulerpartleme 
 |-  ( g e. P <-> ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) )
21 ffn 
 |-  ( g : NN --> NN0 -> g Fn NN )
22 21 3ad2ant1 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) -> g Fn NN )
23 ffvelcdm 
 |-  ( ( g : NN --> NN0 /\ x e. NN ) -> ( g ` x ) e. NN0 )
24 23 3ad2antl1 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( g ` x ) e. NN0 )
25 24 nn0red 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( g ` x ) e. RR )
26 nnre 
 |-  ( x e. NN -> x e. RR )
27 26 adantl 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> x e. RR )
28 25 27 remulcld 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( ( g ` x ) x. x ) e. RR )
29 cnvimass 
 |-  ( `' g " NN ) C_ dom g
30 fdm 
 |-  ( g : NN --> NN0 -> dom g = NN )
31 30 adantr 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> dom g = NN )
32 29 31 sseqtrid 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> ( `' g " NN ) C_ NN )
33 32 sselda 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( `' g " NN ) ) -> k e. NN )
34 ffvelcdm 
 |-  ( ( g : NN --> NN0 /\ k e. NN ) -> ( g ` k ) e. NN0 )
35 34 adantlr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. NN ) -> ( g ` k ) e. NN0 )
36 33 35 syldan 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( `' g " NN ) ) -> ( g ` k ) e. NN0 )
37 33 nnnn0d 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( `' g " NN ) ) -> k e. NN0 )
38 36 37 nn0mulcld 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( `' g " NN ) ) -> ( ( g ` k ) x. k ) e. NN0 )
39 38 nn0cnd 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( `' g " NN ) ) -> ( ( g ` k ) x. k ) e. CC )
40 simpl 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> g : NN --> NN0 )
41 nnex 
 |-  NN e. _V
42 fcdmnn0supp 
 |-  ( ( NN e. _V /\ g : NN --> NN0 ) -> ( g supp 0 ) = ( `' g " NN ) )
43 41 42 mpan 
 |-  ( g : NN --> NN0 -> ( g supp 0 ) = ( `' g " NN ) )
44 43 adantr 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> ( g supp 0 ) = ( `' g " NN ) )
45 eqimss 
 |-  ( ( g supp 0 ) = ( `' g " NN ) -> ( g supp 0 ) C_ ( `' g " NN ) )
46 44 45 syl 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> ( g supp 0 ) C_ ( `' g " NN ) )
47 41 a1i 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> NN e. _V )
48 0nn0 
 |-  0 e. NN0
49 48 a1i 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> 0 e. NN0 )
50 40 46 47 49 suppssr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( NN \ ( `' g " NN ) ) ) -> ( g ` k ) = 0 )
51 50 oveq1d 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( NN \ ( `' g " NN ) ) ) -> ( ( g ` k ) x. k ) = ( 0 x. k ) )
52 eldifi 
 |-  ( k e. ( NN \ ( `' g " NN ) ) -> k e. NN )
53 52 adantl 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( NN \ ( `' g " NN ) ) ) -> k e. NN )
54 nncn 
 |-  ( k e. NN -> k e. CC )
55 mul02 
 |-  ( k e. CC -> ( 0 x. k ) = 0 )
56 53 54 55 3syl 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( NN \ ( `' g " NN ) ) ) -> ( 0 x. k ) = 0 )
57 51 56 eqtrd 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( NN \ ( `' g " NN ) ) ) -> ( ( g ` k ) x. k ) = 0 )
58 nnuz 
 |-  NN = ( ZZ>= ` 1 )
59 58 eqimssi 
 |-  NN C_ ( ZZ>= ` 1 )
60 59 a1i 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> NN C_ ( ZZ>= ` 1 ) )
61 32 39 57 60 sumss 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) = sum_ k e. NN ( ( g ` k ) x. k ) )
62 simpr 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> ( `' g " NN ) e. Fin )
63 62 38 fsumnn0cl 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) e. NN0 )
64 61 63 eqeltrrd 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> sum_ k e. NN ( ( g ` k ) x. k ) e. NN0 )
65 eleq1 
 |-  ( sum_ k e. NN ( ( g ` k ) x. k ) = N -> ( sum_ k e. NN ( ( g ` k ) x. k ) e. NN0 <-> N e. NN0 ) )
66 64 65 syl5ibcom 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> ( sum_ k e. NN ( ( g ` k ) x. k ) = N -> N e. NN0 ) )
67 66 3impia 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) -> N e. NN0 )
68 67 adantr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> N e. NN0 )
69 68 nn0red 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> N e. RR )
70 24 nn0ge0d 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> 0 <_ ( g ` x ) )
71 nnge1 
 |-  ( x e. NN -> 1 <_ x )
72 71 adantl 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> 1 <_ x )
73 25 27 70 72 lemulge11d 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( g ` x ) <_ ( ( g ` x ) x. x ) )
74 62 adantr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ ( x e. NN /\ x e. ( `' g " NN ) ) ) -> ( `' g " NN ) e. Fin )
75 38 nn0red 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( `' g " NN ) ) -> ( ( g ` k ) x. k ) e. RR )
76 75 adantlr 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ ( x e. NN /\ x e. ( `' g " NN ) ) ) /\ k e. ( `' g " NN ) ) -> ( ( g ` k ) x. k ) e. RR )
77 38 nn0ge0d 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ k e. ( `' g " NN ) ) -> 0 <_ ( ( g ` k ) x. k ) )
78 77 adantlr 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ ( x e. NN /\ x e. ( `' g " NN ) ) ) /\ k e. ( `' g " NN ) ) -> 0 <_ ( ( g ` k ) x. k ) )
79 fveq2 
 |-  ( k = x -> ( g ` k ) = ( g ` x ) )
80 id 
 |-  ( k = x -> k = x )
81 79 80 oveq12d 
 |-  ( k = x -> ( ( g ` k ) x. k ) = ( ( g ` x ) x. x ) )
82 simprr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ ( x e. NN /\ x e. ( `' g " NN ) ) ) -> x e. ( `' g " NN ) )
83 74 76 78 81 82 fsumge1 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ ( x e. NN /\ x e. ( `' g " NN ) ) ) -> ( ( g ` x ) x. x ) <_ sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) )
84 83 expr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. NN ) -> ( x e. ( `' g " NN ) -> ( ( g ` x ) x. x ) <_ sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) ) )
85 eldif 
 |-  ( x e. ( NN \ ( `' g " NN ) ) <-> ( x e. NN /\ -. x e. ( `' g " NN ) ) )
86 57 ralrimiva 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) -> A. k e. ( NN \ ( `' g " NN ) ) ( ( g ` k ) x. k ) = 0 )
87 81 eqeq1d 
 |-  ( k = x -> ( ( ( g ` k ) x. k ) = 0 <-> ( ( g ` x ) x. x ) = 0 ) )
88 87 rspccva 
 |-  ( ( A. k e. ( NN \ ( `' g " NN ) ) ( ( g ` k ) x. k ) = 0 /\ x e. ( NN \ ( `' g " NN ) ) ) -> ( ( g ` x ) x. x ) = 0 )
89 86 88 sylan 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. ( NN \ ( `' g " NN ) ) ) -> ( ( g ` x ) x. x ) = 0 )
90 85 89 sylan2br 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ ( x e. NN /\ -. x e. ( `' g " NN ) ) ) -> ( ( g ` x ) x. x ) = 0 )
91 62 adantr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. NN ) -> ( `' g " NN ) e. Fin )
92 38 adantlr 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. NN ) /\ k e. ( `' g " NN ) ) -> ( ( g ` k ) x. k ) e. NN0 )
93 92 nn0red 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. NN ) /\ k e. ( `' g " NN ) ) -> ( ( g ` k ) x. k ) e. RR )
94 92 nn0ge0d 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. NN ) /\ k e. ( `' g " NN ) ) -> 0 <_ ( ( g ` k ) x. k ) )
95 91 93 94 fsumge0 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. NN ) -> 0 <_ sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) )
96 95 adantrr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ ( x e. NN /\ -. x e. ( `' g " NN ) ) ) -> 0 <_ sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) )
97 90 96 eqbrtrd 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ ( x e. NN /\ -. x e. ( `' g " NN ) ) ) -> ( ( g ` x ) x. x ) <_ sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) )
98 97 expr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. NN ) -> ( -. x e. ( `' g " NN ) -> ( ( g ` x ) x. x ) <_ sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) ) )
99 84 98 pm2.61d 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. NN ) -> ( ( g ` x ) x. x ) <_ sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) )
100 61 adantr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. NN ) -> sum_ k e. ( `' g " NN ) ( ( g ` k ) x. k ) = sum_ k e. NN ( ( g ` k ) x. k ) )
101 99 100 breqtrd 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin ) /\ x e. NN ) -> ( ( g ` x ) x. x ) <_ sum_ k e. NN ( ( g ` k ) x. k ) )
102 101 3adantl3 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( ( g ` x ) x. x ) <_ sum_ k e. NN ( ( g ` k ) x. k ) )
103 simpl3 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> sum_ k e. NN ( ( g ` k ) x. k ) = N )
104 102 103 breqtrd 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( ( g ` x ) x. x ) <_ N )
105 25 28 69 73 104 letrd 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( g ` x ) <_ N )
106 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
107 24 106 eleqtrdi 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( g ` x ) e. ( ZZ>= ` 0 ) )
108 68 nn0zd 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> N e. ZZ )
109 elfz5 
 |-  ( ( ( g ` x ) e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( ( g ` x ) e. ( 0 ... N ) <-> ( g ` x ) <_ N ) )
110 107 108 109 syl2anc 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( ( g ` x ) e. ( 0 ... N ) <-> ( g ` x ) <_ N ) )
111 105 110 mpbird 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( g ` x ) e. ( 0 ... N ) )
112 111 adantr 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) /\ x e. ( 1 ... N ) ) -> ( g ` x ) e. ( 0 ... N ) )
113 iftrue 
 |-  ( x e. ( 1 ... N ) -> if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) = ( 0 ... N ) )
114 113 adantl 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) /\ x e. ( 1 ... N ) ) -> if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) = ( 0 ... N ) )
115 112 114 eleqtrrd 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) /\ x e. ( 1 ... N ) ) -> ( g ` x ) e. if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) )
116 nnge1 
 |-  ( ( g ` x ) e. NN -> 1 <_ ( g ` x ) )
117 nnnn0 
 |-  ( x e. NN -> x e. NN0 )
118 117 adantl 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> x e. NN0 )
119 118 nn0ge0d 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> 0 <_ x )
120 lemulge12 
 |-  ( ( ( x e. RR /\ ( g ` x ) e. RR ) /\ ( 0 <_ x /\ 1 <_ ( g ` x ) ) ) -> x <_ ( ( g ` x ) x. x ) )
121 120 expr 
 |-  ( ( ( x e. RR /\ ( g ` x ) e. RR ) /\ 0 <_ x ) -> ( 1 <_ ( g ` x ) -> x <_ ( ( g ` x ) x. x ) ) )
122 27 25 119 121 syl21anc 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( 1 <_ ( g ` x ) -> x <_ ( ( g ` x ) x. x ) ) )
123 letr 
 |-  ( ( x e. RR /\ ( ( g ` x ) x. x ) e. RR /\ N e. RR ) -> ( ( x <_ ( ( g ` x ) x. x ) /\ ( ( g ` x ) x. x ) <_ N ) -> x <_ N ) )
124 27 28 69 123 syl3anc 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( ( x <_ ( ( g ` x ) x. x ) /\ ( ( g ` x ) x. x ) <_ N ) -> x <_ N ) )
125 104 124 mpan2d 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( x <_ ( ( g ` x ) x. x ) -> x <_ N ) )
126 122 125 syld 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( 1 <_ ( g ` x ) -> x <_ N ) )
127 116 126 syl5 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( ( g ` x ) e. NN -> x <_ N ) )
128 simpr 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> x e. NN )
129 128 58 eleqtrdi 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> x e. ( ZZ>= ` 1 ) )
130 elfz5 
 |-  ( ( x e. ( ZZ>= ` 1 ) /\ N e. ZZ ) -> ( x e. ( 1 ... N ) <-> x <_ N ) )
131 129 108 130 syl2anc 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( x e. ( 1 ... N ) <-> x <_ N ) )
132 127 131 sylibrd 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( ( g ` x ) e. NN -> x e. ( 1 ... N ) ) )
133 132 con3d 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( -. x e. ( 1 ... N ) -> -. ( g ` x ) e. NN ) )
134 elnn0 
 |-  ( ( g ` x ) e. NN0 <-> ( ( g ` x ) e. NN \/ ( g ` x ) = 0 ) )
135 24 134 sylib 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( ( g ` x ) e. NN \/ ( g ` x ) = 0 ) )
136 135 ord 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( -. ( g ` x ) e. NN -> ( g ` x ) = 0 ) )
137 133 136 syld 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( -. x e. ( 1 ... N ) -> ( g ` x ) = 0 ) )
138 137 imp 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) /\ -. x e. ( 1 ... N ) ) -> ( g ` x ) = 0 )
139 fvex 
 |-  ( g ` x ) e. _V
140 139 elsn 
 |-  ( ( g ` x ) e. { 0 } <-> ( g ` x ) = 0 )
141 138 140 sylibr 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) /\ -. x e. ( 1 ... N ) ) -> ( g ` x ) e. { 0 } )
142 15 adantl 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) /\ -. x e. ( 1 ... N ) ) -> if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) = { 0 } )
143 141 142 eleqtrrd 
 |-  ( ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) /\ -. x e. ( 1 ... N ) ) -> ( g ` x ) e. if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) )
144 115 143 pm2.61dan 
 |-  ( ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) /\ x e. NN ) -> ( g ` x ) e. if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) )
145 144 ralrimiva 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) -> A. x e. NN ( g ` x ) e. if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) )
146 vex 
 |-  g e. _V
147 146 elixp 
 |-  ( g e. X_ x e. NN if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) <-> ( g Fn NN /\ A. x e. NN ( g ` x ) e. if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) ) )
148 22 145 147 sylanbrc 
 |-  ( ( g : NN --> NN0 /\ ( `' g " NN ) e. Fin /\ sum_ k e. NN ( ( g ` k ) x. k ) = N ) -> g e. X_ x e. NN if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) )
149 20 148 sylbi 
 |-  ( g e. P -> g e. X_ x e. NN if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) )
150 149 ssriv 
 |-  P C_ X_ x e. NN if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } )
151 ssfi 
 |-  ( ( X_ x e. NN if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) e. Fin /\ P C_ X_ x e. NN if ( x e. ( 1 ... N ) , ( 0 ... N ) , { 0 } ) ) -> P e. Fin )
152 19 150 151 mp2an 
 |-  P e. Fin