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 31293
Description: Lemma for subfacp1 31294. 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 31290), while the subset with (𝑓𝑀) ≠ 1 has size 𝑆(𝑁) (by subfacp1lem5 31292). 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 11070 . . . . 5 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ)
21nnnn0d 11389 . . . 4 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ ℕ0)
3 derang.d . . . . 5 𝐷 = (𝑥 ∈ Fin ↦ (#‘{𝑓 ∣ (𝑓:𝑥1-1-onto𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) ≠ 𝑦)}))
4 subfac.n . . . . 5 𝑆 = (𝑛 ∈ ℕ0 ↦ (𝐷‘(1...𝑛)))
53, 4subfacval 31281 . . . 4 ((𝑁 + 1) ∈ ℕ0 → (𝑆‘(𝑁 + 1)) = (𝐷‘(1...(𝑁 + 1))))
62, 5syl 17 . . 3 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝐷‘(1...(𝑁 + 1))))
7 fzfid 12812 . . . . 5 (𝑁 ∈ ℕ → (1...(𝑁 + 1)) ∈ Fin)
83derangval 31275 . . . . 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 6232 . . . 4 (#‘𝐴) = (#‘{𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)})
129, 11syl6eqr 2703 . . 3 (𝑁 ∈ ℕ → (𝐷‘(1...(𝑁 + 1))) = (#‘𝐴))
13 nnuz 11761 . . . . . . . . . . 11 ℕ = (ℤ‘1)
141, 13syl6eleq 2740 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (ℤ‘1))
15 eluzfz1 12386 . . . . . . . . . 10 ((𝑁 + 1) ∈ (ℤ‘1) → 1 ∈ (1...(𝑁 + 1)))
1614, 15syl 17 . . . . . . . . 9 (𝑁 ∈ ℕ → 1 ∈ (1...(𝑁 + 1)))
17 f1of 6175 . . . . . . . . . 10 (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) → 𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
1817adantr 480 . . . . . . . . 9 ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) → 𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)))
19 ffvelrn 6397 . . . . . . . . . 10 ((𝑓:(1...(𝑁 + 1))⟶(1...(𝑁 + 1)) ∧ 1 ∈ (1...(𝑁 + 1))) → (𝑓‘1) ∈ (1...(𝑁 + 1)))
2019expcom 450 . . . . . . . . 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 3708 . . . . . . 7 (𝑁 ∈ ℕ → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ (𝑓‘1) ∈ (1...(𝑁 + 1))})
23 fveq1 6228 . . . . . . . . 9 (𝑔 = 𝑓 → (𝑔‘1) = (𝑓‘1))
2423eleq1d 2715 . . . . . . . 8 (𝑔 = 𝑓 → ((𝑔‘1) ∈ (1...(𝑁 + 1)) ↔ (𝑓‘1) ∈ (1...(𝑁 + 1))))
2524cbvabv 2776 . . . . . . 7 {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} = {𝑓 ∣ (𝑓‘1) ∈ (1...(𝑁 + 1))}
2622, 10, 253sstr4g 3679 . . . . . 6 (𝑁 ∈ ℕ → 𝐴 ⊆ {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
27 ssabral 3706 . . . . . 6 (𝐴 ⊆ {𝑔 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} ↔ ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
2826, 27sylib 208 . . . . 5 (𝑁 ∈ ℕ → ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
29 rabid2 3148 . . . . 5 (𝐴 = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))} ↔ ∀𝑔𝐴 (𝑔‘1) ∈ (1...(𝑁 + 1)))
3028, 29sylibr 224 . . . 4 (𝑁 ∈ ℕ → 𝐴 = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
3130fveq2d 6233 . . 3 (𝑁 ∈ ℕ → (#‘𝐴) = (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
326, 12, 313eqtrd 2689 . 2 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
33 elfz1end 12409 . . . 4 ((𝑁 + 1) ∈ ℕ ↔ (𝑁 + 1) ∈ (1...(𝑁 + 1)))
341, 33sylib 208 . . 3 (𝑁 ∈ ℕ → (𝑁 + 1) ∈ (1...(𝑁 + 1)))
35 eleq1 2718 . . . . . . 7 (𝑥 = 1 → (𝑥 ∈ (1...(𝑁 + 1)) ↔ 1 ∈ (1...(𝑁 + 1))))
36 oveq2 6698 . . . . . . . . . . . . 13 (𝑥 = 1 → (1...𝑥) = (1...1))
37 1z 11445 . . . . . . . . . . . . . 14 1 ∈ ℤ
38 fzsn 12421 . . . . . . . . . . . . . 14 (1 ∈ ℤ → (1...1) = {1})
3937, 38ax-mp 5 . . . . . . . . . . . . 13 (1...1) = {1}
4036, 39syl6eq 2701 . . . . . . . . . . . 12 (𝑥 = 1 → (1...𝑥) = {1})
4140eleq2d 2716 . . . . . . . . . . 11 (𝑥 = 1 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ {1}))
42 fvex 6239 . . . . . . . . . . . 12 (𝑔‘1) ∈ V
4342elsn 4225 . . . . . . . . . . 11 ((𝑔‘1) ∈ {1} ↔ (𝑔‘1) = 1)
4441, 43syl6bb 276 . . . . . . . . . 10 (𝑥 = 1 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) = 1))
4544rabbidv 3220 . . . . . . . . 9 (𝑥 = 1 → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) = 1})
4645fveq2d 6233 . . . . . . . 8 (𝑥 = 1 → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}))
47 oveq1 6697 . . . . . . . . . 10 (𝑥 = 1 → (𝑥 − 1) = (1 − 1))
48 1m1e0 11127 . . . . . . . . . 10 (1 − 1) = 0
4947, 48syl6eq 2701 . . . . . . . . 9 (𝑥 = 1 → (𝑥 − 1) = 0)
5049oveq1d 6705 . . . . . . . 8 (𝑥 = 1 → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
5146, 50eqeq12d 2666 . . . . . . 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 2718 . . . . . . 7 (𝑥 = 𝑚 → (𝑥 ∈ (1...(𝑁 + 1)) ↔ 𝑚 ∈ (1...(𝑁 + 1))))
55 oveq2 6698 . . . . . . . . . . 11 (𝑥 = 𝑚 → (1...𝑥) = (1...𝑚))
5655eleq2d 2716 . . . . . . . . . 10 (𝑥 = 𝑚 → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...𝑚)))
5756rabbidv 3220 . . . . . . . . 9 (𝑥 = 𝑚 → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)})
5857fveq2d 6233 . . . . . . . 8 (𝑥 = 𝑚 → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}))
59 oveq1 6697 . . . . . . . . 9 (𝑥 = 𝑚 → (𝑥 − 1) = (𝑚 − 1))
6059oveq1d 6705 . . . . . . . 8 (𝑥 = 𝑚 → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
6158, 60eqeq12d 2666 . . . . . . 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 2718 . . . . . . 7 (𝑥 = (𝑚 + 1) → (𝑥 ∈ (1...(𝑁 + 1)) ↔ (𝑚 + 1) ∈ (1...(𝑁 + 1))))
65 oveq2 6698 . . . . . . . . . . 11 (𝑥 = (𝑚 + 1) → (1...𝑥) = (1...(𝑚 + 1)))
6665eleq2d 2716 . . . . . . . . . 10 (𝑥 = (𝑚 + 1) → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...(𝑚 + 1))))
6766rabbidv 3220 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))})
6867fveq2d 6233 . . . . . . . 8 (𝑥 = (𝑚 + 1) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}))
69 oveq1 6697 . . . . . . . . 9 (𝑥 = (𝑚 + 1) → (𝑥 − 1) = ((𝑚 + 1) − 1))
7069oveq1d 6705 . . . . . . . 8 (𝑥 = (𝑚 + 1) → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
7168, 70eqeq12d 2666 . . . . . . 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 2718 . . . . . . 7 (𝑥 = (𝑁 + 1) → (𝑥 ∈ (1...(𝑁 + 1)) ↔ (𝑁 + 1) ∈ (1...(𝑁 + 1))))
75 oveq2 6698 . . . . . . . . . . 11 (𝑥 = (𝑁 + 1) → (1...𝑥) = (1...(𝑁 + 1)))
7675eleq2d 2716 . . . . . . . . . 10 (𝑥 = (𝑁 + 1) → ((𝑔‘1) ∈ (1...𝑥) ↔ (𝑔‘1) ∈ (1...(𝑁 + 1))))
7776rabbidv 3220 . . . . . . . . 9 (𝑥 = (𝑁 + 1) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)} = {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))})
7877fveq2d 6233 . . . . . . . 8 (𝑥 = (𝑁 + 1) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑥)}) = (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑁 + 1))}))
79 oveq1 6697 . . . . . . . . 9 (𝑥 = (𝑁 + 1) → (𝑥 − 1) = ((𝑁 + 1) − 1))
8079oveq1d 6705 . . . . . . . 8 (𝑥 = (𝑁 + 1) → ((𝑥 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
8178, 80eqeq12d 2666 . . . . . . 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 13196 . . . . . . 7 (#‘∅) = 0
85 fveq2 6229 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → (𝑓𝑦) = (𝑓‘1))
86 id 22 . . . . . . . . . . . . . . . 16 (𝑦 = 1 → 𝑦 = 1)
8785, 86neeq12d 2884 . . . . . . . . . . . . . . 15 (𝑦 = 1 → ((𝑓𝑦) ≠ 𝑦 ↔ (𝑓‘1) ≠ 1))
8887rspcv 3336 . . . . . . . . . . . . . 14 (1 ∈ (1...(𝑁 + 1)) → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 → (𝑓‘1) ≠ 1))
8916, 88syl 17 . . . . . . . . . . . . 13 (𝑁 ∈ ℕ → (∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦 → (𝑓‘1) ≠ 1))
9089adantld 482 . . . . . . . . . . . 12 (𝑁 ∈ ℕ → ((𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦) → (𝑓‘1) ≠ 1))
9190ss2abdv 3708 . . . . . . . . . . 11 (𝑁 ∈ ℕ → {𝑓 ∣ (𝑓:(1...(𝑁 + 1))–1-1-onto→(1...(𝑁 + 1)) ∧ ∀𝑦 ∈ (1...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)} ⊆ {𝑓 ∣ (𝑓‘1) ≠ 1})
92 df-ne 2824 . . . . . . . . . . . . 13 ((𝑔‘1) ≠ 1 ↔ ¬ (𝑔‘1) = 1)
9323neeq1d 2882 . . . . . . . . . . . . 13 (𝑔 = 𝑓 → ((𝑔‘1) ≠ 1 ↔ (𝑓‘1) ≠ 1))
9492, 93syl5bbr 274 . . . . . . . . . . . 12 (𝑔 = 𝑓 → (¬ (𝑔‘1) = 1 ↔ (𝑓‘1) ≠ 1))
9594cbvabv 2776 . . . . . . . . . . 11 {𝑔 ∣ ¬ (𝑔‘1) = 1} = {𝑓 ∣ (𝑓‘1) ≠ 1}
9691, 10, 953sstr4g 3679 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝐴 ⊆ {𝑔 ∣ ¬ (𝑔‘1) = 1})
97 ssabral 3706 . . . . . . . . . 10 (𝐴 ⊆ {𝑔 ∣ ¬ (𝑔‘1) = 1} ↔ ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
9896, 97sylib 208 . . . . . . . . 9 (𝑁 ∈ ℕ → ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
99 rabeq0 3990 . . . . . . . . 9 ({𝑔𝐴 ∣ (𝑔‘1) = 1} = ∅ ↔ ∀𝑔𝐴 ¬ (𝑔‘1) = 1)
10098, 99sylibr 224 . . . . . . . 8 (𝑁 ∈ ℕ → {𝑔𝐴 ∣ (𝑔‘1) = 1} = ∅)
101100fveq2d 6233 . . . . . . 7 (𝑁 ∈ ℕ → (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (#‘∅))
102 nnnn0 11337 . . . . . . . . . . 11 (𝑁 ∈ ℕ → 𝑁 ∈ ℕ0)
1033, 4subfacf 31283 . . . . . . . . . . . 12 𝑆:ℕ0⟶ℕ0
104103ffvelrni 6398 . . . . . . . . . . 11 (𝑁 ∈ ℕ0 → (𝑆𝑁) ∈ ℕ0)
105102, 104syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆𝑁) ∈ ℕ0)
106 nnm1nn0 11372 . . . . . . . . . . 11 (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ0)
107103ffvelrni 6398 . . . . . . . . . . 11 ((𝑁 − 1) ∈ ℕ0 → (𝑆‘(𝑁 − 1)) ∈ ℕ0)
108106, 107syl 17 . . . . . . . . . 10 (𝑁 ∈ ℕ → (𝑆‘(𝑁 − 1)) ∈ ℕ0)
109105, 108nn0addcld 11393 . . . . . . . . 9 (𝑁 ∈ ℕ → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℕ0)
110109nn0cnd 11391 . . . . . . . 8 (𝑁 ∈ ℕ → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℂ)
111110mul02d 10272 . . . . . . 7 (𝑁 ∈ ℕ → (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = 0)
11284, 101, 1113eqtr4a 2711 . . . . . 6 (𝑁 ∈ ℕ → (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
113112a1d 25 . . . . 5 (𝑁 ∈ ℕ → (1 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) = 1}) = (0 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
114 simplr 807 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℕ)
115114, 13syl6eleq 2740 . . . . . . . . . . 11 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (ℤ‘1))
116 peano2fzr 12392 . . . . . . . . . . 11 ((𝑚 ∈ (ℤ‘1) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (1...(𝑁 + 1)))
117115, 116sylancom 702 . . . . . . . . . 10 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ (1...(𝑁 + 1)))
118117ex 449 . . . . . . . . 9 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → 𝑚 ∈ (1...(𝑁 + 1))))
119118imim1d 82 . . . . . . . 8 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → ((𝑚 ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) → ((𝑚 + 1) ∈ (1...(𝑁 + 1)) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))))
120 oveq1 6697 . . . . . . . . . . 11 ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) = ((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) → ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
121 elfzp1 12429 . . . . . . . . . . . . . . . . 17 (𝑚 ∈ (ℤ‘1) → ((𝑔‘1) ∈ (1...(𝑚 + 1)) ↔ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))))
122115, 121syl 17 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑔‘1) ∈ (1...(𝑚 + 1)) ↔ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))))
123122rabbidv 3220 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))} = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))})
124 unrab 3931 . . . . . . . . . . . . . . 15 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∨ (𝑔‘1) = (𝑚 + 1))}
125123, 124syl6eqr 2703 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))} = ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
126125fveq2d 6233 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = (#‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
127 fzfi 12811 . . . . . . . . . . . . . . . . 17 (1...(𝑁 + 1)) ∈ Fin
128 deranglem 31274 . . . . . . . . . . . . . . . . 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 2726 . . . . . . . . . . . . . . 15 𝐴 ∈ Fin
131 ssrab2 3720 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ⊆ 𝐴
132 ssfi 8221 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ⊆ 𝐴) → {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin)
133130, 131, 132mp2an 708 . . . . . . . . . . . . . 14 {𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin
134 ssrab2 3720 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ⊆ 𝐴
135 ssfi 8221 . . . . . . . . . . . . . . 15 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin)
136130, 134, 135mp2an 708 . . . . . . . . . . . . . 14 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin
137 inrab 3932 . . . . . . . . . . . . . . 15 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))}
138 fzp1disj 12437 . . . . . . . . . . . . . . . . . 18 ((1...𝑚) ∩ {(𝑚 + 1)}) = ∅
13942elsn 4225 . . . . . . . . . . . . . . . . . . . 20 ((𝑔‘1) ∈ {(𝑚 + 1)} ↔ (𝑔‘1) = (𝑚 + 1))
140 inelcm 4065 . . . . . . . . . . . . . . . . . . . 20 (((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) ∈ {(𝑚 + 1)}) → ((1...𝑚) ∩ {(𝑚 + 1)}) ≠ ∅)
141139, 140sylan2br 492 . . . . . . . . . . . . . . . . . . 19 (((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)) → ((1...𝑚) ∩ {(𝑚 + 1)}) ≠ ∅)
142141necon2bi 2853 . . . . . . . . . . . . . . . . . 18 (((1...𝑚) ∩ {(𝑚 + 1)}) = ∅ → ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)))
143138, 142ax-mp 5 . . . . . . . . . . . . . . . . 17 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))
144143rgenw 2953 . . . . . . . . . . . . . . . 16 𝑔𝐴 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))
145 rabeq0 3990 . . . . . . . . . . . . . . . 16 ({𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))} = ∅ ↔ ∀𝑔𝐴 ¬ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1)))
146144, 145mpbir 221 . . . . . . . . . . . . . . 15 {𝑔𝐴 ∣ ((𝑔‘1) ∈ (1...𝑚) ∧ (𝑔‘1) = (𝑚 + 1))} = ∅
147137, 146eqtri 2673 . . . . . . . . . . . . . 14 ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ∅
148 hashun 13209 . . . . . . . . . . . . . 14 (({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∈ Fin ∧ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} ∈ Fin ∧ ({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∩ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ∅) → (#‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
149133, 136, 147, 148mp3an 1464 . . . . . . . . . . . . 13 (#‘({𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)} ∪ {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})) = ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
150126, 149syl6eq 2701 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...(𝑚 + 1))}) = ((#‘{𝑔𝐴 ∣ (𝑔‘1) ∈ (1...𝑚)}) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
151 nncn 11066 . . . . . . . . . . . . . . . 16 (𝑚 ∈ ℕ → 𝑚 ∈ ℂ)
152151ad2antlr 763 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑚 ∈ ℂ)
153 ax-1cn 10032 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
154153a1i 11 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 1 ∈ ℂ)
155152, 154, 154addsubd 10451 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑚 + 1) − 1) = ((𝑚 − 1) + 1))
156155oveq1d 6705 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) + 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
157 subcl 10318 . . . . . . . . . . . . . . 15 ((𝑚 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑚 − 1) ∈ ℂ)
158152, 153, 157sylancl 695 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 − 1) ∈ ℂ)
159109ad2antrr 762 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℕ0)
160159nn0cnd 11391 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑆𝑁) + (𝑆‘(𝑁 − 1))) ∈ ℂ)
161158, 154, 160adddird 10103 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 − 1) + 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))))
162160mulid2d 10096 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
163 exmidne 2833 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘(𝑚 + 1)) = 1 ∨ (𝑔‘(𝑚 + 1)) ≠ 1)
164 orcom 401 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑔‘(𝑚 + 1)) = 1 ∨ (𝑔‘(𝑚 + 1)) ≠ 1) ↔ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1))
165163, 164mpbi 220 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)
166165biantru 525 . . . . . . . . . . . . . . . . . . . . 21 ((𝑔‘1) = (𝑚 + 1) ↔ ((𝑔‘1) = (𝑚 + 1) ∧ ((𝑔‘(𝑚 + 1)) ≠ 1 ∨ (𝑔‘(𝑚 + 1)) = 1)))
167 andi 929 . . . . . . . . . . . . . . . . . . . . 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 3216 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
170 unrab 3931 . . . . . . . . . . . . . . . . . . 19 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∨ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
171169, 170eqtr4i 2676 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)} = ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})
172171fveq2i 6232 . . . . . . . . . . . . . . . . 17 (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = (#‘({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
173 ssrab2 3720 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ⊆ 𝐴
174 ssfi 8221 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∈ Fin)
175130, 173, 174mp2an 708 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∈ Fin
176 ssrab2 3720 . . . . . . . . . . . . . . . . . . 19 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ⊆ 𝐴
177 ssfi 8221 . . . . . . . . . . . . . . . . . . 19 ((𝐴 ∈ Fin ∧ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ⊆ 𝐴) → {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ∈ Fin)
178130, 176, 177mp2an 708 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} ∈ Fin
179 inrab 3932 . . . . . . . . . . . . . . . . . . 19 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∩ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = {𝑔𝐴 ∣ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))}
180 simpr 476 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1) → (𝑔‘(𝑚 + 1)) = 1)
181180necon3ai 2848 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑔‘(𝑚 + 1)) ≠ 1 → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
182181adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) → ¬ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
183 imnan 437 . . . . . . . . . . . . . . . . . . . . . 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 2953 . . . . . . . . . . . . . . . . . . . 20 𝑔𝐴 ¬ (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ∧ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1))
186 rabeq0 3990 . . . . . . . . . . . . . . . . . . . 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 2673 . . . . . . . . . . . . . . . . . 18 ({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∩ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = ∅
189 hashun 13209 . . . . . . . . . . . . . . . . . 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 1464 . . . . . . . . . . . . . . . . 17 (#‘({𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} ∪ {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})) = ((#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
191172, 190eqtri 2673 . . . . . . . . . . . . . . . 16 (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ((#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}))
192 simpll 805 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → 𝑁 ∈ ℕ)
193 nnne0 11091 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → 𝑚 ≠ 0)
194 0p1e1 11170 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0 + 1) = 1
195194eqeq2i 2663 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑚 + 1) = (0 + 1) ↔ (𝑚 + 1) = 1)
196 0cn 10070 . . . . . . . . . . . . . . . . . . . . . . . . . 26 0 ∈ ℂ
197 addcan2 10259 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑚 ∈ ℂ ∧ 0 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
198196, 153, 197mp3an23 1456 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑚 ∈ ℂ → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
199151, 198syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑚 ∈ ℕ → ((𝑚 + 1) = (0 + 1) ↔ 𝑚 = 0))
200195, 199syl5bbr 274 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑚 ∈ ℕ → ((𝑚 + 1) = 1 ↔ 𝑚 = 0))
201200necon3bbid 2860 . . . . . . . . . . . . . . . . . . . . . 22 (𝑚 ∈ ℕ → (¬ (𝑚 + 1) = 1 ↔ 𝑚 ≠ 0))
202193, 201mpbird 247 . . . . . . . . . . . . . . . . . . . . 21 (𝑚 ∈ ℕ → ¬ (𝑚 + 1) = 1)
203202ad2antlr 763 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ¬ (𝑚 + 1) = 1)
20414adantr 480 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) → (𝑁 + 1) ∈ (ℤ‘1))
205 elfzp12 12457 . . . . . . . . . . . . . . . . . . . . . . 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 500 . . . . . . . . . . . . . . . . . . . . 21 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((𝑚 + 1) = 1 ∨ (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1))))
208207ord 391 . . . . . . . . . . . . . . . . . . . 20 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (¬ (𝑚 + 1) = 1 → (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1))))
209203, 208mpd 15 . . . . . . . . . . . . . . . . . . 19 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 + 1) ∈ ((1 + 1)...(𝑁 + 1)))
210 df-2 11117 . . . . . . . . . . . . . . . . . . . 20 2 = (1 + 1)
211210oveq1i 6700 . . . . . . . . . . . . . . . . . . 19 (2...(𝑁 + 1)) = ((1 + 1)...(𝑁 + 1))
212209, 211syl6eleqr 2741 . . . . . . . . . . . . . . . . . 18 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (𝑚 + 1) ∈ (2...(𝑁 + 1)))
213 ovex 6718 . . . . . . . . . . . . . . . . . 18 (𝑚 + 1) ∈ V
214 eqid 2651 . . . . . . . . . . . . . . . . . 18 ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) = ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})
215 fveq1 6228 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = → (𝑔‘1) = (‘1))
216215eqeq1d 2653 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘1) = (𝑚 + 1) ↔ (‘1) = (𝑚 + 1)))
217 fveq1 6228 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = → (𝑔‘(𝑚 + 1)) = (‘(𝑚 + 1)))
218217neeq1d 2882 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘(𝑚 + 1)) ≠ 1 ↔ (‘(𝑚 + 1)) ≠ 1))
219216, 218anbi12d 747 . . . . . . . . . . . . . . . . . . 19 (𝑔 = → (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1) ↔ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) ≠ 1)))
220219cbvrabv 3230 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)} = {𝐴 ∣ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) ≠ 1)}
221 eqid 2651 . . . . . . . . . . . . . . . . . 18 (( I ↾ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})) ∪ {⟨1, (𝑚 + 1)⟩, ⟨(𝑚 + 1), 1⟩}) = (( I ↾ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})) ∪ {⟨1, (𝑚 + 1)⟩, ⟨(𝑚 + 1), 1⟩})
222 f1oeq1 6165 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ↔ 𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1))))
223 fveq2 6229 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦 → (𝑔𝑧) = (𝑔𝑦))
224 id 22 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧 = 𝑦𝑧 = 𝑦)
225223, 224neeq12d 2884 . . . . . . . . . . . . . . . . . . . . . 22 (𝑧 = 𝑦 → ((𝑔𝑧) ≠ 𝑧 ↔ (𝑔𝑦) ≠ 𝑦))
226225cbvralv 3201 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑔𝑦) ≠ 𝑦)
227 fveq1 6228 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑔 = 𝑓 → (𝑔𝑦) = (𝑓𝑦))
228227neeq1d 2882 . . . . . . . . . . . . . . . . . . . . . 22 (𝑔 = 𝑓 → ((𝑔𝑦) ≠ 𝑦 ↔ (𝑓𝑦) ≠ 𝑦))
229228ralbidv 3015 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (∀𝑦 ∈ (2...(𝑁 + 1))(𝑔𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦))
230226, 229syl5bb 272 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦))
231222, 230anbi12d 747 . . . . . . . . . . . . . . . . . . 19 (𝑔 = 𝑓 → ((𝑔:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑧 ∈ (2...(𝑁 + 1))(𝑔𝑧) ≠ 𝑧) ↔ (𝑓:(2...(𝑁 + 1))–1-1-onto→(2...(𝑁 + 1)) ∧ ∀𝑦 ∈ (2...(𝑁 + 1))(𝑓𝑦) ≠ 𝑦)))
232231cbvabv 2776 . . . . . . . . . . . . . . . . . 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 31292 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) = (𝑆𝑁))
234217eqeq1d 2653 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = → ((𝑔‘(𝑚 + 1)) = 1 ↔ (‘(𝑚 + 1)) = 1))
235216, 234anbi12d 747 . . . . . . . . . . . . . . . . . . 19 (𝑔 = → (((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1) ↔ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) = 1)))
236235cbvrabv 3230 . . . . . . . . . . . . . . . . . 18 {𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)} = {𝐴 ∣ ((‘1) = (𝑚 + 1) ∧ (‘(𝑚 + 1)) = 1)}
237 f1oeq1 6165 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (𝑔:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)}) ↔ 𝑓:((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})–1-1-onto→((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})))
238225cbvralv 3201 . . . . . . . . . . . . . . . . . . . . 21 (∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑦) ≠ 𝑦)
239228ralbidv 3015 . . . . . . . . . . . . . . . . . . . . 21 (𝑔 = 𝑓 → (∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑦) ≠ 𝑦 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦))
240238, 239syl5bb 272 . . . . . . . . . . . . . . . . . . . 20 (𝑔 = 𝑓 → (∀𝑧 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑔𝑧) ≠ 𝑧 ↔ ∀𝑦 ∈ ((2...(𝑁 + 1)) ∖ {(𝑚 + 1)})(𝑓𝑦) ≠ 𝑦))
241237, 240anbi12d 747 . . . . . . . . . . . . . . . . . . 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 2776 . . . . . . . . . . . . . . . . . 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 31290 . . . . . . . . . . . . . . . . 17 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)}) = (𝑆‘(𝑁 − 1)))
244233, 243oveq12d 6708 . . . . . . . . . . . . . . . 16 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → ((#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) ≠ 1)}) + (#‘{𝑔𝐴 ∣ ((𝑔‘1) = (𝑚 + 1) ∧ (𝑔‘(𝑚 + 1)) = 1)})) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
245191, 244syl5eq 2697 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}) = ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))
246162, 245eqtr4d 2688 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)}))
247246oveq2d 6706 . . . . . . . . . . . . 13 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (1 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1))))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
248156, 161, 2473eqtrd 2689 . . . . . . . . . . . 12 (((𝑁 ∈ ℕ ∧ 𝑚 ∈ ℕ) ∧ (𝑚 + 1) ∈ (1...(𝑁 + 1))) → (((𝑚 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (((𝑚 − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) + (#‘{𝑔𝐴 ∣ (𝑔‘1) = (𝑚 + 1)})))
249150, 248eqeq12d 2666 . . . . . . . . . . 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 449 . . . . . . . . 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 450 . . . . . 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 11076 . . . 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 11066 . . . 4 (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
260 pncan 10325 . . . 4 ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
261259, 153, 260sylancl 695 . . 3 (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
262261oveq1d 6705 . 2 (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
26332, 258, 2623eqtrd 2689 1 (𝑁 ∈ ℕ → (𝑆‘(𝑁 + 1)) = (𝑁 · ((𝑆𝑁) + (𝑆‘(𝑁 − 1)))))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  {cab 2637  wne 2823  wral 2941  {crab 2945  cdif 3604  cun 3605  cin 3606  wss 3607  c0 3948  {csn 4210  {cpr 4212  cop 4216  cmpt 4762   I cid 5052  cres 5145  wf 5922  1-1-ontowf1o 5925  cfv 5926  (class class class)co 6690  Fincfn 7997  cc 9972  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  cmin 10304  cn 11058  2c2 11108  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364  #chash 13157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-card 8803  df-cda 9028  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-2 11117  df-n0 11331  df-xnn0 11402  df-z 11416  df-uz 11726  df-fz 12365  df-hash 13158
This theorem is referenced by:  subfacp1  31294
  Copyright terms: Public domain W3C validator