Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  subfacp1lem6 Structured version   Visualization version   GIF version

Theorem subfacp1lem6 32560
 Description: Lemma for subfacp1 32561. By induction, we cut up the set of all derangements on 𝑁 + 1 according to the 𝑁 possible values of (𝑓‘1) (since (𝑓‘1) ≠ 1), and for each set for fixed 𝑀 = (𝑓‘1), the subset of derangements with (𝑓‘𝑀) = 1 has size 𝑆(𝑁 − 1) (by subfacp1lem3 32557), while the subset with (𝑓‘𝑀) ≠ 1 has size 𝑆(𝑁) (by subfacp1lem5 32559). Adding it all up yields the desired equation 𝑁(𝑆(𝑁) + 𝑆(𝑁 − 1)) for the number of derangements on 𝑁 + 1. (Contributed by Mario Carneiro, 22-Jan-2015.)
Hypotheses
Ref Expression
derang.d 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥1-1-onto𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) ≠ 𝑦)}))
subfac.n 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))
subfacp1lem.a 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}
Assertion
Ref Expression
subfacp1lem6 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
Distinct variable groups:   𝑓,𝑛,𝑥,𝑦,𝐴   𝑓,𝑁,𝑛,𝑥,𝑦   𝐷,𝑛   𝑆,𝑛,𝑥,𝑦
Allowed substitution hints:   𝐷(𝑥,𝑦,𝑓)   𝑆(𝑓)

Proof of Theorem subfacp1lem6
Dummy variables 𝑔 𝑚 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 peano2nn 11640 . . . . 5 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
21nnnn0d 11946 . . . 4 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
3 derang.d . . . . 5 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥1-1-onto𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) ≠ 𝑦)}))
4 subfac.n . . . . 5 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))
53, 4subfacval 32548 . . . 4 ((𝑁 + 1) ∈ ℕ0 → (𝑆‘(𝑁 + 1)) = (𝐷‘(1...(𝑁 + 1))))
62, 5syl 17 . . 3 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝐷‘(1...(𝑁 + 1))))
7 fzfid 13339 . . . . 5 (𝑁 ∈ ℕ → (1...(𝑁 + 1)) ∈ Fin)
83derangval 32542 . . . . 5 ((1...(𝑁 + 1)) ∈ Fin → (𝐷‘(1...(𝑁 + 1))) = (♯‘{𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}))
97, 8syl 17 . . . 4 (𝑁 ∈ ℕ → (𝐷‘(1...(𝑁 + 1))) = (♯‘{𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}))
10 subfacp1lem.a . . . . 5 𝐴 = {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}
1110fveq2i 6649 . . . 4 (♯‘𝐴) = (♯‘{𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)})
129, 11eqtr4di 2851 . . 3 (𝑁 ∈ ℕ → (𝐷‘(1...(𝑁 + 1))) = (♯‘𝐴))
13 nnuz 12272 . . . . . . . . . . 11 ℕ = (ℤ‘1)
141, 13eleqtrdi 2900 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (ℤ‘1))
15 eluzfz1 12912 . . . . . . . . . 10 ((𝑁 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑁 + 1)))
1614, 15syl 17 . . . . . . . . 9 (𝑁 ∈ ℕ → 1 ∈ (1...(𝑁 + 1)))
17 f1of 6591 . . . . . . . . . 10 (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
1817adantr 484 . . . . . . . . 9 ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) → 𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
19 ffvelrn 6827 . . . . . . . . . 10 ((𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → (𝑓‘1) ∈ (1...(𝑁 + 1)))
2019expcom 417 . . . . . . . . 9 (1 ∈ (1...(𝑁 + 1)) → (𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) → (𝑓‘1) ∈ (1...(𝑁 + 1))))
2116, 18, 20syl2im 40 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) → (𝑓‘1) ∈ (1...(𝑁 + 1))))
2221ss2abdv 3991 . . . . . . 7 (𝑁 ∈ ℕ → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ (𝑓‘1) ∈ (1...(𝑁 + 1))})
23 fveq1 6645 . . . . . . . . 9 (𝑔 = 𝑓 → (𝑔‘1) = (𝑓‘1))
2423eleq1d 2874 . . . . . . . 8 (𝑔 = 𝑓 → ((𝑔‘1) ∈ (1...(𝑁 + 1)) ↔ (𝑓‘1) ∈ (1...(𝑁 + 1))))
2524cbvabv 2866 . . . . . . 7 {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} = {𝑓 ∣ (𝑓‘1) ∈ (1...(𝑁 + 1))}
2622, 10, 253sstr4g 3960 . . . . . 6 (𝑁 ∈ ℕ → 𝐴 ⊆ {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
27 ssabral 3990 . . . . . 6 (𝐴 ⊆ {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} ↔ ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
2826, 27sylib 221 . . . . 5 (𝑁 ∈ ℕ → ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
29 rabid2 3334 . . . . 5 (𝐴 = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} ↔ ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
3028, 29sylibr 237 . . . 4 (𝑁 ∈ ℕ → 𝐴 = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
3130fveq2d 6650 . . 3 (𝑁 ∈ ℕ → (♯‘𝐴) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
326, 12, 313eqtrd 2837 . 2 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
33 elfz1end 12935 . . . 4 ((𝑁 + 1) ∈ ℕ ↔ (𝑁 + 1) ∈ (1...(𝑁 + 1)))
341, 33sylib 221 . . 3 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (1...(𝑁 + 1)))
35 eleq1 2877 . . . . . . 7 (𝑥 = 1 → (𝑥 ∈ (1...(𝑁 + 1)) ↔ 1 ∈ (1...(𝑁 + 1))))
36 oveq2 7144 . . . . . . . . . . . . 13 (𝑥 = 1 → (1...𝑥) = (1...1))
37 1z 12003 . . . . . . . . . . . . . 14 1 ∈ ℤ
38 fzsn 12947 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (1...1) = {1})
3937, 38ax-mp 5 . . . . . . . . . . . . 13 (1...1) = {1}
4036, 39eqtrdi 2849 . . . . . . . . . . . 12 (𝑥 = 1 → (1...𝑥) = {1})
4140eleq2d 2875 . . . . . . . . . . 11 (𝑥 = 1 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ {1}))
42 fvex 6659 . . . . . . . . . . . 12 (𝑔‘1) ∈ V
4342elsn 4540 . . . . . . . . . . 11 ((𝑔‘1) ∈ {1} ↔ (𝑔‘1) = 1)
4441, 43syl6bb 290 . . . . . . . . . 10 (𝑥 = 1 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) = 1))
4544rabbidv 3427 . . . . . . . . 9 (𝑥 = 1 → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) = 1})
4645fveq2d 6650 . . . . . . . 8 (𝑥 = 1 → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}))
47 oveq1 7143 . . . . . . . . . 10 (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
48 1m1e0 11700 . . . . . . . . . 10 (1 − 1) = 0
4947, 48eqtrdi 2849 . . . . . . . . 9 (𝑥 = 1 → (𝑥 − 1) = 0)
5049oveq1d 7151 . . . . . . . 8 (𝑥 = 1 → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
5146, 50eqeq12d 2814 . . . . . . 7 (𝑥 = 1 → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
5235, 51imbi12d 348 . . . . . 6 (𝑥 = 1 → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ (1 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
5352imbi2d 344 . . . . 5 (𝑥 = 1 → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → (1 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
54 eleq1 2877 . . . . . . 7 (𝑥 = 𝑚 → (𝑥 ∈ (1...(𝑁 + 1)) ↔ 𝑚 ∈ (1...(𝑁 + 1))))
55 oveq2 7144 . . . . . . . . . . 11 (𝑥 = 𝑚 → (1...𝑥) = (1...𝑚))
5655eleq2d 2875 . . . . . . . . . 10 (𝑥 = 𝑚 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...𝑚)))
5756rabbidv 3427 . . . . . . . . 9 (𝑥 = 𝑚 → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)})
5857fveq2d 6650 . . . . . . . 8 (𝑥 = 𝑚 → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}))
59 oveq1 7143 . . . . . . . . 9 (𝑥 = 𝑚 → (𝑥 − 1) = (𝑚 − 1))
6059oveq1d 7151 . . . . . . . 8 (𝑥 = 𝑚 → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
6158, 60eqeq12d 2814 . . . . . . 7 (𝑥 = 𝑚 → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
6254, 61imbi12d 348 . . . . . 6 (𝑥 = 𝑚 → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ (𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
6362imbi2d 344 . . . . 5 (𝑥 = 𝑚 → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → (𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
64 eleq1 2877 . . . . . . 7 (𝑥 = (𝑚 + 1) → (𝑥 ∈ (1...(𝑁 + 1)) ↔ (𝑚 + 1) ∈ (1...(𝑁 + 1))))
65 oveq2 7144 . . . . . . . . . . 11 (𝑥 = (𝑚 + 1) → (1...𝑥) = (1...(𝑚 + 1)))
6665eleq2d 2875 . . . . . . . . . 10 (𝑥 = (𝑚 + 1) → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...(𝑚 + 1))))
6766rabbidv 3427 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))})
6867fveq2d 6650 . . . . . . . 8 (𝑥 = (𝑚 + 1) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}))
69 oveq1 7143 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → (𝑥 − 1) = ((𝑚 + 1) − 1))
7069oveq1d 7151 . . . . . . . 8 (𝑥 = (𝑚 + 1) → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
7168, 70eqeq12d 2814 . . . . . . 7 (𝑥 = (𝑚 + 1) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
7264, 71imbi12d 348 . . . . . 6 (𝑥 = (𝑚 + 1) → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
7372imbi2d 344 . . . . 5 (𝑥 = (𝑚 + 1) → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
74 eleq1 2877 . . . . . . 7 (𝑥 = (𝑁 + 1) → (𝑥 ∈ (1...(𝑁 + 1)) ↔ (𝑁 + 1) ∈ (1...(𝑁 + 1))))
75 oveq2 7144 . . . . . . . . . . 11 (𝑥 = (𝑁 + 1) → (1...𝑥) = (1...(𝑁 + 1)))
7675eleq2d 2875 . . . . . . . . . 10 (𝑥 = (𝑁 + 1) → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...(𝑁 + 1))))
7776rabbidv 3427 . . . . . . . . 9 (𝑥 = (𝑁 + 1) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
7877fveq2d 6650 . . . . . . . 8 (𝑥 = (𝑁 + 1) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
79 oveq1 7143 . . . . . . . . 9 (𝑥 = (𝑁 + 1) → (𝑥 − 1) = ((𝑁 + 1) − 1))
8079oveq1d 7151 . . . . . . . 8 (𝑥 = (𝑁 + 1) → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
8178, 80eqeq12d 2814 . . . . . . 7 (𝑥 = (𝑁 + 1) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
8274, 81imbi12d 348 . . . . . 6 (𝑥 = (𝑁 + 1) → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
8382imbi2d 344 . . . . 5 (𝑥 = (𝑁 + 1) → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
84 hash0 13727 . . . . . . 7 (♯‘∅) = 0
85 fveq2 6646 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → (𝑓𝑦) = (𝑓‘1))
86 id 22 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → 𝑦 = 1)
8785, 86neeq12d 3048 . . . . . . . . . . . . . . 15 (𝑦 = 1 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑓‘1) ≠ 1))
8887rspcv 3566 . . . . . . . . . . . . . 14 (1 ∈ (1...(𝑁 + 1)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 → (𝑓‘1) ≠ 1))
8916, 88syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 → (𝑓‘1) ≠ 1))
9089adantld 494 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) → (𝑓‘1) ≠ 1))
9190ss2abdv 3991 . . . . . . . . . . 11 (𝑁 ∈ ℕ → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ (𝑓‘1) ≠ 1})
92 df-ne 2988 . . . . . . . . . . . . 13 ((𝑔‘1) ≠ 1 ↔ ¬ (𝑔‘1) = 1)
9323neeq1d 3046 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → ((𝑔‘1) ≠ 1 ↔ (𝑓‘1) ≠ 1))
9492, 93bitr3id 288 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (¬ (𝑔‘1) = 1 ↔ (𝑓‘1) ≠ 1))
9594cbvabv 2866 . . . . . . . . . . 11 {𝑔 ∣ ¬ (𝑔‘1) = 1} = {𝑓 ∣ (𝑓‘1) ≠ 1}
9691, 10, 953sstr4g 3960 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝐴 ⊆ {𝑔 ∣ ¬ (𝑔‘1) = 1})
97 ssabral 3990 . . . . . . . . . 10 (𝐴 ⊆ {𝑔 ∣ ¬ (𝑔‘1) = 1} ↔ ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
9896, 97sylib 221 . . . . . . . . 9 (𝑁 ∈ ℕ → ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
99 rabeq0 4292 . . . . . . . . 9 ({𝑔𝐴 ∣ (𝑔‘1) = 1} = ∅ ↔ ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
10098, 99sylibr 237 . . . . . . . 8 (𝑁 ∈ ℕ → {𝑔𝐴 ∣ (𝑔‘1) = 1} = ∅)
101100fveq2d 6650 . . . . . . 7 (𝑁 ∈ ℕ → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (♯‘∅))
102 nnnn0 11895 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
1033, 4subfacf 32550 . . . . . . . . . . . 12 𝑆:ℕ0⟶ℕ0
104103ffvelrni 6828 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (𝑆𝑁) ∈ ℕ0)
105102, 104syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆𝑁) ∈ ℕ0)
106 nnm1nn0 11929 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
107103ffvelrni 6828 . . . . . . . . . . 11 ((𝑁 − 1) ∈ ℕ0 → (𝑆‘(𝑁 − 1)) ∈ ℕ0)
108106, 107syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆‘(𝑁 − 1)) ∈ ℕ0)
109105, 108nn0addcld 11950 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℕ0)
110109nn0cnd 11948 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℂ)
111110mul02d 10830 . . . . . . 7 (𝑁 ∈ ℕ → (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = 0)
11284, 101, 1113eqtr4a 2859 . . . . . 6 (𝑁 ∈ ℕ → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
113112a1d 25 . . . . 5 (𝑁 ∈ ℕ → (1 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
114 simplr 768 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℕ)
115114, 13eleqtrdi 2900 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (ℤ‘1))
116 peano2fzr 12918 . . . . . . . . . . 11 ((𝑚 ∈ (ℤ‘1) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (1...(𝑁 + 1)))
117115, 116sylancom 591 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (1...(𝑁 + 1)))
118117ex 416 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → 𝑚 ∈ (1...(𝑁 + 1))))
119118imim1d 82 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
120 oveq1 7143 . . . . . . . . . . 11 ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
121 elfzp1 12955 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (ℤ‘1) → ((𝑔‘1) ∈ (1...(𝑚 + 1)) ↔ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))))
122115, 121syl 17 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑔‘1) ∈ (1...(𝑚 + 1)) ↔ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))))
123122rabbidv 3427 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))} = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))})
124 unrab 4226 . . . . . . . . . . . . . . 15 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))}
125123, 124eqtr4di 2851 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))} = ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
126125fveq2d 6650 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (♯‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
127 fzfi 13338 . . . . . . . . . . . . . . . . 17 (1...(𝑁 + 1)) ∈ Fin
128 deranglem 32541 . . . . . . . . . . . . . . . . 17 ((1...(𝑁 + 1)) ∈ Fin → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ∈ Fin)
129127, 128ax-mp 5 . . . . . . . . . . . . . . . 16 {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ∈ Fin
13010, 129eqeltri 2886 . . . . . . . . . . . . . . 15 𝐴 ∈ Fin
131 ssrab2 4007 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ⊆ 𝐴
132 ssfi 8725 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ⊆ 𝐴) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin)
133130, 131, 132mp2an 691 . . . . . . . . . . . . . 14 {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin
134 ssrab2 4007 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ⊆ 𝐴
135 ssfi 8725 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin)
136130, 134, 135mp2an 691 . . . . . . . . . . . . . 14 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin
137 inrab 4227 . . . . . . . . . . . . . . 15 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))}
138 fzp1disj 12964 . . . . . . . . . . . . . . . . . 18 ((1...𝑚) ∩ {(𝑚 + 1)}) = ∅
13942elsn 4540 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) ∈ {(𝑚 + 1)} ↔ (𝑔‘1) = (𝑚 + 1))
140 inelcm 4372 . . . . . . . . . . . . . . . . . . . 20 (((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) ∈ {(𝑚 + 1)}) → ((1...𝑚) ∩ {(𝑚 + 1)}) ≠ ∅)
141139, 140sylan2br 597 . . . . . . . . . . . . . . . . . . 19 (((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)) → ((1...𝑚) ∩ {(𝑚 + 1)}) ≠ ∅)
142141necon2bi 3017 . . . . . . . . . . . . . . . . . 18 (((1...𝑚) ∩ {(𝑚 + 1)}) = ∅ → ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)))
143138, 142ax-mp 5 . . . . . . . . . . . . . . . . 17 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))
144143rgenw 3118 . . . . . . . . . . . . . . . 16 𝑔𝐴 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))
145 rabeq0 4292 . . . . . . . . . . . . . . . 16 ({𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))} = ∅ ↔ ∀𝑔𝐴 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)))
146144, 145mpbir 234 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))} = ∅
147137, 146eqtri 2821 . . . . . . . . . . . . . 14 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ∅
148 hashun 13742 . . . . . . . . . . . . . 14 (({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin ∧ ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ∅) → (♯‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
149133, 136, 147, 148mp3an 1458 . . . . . . . . . . . . 13 (♯‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
150126, 149eqtrdi 2849 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
151 nncn 11636 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
152151ad2antlr 726 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℂ)
153 ax-1cn 10587 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
154153a1i 11 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 1 ∈ ℂ)
155152, 154, 154addsubd 11010 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑚 + 1) − 1) = ((𝑚 − 1) + 1))
156155oveq1d 7151 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) + 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
157 subcl 10877 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑚 − 1) ∈ ℂ)
158152, 153, 157sylancl 589 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 − 1) ∈ ℂ)
159109ad2antrr 725 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℕ0)
160159nn0cnd 11948 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℂ)
161158, 154, 160adddird 10658 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 − 1) + 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
162160mulid2d 10651 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
163 exmidne 2997 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘(𝑚 + 1)) = 1 ∨ (𝑔‘(𝑚 + 1)) ≠ 1)
164 orcom 867 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔‘(𝑚 + 1)) = 1 ∨ (𝑔‘(𝑚 + 1)) ≠ 1) ↔ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1))
165163, 164mpbi 233 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)
166165biantru 533 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔‘1) = (𝑚 + 1) ↔ ((𝑔‘1) = (𝑚 + 1) ∧ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)))
167 andi 1005 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔‘1) = (𝑚 + 1) ∧ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)) ↔ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
168166, 167bitri 278 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) = (𝑚 + 1) ↔ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
169168rabbii 3420 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
170 unrab 4226 . . . . . . . . . . . . . . . . . . 19 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
171169, 170eqtr4i 2824 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} = ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})
172171fveq2i 6649 . . . . . . . . . . . . . . . . 17 (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = (♯‘({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
173 ssrab2 4007 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ⊆ 𝐴
174 ssfi 8725 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∈ Fin)
175130, 173, 174mp2an 691 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∈ Fin
176 ssrab2 4007 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ⊆ 𝐴
177 ssfi 8725 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ∈ Fin)
178130, 176, 177mp2an 691 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ∈ Fin
179 inrab 4227 . . . . . . . . . . . . . . . . . . 19 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∩ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
180 simpr 488 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1) → (𝑔‘(𝑚 + 1)) = 1)
181180necon3ai 3012 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘(𝑚 + 1)) ≠ 1 → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
182181adantl 485 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
183 imnan 403 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)) ↔ ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
184182, 183mpbi 233 . . . . . . . . . . . . . . . . . . . . 21 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
185184rgenw 3118 . . . . . . . . . . . . . . . . . . . 20 𝑔𝐴 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
186 rabeq0 4292 . . . . . . . . . . . . . . . . . . . 20 ({𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))} = ∅ ↔ ∀𝑔𝐴 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
187185, 186mpbir 234 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))} = ∅
188179, 187eqtri 2821 . . . . . . . . . . . . . . . . . 18 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∩ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = ∅
189 hashun 13742 . . . . . . . . . . . . . . . . . 18 (({𝑔𝐴 ∣ ((𝑔‘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)})))
190175, 178, 188, 189mp3an 1458 . . . . . . . . . . . . . . . . 17 (♯‘({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})) = ((♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
191172, 190eqtri 2821 . . . . . . . . . . . . . . . 16 (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ((♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
192 simpll 766 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑁 ∈ ℕ)
193 nnne0 11662 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
194 0p1e1 11750 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 + 1) = 1
195194eqeq2i 2811 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 + 1) = (0 + 1) ↔ (𝑚 + 1) = 1)
196 0cn 10625 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ ℂ
197 addcan2 10817 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 ∈ ℂ ∧ 0 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
198196, 153, 197mp3an23 1450 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℂ → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
199151, 198syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ ℕ → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
200195, 199bitr3id 288 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ ℕ → ((𝑚 + 1) = 1 ↔ 𝑚 = 0))
201200necon3bbid 3024 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → (¬ (𝑚 + 1) = 1 ↔ 𝑚 ≠ 0))
202193, 201mpbird 260 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ → ¬ (𝑚 + 1) = 1)
203202ad2antlr 726 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ¬ (𝑚 + 1) = 1)
20414adantr 484 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑁 + 1) ∈ (ℤ‘1))
205 elfzp12 12984 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 + 1) ∈ (ℤ‘1) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) ↔ ((𝑚 + 1) = 1 ∨ (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1)))))
206204, 205syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) ↔ ((𝑚 + 1) = 1 ∨ (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1)))))
207206biimpa 480 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑚 + 1) = 1 ∨ (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1))))
208207ord 861 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (¬ (𝑚 + 1) = 1 → (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1))))
209203, 208mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1)))
210 df-2 11691 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
211210oveq1i 7146 . . . . . . . . . . . . . . . . . . 19 (2...(𝑁 + 1)) = ((1 + 1)...(𝑁 + 1))
212209, 211eleqtrrdi 2901 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 + 1) ∈ (2...(𝑁 + 1)))
213 ovex 7169 . . . . . . . . . . . . . . . . . 18 (𝑚 + 1) ∈ V
214 eqid 2798 . . . . . . . . . . . . . . . . . 18 ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) = ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})
215 fveq1 6645 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = → (𝑔‘1) = (‘1))
216215eqeq1d 2800 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘1) = (𝑚 + 1) ↔ (‘1) = (𝑚 + 1)))
217 fveq1 6645 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = → (𝑔‘(𝑚 + 1)) = (‘(𝑚 + 1)))
218217neeq1d 3046 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘(𝑚 + 1)) ≠ 1 ↔ (‘(𝑚 + 1)) ≠ 1))
219216, 218anbi12d 633 . . . . . . . . . . . . . . . . . . 19 (𝑔 = → (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ↔ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) ≠ 1)))
220219cbvrabv 3439 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} = {𝐴 ∣ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) ≠ 1)}
221 eqid 2798 . . . . . . . . . . . . . . . . . 18 (( I ↾ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})) ∪ {⟨1, (𝑚 + 1)⟩, ⟨(𝑚 + 1), 1⟩}) = (( I ↾ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})) ∪ {⟨1, (𝑚 + 1)⟩, ⟨(𝑚 + 1), 1⟩})
222 f1oeq1 6580 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
223 fveq2 6646 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑔𝑧) = (𝑔𝑦))
224 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦𝑧 = 𝑦)
225223, 224neeq12d 3048 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → ((𝑔𝑧) ≠ 𝑧 ↔ (𝑔𝑦) ≠ 𝑦))
226225cbvralvw 3396 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑔𝑦) ≠ 𝑦)
227 fveq1 6645 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑓 → (𝑔𝑦) = (𝑓𝑦))
228227neeq1d 3046 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑓 → ((𝑔𝑦) ≠ 𝑦 ↔ (𝑓𝑦) ≠ 𝑦))
229228ralbidv 3162 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑔𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦))
230226, 229syl5bb 286 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦))
231222, 230anbi12d 633 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧) ↔ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)))
232231cbvabv 2866 . . . . . . . . . . . . . . . . . 18 {𝑔 ∣ (𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧)} = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}
2333, 4, 10, 192, 212, 213, 214, 220, 221, 232subfacp1lem5 32559 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) = (𝑆𝑁))
234217eqeq1d 2800 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘(𝑚 + 1)) = 1 ↔ (‘(𝑚 + 1)) = 1))
235216, 234anbi12d 633 . . . . . . . . . . . . . . . . . . 19 (𝑔 = → (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1) ↔ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) = 1)))
236235cbvrabv 3439 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} = {𝐴 ∣ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) = 1)}
237 f1oeq1 6580 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) ↔ 𝑓:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})))
238225cbvralvw 3396 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑦) ≠ 𝑦)
239228ralbidv 3162 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦))
240238, 239syl5bb 286 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦))
241237, 240anbi12d 633 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑔:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) ∧ ∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧) ↔ (𝑓:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) ∧ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦)))
242241cbvabv 2866 . . . . . . . . . . . . . . . . . 18 {𝑔 ∣ (𝑔:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) ∧ ∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧)} = {𝑓 ∣ (𝑓:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) ∧ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦)}
2433, 4, 10, 192, 212, 213, 214, 236, 242subfacp1lem3 32557 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = (𝑆‘(𝑁 − 1)))
244233, 243oveq12d 7154 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
245191, 244syl5eq 2845 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
246162, 245eqtr4d 2836 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
247246oveq2d 7152 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
248156, 161, 2473eqtrd 2837 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
249150, 248eqeq12d 2814 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))))
250120, 249syl5ibr 249 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
251250ex 416 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
252251a2d 29 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
253119, 252syld 47 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
254253expcom 417 . . . . . 6 (𝑚 ∈ ℕ → (𝑁 ∈ ℕ → ((𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
255254a2d 29 . . . . 5 (𝑚 ∈ ℕ → ((𝑁 ∈ ℕ → (𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) → (𝑁 ∈ ℕ → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
25653, 63, 73, 83, 113, 255nnind 11646 . . . 4 ((𝑁 + 1) ∈ ℕ → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
2571, 256mpcom 38 . . 3 (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
25834, 257mpd 15 . 2 (𝑁 ∈ ℕ → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
259 nncn 11636 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
260 pncan 10884 . . . 4 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
261259, 153, 260sylancl 589 . . 3 (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
262261oveq1d 7151 . 2 (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
26332, 258, 2623eqtrd 2837 1 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111  {cab 2776   ≠ wne 2987  ∀wral 3106  {crab 3110   ∖ cdif 3878   ∪ cun 3879   ∩ cin 3880   ⊆ wss 3881  ∅c0 4243  {csn 4525  {cpr 4527  ⟨cop 4531   ↦ cmpt 5111   I cid 5425   ↾ cres 5522  ⟶wf 6321  –1-1-onto→wf1o 6324  ‘cfv 6325  (class class class)co 7136  Fincfn 8495  ℂcc 10527  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534   − cmin 10862  ℕcn 11628  2c2 11683  ℕ0cn0 11888  ℤcz 11972  ℤ≥cuz 12234  ...cfz 12888  ♯chash 13689 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5155  ax-sep 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-nel 3092  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4802  df-int 4840  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-tr 5138  df-id 5426  df-eprel 5431  df-po 5439  df-so 5440  df-fr 5479  df-we 5481  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-res 5532  df-ima 5533  df-pred 6117  df-ord 6163  df-on 6164  df-lim 6165  df-suc 6166  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-f1 6330  df-fo 6331  df-f1o 6332  df-fv 6333  df-riota 7094  df-ov 7139  df-oprab 7140  df-mpo 7141  df-om 7564  df-1st 7674  df-2nd 7675  df-wrecs 7933  df-recs 7994  df-rdg 8032  df-1o 8088  df-2o 8089  df-oadd 8092  df-er 8275  df-map 8394  df-pm 8395  df-en 8496  df-dom 8497  df-sdom 8498  df-fin 8499  df-dju 9317  df-card 9355  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11629  df-2 11691  df-n0 11889  df-xnn0 11959  df-z 11973  df-uz 12235  df-fz 12889  df-hash 13690 This theorem is referenced by:  subfacp1  32561
 Copyright terms: Public domain W3C validator