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

Theorem subfacp1lem6 31505
 Description: Lemma for subfacp1 31506. 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 31502), while the subset with (𝑓‘𝑀) ≠ 1 has size 𝑆(𝑁) (by subfacp1lem5 31504). 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 11234 . . . . 5 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
21nnnn0d 11553 . . . 4 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
3 derang.d . . . . 5 𝐷 = (𝑥 ∈ Fin ↦ (♯‘{𝑓 ∣ (𝑓:𝑥1-1-onto𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) ≠ 𝑦)}))
4 subfac.n . . . . 5 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))
53, 4subfacval 31493 . . . 4 ((𝑁 + 1) ∈ ℕ0 → (𝑆‘(𝑁 + 1)) = (𝐷‘(1...(𝑁 + 1))))
62, 5syl 17 . . 3 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝐷‘(1...(𝑁 + 1))))
7 fzfid 12980 . . . . 5 (𝑁 ∈ ℕ → (1...(𝑁 + 1)) ∈ Fin)
83derangval 31487 . . . . 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 6335 . . . 4 (♯‘𝐴) = (♯‘{𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)})
129, 11syl6eqr 2823 . . 3 (𝑁 ∈ ℕ → (𝐷‘(1...(𝑁 + 1))) = (♯‘𝐴))
13 nnuz 11925 . . . . . . . . . . 11 ℕ = (ℤ‘1)
141, 13syl6eleq 2860 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (ℤ‘1))
15 eluzfz1 12555 . . . . . . . . . 10 ((𝑁 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑁 + 1)))
1614, 15syl 17 . . . . . . . . 9 (𝑁 ∈ ℕ → 1 ∈ (1...(𝑁 + 1)))
17 f1of 6278 . . . . . . . . . 10 (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
1817adantr 466 . . . . . . . . 9 ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) → 𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
19 ffvelrn 6500 . . . . . . . . . 10 ((𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → (𝑓‘1) ∈ (1...(𝑁 + 1)))
2019expcom 398 . . . . . . . . 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 3824 . . . . . . 7 (𝑁 ∈ ℕ → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ (𝑓‘1) ∈ (1...(𝑁 + 1))})
23 fveq1 6331 . . . . . . . . 9 (𝑔 = 𝑓 → (𝑔‘1) = (𝑓‘1))
2423eleq1d 2835 . . . . . . . 8 (𝑔 = 𝑓 → ((𝑔‘1) ∈ (1...(𝑁 + 1)) ↔ (𝑓‘1) ∈ (1...(𝑁 + 1))))
2524cbvabv 2896 . . . . . . 7 {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} = {𝑓 ∣ (𝑓‘1) ∈ (1...(𝑁 + 1))}
2622, 10, 253sstr4g 3795 . . . . . 6 (𝑁 ∈ ℕ → 𝐴 ⊆ {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
27 ssabral 3822 . . . . . 6 (𝐴 ⊆ {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} ↔ ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
2826, 27sylib 208 . . . . 5 (𝑁 ∈ ℕ → ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
29 rabid2 3267 . . . . 5 (𝐴 = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} ↔ ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
3028, 29sylibr 224 . . . 4 (𝑁 ∈ ℕ → 𝐴 = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
3130fveq2d 6336 . . 3 (𝑁 ∈ ℕ → (♯‘𝐴) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
326, 12, 313eqtrd 2809 . 2 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
33 elfz1end 12578 . . . 4 ((𝑁 + 1) ∈ ℕ ↔ (𝑁 + 1) ∈ (1...(𝑁 + 1)))
341, 33sylib 208 . . 3 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (1...(𝑁 + 1)))
35 eleq1 2838 . . . . . . 7 (𝑥 = 1 → (𝑥 ∈ (1...(𝑁 + 1)) ↔ 1 ∈ (1...(𝑁 + 1))))
36 oveq2 6801 . . . . . . . . . . . . 13 (𝑥 = 1 → (1...𝑥) = (1...1))
37 1z 11609 . . . . . . . . . . . . . 14 1 ∈ ℤ
38 fzsn 12590 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (1...1) = {1})
3937, 38ax-mp 5 . . . . . . . . . . . . 13 (1...1) = {1}
4036, 39syl6eq 2821 . . . . . . . . . . . 12 (𝑥 = 1 → (1...𝑥) = {1})
4140eleq2d 2836 . . . . . . . . . . 11 (𝑥 = 1 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ {1}))
42 fvex 6342 . . . . . . . . . . . 12 (𝑔‘1) ∈ V
4342elsn 4331 . . . . . . . . . . 11 ((𝑔‘1) ∈ {1} ↔ (𝑔‘1) = 1)
4441, 43syl6bb 276 . . . . . . . . . 10 (𝑥 = 1 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) = 1))
4544rabbidv 3339 . . . . . . . . 9 (𝑥 = 1 → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) = 1})
4645fveq2d 6336 . . . . . . . 8 (𝑥 = 1 → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}))
47 oveq1 6800 . . . . . . . . . 10 (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
48 1m1e0 11291 . . . . . . . . . 10 (1 − 1) = 0
4947, 48syl6eq 2821 . . . . . . . . 9 (𝑥 = 1 → (𝑥 − 1) = 0)
5049oveq1d 6808 . . . . . . . 8 (𝑥 = 1 → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
5146, 50eqeq12d 2786 . . . . . . 7 (𝑥 = 1 → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
5235, 51imbi12d 333 . . . . . 6 (𝑥 = 1 → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ (1 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
5352imbi2d 329 . . . . 5 (𝑥 = 1 → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → (1 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
54 eleq1 2838 . . . . . . 7 (𝑥 = 𝑚 → (𝑥 ∈ (1...(𝑁 + 1)) ↔ 𝑚 ∈ (1...(𝑁 + 1))))
55 oveq2 6801 . . . . . . . . . . 11 (𝑥 = 𝑚 → (1...𝑥) = (1...𝑚))
5655eleq2d 2836 . . . . . . . . . 10 (𝑥 = 𝑚 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...𝑚)))
5756rabbidv 3339 . . . . . . . . 9 (𝑥 = 𝑚 → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)})
5857fveq2d 6336 . . . . . . . 8 (𝑥 = 𝑚 → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}))
59 oveq1 6800 . . . . . . . . 9 (𝑥 = 𝑚 → (𝑥 − 1) = (𝑚 − 1))
6059oveq1d 6808 . . . . . . . 8 (𝑥 = 𝑚 → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
6158, 60eqeq12d 2786 . . . . . . 7 (𝑥 = 𝑚 → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
6254, 61imbi12d 333 . . . . . 6 (𝑥 = 𝑚 → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ (𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
6362imbi2d 329 . . . . 5 (𝑥 = 𝑚 → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → (𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
64 eleq1 2838 . . . . . . 7 (𝑥 = (𝑚 + 1) → (𝑥 ∈ (1...(𝑁 + 1)) ↔ (𝑚 + 1) ∈ (1...(𝑁 + 1))))
65 oveq2 6801 . . . . . . . . . . 11 (𝑥 = (𝑚 + 1) → (1...𝑥) = (1...(𝑚 + 1)))
6665eleq2d 2836 . . . . . . . . . 10 (𝑥 = (𝑚 + 1) → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...(𝑚 + 1))))
6766rabbidv 3339 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))})
6867fveq2d 6336 . . . . . . . 8 (𝑥 = (𝑚 + 1) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}))
69 oveq1 6800 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → (𝑥 − 1) = ((𝑚 + 1) − 1))
7069oveq1d 6808 . . . . . . . 8 (𝑥 = (𝑚 + 1) → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
7168, 70eqeq12d 2786 . . . . . . 7 (𝑥 = (𝑚 + 1) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
7264, 71imbi12d 333 . . . . . 6 (𝑥 = (𝑚 + 1) → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
7372imbi2d 329 . . . . 5 (𝑥 = (𝑚 + 1) → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
74 eleq1 2838 . . . . . . 7 (𝑥 = (𝑁 + 1) → (𝑥 ∈ (1...(𝑁 + 1)) ↔ (𝑁 + 1) ∈ (1...(𝑁 + 1))))
75 oveq2 6801 . . . . . . . . . . 11 (𝑥 = (𝑁 + 1) → (1...𝑥) = (1...(𝑁 + 1)))
7675eleq2d 2836 . . . . . . . . . 10 (𝑥 = (𝑁 + 1) → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...(𝑁 + 1))))
7776rabbidv 3339 . . . . . . . . 9 (𝑥 = (𝑁 + 1) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
7877fveq2d 6336 . . . . . . . 8 (𝑥 = (𝑁 + 1) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
79 oveq1 6800 . . . . . . . . 9 (𝑥 = (𝑁 + 1) → (𝑥 − 1) = ((𝑁 + 1) − 1))
8079oveq1d 6808 . . . . . . . 8 (𝑥 = (𝑁 + 1) → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
8178, 80eqeq12d 2786 . . . . . . 7 (𝑥 = (𝑁 + 1) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
8274, 81imbi12d 333 . . . . . 6 (𝑥 = (𝑁 + 1) → ((𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) ↔ ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
8382imbi2d 329 . . . . 5 (𝑥 = (𝑁 + 1) → ((𝑁 ∈ ℕ → (𝑥 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))) ↔ (𝑁 ∈ ℕ → ((𝑁 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))))
84 hash0 13360 . . . . . . 7 (♯‘∅) = 0
85 fveq2 6332 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → (𝑓𝑦) = (𝑓‘1))
86 id 22 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → 𝑦 = 1)
8785, 86neeq12d 3004 . . . . . . . . . . . . . . 15 (𝑦 = 1 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑓‘1) ≠ 1))
8887rspcv 3456 . . . . . . . . . . . . . 14 (1 ∈ (1...(𝑁 + 1)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 → (𝑓‘1) ≠ 1))
8916, 88syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 → (𝑓‘1) ≠ 1))
9089adantld 478 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) → (𝑓‘1) ≠ 1))
9190ss2abdv 3824 . . . . . . . . . . 11 (𝑁 ∈ ℕ → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ (𝑓‘1) ≠ 1})
92 df-ne 2944 . . . . . . . . . . . . 13 ((𝑔‘1) ≠ 1 ↔ ¬ (𝑔‘1) = 1)
9323neeq1d 3002 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → ((𝑔‘1) ≠ 1 ↔ (𝑓‘1) ≠ 1))
9492, 93syl5bbr 274 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (¬ (𝑔‘1) = 1 ↔ (𝑓‘1) ≠ 1))
9594cbvabv 2896 . . . . . . . . . . 11 {𝑔 ∣ ¬ (𝑔‘1) = 1} = {𝑓 ∣ (𝑓‘1) ≠ 1}
9691, 10, 953sstr4g 3795 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝐴 ⊆ {𝑔 ∣ ¬ (𝑔‘1) = 1})
97 ssabral 3822 . . . . . . . . . 10 (𝐴 ⊆ {𝑔 ∣ ¬ (𝑔‘1) = 1} ↔ ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
9896, 97sylib 208 . . . . . . . . 9 (𝑁 ∈ ℕ → ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
99 rabeq0 4103 . . . . . . . . 9 ({𝑔𝐴 ∣ (𝑔‘1) = 1} = ∅ ↔ ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
10098, 99sylibr 224 . . . . . . . 8 (𝑁 ∈ ℕ → {𝑔𝐴 ∣ (𝑔‘1) = 1} = ∅)
101100fveq2d 6336 . . . . . . 7 (𝑁 ∈ ℕ → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (♯‘∅))
102 nnnn0 11501 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
1033, 4subfacf 31495 . . . . . . . . . . . 12 𝑆:ℕ0⟶ℕ0
104103ffvelrni 6501 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (𝑆𝑁) ∈ ℕ0)
105102, 104syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆𝑁) ∈ ℕ0)
106 nnm1nn0 11536 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
107103ffvelrni 6501 . . . . . . . . . . 11 ((𝑁 − 1) ∈ ℕ0 → (𝑆‘(𝑁 − 1)) ∈ ℕ0)
108106, 107syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆‘(𝑁 − 1)) ∈ ℕ0)
109105, 108nn0addcld 11557 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℕ0)
110109nn0cnd 11555 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℂ)
111110mul02d 10436 . . . . . . 7 (𝑁 ∈ ℕ → (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = 0)
11284, 101, 1113eqtr4a 2831 . . . . . 6 (𝑁 ∈ ℕ → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
113112a1d 25 . . . . 5 (𝑁 ∈ ℕ → (1 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
114 simplr 752 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℕ)
115114, 13syl6eleq 2860 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (ℤ‘1))
116 peano2fzr 12561 . . . . . . . . . . 11 ((𝑚 ∈ (ℤ‘1) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (1...(𝑁 + 1)))
117115, 116sylancom 576 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (1...(𝑁 + 1)))
118117ex 397 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → 𝑚 ∈ (1...(𝑁 + 1))))
119118imim1d 82 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
120 oveq1 6800 . . . . . . . . . . 11 ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
121 elfzp1 12598 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (ℤ‘1) → ((𝑔‘1) ∈ (1...(𝑚 + 1)) ↔ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))))
122115, 121syl 17 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑔‘1) ∈ (1...(𝑚 + 1)) ↔ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))))
123122rabbidv 3339 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))} = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))})
124 unrab 4046 . . . . . . . . . . . . . . 15 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))}
125123, 124syl6eqr 2823 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))} = ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
126125fveq2d 6336 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (♯‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
127 fzfi 12979 . . . . . . . . . . . . . . . . 17 (1...(𝑁 + 1)) ∈ Fin
128 deranglem 31486 . . . . . . . . . . . . . . . . 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 2846 . . . . . . . . . . . . . . 15 𝐴 ∈ Fin
131 ssrab2 3836 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ⊆ 𝐴
132 ssfi 8336 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ⊆ 𝐴) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin)
133130, 131, 132mp2an 672 . . . . . . . . . . . . . 14 {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin
134 ssrab2 3836 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ⊆ 𝐴
135 ssfi 8336 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin)
136130, 134, 135mp2an 672 . . . . . . . . . . . . . 14 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin
137 inrab 4047 . . . . . . . . . . . . . . 15 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))}
138 fzp1disj 12606 . . . . . . . . . . . . . . . . . 18 ((1...𝑚) ∩ {(𝑚 + 1)}) = ∅
13942elsn 4331 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) ∈ {(𝑚 + 1)} ↔ (𝑔‘1) = (𝑚 + 1))
140 inelcm 4175 . . . . . . . . . . . . . . . . . . . 20 (((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) ∈ {(𝑚 + 1)}) → ((1...𝑚) ∩ {(𝑚 + 1)}) ≠ ∅)
141139, 140sylan2br 582 . . . . . . . . . . . . . . . . . . 19 (((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)) → ((1...𝑚) ∩ {(𝑚 + 1)}) ≠ ∅)
142141necon2bi 2973 . . . . . . . . . . . . . . . . . 18 (((1...𝑚) ∩ {(𝑚 + 1)}) = ∅ → ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)))
143138, 142ax-mp 5 . . . . . . . . . . . . . . . . 17 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))
144143rgenw 3073 . . . . . . . . . . . . . . . 16 𝑔𝐴 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))
145 rabeq0 4103 . . . . . . . . . . . . . . . 16 ({𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))} = ∅ ↔ ∀𝑔𝐴 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)))
146144, 145mpbir 221 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))} = ∅
147137, 146eqtri 2793 . . . . . . . . . . . . . 14 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ∅
148 hashun 13373 . . . . . . . . . . . . . 14 (({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin ∧ ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ∅) → (♯‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
149133, 136, 147, 148mp3an 1572 . . . . . . . . . . . . 13 (♯‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
150126, 149syl6eq 2821 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
151 nncn 11230 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
152151ad2antlr 706 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℂ)
153 ax-1cn 10196 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
154153a1i 11 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 1 ∈ ℂ)
155152, 154, 154addsubd 10615 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑚 + 1) − 1) = ((𝑚 − 1) + 1))
156155oveq1d 6808 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) + 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
157 subcl 10482 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑚 − 1) ∈ ℂ)
158152, 153, 157sylancl 574 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 − 1) ∈ ℂ)
159109ad2antrr 705 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℕ0)
160159nn0cnd 11555 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℂ)
161158, 154, 160adddird 10267 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 − 1) + 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
162160mulid2d 10260 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
163 exmidne 2953 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘(𝑚 + 1)) = 1 ∨ (𝑔‘(𝑚 + 1)) ≠ 1)
164 orcom 857 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔‘(𝑚 + 1)) = 1 ∨ (𝑔‘(𝑚 + 1)) ≠ 1) ↔ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1))
165163, 164mpbi 220 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)
166165biantru 519 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔‘1) = (𝑚 + 1) ↔ ((𝑔‘1) = (𝑚 + 1) ∧ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)))
167 andi 987 . . . . . . . . . . . . . . . . . . . . 21 (((𝑔‘1) = (𝑚 + 1) ∧ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)) ↔ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
168166, 167bitri 264 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) = (𝑚 + 1) ↔ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
169168rabbii 3335 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
170 unrab 4046 . . . . . . . . . . . . . . . . . . 19 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
171169, 170eqtr4i 2796 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} = ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})
172171fveq2i 6335 . . . . . . . . . . . . . . . . 17 (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = (♯‘({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
173 ssrab2 3836 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ⊆ 𝐴
174 ssfi 8336 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∈ Fin)
175130, 173, 174mp2an 672 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∈ Fin
176 ssrab2 3836 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ⊆ 𝐴
177 ssfi 8336 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ∈ Fin)
178130, 176, 177mp2an 672 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ∈ Fin
179 inrab 4047 . . . . . . . . . . . . . . . . . . 19 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∩ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
180 simpr 471 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1) → (𝑔‘(𝑚 + 1)) = 1)
181180necon3ai 2968 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘(𝑚 + 1)) ≠ 1 → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
182181adantl 467 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
183 imnan 386 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)) ↔ ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
184182, 183mpbi 220 . . . . . . . . . . . . . . . . . . . . 21 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
185184rgenw 3073 . . . . . . . . . . . . . . . . . . . 20 𝑔𝐴 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
186 rabeq0 4103 . . . . . . . . . . . . . . . . . . . 20 ({𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))} = ∅ ↔ ∀𝑔𝐴 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)))
187185, 186mpbir 221 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))} = ∅
188179, 187eqtri 2793 . . . . . . . . . . . . . . . . . 18 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∩ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = ∅
189 hashun 13373 . . . . . . . . . . . . . . . . . 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 1572 . . . . . . . . . . . . . . . . 17 (♯‘({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})) = ((♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
191172, 190eqtri 2793 . . . . . . . . . . . . . . . 16 (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ((♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
192 simpll 750 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑁 ∈ ℕ)
193 nnne0 11255 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
194 0p1e1 11334 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 + 1) = 1
195194eqeq2i 2783 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 + 1) = (0 + 1) ↔ (𝑚 + 1) = 1)
196 0cn 10234 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ ℂ
197 addcan2 10423 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 ∈ ℂ ∧ 0 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
198196, 153, 197mp3an23 1564 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℂ → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
199151, 198syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ ℕ → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
200195, 199syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ ℕ → ((𝑚 + 1) = 1 ↔ 𝑚 = 0))
201200necon3bbid 2980 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → (¬ (𝑚 + 1) = 1 ↔ 𝑚 ≠ 0))
202193, 201mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ → ¬ (𝑚 + 1) = 1)
203202ad2antlr 706 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ¬ (𝑚 + 1) = 1)
20414adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑁 + 1) ∈ (ℤ‘1))
205 elfzp12 12626 . . . . . . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑚 + 1) = 1 ∨ (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1))))
208207ord 851 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (¬ (𝑚 + 1) = 1 → (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1))))
209203, 208mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1)))
210 df-2 11281 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
211210oveq1i 6803 . . . . . . . . . . . . . . . . . . 19 (2...(𝑁 + 1)) = ((1 + 1)...(𝑁 + 1))
212209, 211syl6eleqr 2861 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 + 1) ∈ (2...(𝑁 + 1)))
213 ovex 6823 . . . . . . . . . . . . . . . . . 18 (𝑚 + 1) ∈ V
214 eqid 2771 . . . . . . . . . . . . . . . . . 18 ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) = ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})
215 fveq1 6331 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = → (𝑔‘1) = (‘1))
216215eqeq1d 2773 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘1) = (𝑚 + 1) ↔ (‘1) = (𝑚 + 1)))
217 fveq1 6331 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = → (𝑔‘(𝑚 + 1)) = (‘(𝑚 + 1)))
218217neeq1d 3002 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘(𝑚 + 1)) ≠ 1 ↔ (‘(𝑚 + 1)) ≠ 1))
219216, 218anbi12d 616 . . . . . . . . . . . . . . . . . . 19 (𝑔 = → (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ↔ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) ≠ 1)))
220219cbvrabv 3349 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} = {𝐴 ∣ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) ≠ 1)}
221 eqid 2771 . . . . . . . . . . . . . . . . . 18 (( I ↾ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})) ∪ {⟨1, (𝑚 + 1)⟩, ⟨(𝑚 + 1), 1⟩}) = (( I ↾ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})) ∪ {⟨1, (𝑚 + 1)⟩, ⟨(𝑚 + 1), 1⟩})
222 f1oeq1 6268 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
223 fveq2 6332 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑔𝑧) = (𝑔𝑦))
224 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦𝑧 = 𝑦)
225223, 224neeq12d 3004 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → ((𝑔𝑧) ≠ 𝑧 ↔ (𝑔𝑦) ≠ 𝑦))
226225cbvralv 3320 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑔𝑦) ≠ 𝑦)
227 fveq1 6331 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑓 → (𝑔𝑦) = (𝑓𝑦))
228227neeq1d 3002 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑓 → ((𝑔𝑦) ≠ 𝑦 ↔ (𝑓𝑦) ≠ 𝑦))
229228ralbidv 3135 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑔𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦))
230226, 229syl5bb 272 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦))
231222, 230anbi12d 616 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧) ↔ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)))
232231cbvabv 2896 . . . . . . . . . . . . . . . . . 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 31504 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) = (𝑆𝑁))
234217eqeq1d 2773 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘(𝑚 + 1)) = 1 ↔ (‘(𝑚 + 1)) = 1))
235216, 234anbi12d 616 . . . . . . . . . . . . . . . . . . 19 (𝑔 = → (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1) ↔ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) = 1)))
236235cbvrabv 3349 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} = {𝐴 ∣ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) = 1)}
237 f1oeq1 6268 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) ↔ 𝑓:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})))
238225cbvralv 3320 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑦) ≠ 𝑦)
239228ralbidv 3135 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦))
240238, 239syl5bb 272 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦))
241237, 240anbi12d 616 . . . . . . . . . . . . . . . . . . 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 2896 . . . . . . . . . . . . . . . . . 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 31502 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = (𝑆‘(𝑁 − 1)))
244233, 243oveq12d 6811 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (♯‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
245191, 244syl5eq 2817 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
246162, 245eqtr4d 2808 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
247246oveq2d 6809 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
248156, 161, 2473eqtrd 2809 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
249150, 248eqeq12d 2786 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) ↔ ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (♯‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))))
250120, 249syl5ibr 236 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → (♯‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
251250ex 397 . . . . . . . . 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 398 . . . . . 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 11240 . . . 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 11230 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
260 pncan 10489 . . . 4 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
261259, 153, 260sylancl 574 . . 3 (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
262261oveq1d 6808 . 2 (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
26332, 258, 2623eqtrd 2809 1 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 382   ∨ wo 834   = wceq 1631   ∈ wcel 2145  {cab 2757   ≠ wne 2943  ∀wral 3061  {crab 3065   ∖ cdif 3720   ∪ cun 3721   ∩ cin 3722   ⊆ wss 3723  ∅c0 4063  {csn 4316  {cpr 4318  ⟨cop 4322   ↦ cmpt 4863   I cid 5156   ↾ cres 5251  ⟶wf 6027  –1-1-onto→wf1o 6030  ‘cfv 6031  (class class class)co 6793  Fincfn 8109  ℂcc 10136  0cc0 10138  1c1 10139   + caddc 10141   · cmul 10143   − cmin 10468  ℕcn 11222  2c2 11272  ℕ0cn0 11494  ℤcz 11579  ℤ≥cuz 11888  ...cfz 12533  ♯chash 13321 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-2o 7714  df-oadd 7717  df-er 7896  df-map 8011  df-pm 8012  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-card 8965  df-cda 9192  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-2 11281  df-n0 11495  df-xnn0 11566  df-z 11580  df-uz 11889  df-fz 12534  df-hash 13322 This theorem is referenced by:  subfacp1  31506
 Copyright terms: Public domain W3C validator