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 31141
Description: Lemma for subfacp1 31142. 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 31138), while the subset with (𝑓𝑀) ≠ 1 has size 𝑆(𝑁) (by subfacp1lem5 31140). 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 11017 . . . . 5 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
21nnnn0d 11336 . . . 4 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
3 derang.d . . . . 5 𝐷 = (𝑥 ∈ Fin ↦ (#‘{𝑓 ∣ (𝑓:𝑥1-1-onto𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) ≠ 𝑦)}))
4 subfac.n . . . . 5 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))
53, 4subfacval 31129 . . . 4 ((𝑁 + 1) ∈ ℕ0 → (𝑆‘(𝑁 + 1)) = (𝐷‘(1...(𝑁 + 1))))
62, 5syl 17 . . 3 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝐷‘(1...(𝑁 + 1))))
7 fzfid 12755 . . . . 5 (𝑁 ∈ ℕ → (1...(𝑁 + 1)) ∈ Fin)
83derangval 31123 . . . . 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 6181 . . . 4 (#‘𝐴) = (#‘{𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)})
129, 11syl6eqr 2672 . . 3 (𝑁 ∈ ℕ → (𝐷‘(1...(𝑁 + 1))) = (#‘𝐴))
13 nnuz 11708 . . . . . . . . . . 11 ℕ = (ℤ‘1)
141, 13syl6eleq 2709 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (ℤ‘1))
15 eluzfz1 12333 . . . . . . . . . 10 ((𝑁 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑁 + 1)))
1614, 15syl 17 . . . . . . . . 9 (𝑁 ∈ ℕ → 1 ∈ (1...(𝑁 + 1)))
17 f1of 6124 . . . . . . . . . 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 6343 . . . . . . . . . 10 ((𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → (𝑓‘1) ∈ (1...(𝑁 + 1)))
2019expcom 451 . . . . . . . . 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 3667 . . . . . . 7 (𝑁 ∈ ℕ → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ (𝑓‘1) ∈ (1...(𝑁 + 1))})
23 fveq1 6177 . . . . . . . . 9 (𝑔 = 𝑓 → (𝑔‘1) = (𝑓‘1))
2423eleq1d 2684 . . . . . . . 8 (𝑔 = 𝑓 → ((𝑔‘1) ∈ (1...(𝑁 + 1)) ↔ (𝑓‘1) ∈ (1...(𝑁 + 1))))
2524cbvabv 2745 . . . . . . 7 {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} = {𝑓 ∣ (𝑓‘1) ∈ (1...(𝑁 + 1))}
2622, 10, 253sstr4g 3638 . . . . . 6 (𝑁 ∈ ℕ → 𝐴 ⊆ {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
27 ssabral 3665 . . . . . 6 (𝐴 ⊆ {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} ↔ ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
2826, 27sylib 208 . . . . 5 (𝑁 ∈ ℕ → ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
29 rabid2 3113 . . . . 5 (𝐴 = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} ↔ ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
3028, 29sylibr 224 . . . 4 (𝑁 ∈ ℕ → 𝐴 = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
3130fveq2d 6182 . . 3 (𝑁 ∈ ℕ → (#‘𝐴) = (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
326, 12, 313eqtrd 2658 . 2 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
33 elfz1end 12356 . . . 4 ((𝑁 + 1) ∈ ℕ ↔ (𝑁 + 1) ∈ (1...(𝑁 + 1)))
341, 33sylib 208 . . 3 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (1...(𝑁 + 1)))
35 eleq1 2687 . . . . . . 7 (𝑥 = 1 → (𝑥 ∈ (1...(𝑁 + 1)) ↔ 1 ∈ (1...(𝑁 + 1))))
36 oveq2 6643 . . . . . . . . . . . . 13 (𝑥 = 1 → (1...𝑥) = (1...1))
37 1z 11392 . . . . . . . . . . . . . 14 1 ∈ ℤ
38 fzsn 12368 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (1...1) = {1})
3937, 38ax-mp 5 . . . . . . . . . . . . 13 (1...1) = {1}
4036, 39syl6eq 2670 . . . . . . . . . . . 12 (𝑥 = 1 → (1...𝑥) = {1})
4140eleq2d 2685 . . . . . . . . . . 11 (𝑥 = 1 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ {1}))
42 fvex 6188 . . . . . . . . . . . 12 (𝑔‘1) ∈ V
4342elsn 4183 . . . . . . . . . . 11 ((𝑔‘1) ∈ {1} ↔ (𝑔‘1) = 1)
4441, 43syl6bb 276 . . . . . . . . . 10 (𝑥 = 1 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) = 1))
4544rabbidv 3184 . . . . . . . . 9 (𝑥 = 1 → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) = 1})
4645fveq2d 6182 . . . . . . . 8 (𝑥 = 1 → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}))
47 oveq1 6642 . . . . . . . . . 10 (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
48 1m1e0 11074 . . . . . . . . . 10 (1 − 1) = 0
4947, 48syl6eq 2670 . . . . . . . . 9 (𝑥 = 1 → (𝑥 − 1) = 0)
5049oveq1d 6650 . . . . . . . 8 (𝑥 = 1 → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
5146, 50eqeq12d 2635 . . . . . . 7 (𝑥 = 1 → ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
5235, 51imbi12d 334 . . . . . 6 (𝑥 = 1 → ((𝑥 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ (1 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
5352imbi2d 330 . . . . 5 (𝑥 = 1 → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → (1 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
54 eleq1 2687 . . . . . . 7 (𝑥 = 𝑚 → (𝑥 ∈ (1...(𝑁 + 1)) ↔ 𝑚 ∈ (1...(𝑁 + 1))))
55 oveq2 6643 . . . . . . . . . . 11 (𝑥 = 𝑚 → (1...𝑥) = (1...𝑚))
5655eleq2d 2685 . . . . . . . . . 10 (𝑥 = 𝑚 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...𝑚)))
5756rabbidv 3184 . . . . . . . . 9 (𝑥 = 𝑚 → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)})
5857fveq2d 6182 . . . . . . . 8 (𝑥 = 𝑚 → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}))
59 oveq1 6642 . . . . . . . . 9 (𝑥 = 𝑚 → (𝑥 − 1) = (𝑚 − 1))
6059oveq1d 6650 . . . . . . . 8 (𝑥 = 𝑚 → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
6158, 60eqeq12d 2635 . . . . . . 7 (𝑥 = 𝑚 → ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
6254, 61imbi12d 334 . . . . . 6 (𝑥 = 𝑚 → ((𝑥 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ (𝑚 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
6362imbi2d 330 . . . . 5 (𝑥 = 𝑚 → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → (𝑚 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
64 eleq1 2687 . . . . . . 7 (𝑥 = (𝑚 + 1) → (𝑥 ∈ (1...(𝑁 + 1)) ↔ (𝑚 + 1) ∈ (1...(𝑁 + 1))))
65 oveq2 6643 . . . . . . . . . . 11 (𝑥 = (𝑚 + 1) → (1...𝑥) = (1...(𝑚 + 1)))
6665eleq2d 2685 . . . . . . . . . 10 (𝑥 = (𝑚 + 1) → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...(𝑚 + 1))))
6766rabbidv 3184 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))})
6867fveq2d 6182 . . . . . . . 8 (𝑥 = (𝑚 + 1) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}))
69 oveq1 6642 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → (𝑥 − 1) = ((𝑚 + 1) − 1))
7069oveq1d 6650 . . . . . . . 8 (𝑥 = (𝑚 + 1) → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
7168, 70eqeq12d 2635 . . . . . . 7 (𝑥 = (𝑚 + 1) → ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
7264, 71imbi12d 334 . . . . . 6 (𝑥 = (𝑚 + 1) → ((𝑥 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
7372imbi2d 330 . . . . 5 (𝑥 = (𝑚 + 1) → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
74 eleq1 2687 . . . . . . 7 (𝑥 = (𝑁 + 1) → (𝑥 ∈ (1...(𝑁 + 1)) ↔ (𝑁 + 1) ∈ (1...(𝑁 + 1))))
75 oveq2 6643 . . . . . . . . . . 11 (𝑥 = (𝑁 + 1) → (1...𝑥) = (1...(𝑁 + 1)))
7675eleq2d 2685 . . . . . . . . . 10 (𝑥 = (𝑁 + 1) → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...(𝑁 + 1))))
7776rabbidv 3184 . . . . . . . . 9 (𝑥 = (𝑁 + 1) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
7877fveq2d 6182 . . . . . . . 8 (𝑥 = (𝑁 + 1) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
79 oveq1 6642 . . . . . . . . 9 (𝑥 = (𝑁 + 1) → (𝑥 − 1) = ((𝑁 + 1) − 1))
8079oveq1d 6650 . . . . . . . 8 (𝑥 = (𝑁 + 1) → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
8178, 80eqeq12d 2635 . . . . . . 7 (𝑥 = (𝑁 + 1) → ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
8274, 81imbi12d 334 . . . . . 6 (𝑥 = (𝑁 + 1) → ((𝑥 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
8382imbi2d 330 . . . . 5 (𝑥 = (𝑁 + 1) → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
84 hash0 13141 . . . . . . 7 (#‘∅) = 0
85 fveq2 6178 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → (𝑓𝑦) = (𝑓‘1))
86 id 22 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → 𝑦 = 1)
8785, 86neeq12d 2852 . . . . . . . . . . . . . . 15 (𝑦 = 1 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑓‘1) ≠ 1))
8887rspcv 3300 . . . . . . . . . . . . . 14 (1 ∈ (1...(𝑁 + 1)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 → (𝑓‘1) ≠ 1))
8916, 88syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 → (𝑓‘1) ≠ 1))
9089adantld 483 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) → (𝑓‘1) ≠ 1))
9190ss2abdv 3667 . . . . . . . . . . 11 (𝑁 ∈ ℕ → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ (𝑓‘1) ≠ 1})
92 df-ne 2792 . . . . . . . . . . . . 13 ((𝑔‘1) ≠ 1 ↔ ¬ (𝑔‘1) = 1)
9323neeq1d 2850 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → ((𝑔‘1) ≠ 1 ↔ (𝑓‘1) ≠ 1))
9492, 93syl5bbr 274 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (¬ (𝑔‘1) = 1 ↔ (𝑓‘1) ≠ 1))
9594cbvabv 2745 . . . . . . . . . . 11 {𝑔 ∣ ¬ (𝑔‘1) = 1} = {𝑓 ∣ (𝑓‘1) ≠ 1}
9691, 10, 953sstr4g 3638 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝐴 ⊆ {𝑔 ∣ ¬ (𝑔‘1) = 1})
97 ssabral 3665 . . . . . . . . . 10 (𝐴 ⊆ {𝑔 ∣ ¬ (𝑔‘1) = 1} ↔ ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
9896, 97sylib 208 . . . . . . . . 9 (𝑁 ∈ ℕ → ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
99 rabeq0 3948 . . . . . . . . 9 ({𝑔𝐴 ∣ (𝑔‘1) = 1} = ∅ ↔ ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
10098, 99sylibr 224 . . . . . . . 8 (𝑁 ∈ ℕ → {𝑔𝐴 ∣ (𝑔‘1) = 1} = ∅)
101100fveq2d 6182 . . . . . . 7 (𝑁 ∈ ℕ → (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (#‘∅))
102 nnnn0 11284 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
1033, 4subfacf 31131 . . . . . . . . . . . 12 𝑆:ℕ0⟶ℕ0
104103ffvelrni 6344 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (𝑆𝑁) ∈ ℕ0)
105102, 104syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆𝑁) ∈ ℕ0)
106 nnm1nn0 11319 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
107103ffvelrni 6344 . . . . . . . . . . 11 ((𝑁 − 1) ∈ ℕ0 → (𝑆‘(𝑁 − 1)) ∈ ℕ0)
108106, 107syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆‘(𝑁 − 1)) ∈ ℕ0)
109105, 108nn0addcld 11340 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℕ0)
110109nn0cnd 11338 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℂ)
111110mul02d 10219 . . . . . . 7 (𝑁 ∈ ℕ → (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = 0)
11284, 101, 1113eqtr4a 2680 . . . . . 6 (𝑁 ∈ ℕ → (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
113112a1d 25 . . . . 5 (𝑁 ∈ ℕ → (1 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
114 simplr 791 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℕ)
115114, 13syl6eleq 2709 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (ℤ‘1))
116 peano2fzr 12339 . . . . . . . . . . 11 ((𝑚 ∈ (ℤ‘1) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (1...(𝑁 + 1)))
117115, 116sylancom 700 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (1...(𝑁 + 1)))
118117ex 450 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → 𝑚 ∈ (1...(𝑁 + 1))))
119118imim1d 82 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
120 oveq1 6642 . . . . . . . . . . 11 ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
121 elfzp1 12376 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (ℤ‘1) → ((𝑔‘1) ∈ (1...(𝑚 + 1)) ↔ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))))
122115, 121syl 17 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑔‘1) ∈ (1...(𝑚 + 1)) ↔ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))))
123122rabbidv 3184 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))} = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))})
124 unrab 3890 . . . . . . . . . . . . . . 15 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))}
125123, 124syl6eqr 2672 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))} = ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
126125fveq2d 6182 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (#‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
127 fzfi 12754 . . . . . . . . . . . . . . . . 17 (1...(𝑁 + 1)) ∈ Fin
128 deranglem 31122 . . . . . . . . . . . . . . . . 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 2695 . . . . . . . . . . . . . . 15 𝐴 ∈ Fin
131 ssrab2 3679 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ⊆ 𝐴
132 ssfi 8165 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ⊆ 𝐴) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin)
133130, 131, 132mp2an 707 . . . . . . . . . . . . . 14 {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin
134 ssrab2 3679 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ⊆ 𝐴
135 ssfi 8165 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin)
136130, 134, 135mp2an 707 . . . . . . . . . . . . . 14 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin
137 inrab 3891 . . . . . . . . . . . . . . 15 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))}
138 fzp1disj 12384 . . . . . . . . . . . . . . . . . 18 ((1...𝑚) ∩ {(𝑚 + 1)}) = ∅
13942elsn 4183 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) ∈ {(𝑚 + 1)} ↔ (𝑔‘1) = (𝑚 + 1))
140 inelcm 4023 . . . . . . . . . . . . . . . . . . . 20 (((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) ∈ {(𝑚 + 1)}) → ((1...𝑚) ∩ {(𝑚 + 1)}) ≠ ∅)
141139, 140sylan2br 493 . . . . . . . . . . . . . . . . . . 19 (((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)) → ((1...𝑚) ∩ {(𝑚 + 1)}) ≠ ∅)
142141necon2bi 2821 . . . . . . . . . . . . . . . . . 18 (((1...𝑚) ∩ {(𝑚 + 1)}) = ∅ → ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)))
143138, 142ax-mp 5 . . . . . . . . . . . . . . . . 17 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))
144143rgenw 2921 . . . . . . . . . . . . . . . 16 𝑔𝐴 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))
145 rabeq0 3948 . . . . . . . . . . . . . . . 16 ({𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))} = ∅ ↔ ∀𝑔𝐴 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)))
146144, 145mpbir 221 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))} = ∅
147137, 146eqtri 2642 . . . . . . . . . . . . . 14 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ∅
148 hashun 13154 . . . . . . . . . . . . . 14 (({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin ∧ ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ∅) → (#‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
149133, 136, 147, 148mp3an 1422 . . . . . . . . . . . . 13 (#‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
150126, 149syl6eq 2670 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
151 nncn 11013 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
152151ad2antlr 762 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℂ)
153 ax-1cn 9979 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
154153a1i 11 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 1 ∈ ℂ)
155152, 154, 154addsubd 10398 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑚 + 1) − 1) = ((𝑚 − 1) + 1))
156155oveq1d 6650 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) + 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
157 subcl 10265 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑚 − 1) ∈ ℂ)
158152, 153, 157sylancl 693 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 − 1) ∈ ℂ)
159109ad2antrr 761 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℕ0)
160159nn0cnd 11338 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℂ)
161158, 154, 160adddird 10050 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 − 1) + 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
162160mulid2d 10043 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
163 exmidne 2801 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑔‘(𝑚 + 1)) = 1 ∨ (𝑔‘(𝑚 + 1)) ≠ 1)
164 orcom 402 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑔‘(𝑚 + 1)) = 1 ∨ (𝑔‘(𝑚 + 1)) ≠ 1) ↔ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1))
165163, 164mpbi 220 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)
166165biantru 526 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘1) = (𝑚 + 1) ↔ ((𝑔‘1) = (𝑚 + 1) ∧ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)))
167 andi 910 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔‘1) = (𝑚 + 1) ∧ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)) ↔ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
168166, 167bitri 264 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔‘1) = (𝑚 + 1) ↔ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
169168a1i 11 . . . . . . . . . . . . . . . . . . . 20 (𝑔𝐴 → ((𝑔‘1) = (𝑚 + 1) ↔ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))))
170169rabbiia 3180 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
171 unrab 3890 . . . . . . . . . . . . . . . . . . 19 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
172170, 171eqtr4i 2645 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} = ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})
173172fveq2i 6181 . . . . . . . . . . . . . . . . 17 (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = (#‘({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
174 ssrab2 3679 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ⊆ 𝐴
175 ssfi 8165 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∈ Fin)
176130, 174, 175mp2an 707 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∈ Fin
177 ssrab2 3679 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ⊆ 𝐴
178 ssfi 8165 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ∈ Fin)
179130, 177, 178mp2an 707 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ∈ Fin
180 inrab 3891 . . . . . . . . . . . . . . . . . . 19 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∩ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
181 simpr 477 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1) → (𝑔‘(𝑚 + 1)) = 1)
182181necon3ai 2816 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘(𝑚 + 1)) ≠ 1 → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
183182adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
184 imnan 438 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)) ↔ ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
185183, 184mpbi 220 . . . . . . . . . . . . . . . . . . . . 21 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
186185rgenw 2921 . . . . . . . . . . . . . . . . . . . 20 𝑔𝐴 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
187 rabeq0 3948 . . . . . . . . . . . . . . . . . . . 20 ({𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))} = ∅ ↔ ∀𝑔𝐴 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
188186, 187mpbir 221 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))} = ∅
189180, 188eqtri 2642 . . . . . . . . . . . . . . . . . 18 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∩ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = ∅
190 hashun 13154 . . . . . . . . . . . . . . . . . 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)})))
191176, 179, 189, 190mp3an 1422 . . . . . . . . . . . . . . . . 17 (#‘({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})) = ((#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
192173, 191eqtri 2642 . . . . . . . . . . . . . . . 16 (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ((#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
193 simpll 789 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑁 ∈ ℕ)
194 nnne0 11038 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
195 0p1e1 11117 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 + 1) = 1
196195eqeq2i 2632 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 + 1) = (0 + 1) ↔ (𝑚 + 1) = 1)
197 0cn 10017 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ ℂ
198 addcan2 10206 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 ∈ ℂ ∧ 0 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
199197, 153, 198mp3an23 1414 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℂ → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
200151, 199syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ ℕ → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
201196, 200syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ ℕ → ((𝑚 + 1) = 1 ↔ 𝑚 = 0))
202201necon3bbid 2828 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → (¬ (𝑚 + 1) = 1 ↔ 𝑚 ≠ 0))
203194, 202mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ → ¬ (𝑚 + 1) = 1)
204203ad2antlr 762 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ¬ (𝑚 + 1) = 1)
20514adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑁 + 1) ∈ (ℤ‘1))
206 elfzp12 12403 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 + 1) ∈ (ℤ‘1) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) ↔ ((𝑚 + 1) = 1 ∨ (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1)))))
207205, 206syl 17 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) ↔ ((𝑚 + 1) = 1 ∨ (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1)))))
208207biimpa 501 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑚 + 1) = 1 ∨ (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1))))
209208ord 392 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (¬ (𝑚 + 1) = 1 → (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1))))
210204, 209mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1)))
211 df-2 11064 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
212211oveq1i 6645 . . . . . . . . . . . . . . . . . . 19 (2...(𝑁 + 1)) = ((1 + 1)...(𝑁 + 1))
213210, 212syl6eleqr 2710 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 + 1) ∈ (2...(𝑁 + 1)))
214 ovex 6663 . . . . . . . . . . . . . . . . . 18 (𝑚 + 1) ∈ V
215 eqid 2620 . . . . . . . . . . . . . . . . . 18 ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) = ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})
216 fveq1 6177 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = → (𝑔‘1) = (‘1))
217216eqeq1d 2622 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘1) = (𝑚 + 1) ↔ (‘1) = (𝑚 + 1)))
218 fveq1 6177 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = → (𝑔‘(𝑚 + 1)) = (‘(𝑚 + 1)))
219218neeq1d 2850 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘(𝑚 + 1)) ≠ 1 ↔ (‘(𝑚 + 1)) ≠ 1))
220217, 219anbi12d 746 . . . . . . . . . . . . . . . . . . 19 (𝑔 = → (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ↔ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) ≠ 1)))
221220cbvrabv 3194 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} = {𝐴 ∣ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) ≠ 1)}
222 eqid 2620 . . . . . . . . . . . . . . . . . 18 (( I ↾ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})) ∪ {⟨1, (𝑚 + 1)⟩, ⟨(𝑚 + 1), 1⟩}) = (( I ↾ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})) ∪ {⟨1, (𝑚 + 1)⟩, ⟨(𝑚 + 1), 1⟩})
223 f1oeq1 6114 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
224 fveq2 6178 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑔𝑧) = (𝑔𝑦))
225 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦𝑧 = 𝑦)
226224, 225neeq12d 2852 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → ((𝑔𝑧) ≠ 𝑧 ↔ (𝑔𝑦) ≠ 𝑦))
227226cbvralv 3166 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑔𝑦) ≠ 𝑦)
228 fveq1 6177 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑓 → (𝑔𝑦) = (𝑓𝑦))
229228neeq1d 2850 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑓 → ((𝑔𝑦) ≠ 𝑦 ↔ (𝑓𝑦) ≠ 𝑦))
230229ralbidv 2983 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑔𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦))
231227, 230syl5bb 272 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦))
232223, 231anbi12d 746 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧) ↔ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)))
233232cbvabv 2745 . . . . . . . . . . . . . . . . . 18 {𝑔 ∣ (𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧)} = {𝑓 ∣ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)}
2343, 4, 10, 193, 213, 214, 215, 221, 222, 233subfacp1lem5 31140 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) = (𝑆𝑁))
235218eqeq1d 2622 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘(𝑚 + 1)) = 1 ↔ (‘(𝑚 + 1)) = 1))
236217, 235anbi12d 746 . . . . . . . . . . . . . . . . . . 19 (𝑔 = → (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1) ↔ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) = 1)))
237236cbvrabv 3194 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} = {𝐴 ∣ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) = 1)}
238 f1oeq1 6114 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) ↔ 𝑓:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})))
239226cbvralv 3166 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑦) ≠ 𝑦)
240229ralbidv 2983 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦))
241239, 240syl5bb 272 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦))
242238, 241anbi12d 746 . . . . . . . . . . . . . . . . . . 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)})(𝑓𝑦) ≠ 𝑦)))
243242cbvabv 2745 . . . . . . . . . . . . . . . . . 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)})(𝑓𝑦) ≠ 𝑦)}
2443, 4, 10, 193, 213, 214, 215, 237, 243subfacp1lem3 31138 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = (𝑆‘(𝑁 − 1)))
245234, 244oveq12d 6653 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
246192, 245syl5eq 2666 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
247162, 246eqtr4d 2657 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
248247oveq2d 6651 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
249156, 161, 2483eqtrd 2658 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
250150, 249eqeq12d 2635 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))))
251120, 250syl5ibr 236 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
252251ex 450 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
253252a2d 29 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
254119, 253syld 47 . . . . . . 7 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
255254expcom 451 . . . . . 6 (𝑚 ∈ ℕ → (𝑁 ∈ ℕ → ((𝑚 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
256255a2d 29 . . . . 5 (𝑚 ∈ ℕ → ((𝑁 ∈ ℕ → (𝑚 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) → (𝑁 ∈ ℕ → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
25753, 63, 73, 83, 113, 256nnind 11023 . . . 4 ((𝑁 + 1) ∈ ℕ → (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
2581, 257mpcom 38 . . 3 (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
25934, 258mpd 15 . 2 (𝑁 ∈ ℕ → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
260 nncn 11013 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
261 pncan 10272 . . . 4 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
262260, 153, 261sylancl 693 . . 3 (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
263262oveq1d 6650 . 2 (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
26432, 259, 2633eqtrd 2658 1 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1481  wcel 1988  {cab 2606  wne 2791  wral 2909  {crab 2913  cdif 3564  cun 3565  cin 3566  wss 3567  c0 3907  {csn 4168  {cpr 4170  cop 4174  cmpt 4720   I cid 5013  cres 5106  wf 5872  1-1-ontowf1o 5875  cfv 5876  (class class class)co 6635  Fincfn 7940  cc 9919  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926  cmin 10251  cn 11005  2c2 11055  0cn0 11277  cz 11362  cuz 11672  ...cfz 12311  #chash 13100
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-om 7051  df-1st 7153  df-2nd 7154  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-card 8750  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-nn 11006  df-2 11064  df-n0 11278  df-xnn0 11349  df-z 11363  df-uz 11673  df-fz 12312  df-hash 13101
This theorem is referenced by:  subfacp1  31142
  Copyright terms: Public domain W3C validator