Metamath Proof Explorer

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 ⊢ 𝐷 = ( 𝑥 ∈ Fin ↦ ( ♯ ‘ { 𝑓 ∣ ( 𝑓 : 𝑥 –1-1-onto→ 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) } ) )
subfac.n ⊢ 𝑆 = ( 𝑛 ∈ ℕ0 ↦ ( 𝐷 ‘ ( 1 ... 𝑛 ) ) )
subfacp1lem.a ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : ( 1 ... ( 𝑁 + 1 ) ) –1-1-onto→ ( 1 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑦 ∈ ( 1 ... ( 𝑁 + 1 ) ) ( 𝑓 ‘ 𝑦 ) ≠ 𝑦 ) }
Assertion subfacp1lem6 ( 𝑁 ∈ ℕ → ( 𝑆 ‘ ( 𝑁 + 1 ) ) = ( 𝑁 · ( ( 𝑆 ‘ 𝑁 ) + ( 𝑆 ‘ ( 𝑁 − 1 ) ) ) ) )

Proof

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