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

Theorem subfacp1lem6 32330
Description: Lemma for subfacp1 32331. 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 32327), while the subset with (𝑓𝑀) ≠ 1 has size 𝑆(𝑁) (by subfacp1lem5 32329). 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 11639 . . . . 5 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
21nnnn0d 11944 . . . 4 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
3 derang.d . . . . 5 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥1-1-onto𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) ≠ 𝑦)}))
4 subfac.n . . . . 5 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))
53, 4subfacval 32318 . . . 4 ((𝑁 + 1) ∈ ℕ0 → (𝑆‘(𝑁 + 1)) = (𝐷‘(1...(𝑁 + 1))))
62, 5syl 17 . . 3 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝐷‘(1...(𝑁 + 1))))
7 fzfid 13331 . . . . 5 (𝑁 ∈ ℕ → (1...(𝑁 + 1)) ∈ Fin)
83derangval 32312 . . . . 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 6667 . . . 4 (♯‘𝐴) = (♯‘{𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)})
129, 11syl6eqr 2874 . . 3 (𝑁 ∈ ℕ → (𝐷‘(1...(𝑁 + 1))) = (♯‘𝐴))
13 nnuz 12270 . . . . . . . . . . 11 ℕ = (ℤ‘1)
141, 13eleqtrdi 2923 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (ℤ‘1))
15 eluzfz1 12904 . . . . . . . . . 10 ((𝑁 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑁 + 1)))
1614, 15syl 17 . . . . . . . . 9 (𝑁 ∈ ℕ → 1 ∈ (1...(𝑁 + 1)))
17 f1of 6609 . . . . . . . . . 10 (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
1817adantr 481 . . . . . . . . 9 ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) → 𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
19 ffvelrn 6842 . . . . . . . . . 10 ((𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → (𝑓‘1) ∈ (1...(𝑁 + 1)))
2019expcom 414 . . . . . . . . 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 4043 . . . . . . 7 (𝑁 ∈ ℕ → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ (𝑓‘1) ∈ (1...(𝑁 + 1))})
23 fveq1 6663 . . . . . . . . 9 (𝑔 = 𝑓 → (𝑔‘1) = (𝑓‘1))
2423eleq1d 2897 . . . . . . . 8 (𝑔 = 𝑓 → ((𝑔‘1) ∈ (1...(𝑁 + 1)) ↔ (𝑓‘1) ∈ (1...(𝑁 + 1))))
2524cbvabv 2889 . . . . . . 7 {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} = {𝑓 ∣ (𝑓‘1) ∈ (1...(𝑁 + 1))}
2622, 10, 253sstr4g 4011 . . . . . 6 (𝑁 ∈ ℕ → 𝐴 ⊆ {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
27 ssabral 4041 . . . . . 6 (𝐴 ⊆ {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} ↔ ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
2826, 27sylib 219 . . . . 5 (𝑁 ∈ ℕ → ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
29 rabid2 3382 . . . . 5 (𝐴 = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} ↔ ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
3028, 29sylibr 235 . . . 4 (𝑁 ∈ ℕ → 𝐴 = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
3130fveq2d 6668 . . 3 (𝑁 ∈ ℕ → (♯‘𝐴) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
326, 12, 313eqtrd 2860 . 2 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
33 elfz1end 12927 . . . 4 ((𝑁 + 1) ∈ ℕ ↔ (𝑁 + 1) ∈ (1...(𝑁 + 1)))
341, 33sylib 219 . . 3 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (1...(𝑁 + 1)))
35 eleq1 2900 . . . . . . 7 (𝑥 = 1 → (𝑥 ∈ (1...(𝑁 + 1)) ↔ 1 ∈ (1...(𝑁 + 1))))
36 oveq2 7153 . . . . . . . . . . . . 13 (𝑥 = 1 → (1...𝑥) = (1...1))
37 1z 12001 . . . . . . . . . . . . . 14 1 ∈ ℤ
38 fzsn 12939 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (1...1) = {1})
3937, 38ax-mp 5 . . . . . . . . . . . . 13 (1...1) = {1}
4036, 39syl6eq 2872 . . . . . . . . . . . 12 (𝑥 = 1 → (1...𝑥) = {1})
4140eleq2d 2898 . . . . . . . . . . 11 (𝑥 = 1 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ {1}))
42 fvex 6677 . . . . . . . . . . . 12 (𝑔‘1) ∈ V
4342elsn 4574 . . . . . . . . . . 11 ((𝑔‘1) ∈ {1} ↔ (𝑔‘1) = 1)
4441, 43syl6bb 288 . . . . . . . . . 10 (𝑥 = 1 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) = 1))
4544rabbidv 3481 . . . . . . . . 9 (𝑥 = 1 → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) = 1})
4645fveq2d 6668 . . . . . . . 8 (𝑥 = 1 → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}))
47 oveq1 7152 . . . . . . . . . 10 (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
48 1m1e0 11698 . . . . . . . . . 10 (1 − 1) = 0
4947, 48syl6eq 2872 . . . . . . . . 9 (𝑥 = 1 → (𝑥 − 1) = 0)
5049oveq1d 7160 . . . . . . . 8 (𝑥 = 1 → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
5146, 50eqeq12d 2837 . . . . . . 7 (𝑥 = 1 → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
5235, 51imbi12d 346 . . . . . 6 (𝑥 = 1 → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ (1 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
5352imbi2d 342 . . . . 5 (𝑥 = 1 → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → (1 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
54 eleq1 2900 . . . . . . 7 (𝑥 = 𝑚 → (𝑥 ∈ (1...(𝑁 + 1)) ↔ 𝑚 ∈ (1...(𝑁 + 1))))
55 oveq2 7153 . . . . . . . . . . 11 (𝑥 = 𝑚 → (1...𝑥) = (1...𝑚))
5655eleq2d 2898 . . . . . . . . . 10 (𝑥 = 𝑚 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...𝑚)))
5756rabbidv 3481 . . . . . . . . 9 (𝑥 = 𝑚 → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)})
5857fveq2d 6668 . . . . . . . 8 (𝑥 = 𝑚 → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}))
59 oveq1 7152 . . . . . . . . 9 (𝑥 = 𝑚 → (𝑥 − 1) = (𝑚 − 1))
6059oveq1d 7160 . . . . . . . 8 (𝑥 = 𝑚 → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
6158, 60eqeq12d 2837 . . . . . . 7 (𝑥 = 𝑚 → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
6254, 61imbi12d 346 . . . . . 6 (𝑥 = 𝑚 → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ (𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
6362imbi2d 342 . . . . 5 (𝑥 = 𝑚 → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → (𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
64 eleq1 2900 . . . . . . 7 (𝑥 = (𝑚 + 1) → (𝑥 ∈ (1...(𝑁 + 1)) ↔ (𝑚 + 1) ∈ (1...(𝑁 + 1))))
65 oveq2 7153 . . . . . . . . . . 11 (𝑥 = (𝑚 + 1) → (1...𝑥) = (1...(𝑚 + 1)))
6665eleq2d 2898 . . . . . . . . . 10 (𝑥 = (𝑚 + 1) → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...(𝑚 + 1))))
6766rabbidv 3481 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))})
6867fveq2d 6668 . . . . . . . 8 (𝑥 = (𝑚 + 1) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}))
69 oveq1 7152 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → (𝑥 − 1) = ((𝑚 + 1) − 1))
7069oveq1d 7160 . . . . . . . 8 (𝑥 = (𝑚 + 1) → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
7168, 70eqeq12d 2837 . . . . . . 7 (𝑥 = (𝑚 + 1) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
7264, 71imbi12d 346 . . . . . 6 (𝑥 = (𝑚 + 1) → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
7372imbi2d 342 . . . . 5 (𝑥 = (𝑚 + 1) → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
74 eleq1 2900 . . . . . . 7 (𝑥 = (𝑁 + 1) → (𝑥 ∈ (1...(𝑁 + 1)) ↔ (𝑁 + 1) ∈ (1...(𝑁 + 1))))
75 oveq2 7153 . . . . . . . . . . 11 (𝑥 = (𝑁 + 1) → (1...𝑥) = (1...(𝑁 + 1)))
7675eleq2d 2898 . . . . . . . . . 10 (𝑥 = (𝑁 + 1) → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...(𝑁 + 1))))
7776rabbidv 3481 . . . . . . . . 9 (𝑥 = (𝑁 + 1) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
7877fveq2d 6668 . . . . . . . 8 (𝑥 = (𝑁 + 1) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
79 oveq1 7152 . . . . . . . . 9 (𝑥 = (𝑁 + 1) → (𝑥 − 1) = ((𝑁 + 1) − 1))
8079oveq1d 7160 . . . . . . . 8 (𝑥 = (𝑁 + 1) → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
8178, 80eqeq12d 2837 . . . . . . 7 (𝑥 = (𝑁 + 1) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
8274, 81imbi12d 346 . . . . . 6 (𝑥 = (𝑁 + 1) → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
8382imbi2d 342 . . . . 5 (𝑥 = (𝑁 + 1) → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
84 hash0 13718 . . . . . . 7 (♯‘∅) = 0
85 fveq2 6664 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → (𝑓𝑦) = (𝑓‘1))
86 id 22 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → 𝑦 = 1)
8785, 86neeq12d 3077 . . . . . . . . . . . . . . 15 (𝑦 = 1 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑓‘1) ≠ 1))
8887rspcv 3617 . . . . . . . . . . . . . 14 (1 ∈ (1...(𝑁 + 1)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 → (𝑓‘1) ≠ 1))
8916, 88syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 → (𝑓‘1) ≠ 1))
9089adantld 491 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) → (𝑓‘1) ≠ 1))
9190ss2abdv 4043 . . . . . . . . . . 11 (𝑁 ∈ ℕ → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ (𝑓‘1) ≠ 1})
92 df-ne 3017 . . . . . . . . . . . . 13 ((𝑔‘1) ≠ 1 ↔ ¬ (𝑔‘1) = 1)
9323neeq1d 3075 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → ((𝑔‘1) ≠ 1 ↔ (𝑓‘1) ≠ 1))
9492, 93syl5bbr 286 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (¬ (𝑔‘1) = 1 ↔ (𝑓‘1) ≠ 1))
9594cbvabv 2889 . . . . . . . . . . 11 {𝑔 ∣ ¬ (𝑔‘1) = 1} = {𝑓 ∣ (𝑓‘1) ≠ 1}
9691, 10, 953sstr4g 4011 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝐴 ⊆ {𝑔 ∣ ¬ (𝑔‘1) = 1})
97 ssabral 4041 . . . . . . . . . 10 (𝐴 ⊆ {𝑔 ∣ ¬ (𝑔‘1) = 1} ↔ ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
9896, 97sylib 219 . . . . . . . . 9 (𝑁 ∈ ℕ → ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
99 rabeq0 4337 . . . . . . . . 9 ({𝑔𝐴 ∣ (𝑔‘1) = 1} = ∅ ↔ ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
10098, 99sylibr 235 . . . . . . . 8 (𝑁 ∈ ℕ → {𝑔𝐴 ∣ (𝑔‘1) = 1} = ∅)
101100fveq2d 6668 . . . . . . 7 (𝑁 ∈ ℕ → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (♯‘∅))
102 nnnn0 11893 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
1033, 4subfacf 32320 . . . . . . . . . . . 12 𝑆:ℕ0⟶ℕ0
104103ffvelrni 6843 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (𝑆𝑁) ∈ ℕ0)
105102, 104syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆𝑁) ∈ ℕ0)
106 nnm1nn0 11927 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
107103ffvelrni 6843 . . . . . . . . . . 11 ((𝑁 − 1) ∈ ℕ0 → (𝑆‘(𝑁 − 1)) ∈ ℕ0)
108106, 107syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆‘(𝑁 − 1)) ∈ ℕ0)
109105, 108nn0addcld 11948 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℕ0)
110109nn0cnd 11946 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℂ)
111110mul02d 10827 . . . . . . 7 (𝑁 ∈ ℕ → (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = 0)
11284, 101, 1113eqtr4a 2882 . . . . . 6 (𝑁 ∈ ℕ → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
113112a1d 25 . . . . 5 (𝑁 ∈ ℕ → (1 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
114 simplr 765 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℕ)
115114, 13eleqtrdi 2923 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (ℤ‘1))
116 peano2fzr 12910 . . . . . . . . . . 11 ((𝑚 ∈ (ℤ‘1) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (1...(𝑁 + 1)))
117115, 116sylancom 588 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (1...(𝑁 + 1)))
118117ex 413 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → 𝑚 ∈ (1...(𝑁 + 1))))
119118imim1d 82 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
120 oveq1 7152 . . . . . . . . . . 11 ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
121 elfzp1 12947 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (ℤ‘1) → ((𝑔‘1) ∈ (1...(𝑚 + 1)) ↔ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))))
122115, 121syl 17 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑔‘1) ∈ (1...(𝑚 + 1)) ↔ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))))
123122rabbidv 3481 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))} = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))})
124 unrab 4273 . . . . . . . . . . . . . . 15 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))}
125123, 124syl6eqr 2874 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))} = ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
126125fveq2d 6668 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (♯‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
127 fzfi 13330 . . . . . . . . . . . . . . . . 17 (1...(𝑁 + 1)) ∈ Fin
128 deranglem 32311 . . . . . . . . . . . . . . . . 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 2909 . . . . . . . . . . . . . . 15 𝐴 ∈ Fin
131 ssrab2 4055 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ⊆ 𝐴
132 ssfi 8727 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ⊆ 𝐴) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin)
133130, 131, 132mp2an 688 . . . . . . . . . . . . . 14 {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin
134 ssrab2 4055 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ⊆ 𝐴
135 ssfi 8727 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin)
136130, 134, 135mp2an 688 . . . . . . . . . . . . . 14 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin
137 inrab 4274 . . . . . . . . . . . . . . 15 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))}
138 fzp1disj 12956 . . . . . . . . . . . . . . . . . 18 ((1...𝑚) ∩ {(𝑚 + 1)}) = ∅
13942elsn 4574 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) ∈ {(𝑚 + 1)} ↔ (𝑔‘1) = (𝑚 + 1))
140 inelcm 4412 . . . . . . . . . . . . . . . . . . . 20 (((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) ∈ {(𝑚 + 1)}) → ((1...𝑚) ∩ {(𝑚 + 1)}) ≠ ∅)
141139, 140sylan2br 594 . . . . . . . . . . . . . . . . . . 19 (((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)) → ((1...𝑚) ∩ {(𝑚 + 1)}) ≠ ∅)
142141necon2bi 3046 . . . . . . . . . . . . . . . . . 18 (((1...𝑚) ∩ {(𝑚 + 1)}) = ∅ → ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)))
143138, 142ax-mp 5 . . . . . . . . . . . . . . . . 17 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))
144143rgenw 3150 . . . . . . . . . . . . . . . 16 𝑔𝐴 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))
145 rabeq0 4337 . . . . . . . . . . . . . . . 16 ({𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))} = ∅ ↔ ∀𝑔𝐴 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)))
146144, 145mpbir 232 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))} = ∅
147137, 146eqtri 2844 . . . . . . . . . . . . . 14 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ∅
148 hashun 13733 . . . . . . . . . . . . . 14 (({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin ∧ ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ∅) → (♯‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
149133, 136, 147, 148mp3an 1452 . . . . . . . . . . . . 13 (♯‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
150126, 149syl6eq 2872 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
151 nncn 11635 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
152151ad2antlr 723 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℂ)
153 ax-1cn 10584 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
154153a1i 11 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 1 ∈ ℂ)
155152, 154, 154addsubd 11007 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑚 + 1) − 1) = ((𝑚 − 1) + 1))
156155oveq1d 7160 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) + 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
157 subcl 10874 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑚 − 1) ∈ ℂ)
158152, 153, 157sylancl 586 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 − 1) ∈ ℂ)
159109ad2antrr 722 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℕ0)
160159nn0cnd 11946 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℂ)
161158, 154, 160adddird 10655 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 − 1) + 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
162160mulid2d 10648 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
163 exmidne 3026 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘(𝑚 + 1)) = 1 ∨ (𝑔‘(𝑚 + 1)) ≠ 1)
164 orcom 864 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔‘(𝑚 + 1)) = 1 ∨ (𝑔‘(𝑚 + 1)) ≠ 1) ↔ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1))
165163, 164mpbi 231 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)
166165biantru 530 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔‘1) = (𝑚 + 1) ↔ ((𝑔‘1) = (𝑚 + 1) ∧ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)))
167 andi 1001 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔‘1) = (𝑚 + 1) ∧ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)) ↔ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
168166, 167bitri 276 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) = (𝑚 + 1) ↔ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
169168rabbii 3474 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
170 unrab 4273 . . . . . . . . . . . . . . . . . . 19 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
171169, 170eqtr4i 2847 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} = ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})
172171fveq2i 6667 . . . . . . . . . . . . . . . . 17 (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = (♯‘({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
173 ssrab2 4055 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ⊆ 𝐴
174 ssfi 8727 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∈ Fin)
175130, 173, 174mp2an 688 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∈ Fin
176 ssrab2 4055 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ⊆ 𝐴
177 ssfi 8727 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ∈ Fin)
178130, 176, 177mp2an 688 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ∈ Fin
179 inrab 4274 . . . . . . . . . . . . . . . . . . 19 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∩ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
180 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1) → (𝑔‘(𝑚 + 1)) = 1)
181180necon3ai 3041 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘(𝑚 + 1)) ≠ 1 → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
182181adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
183 imnan 400 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)) ↔ ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
184182, 183mpbi 231 . . . . . . . . . . . . . . . . . . . . 21 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
185184rgenw 3150 . . . . . . . . . . . . . . . . . . . 20 𝑔𝐴 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
186 rabeq0 4337 . . . . . . . . . . . . . . . . . . . 20 ({𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))} = ∅ ↔ ∀𝑔𝐴 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
187185, 186mpbir 232 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))} = ∅
188179, 187eqtri 2844 . . . . . . . . . . . . . . . . . 18 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∩ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = ∅
189 hashun 13733 . . . . . . . . . . . . . . . . . 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 1452 . . . . . . . . . . . . . . . . 17 (♯‘({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})) = ((♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
191172, 190eqtri 2844 . . . . . . . . . . . . . . . 16 (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ((♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
192 simpll 763 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑁 ∈ ℕ)
193 nnne0 11660 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
194 0p1e1 11748 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 + 1) = 1
195194eqeq2i 2834 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 + 1) = (0 + 1) ↔ (𝑚 + 1) = 1)
196 0cn 10622 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ ℂ
197 addcan2 10814 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 ∈ ℂ ∧ 0 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
198196, 153, 197mp3an23 1444 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℂ → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
199151, 198syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ ℕ → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
200195, 199syl5bbr 286 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ ℕ → ((𝑚 + 1) = 1 ↔ 𝑚 = 0))
201200necon3bbid 3053 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → (¬ (𝑚 + 1) = 1 ↔ 𝑚 ≠ 0))
202193, 201mpbird 258 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ → ¬ (𝑚 + 1) = 1)
203202ad2antlr 723 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ¬ (𝑚 + 1) = 1)
20414adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑁 + 1) ∈ (ℤ‘1))
205 elfzp12 12976 . . . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑚 + 1) = 1 ∨ (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1))))
208207ord 858 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (¬ (𝑚 + 1) = 1 → (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1))))
209203, 208mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1)))
210 df-2 11689 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
211210oveq1i 7155 . . . . . . . . . . . . . . . . . . 19 (2...(𝑁 + 1)) = ((1 + 1)...(𝑁 + 1))
212209, 211eleqtrrdi 2924 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 + 1) ∈ (2...(𝑁 + 1)))
213 ovex 7178 . . . . . . . . . . . . . . . . . 18 (𝑚 + 1) ∈ V
214 eqid 2821 . . . . . . . . . . . . . . . . . 18 ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) = ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})
215 fveq1 6663 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = → (𝑔‘1) = (‘1))
216215eqeq1d 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘1) = (𝑚 + 1) ↔ (‘1) = (𝑚 + 1)))
217 fveq1 6663 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = → (𝑔‘(𝑚 + 1)) = (‘(𝑚 + 1)))
218217neeq1d 3075 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘(𝑚 + 1)) ≠ 1 ↔ (‘(𝑚 + 1)) ≠ 1))
219216, 218anbi12d 630 . . . . . . . . . . . . . . . . . . 19 (𝑔 = → (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ↔ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) ≠ 1)))
220219cbvrabv 3492 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} = {𝐴 ∣ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) ≠ 1)}
221 eqid 2821 . . . . . . . . . . . . . . . . . 18 (( I ↾ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})) ∪ {⟨1, (𝑚 + 1)⟩, ⟨(𝑚 + 1), 1⟩}) = (( I ↾ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})) ∪ {⟨1, (𝑚 + 1)⟩, ⟨(𝑚 + 1), 1⟩})
222 f1oeq1 6598 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
223 fveq2 6664 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑔𝑧) = (𝑔𝑦))
224 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦𝑧 = 𝑦)
225223, 224neeq12d 3077 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → ((𝑔𝑧) ≠ 𝑧 ↔ (𝑔𝑦) ≠ 𝑦))
226225cbvralvw 3450 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑔𝑦) ≠ 𝑦)
227 fveq1 6663 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑓 → (𝑔𝑦) = (𝑓𝑦))
228227neeq1d 3075 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑓 → ((𝑔𝑦) ≠ 𝑦 ↔ (𝑓𝑦) ≠ 𝑦))
229228ralbidv 3197 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑔𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦))
230226, 229syl5bb 284 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦))
231222, 230anbi12d 630 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧) ↔ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)))
232231cbvabv 2889 . . . . . . . . . . . . . . . . . 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 32329 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) = (𝑆𝑁))
234217eqeq1d 2823 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘(𝑚 + 1)) = 1 ↔ (‘(𝑚 + 1)) = 1))
235216, 234anbi12d 630 . . . . . . . . . . . . . . . . . . 19 (𝑔 = → (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1) ↔ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) = 1)))
236235cbvrabv 3492 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} = {𝐴 ∣ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) = 1)}
237 f1oeq1 6598 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) ↔ 𝑓:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})))
238225cbvralvw 3450 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑦) ≠ 𝑦)
239228ralbidv 3197 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦))
240238, 239syl5bb 284 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦))
241237, 240anbi12d 630 . . . . . . . . . . . . . . . . . . 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 2889 . . . . . . . . . . . . . . . . . 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 32327 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = (𝑆‘(𝑁 − 1)))
244233, 243oveq12d 7163 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
245191, 244syl5eq 2868 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
246162, 245eqtr4d 2859 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
247246oveq2d 7161 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
248156, 161, 2473eqtrd 2860 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
249150, 248eqeq12d 2837 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))))
250120, 249syl5ibr 247 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
251250ex 413 . . . . . . . . 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 414 . . . . . 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 11645 . . . 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 11635 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
260 pncan 10881 . . . 4 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
261259, 153, 260sylancl 586 . . 3 (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
262261oveq1d 7160 . 2 (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
26332, 258, 2623eqtrd 2860 1 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 841   = wceq 1528  wcel 2105  {cab 2799  wne 3016  wral 3138  {crab 3142  cdif 3932  cun 3933  cin 3934  wss 3935  c0 4290  {csn 4559  {cpr 4561  cop 4565  cmpt 5138   I cid 5453  cres 5551  wf 6345  1-1-ontowf1o 6348  cfv 6349  (class class class)co 7145  Fincfn 8498  cc 10524  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  cmin 10859  cn 11627  2c2 11681  0cn0 11886  cz 11970  cuz 12232  ...cfz 12882  chash 13680
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-rep 5182  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3or 1080  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-nel 3124  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-pss 3953  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4833  df-int 4870  df-iun 4914  df-br 5059  df-opab 5121  df-mpt 5139  df-tr 5165  df-id 5454  df-eprel 5459  df-po 5468  df-so 5469  df-fr 5508  df-we 5510  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-pred 6142  df-ord 6188  df-on 6189  df-lim 6190  df-suc 6191  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-f1 6354  df-fo 6355  df-f1o 6356  df-fv 6357  df-riota 7103  df-ov 7148  df-oprab 7149  df-mpo 7150  df-om 7569  df-1st 7680  df-2nd 7681  df-wrecs 7938  df-recs 7999  df-rdg 8037  df-1o 8093  df-2o 8094  df-oadd 8097  df-er 8279  df-map 8398  df-pm 8399  df-en 8499  df-dom 8500  df-sdom 8501  df-fin 8502  df-dju 9319  df-card 9357  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-nn 11628  df-2 11689  df-n0 11887  df-xnn0 11957  df-z 11971  df-uz 12233  df-fz 12883  df-hash 13681
This theorem is referenced by:  subfacp1  32331
  Copyright terms: Public domain W3C validator