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 \in Fin ⟼ \|\{f \| (f : x \underset{1-1 onto}{⟶} x \land \forall y \in x f (y) \neq y)\}\|)$
	subfac.n	$⊢ S = (n \in ℕ_{0} ⟼ D ((1 \dots n)))$
	subfacp1lem.a	$⊢ A = \{f \| (f : (1 \dots N + 1) \underset{1-1 onto}{⟶} (1 \dots N + 1) \land \forall y \in (1 \dots N + 1) f (y) \neq y)\}$
Assertion	subfacp1lem6	$⊢ N \in ℕ \to S (N + 1) = N (S (N) + S (N - 1))$

Proof

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

Metamath Proof Explorer

Theorem subfacp1lem6

Proof