Theorem subfacp1lem6

Description: Lemma for subfacp1 . By induction, we cut up the set of all derangements on N + 1 according to the N possible values of ( f1 ) (since ( f1 ) =/= 1 ), and for each set for fixed M = ( f1 ) , the subset of derangements with ( fM ) = 1 has size S ( N - 1 ) (by subfacp1lem3 ), while the subset with ( fM ) =/= 1 has size S ( N ) (by subfacp1lem5 ). Adding it all up yields the desired equation N ( S ( N ) + S ( N - 1 ) ) for the number of derangements on N + 1 . (Contributed by Mario Carneiro, 22-Jan-2015)

	Ref	Expression
Hypotheses	derang.d	|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
	subfac.n	|- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
	subfacp1lem.a	|- A = { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
Assertion	subfacp1lem6	|- ( N e. NN -> ( S ` ( N + 1 ) ) = ( N x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		derang.d	|- D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
2		subfac.n	|- S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
3		subfacp1lem.a	|- A = { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
4		peano2nn	|- ( N e. NN -> ( N + 1 ) e. NN )
5	4	nnnn0d	|- ( N e. NN -> ( N + 1 ) e. NN0 )
6	1 2	subfacval	|- ( ( N + 1 ) e. NN0 -> ( S ` ( N + 1 ) ) = ( D ` ( 1 ... ( N + 1 ) ) ) )
7	5 6	syl	|- ( N e. NN -> ( S ` ( N + 1 ) ) = ( D ` ( 1 ... ( N + 1 ) ) ) )
8		fzfid	|- ( N e. NN -> ( 1 ... ( N + 1 ) ) e. Fin )
9	1	derangval	|- ( ( 1 ... ( N + 1 ) ) e. Fin -> ( D ` ( 1 ... ( N + 1 ) ) ) = ( # ` { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } ) )
10	8 9	syl	|- ( N e. NN -> ( D ` ( 1 ... ( N + 1 ) ) ) = ( # ` { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } ) )
11	3	fveq2i	|- ( # ` A ) = ( # ` { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } )
12	10 11	eqtr4di	|- ( N e. NN -> ( D ` ( 1 ... ( N + 1 ) ) ) = ( # ` A ) )
13		nnuz	|- NN = ( ZZ>= ` 1 )
14	4 13	eleqtrdi	|- ( N e. NN -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
15		eluzfz1	|- ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( N + 1 ) ) )
16	14 15	syl	|- ( N e. NN -> 1 e. ( 1 ... ( N + 1 ) ) )
17		f1of	|- ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> f : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
18	17	adantr	|- ( ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) -> f : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
19		ffvelrn	|- ( ( f : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ 1 e. ( 1 ... ( N + 1 ) ) ) -> ( f ` 1 ) e. ( 1 ... ( N + 1 ) ) )
20	19	expcom	|- ( 1 e. ( 1 ... ( N + 1 ) ) -> ( f : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) -> ( f ` 1 ) e. ( 1 ... ( N + 1 ) ) ) )
21	16 18 20	syl2im	|- ( N e. NN -> ( ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) -> ( f ` 1 ) e. ( 1 ... ( N + 1 ) ) ) )
22	21	ss2abdv	|- ( N e. NN -> { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } C_ { f | ( f ` 1 ) e. ( 1 ... ( N + 1 ) ) } )
23		fveq1	|- ( g = f -> ( g ` 1 ) = ( f ` 1 ) )
24	23	eleq1d	|- ( g = f -> ( ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) <-> ( f ` 1 ) e. ( 1 ... ( N + 1 ) ) ) )
25	24	cbvabv	|- { g | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } = { f | ( f ` 1 ) e. ( 1 ... ( N + 1 ) ) }
26	22 3 25	3sstr4g	|- ( N e. NN -> A C_ { g | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } )
27		ssabral	|- ( A C_ { g | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } <-> A. g e. A ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) )
28	26 27	sylib	|- ( N e. NN -> A. g e. A ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) )
29		rabid2	|- ( A = { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } <-> A. g e. A ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) )
30	28 29	sylibr	|- ( N e. NN -> A = { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } )
31	30	fveq2d	|- ( N e. NN -> ( # ` A ) = ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } ) )
32	7 12 31	3eqtrd	|- ( N e. NN -> ( S ` ( N + 1 ) ) = ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } ) )
33		elfz1end	|- ( ( N + 1 ) e. NN <-> ( N + 1 ) e. ( 1 ... ( N + 1 ) ) )
34	4 33	sylib	|- ( N e. NN -> ( N + 1 ) e. ( 1 ... ( N + 1 ) ) )
35		eleq1	|- ( x = 1 -> ( x e. ( 1 ... ( N + 1 ) ) <-> 1 e. ( 1 ... ( N + 1 ) ) ) )
36		oveq2	|- ( x = 1 -> ( 1 ... x ) = ( 1 ... 1 ) )
37		1z	|- 1 e. ZZ
38		fzsn	|- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
39	37 38	ax-mp	|- ( 1 ... 1 ) = { 1 }
40	36 39	eqtrdi	|- ( x = 1 -> ( 1 ... x ) = { 1 } )
41	40	eleq2d	|- ( x = 1 -> ( ( g ` 1 ) e. ( 1 ... x ) <-> ( g ` 1 ) e. { 1 } ) )
42		fvex	|- ( g ` 1 ) e. _V
43	42	elsn	|- ( ( g ` 1 ) e. { 1 } <-> ( g ` 1 ) = 1 )
44	41 43	bitrdi	|- ( x = 1 -> ( ( g ` 1 ) e. ( 1 ... x ) <-> ( g ` 1 ) = 1 ) )
45	44	rabbidv	|- ( x = 1 -> { g e. A | ( g ` 1 ) e. ( 1 ... x ) } = { g e. A | ( g ` 1 ) = 1 } )
46	45	fveq2d	|- ( x = 1 -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( # ` { g e. A | ( g ` 1 ) = 1 } ) )
47		oveq1	|- ( x = 1 -> ( x - 1 ) = ( 1 - 1 ) )
48		1m1e0	|- ( 1 - 1 ) = 0
49	47 48	eqtrdi	|- ( x = 1 -> ( x - 1 ) = 0 )
50	49	oveq1d	|- ( x = 1 -> ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = ( 0 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )
51	46 50	eqeq12d	|- ( x = 1 -> ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) <-> ( # ` { g e. A | ( g ` 1 ) = 1 } ) = ( 0 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) )
52	35 51	imbi12d	|- ( x = 1 -> ( ( x e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) <-> ( 1 e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) = 1 } ) = ( 0 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) )
53	52	imbi2d	|- ( x = 1 -> ( ( N e. NN -> ( x e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) <-> ( N e. NN -> ( 1 e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) = 1 } ) = ( 0 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) ) )
54		eleq1	|- ( x = m -> ( x e. ( 1 ... ( N + 1 ) ) <-> m e. ( 1 ... ( N + 1 ) ) ) )
55		oveq2	|- ( x = m -> ( 1 ... x ) = ( 1 ... m ) )
56	55	eleq2d	|- ( x = m -> ( ( g ` 1 ) e. ( 1 ... x ) <-> ( g ` 1 ) e. ( 1 ... m ) ) )
57	56	rabbidv	|- ( x = m -> { g e. A | ( g ` 1 ) e. ( 1 ... x ) } = { g e. A | ( g ` 1 ) e. ( 1 ... m ) } )
58	57	fveq2d	|- ( x = m -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) )
59		oveq1	|- ( x = m -> ( x - 1 ) = ( m - 1 ) )
60	59	oveq1d	|- ( x = m -> ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )
61	58 60	eqeq12d	|- ( x = m -> ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) <-> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) )
62	54 61	imbi12d	|- ( x = m -> ( ( x e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) <-> ( m e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) )
63	62	imbi2d	|- ( x = m -> ( ( N e. NN -> ( x e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) <-> ( N e. NN -> ( m e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) ) )
64		eleq1	|- ( x = ( m + 1 ) -> ( x e. ( 1 ... ( N + 1 ) ) <-> ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) )
65		oveq2	|- ( x = ( m + 1 ) -> ( 1 ... x ) = ( 1 ... ( m + 1 ) ) )
66	65	eleq2d	|- ( x = ( m + 1 ) -> ( ( g ` 1 ) e. ( 1 ... x ) <-> ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) ) )
67	66	rabbidv	|- ( x = ( m + 1 ) -> { g e. A | ( g ` 1 ) e. ( 1 ... x ) } = { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } )
68	67	fveq2d	|- ( x = ( m + 1 ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) )
69		oveq1	|- ( x = ( m + 1 ) -> ( x - 1 ) = ( ( m + 1 ) - 1 ) )
70	69	oveq1d	|- ( x = ( m + 1 ) -> ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )
71	68 70	eqeq12d	|- ( x = ( m + 1 ) -> ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) <-> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) )
72	64 71	imbi12d	|- ( x = ( m + 1 ) -> ( ( x e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) <-> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) )
73	72	imbi2d	|- ( x = ( m + 1 ) -> ( ( N e. NN -> ( x e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) <-> ( N e. NN -> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) ) )
74		eleq1	|- ( x = ( N + 1 ) -> ( x e. ( 1 ... ( N + 1 ) ) <-> ( N + 1 ) e. ( 1 ... ( N + 1 ) ) ) )
75		oveq2	|- ( x = ( N + 1 ) -> ( 1 ... x ) = ( 1 ... ( N + 1 ) ) )
76	75	eleq2d	|- ( x = ( N + 1 ) -> ( ( g ` 1 ) e. ( 1 ... x ) <-> ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) ) )
77	76	rabbidv	|- ( x = ( N + 1 ) -> { g e. A | ( g ` 1 ) e. ( 1 ... x ) } = { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } )
78	77	fveq2d	|- ( x = ( N + 1 ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } ) )
79		oveq1	|- ( x = ( N + 1 ) -> ( x - 1 ) = ( ( N + 1 ) - 1 ) )
80	79	oveq1d	|- ( x = ( N + 1 ) -> ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = ( ( ( N + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )
81	78 80	eqeq12d	|- ( x = ( N + 1 ) -> ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) <-> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } ) = ( ( ( N + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) )
82	74 81	imbi12d	|- ( x = ( N + 1 ) -> ( ( x e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) <-> ( ( N + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } ) = ( ( ( N + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) )
83	82	imbi2d	|- ( x = ( N + 1 ) -> ( ( N e. NN -> ( x e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... x ) } ) = ( ( x - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) <-> ( N e. NN -> ( ( N + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } ) = ( ( ( N + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) ) )
84		hash0	|- ( # ` (/) ) = 0
85		fveq2	|- ( y = 1 -> ( f ` y ) = ( f ` 1 ) )
86		id	|- ( y = 1 -> y = 1 )
87	85 86	neeq12d	|- ( y = 1 -> ( ( f ` y ) =/= y <-> ( f ` 1 ) =/= 1 ) )
88	87	rspcv	|- ( 1 e. ( 1 ... ( N + 1 ) ) -> ( A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y -> ( f ` 1 ) =/= 1 ) )
89	16 88	syl	|- ( N e. NN -> ( A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y -> ( f ` 1 ) =/= 1 ) )
90	89	adantld	|- ( N e. NN -> ( ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) -> ( f ` 1 ) =/= 1 ) )
91	90	ss2abdv	|- ( N e. NN -> { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } C_ { f | ( f ` 1 ) =/= 1 } )
92		df-ne	|- ( ( g ` 1 ) =/= 1 <-> -. ( g ` 1 ) = 1 )
93	23	neeq1d	|- ( g = f -> ( ( g ` 1 ) =/= 1 <-> ( f ` 1 ) =/= 1 ) )
94	92 93	bitr3id	|- ( g = f -> ( -. ( g ` 1 ) = 1 <-> ( f ` 1 ) =/= 1 ) )
95	94	cbvabv	|- { g | -. ( g ` 1 ) = 1 } = { f | ( f ` 1 ) =/= 1 }
96	91 3 95	3sstr4g	|- ( N e. NN -> A C_ { g | -. ( g ` 1 ) = 1 } )
97		ssabral	|- ( A C_ { g | -. ( g ` 1 ) = 1 } <-> A. g e. A -. ( g ` 1 ) = 1 )
98	96 97	sylib	|- ( N e. NN -> A. g e. A -. ( g ` 1 ) = 1 )
99		rabeq0	|- ( { g e. A | ( g ` 1 ) = 1 } = (/) <-> A. g e. A -. ( g ` 1 ) = 1 )
100	98 99	sylibr	|- ( N e. NN -> { g e. A | ( g ` 1 ) = 1 } = (/) )
101	100	fveq2d	|- ( N e. NN -> ( # ` { g e. A | ( g ` 1 ) = 1 } ) = ( # ` (/) ) )
102		nnnn0	|- ( N e. NN -> N e. NN0 )
103	1 2	subfacf	|- S : NN0 --> NN0
104	103	ffvelrni	|- ( N e. NN0 -> ( S ` N ) e. NN0 )
105	102 104	syl	|- ( N e. NN -> ( S ` N ) e. NN0 )
106		nnm1nn0	|- ( N e. NN -> ( N - 1 ) e. NN0 )
107	103	ffvelrni	|- ( ( N - 1 ) e. NN0 -> ( S ` ( N - 1 ) ) e. NN0 )
108	106 107	syl	|- ( N e. NN -> ( S ` ( N - 1 ) ) e. NN0 )
109	105 108	nn0addcld	|- ( N e. NN -> ( ( S ` N ) + ( S ` ( N - 1 ) ) ) e. NN0 )
110	109	nn0cnd	|- ( N e. NN -> ( ( S ` N ) + ( S ` ( N - 1 ) ) ) e. CC )
111	110	mul02d	|- ( N e. NN -> ( 0 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = 0 )
112	84 101 111	3eqtr4a	|- ( N e. NN -> ( # ` { g e. A | ( g ` 1 ) = 1 } ) = ( 0 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )
113	112	a1d	|- ( N e. NN -> ( 1 e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) = 1 } ) = ( 0 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) )
114		simplr	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> m e. NN )
115	114 13	eleqtrdi	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> m e. ( ZZ>= ` 1 ) )
116		peano2fzr	|- ( ( m e. ( ZZ>= ` 1 ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> m e. ( 1 ... ( N + 1 ) ) )
117	115 116	sylancom	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> m e. ( 1 ... ( N + 1 ) ) )
118	117	ex	|- ( ( N e. NN /\ m e. NN ) -> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) -> m e. ( 1 ... ( N + 1 ) ) ) )
119	118	imim1d	|- ( ( N e. NN /\ m e. NN ) -> ( ( m e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) -> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) )
120		oveq1	|- ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) -> ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) + ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) = ( ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) + ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) )
121		elfzp1	|- ( m e. ( ZZ>= ` 1 ) -> ( ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) <-> ( ( g ` 1 ) e. ( 1 ... m ) \/ ( g ` 1 ) = ( m + 1 ) ) ) )
122	115 121	syl	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) <-> ( ( g ` 1 ) e. ( 1 ... m ) \/ ( g ` 1 ) = ( m + 1 ) ) ) )
123	122	rabbidv	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } = { g e. A | ( ( g ` 1 ) e. ( 1 ... m ) \/ ( g ` 1 ) = ( m + 1 ) ) } )
124		unrab	|- ( { g e. A | ( g ` 1 ) e. ( 1 ... m ) } u. { g e. A | ( g ` 1 ) = ( m + 1 ) } ) = { g e. A | ( ( g ` 1 ) e. ( 1 ... m ) \/ ( g ` 1 ) = ( m + 1 ) ) }
125	123 124	eqtr4di	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } = ( { g e. A | ( g ` 1 ) e. ( 1 ... m ) } u. { g e. A | ( g ` 1 ) = ( m + 1 ) } ) )
126	125	fveq2d	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( # ` ( { g e. A | ( g ` 1 ) e. ( 1 ... m ) } u. { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) )
127		fzfi	|- ( 1 ... ( N + 1 ) ) e. Fin
128		deranglem	|- ( ( 1 ... ( N + 1 ) ) e. Fin -> { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } e. Fin )
129	127 128	ax-mp	|- { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } e. Fin
130	3 129	eqeltri	|- A e. Fin
131		ssrab2	|- { g e. A | ( g ` 1 ) e. ( 1 ... m ) } C_ A
132		ssfi	|- ( ( A e. Fin /\ { g e. A | ( g ` 1 ) e. ( 1 ... m ) } C_ A ) -> { g e. A | ( g ` 1 ) e. ( 1 ... m ) } e. Fin )
133	130 131 132	mp2an	|- { g e. A | ( g ` 1 ) e. ( 1 ... m ) } e. Fin
134		ssrab2	|- { g e. A | ( g ` 1 ) = ( m + 1 ) } C_ A
135		ssfi	|- ( ( A e. Fin /\ { g e. A | ( g ` 1 ) = ( m + 1 ) } C_ A ) -> { g e. A | ( g ` 1 ) = ( m + 1 ) } e. Fin )
136	130 134 135	mp2an	|- { g e. A | ( g ` 1 ) = ( m + 1 ) } e. Fin
137		inrab	|- ( { g e. A | ( g ` 1 ) e. ( 1 ... m ) } i^i { g e. A | ( g ` 1 ) = ( m + 1 ) } ) = { g e. A | ( ( g ` 1 ) e. ( 1 ... m ) /\ ( g ` 1 ) = ( m + 1 ) ) }
138		fzp1disj	|- ( ( 1 ... m ) i^i { ( m + 1 ) } ) = (/)
139	42	elsn	|- ( ( g ` 1 ) e. { ( m + 1 ) } <-> ( g ` 1 ) = ( m + 1 ) )
140		inelcm	|- ( ( ( g ` 1 ) e. ( 1 ... m ) /\ ( g ` 1 ) e. { ( m + 1 ) } ) -> ( ( 1 ... m ) i^i { ( m + 1 ) } ) =/= (/) )
141	139 140	sylan2br	|- ( ( ( g ` 1 ) e. ( 1 ... m ) /\ ( g ` 1 ) = ( m + 1 ) ) -> ( ( 1 ... m ) i^i { ( m + 1 ) } ) =/= (/) )
142	141	necon2bi	|- ( ( ( 1 ... m ) i^i { ( m + 1 ) } ) = (/) -> -. ( ( g ` 1 ) e. ( 1 ... m ) /\ ( g ` 1 ) = ( m + 1 ) ) )
143	138 142	ax-mp	|- -. ( ( g ` 1 ) e. ( 1 ... m ) /\ ( g ` 1 ) = ( m + 1 ) )
144	143	rgenw	|- A. g e. A -. ( ( g ` 1 ) e. ( 1 ... m ) /\ ( g ` 1 ) = ( m + 1 ) )
145		rabeq0	|- ( { g e. A | ( ( g ` 1 ) e. ( 1 ... m ) /\ ( g ` 1 ) = ( m + 1 ) ) } = (/) <-> A. g e. A -. ( ( g ` 1 ) e. ( 1 ... m ) /\ ( g ` 1 ) = ( m + 1 ) ) )
146	144 145	mpbir	|- { g e. A | ( ( g ` 1 ) e. ( 1 ... m ) /\ ( g ` 1 ) = ( m + 1 ) ) } = (/)
147	137 146	eqtri	|- ( { g e. A | ( g ` 1 ) e. ( 1 ... m ) } i^i { g e. A | ( g ` 1 ) = ( m + 1 ) } ) = (/)
148		hashun	|- ( ( { g e. A | ( g ` 1 ) e. ( 1 ... m ) } e. Fin /\ { g e. A | ( g ` 1 ) = ( m + 1 ) } e. Fin /\ ( { g e. A | ( g ` 1 ) e. ( 1 ... m ) } i^i { g e. A | ( g ` 1 ) = ( m + 1 ) } ) = (/) ) -> ( # ` ( { g e. A | ( g ` 1 ) e. ( 1 ... m ) } u. { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) = ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) + ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) )
149	133 136 147 148	mp3an	|- ( # ` ( { g e. A | ( g ` 1 ) e. ( 1 ... m ) } u. { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) = ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) + ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) )
150	126 149	eqtrdi	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) + ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) )
151		nncn	|- ( m e. NN -> m e. CC )
152	151	ad2antlr	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> m e. CC )
153		ax-1cn	|- 1 e. CC
154	153	a1i	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> 1 e. CC )
155	152 154 154	addsubd	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( m + 1 ) - 1 ) = ( ( m - 1 ) + 1 ) )
156	155	oveq1d	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = ( ( ( m - 1 ) + 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )
157		subcl	|- ( ( m e. CC /\ 1 e. CC ) -> ( m - 1 ) e. CC )
158	152 153 157	sylancl	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( m - 1 ) e. CC )
159	109	ad2antrr	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( S ` N ) + ( S ` ( N - 1 ) ) ) e. NN0 )
160	159	nn0cnd	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( S ` N ) + ( S ` ( N - 1 ) ) ) e. CC )
161	158 154 160	adddird	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( m - 1 ) + 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = ( ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) + ( 1 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) )
162	160	mulid2d	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( 1 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = ( ( S ` N ) + ( S ` ( N - 1 ) ) ) )
163		exmidne	|- ( ( g ` ( m + 1 ) ) = 1 \/ ( g ` ( m + 1 ) ) =/= 1 )
164		orcom	|- ( ( ( g ` ( m + 1 ) ) = 1 \/ ( g ` ( m + 1 ) ) =/= 1 ) <-> ( ( g ` ( m + 1 ) ) =/= 1 \/ ( g ` ( m + 1 ) ) = 1 ) )
165	163 164	mpbi	|- ( ( g ` ( m + 1 ) ) =/= 1 \/ ( g ` ( m + 1 ) ) = 1 )
166	165	biantru	|- ( ( g ` 1 ) = ( m + 1 ) <-> ( ( g ` 1 ) = ( m + 1 ) /\ ( ( g ` ( m + 1 ) ) =/= 1 \/ ( g ` ( m + 1 ) ) = 1 ) ) )
167		andi	|- ( ( ( g ` 1 ) = ( m + 1 ) /\ ( ( g ` ( m + 1 ) ) =/= 1 \/ ( g ` ( m + 1 ) ) = 1 ) ) <-> ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) \/ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) ) )
168	166 167	bitri	|- ( ( g ` 1 ) = ( m + 1 ) <-> ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) \/ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) ) )
169	168	rabbii	|- { g e. A | ( g ` 1 ) = ( m + 1 ) } = { g e. A | ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) \/ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) ) }
170		unrab	|- ( { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } u. { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) = { g e. A | ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) \/ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) ) }
171	169 170	eqtr4i	|- { g e. A | ( g ` 1 ) = ( m + 1 ) } = ( { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } u. { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } )
172	171	fveq2i	|- ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) = ( # ` ( { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } u. { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) )
173		ssrab2	|- { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } C_ A
174		ssfi	|- ( ( A e. Fin /\ { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } C_ A ) -> { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } e. Fin )
175	130 173 174	mp2an	|- { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } e. Fin
176		ssrab2	|- { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } C_ A
177		ssfi	|- ( ( A e. Fin /\ { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } C_ A ) -> { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } e. Fin )
178	130 176 177	mp2an	|- { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } e. Fin
179		inrab	|- ( { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } i^i { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) = { g e. A | ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) /\ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) ) }
180		simpr	|- ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) -> ( g ` ( m + 1 ) ) = 1 )
181	180	necon3ai	|- ( ( g ` ( m + 1 ) ) =/= 1 -> -. ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) )
182	181	adantl	|- ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) -> -. ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) )
183		imnan	|- ( ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) -> -. ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) ) <-> -. ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) /\ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) ) )
184	182 183	mpbi	|- -. ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) /\ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) )
185	184	rgenw	|- A. g e. A -. ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) /\ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) )
186		rabeq0	|- ( { g e. A | ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) /\ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) ) } = (/) <-> A. g e. A -. ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) /\ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) ) )
187	185 186	mpbir	|- { g e. A | ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) /\ ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) ) } = (/)
188	179 187	eqtri	|- ( { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } i^i { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) = (/)
189		hashun	|- ( ( { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } e. Fin /\ { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } e. Fin /\ ( { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } i^i { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) = (/) ) -> ( # ` ( { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } u. { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) ) = ( ( # ` { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } ) + ( # ` { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) ) )
190	175 178 188 189	mp3an	|- ( # ` ( { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } u. { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) ) = ( ( # ` { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } ) + ( # ` { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) )
191	172 190	eqtri	|- ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) = ( ( # ` { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } ) + ( # ` { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) )
192		simpll	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> N e. NN )
193		nnne0	|- ( m e. NN -> m =/= 0 )
194		0p1e1	|- ( 0 + 1 ) = 1
195	194	eqeq2i	|- ( ( m + 1 ) = ( 0 + 1 ) <-> ( m + 1 ) = 1 )
196		0cn	|- 0 e. CC
197		addcan2	|- ( ( m e. CC /\ 0 e. CC /\ 1 e. CC ) -> ( ( m + 1 ) = ( 0 + 1 ) <-> m = 0 ) )
198	196 153 197	mp3an23	|- ( m e. CC -> ( ( m + 1 ) = ( 0 + 1 ) <-> m = 0 ) )
199	151 198	syl	|- ( m e. NN -> ( ( m + 1 ) = ( 0 + 1 ) <-> m = 0 ) )
200	195 199	bitr3id	|- ( m e. NN -> ( ( m + 1 ) = 1 <-> m = 0 ) )
201	200	necon3bbid	|- ( m e. NN -> ( -. ( m + 1 ) = 1 <-> m =/= 0 ) )
202	193 201	mpbird	|- ( m e. NN -> -. ( m + 1 ) = 1 )
203	202	ad2antlr	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> -. ( m + 1 ) = 1 )
204	14	adantr	|- ( ( N e. NN /\ m e. NN ) -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
205		elfzp12	|- ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) <-> ( ( m + 1 ) = 1 \/ ( m + 1 ) e. ( ( 1 + 1 ) ... ( N + 1 ) ) ) ) )
206	204 205	syl	|- ( ( N e. NN /\ m e. NN ) -> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) <-> ( ( m + 1 ) = 1 \/ ( m + 1 ) e. ( ( 1 + 1 ) ... ( N + 1 ) ) ) ) )
207	206	biimpa	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( m + 1 ) = 1 \/ ( m + 1 ) e. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
208	207	ord	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( -. ( m + 1 ) = 1 -> ( m + 1 ) e. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
209	203 208	mpd	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( m + 1 ) e. ( ( 1 + 1 ) ... ( N + 1 ) ) )
210		df-2	|- 2 = ( 1 + 1 )
211	210	oveq1i	|- ( 2 ... ( N + 1 ) ) = ( ( 1 + 1 ) ... ( N + 1 ) )
212	209 211	eleqtrrdi	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( m + 1 ) e. ( 2 ... ( N + 1 ) ) )
213		ovex	|- ( m + 1 ) e. _V
214		eqid	|- ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) = ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } )
215		fveq1	|- ( g = h -> ( g ` 1 ) = ( h ` 1 ) )
216	215	eqeq1d	|- ( g = h -> ( ( g ` 1 ) = ( m + 1 ) <-> ( h ` 1 ) = ( m + 1 ) ) )
217		fveq1	|- ( g = h -> ( g ` ( m + 1 ) ) = ( h ` ( m + 1 ) ) )
218	217	neeq1d	|- ( g = h -> ( ( g ` ( m + 1 ) ) =/= 1 <-> ( h ` ( m + 1 ) ) =/= 1 ) )
219	216 218	anbi12d	|- ( g = h -> ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) <-> ( ( h ` 1 ) = ( m + 1 ) /\ ( h ` ( m + 1 ) ) =/= 1 ) ) )
220	219	cbvrabv	|- { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } = { h e. A | ( ( h ` 1 ) = ( m + 1 ) /\ ( h ` ( m + 1 ) ) =/= 1 ) }
221		eqid	|- ( ( _I |` ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ) u. { <. 1 , ( m + 1 ) >. , <. ( m + 1 ) , 1 >. } ) = ( ( _I |` ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ) u. { <. 1 , ( m + 1 ) >. , <. ( m + 1 ) , 1 >. } )
222		f1oeq1	|- ( g = f -> ( g : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) <-> f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) ) )
223		fveq2	|- ( z = y -> ( g ` z ) = ( g ` y ) )
224		id	|- ( z = y -> z = y )
225	223 224	neeq12d	|- ( z = y -> ( ( g ` z ) =/= z <-> ( g ` y ) =/= y ) )
226	225	cbvralvw	|- ( A. z e. ( 2 ... ( N + 1 ) ) ( g ` z ) =/= z <-> A. y e. ( 2 ... ( N + 1 ) ) ( g ` y ) =/= y )
227		fveq1	|- ( g = f -> ( g ` y ) = ( f ` y ) )
228	227	neeq1d	|- ( g = f -> ( ( g ` y ) =/= y <-> ( f ` y ) =/= y ) )
229	228	ralbidv	|- ( g = f -> ( A. y e. ( 2 ... ( N + 1 ) ) ( g ` y ) =/= y <-> A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) )
230	226 229	syl5bb	|- ( g = f -> ( A. z e. ( 2 ... ( N + 1 ) ) ( g ` z ) =/= z <-> A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) )
231	222 230	anbi12d	|- ( g = f -> ( ( g : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. z e. ( 2 ... ( N + 1 ) ) ( g ` z ) =/= z ) <-> ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) ) )
232	231	cbvabv	|- { g | ( g : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. z e. ( 2 ... ( N + 1 ) ) ( g ` z ) =/= z ) } = { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
233	1 2 3 192 212 213 214 220 221 232	subfacp1lem5	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( # ` { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } ) = ( S ` N ) )
234	217	eqeq1d	|- ( g = h -> ( ( g ` ( m + 1 ) ) = 1 <-> ( h ` ( m + 1 ) ) = 1 ) )
235	216 234	anbi12d	|- ( g = h -> ( ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) <-> ( ( h ` 1 ) = ( m + 1 ) /\ ( h ` ( m + 1 ) ) = 1 ) ) )
236	235	cbvrabv	|- { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } = { h e. A | ( ( h ` 1 ) = ( m + 1 ) /\ ( h ` ( m + 1 ) ) = 1 ) }
237		f1oeq1	|- ( g = f -> ( g : ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) -1-1-onto-> ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) <-> f : ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) -1-1-onto-> ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ) )
238	225	cbvralvw	|- ( A. z e. ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ( g ` z ) =/= z <-> A. y e. ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ( g ` y ) =/= y )
239	228	ralbidv	|- ( g = f -> ( A. y e. ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ( g ` y ) =/= y <-> A. y e. ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ( f ` y ) =/= y ) )
240	238 239	syl5bb	|- ( g = f -> ( A. z e. ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ( g ` z ) =/= z <-> A. y e. ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ( f ` y ) =/= y ) )
241	237 240	anbi12d	|- ( g = f -> ( ( g : ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) -1-1-onto-> ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) /\ A. z e. ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ( g ` z ) =/= z ) <-> ( f : ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) -1-1-onto-> ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) /\ A. y e. ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ( f ` y ) =/= y ) ) )
242	241	cbvabv	|- { g | ( g : ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) -1-1-onto-> ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) /\ A. z e. ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ( g ` z ) =/= z ) } = { f | ( f : ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) -1-1-onto-> ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) /\ A. y e. ( ( 2 ... ( N + 1 ) ) \ { ( m + 1 ) } ) ( f ` y ) =/= y ) }
243	1 2 3 192 212 213 214 236 242	subfacp1lem3	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( # ` { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) = ( S ` ( N - 1 ) ) )
244	233 243	oveq12d	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( # ` { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) =/= 1 ) } ) + ( # ` { g e. A | ( ( g ` 1 ) = ( m + 1 ) /\ ( g ` ( m + 1 ) ) = 1 ) } ) ) = ( ( S ` N ) + ( S ` ( N - 1 ) ) ) )
245	191 244	eqtrid	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) = ( ( S ` N ) + ( S ` ( N - 1 ) ) ) )
246	162 245	eqtr4d	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( 1 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) )
247	246	oveq2d	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) + ( 1 x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) = ( ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) + ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) )
248	156 161 247	3eqtrd	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = ( ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) + ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) )
249	150 248	eqeq12d	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) <-> ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) + ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) = ( ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) + ( # ` { g e. A | ( g ` 1 ) = ( m + 1 ) } ) ) ) )
250	120 249	syl5ibr	|- ( ( ( N e. NN /\ m e. NN ) /\ ( m + 1 ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) )
251	250	ex	|- ( ( N e. NN /\ m e. NN ) -> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) )
252	251	a2d	|- ( ( N e. NN /\ m e. NN ) -> ( ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) -> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) )
253	119 252	syld	|- ( ( N e. NN /\ m e. NN ) -> ( ( m e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) -> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) )
254	253	expcom	|- ( m e. NN -> ( N e. NN -> ( ( m e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) -> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) ) )
255	254	a2d	|- ( m e. NN -> ( ( N e. NN -> ( m e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... m ) } ) = ( ( m - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) -> ( N e. NN -> ( ( m + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( m + 1 ) ) } ) = ( ( ( m + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) ) )
256	53 63 73 83 113 255	nnind	|- ( ( N + 1 ) e. NN -> ( N e. NN -> ( ( N + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } ) = ( ( ( N + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) ) )
257	4 256	mpcom	|- ( N e. NN -> ( ( N + 1 ) e. ( 1 ... ( N + 1 ) ) -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } ) = ( ( ( N + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) ) )
258	34 257	mpd	|- ( N e. NN -> ( # ` { g e. A | ( g ` 1 ) e. ( 1 ... ( N + 1 ) ) } ) = ( ( ( N + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )
259		nncn	|- ( N e. NN -> N e. CC )
260		pncan	|- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
261	259 153 260	sylancl	|- ( N e. NN -> ( ( N + 1 ) - 1 ) = N )
262	261	oveq1d	|- ( N e. NN -> ( ( ( N + 1 ) - 1 ) x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) = ( N x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )
263	32 258 262	3eqtrd	|- ( N e. NN -> ( S ` ( N + 1 ) ) = ( N x. ( ( S ` N ) + ( S ` ( N - 1 ) ) ) ) )