Theorem sticksstones22 42149

Description: Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024.)

Hypotheses

Ref	Expression
sticksstones22.1	⊢ (𝜑 → 𝑁 ∈ ℕ0)
sticksstones22.2	⊢ (𝜑 → 𝑆 ∈ Fin)
sticksstones22.3	⊢ (𝜑 → 𝑆 ≠ ∅)
sticksstones22.4	⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}

Assertion

Ref	Expression
sticksstones22	⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))

Distinct variable groups:   𝑓,𝑁   𝑆,𝑓,𝑖   𝜑,𝑓,𝑖

Allowed substitution hints:   𝐴(𝑓,𝑖)   𝑁(𝑖)

Proof of Theorem sticksstones22

Dummy variables 𝑥 𝑠 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sticksstones22.4	. . . 4 ⊢ 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}
2	1	a1i 11	. . 3 ⊢ (𝜑 → 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)})
3	2	fveq2d 6844	. 2 ⊢ (𝜑 → (♯‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}))
4		sticksstones22.1	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
5		breq2 5106	. . . . . . . 8 ⊢ (𝑥 = 0 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0))
6	5	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)))
7	6	abbidv 2795	. . . . . 6 ⊢ (𝑥 = 0 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)})
8	7	fveq2d 6844	. . . . 5 ⊢ (𝑥 = 0 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}))
9		oveq1 7376	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 + (♯‘𝑆)) = (0 + (♯‘𝑆)))
10	9	oveq1d 7384	. . . . 5 ⊢ (𝑥 = 0 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
11	8, 10	eqeq12d 2745	. . . 4 ⊢ (𝑥 = 0 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆))))
12		breq2 5106	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
13	12	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)))
14	13	abbidv 2795	. . . . . 6 ⊢ (𝑥 = 𝑦 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)})
15	14	fveq2d 6844	. . . . 5 ⊢ (𝑥 = 𝑦 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}))
16		oveq1 7376	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 + (♯‘𝑆)) = (𝑦 + (♯‘𝑆)))
17	16	oveq1d 7384	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆)))
18	15, 17	eqeq12d 2745	. . . 4 ⊢ (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))))
19		breq2 5106	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)))
20	19	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
21	20	abbidv 2795	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))})
22	21	fveq2d 6844	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}))
23		oveq1 7376	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 + (♯‘𝑆)) = ((𝑦 + 1) + (♯‘𝑆)))
24	23	oveq1d 7384	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
25	22, 24	eqeq12d 2745	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆))))
26		breq2 5106	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁))
27	26	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)))
28	27	abbidv 2795	. . . . . 6 ⊢ (𝑥 = 𝑁 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)})
29	28	fveq2d 6844	. . . . 5 ⊢ (𝑥 = 𝑁 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}))
30		oveq1 7376	. . . . . 6 ⊢ (𝑥 = 𝑁 → (𝑥 + (♯‘𝑆)) = (𝑁 + (♯‘𝑆)))
31	30	oveq1d 7384	. . . . 5 ⊢ (𝑥 = 𝑁 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
32	29, 31	eqeq12d 2745	. . . 4 ⊢ (𝑥 = 𝑁 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆))))
33		simprl 770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 𝑓:𝑆⟶ℕ0)
34		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)
35		sticksstones22.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ∈ Fin)
36	35	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → 𝑆 ∈ Fin)
37		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → 𝑓:𝑆⟶ℕ0)
38	37	ffvelcdmda 7038	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
39	36, 38	fsumnn0cl 15678	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
40	33, 39	syldan 591	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
41	40	nn0ge0d 12482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 0 ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
42		0red 11153	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 0 ∈ ℝ)
43	40	nn0red 12480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
44	42, 43	lenltd 11296	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (0 ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ↔ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0))
45	41, 44	mpbid 232	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0)
46	34, 45	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0 ∧ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0))
47	43, 42	eqleltd 11294	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0 ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0 ∧ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0)))
48	46, 47	mpbird 257	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)
49	33, 48	jca 511	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0))
50	49	ex 412	. . . . . . . 8 ⊢ (𝜑 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)))
51		simprl 770	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 𝑓:𝑆⟶ℕ0)
52		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)
53		0red 11153	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 0 ∈ ℝ)
54	53	leidd 11720	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 0 ≤ 0)
55	52, 54	eqbrtrd 5124	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)
56	51, 55	jca 511	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0))
57	56	ex 412	. . . . . . . 8 ⊢ (𝜑 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)))
58	50, 57	impbid 212	. . . . . . 7 ⊢ (𝜑 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)))
59	58	abbidv 2795	. . . . . 6 ⊢ (𝜑 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)})
60	59	fveq2d 6844	. . . . 5 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}))
61		0nn0 12433	. . . . . . . 8 ⊢ 0 ∈ ℕ0
62	61	a1i 11	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℕ0)
63		sticksstones22.3	. . . . . . 7 ⊢ (𝜑 → 𝑆 ≠ ∅)
64		eqid 2729	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}
65	62, 35, 63, 64	sticksstones21 42148	. . . . . 6 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}) = ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
66		hashnncl 14307	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ Fin → ((♯‘𝑆) ∈ ℕ ↔ 𝑆 ≠ ∅))
67	35, 66	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((♯‘𝑆) ∈ ℕ ↔ 𝑆 ≠ ∅))
68	67	bicomd 223	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆 ≠ ∅ ↔ (♯‘𝑆) ∈ ℕ))
69	68	biimpd 229	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ≠ ∅ → (♯‘𝑆) ∈ ℕ))
70	63, 69	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ)
71	70	nncnd 12178	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑆) ∈ ℂ)
72		1cnd 11145	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
73	71, 72	subcld 11509	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑆) − 1) ∈ ℂ)
74	73	addlidd 11351	. . . . . . . . 9 ⊢ (𝜑 → (0 + ((♯‘𝑆) − 1)) = ((♯‘𝑆) − 1))
75	74	oveq1d 7384	. . . . . . . 8 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)))
76		nnm1nn0 12459	. . . . . . . . . 10 ⊢ ((♯‘𝑆) ∈ ℕ → ((♯‘𝑆) − 1) ∈ ℕ0)
77	70, 76	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑆) − 1) ∈ ℕ0)
78		bcnn 14253	. . . . . . . . 9 ⊢ (((♯‘𝑆) − 1) ∈ ℕ0 → (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)) = 1)
79	77, 78	syl 17	. . . . . . . 8 ⊢ (𝜑 → (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)) = 1)
80	75, 79	eqtrd 2764	. . . . . . 7 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = 1)
81		eqidd 2730	. . . . . . 7 ⊢ (𝜑 → 1 = 1)
82	70	nnnn0d 12479	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ0)
83		bcnn 14253	. . . . . . . . . 10 ⊢ ((♯‘𝑆) ∈ ℕ0 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
84	82, 83	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
85	84	eqcomd 2735	. . . . . . . 8 ⊢ (𝜑 → 1 = ((♯‘𝑆)C(♯‘𝑆)))
86	71	addlidd 11351	. . . . . . . . . 10 ⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
87	86	eqcomd 2735	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑆) = (0 + (♯‘𝑆)))
88	87	oveq1d 7384	. . . . . . . 8 ⊢ (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
89	85, 88	eqtrd 2764	. . . . . . 7 ⊢ (𝜑 → 1 = ((0 + (♯‘𝑆))C(♯‘𝑆)))
90	80, 81, 89	3eqtrd 2768	. . . . . 6 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
91	65, 90	eqtrd 2764	. . . . 5 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
92	60, 91	eqtrd 2764	. . . 4 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
93		simprl 770	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑓:𝑆⟶ℕ0)
94		simprr 772	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))
95	35	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → 𝑆 ∈ Fin)
96		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → 𝑓:𝑆⟶ℕ0)
97	96	ffvelcdmda 7038	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
98	95, 97	fsumnn0cl 15678	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
99	93, 98	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
100	99	nn0red 12480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
101		nn0re 12427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℝ)
102	101	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℝ)
103	102	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℝ)
104		1red 11151	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 1 ∈ ℝ)
105	103, 104	readdcld 11179	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
106	100, 105	leloed 11293	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1) ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
107	94, 106	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
108	99	nn0zd 12531	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ)
109		nn0z 12530	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℤ)
110	109	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℤ)
111	110	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℤ)
112		zleltp1 12560	. . . . . . . . . . . . . . . . 17 ⊢ ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1)))
113	112	bicomd 223	. . . . . . . . . . . . . . . 16 ⊢ ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
114	108, 111, 113	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
115	114	orbi1d 916	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)) ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
116	107, 115	mpbid 232	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
117	93, 116	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
118		andi 1009	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ↔ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
119	118	bicomi 224	. . . . . . . . . . . 12 ⊢ (((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ↔ (𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
120	117, 119	sylibr 234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
121	120	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))))
122		simprl 770	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶ℕ0)
123	122, 98	syldan 591	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
124	123	nn0red 12480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
125	102	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℝ)
126		1red 11151	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 1 ∈ ℝ)
127	125, 126	readdcld 11179	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑦 + 1) ∈ ℝ)
128		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
129	125	lep1d 12090	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ≤ (𝑦 + 1))
130	124, 125, 127, 128, 129	letrd 11307	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))
131	122, 130	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)))
132	131	ex 412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
133		simprl 770	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓:𝑆⟶ℕ0)
134		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
135	102	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑦 ∈ ℝ)
136		1red 11151	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 1 ∈ ℝ)
137	135, 136	readdcld 11179	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
138	137	leidd 11720	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑦 + 1) ≤ (𝑦 + 1))
139	134, 138	eqbrtrd 5124	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))
140	133, 139	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)))
141	140	ex 412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
142	132, 141	jaod 859	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
143	121, 142	impbid 212	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)) ↔ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))))
144	143	abbidv 2795	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
145		unab 4267	. . . . . . . . . 10 ⊢ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))}
146	145	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
147	146	eqcomd 2735	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
148	144, 147	eqtrd 2764	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
149	148	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
150	149	fveq2d 6844	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
151	35	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑆 ∈ Fin)
152		fzfid 13914	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (0...𝑦) ∈ Fin)
153	151, 152	jca 511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin))
154		xpfi 9245	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin) → (𝑆 × (0...𝑦)) ∈ Fin)
155	153, 154	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 × (0...𝑦)) ∈ Fin)
156		pwfi 9244	. . . . . . . . . . 11 ⊢ ((𝑆 × (0...𝑦)) ∈ Fin ↔ 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
157	155, 156	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
158		fsetsspwxp 8803	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦))
159	158	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦)))
160	157, 159	ssfid 9188	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ∈ Fin)
161		ffn 6670	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝑆⟶ℕ0 → 𝑓 Fn 𝑆)
162	122, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓 Fn 𝑆)
163		0zd 12517	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ∈ ℤ)
164	110	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℤ)
165	164	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℤ)
166	122	ffvelcdmda 7038	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℕ0)
167	166	nn0zd 12531	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℤ)
168	166	nn0ge0d 12482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ≤ (𝑓‘𝑠))
169	128	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
170	125	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 ∈ ℝ)
171	166	nn0red 12480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℝ)
172	171	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℝ)
173	124	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
174	173	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
175		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 < (𝑓‘𝑠))
176		simplll 774	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝜑)
177		simpllr 775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℕ0)
178		simplrl 776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑓:𝑆⟶ℕ0)
179	176, 177, 178	jca31 514	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0))
180		difssd 4096	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
181	35, 180	ssfid 9188	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑆 ∖ {𝑠}) ∈ Fin)
182	181	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
183	182	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
184		eldifi 4090	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 ∈ (𝑆 ∖ {𝑠}) → 𝑖 ∈ 𝑆)
185	184	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) → 𝑖 ∈ 𝑆)
186	97	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
187	185, 186	mpdan 687	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) → (𝑓‘𝑖) ∈ ℕ0)
188	183, 187	fsumnn0cl 15678	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
189	179, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
190	189	nn0ge0d 12482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))
191		difssd 4096	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
192	95, 191	ssfid 9188	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
193	192, 187	fsumnn0cl 15678	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
194	179, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
195	194	nn0red 12480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℝ)
196	171, 195	addge01d 11742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ↔ (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))))
197	190, 196	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
198		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
199	179, 198	jca 511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆))
200		nfv 1914	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑖(((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆)
201		nfcv 2891	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑖(𝑓‘𝑠)
202	95	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → 𝑆 ∈ Fin)
203	97	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
204	203	nn0cnd 12481	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℂ)
205		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
206		fveq2 6840	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑠 → (𝑓‘𝑖) = (𝑓‘𝑠))
207	200, 201, 202, 204, 205, 206	fsumsplit1 15687	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
208	199, 207	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
209	208	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)) = Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
210	197, 209	breqtrd 5128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
211	210	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
212	170, 172, 174, 175, 211	ltletrd 11310	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
213	170, 174	ltnled 11297	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑦 < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ↔ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
214	212, 213	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
215	169, 214	pm2.21dd 195	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → ¬ 𝑦 < (𝑓‘𝑠))
216	215	pm2.01da 798	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ¬ 𝑦 < (𝑓‘𝑠))
217	177, 101	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℝ)
218	171, 217	lenltd 11296	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) ≤ 𝑦 ↔ ¬ 𝑦 < (𝑓‘𝑠)))
219	216, 218	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ 𝑦)
220	163, 165, 167, 168, 219	elfzd 13452	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ (0...𝑦))
221	220	ralrimiva 3125	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦))
222	162, 221	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦)))
223		ffnfv 7073	. . . . . . . . . . . 12 ⊢ (𝑓:𝑆⟶(0...𝑦) ↔ (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦)))
224	222, 223	sylibr 234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶(0...𝑦))
225	224	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) → 𝑓:𝑆⟶(0...𝑦)))
226	225	ss2abdv 4026	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ⊆ {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)})
227	160, 226	ssfid 9188	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin)
228	227	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin)
229		fzfid 13914	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (0...(𝑦 + 1)) ∈ Fin)
230	151, 229	jca 511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin))
231		xpfi 9245	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
232	230, 231	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
233		pwfi 9244	. . . . . . . . . . 11 ⊢ ((𝑆 × (0...(𝑦 + 1))) ∈ Fin ↔ 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
234	232, 233	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
235		fsetsspwxp 8803	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1)))
236	235	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1))))
237	234, 236	ssfid 9188	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ∈ Fin)
238	161	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓 Fn 𝑆)
239		0zd 12517	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 0 ∈ ℤ)
240		simpllr 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℕ0)
241	240	nn0zd 12531	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℤ)
242	241	peano2zd 12617	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑦 + 1) ∈ ℤ)
243	133	ffvelcdmda 7038	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℕ0)
244	243	nn0zd 12531	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℤ)
245	243	nn0ge0d 12482	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 0 ≤ (𝑓‘𝑠))
246	134	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
247	137	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) ∈ ℝ)
248	133	ad2antrr 726	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 𝑓:𝑆⟶ℕ0)
249		simplr 768	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 𝑠 ∈ 𝑆)
250	248, 249	ffvelcdmd 7039	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℕ0)
251	250	nn0red 12480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℝ)
252	246, 247	eqeltrd 2828	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
253		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) < (𝑓‘𝑠))
254	133, 188	syldan 591	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
255	254	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
256	255	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
257	256	nn0ge0d 12482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))
258	256	nn0red 12480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℝ)
259	251, 258	addge01d 11742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ↔ (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))))
260	257, 259	mpbid 232	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
261	133, 207	syldanl 602	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
262	261	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
263	262	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)) = Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
264	260, 263	breqtrd 5128	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
265	247, 251, 252, 253, 264	ltletrd 11310	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
266	247, 265	ltned 11286	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) ≠ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
267	266	necomd 2980	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≠ (𝑦 + 1))
268	246, 267	pm2.21ddne 3009	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → ¬ (𝑦 + 1) < (𝑓‘𝑠))
269	268	pm2.01da 798	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → ¬ (𝑦 + 1) < (𝑓‘𝑠))
270	243	nn0red 12480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℝ)
271	137	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑦 + 1) ∈ ℝ)
272	270, 271	lenltd 11296	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) ≤ (𝑦 + 1) ↔ ¬ (𝑦 + 1) < (𝑓‘𝑠)))
273	269, 272	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ (𝑦 + 1))
274	239, 242, 244, 245, 273	elfzd 13452	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ (0...(𝑦 + 1)))
275	274	ralrimiva 3125	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1)))
276	238, 275	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1))))
277		ffnfv 7073	. . . . . . . . . . . 12 ⊢ (𝑓:𝑆⟶(0...(𝑦 + 1)) ↔ (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1))))
278	276, 277	sylibr 234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓:𝑆⟶(0...(𝑦 + 1)))
279	278	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)) → 𝑓:𝑆⟶(0...(𝑦 + 1))))
280	279	ss2abdv 4026	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ⊆ {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))})
281	237, 280	ssfid 9188	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin)
282	281	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin)
283		inab 4268	. . . . . . . . . 10 ⊢ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))}
284	283	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
285	98	adantrr 717	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
286	285	nn0zd 12531	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ)
287	286	zred 12614	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
288	125	ltp1d 12089	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 < (𝑦 + 1))
289	287, 125, 127, 128, 288	lelttrd 11308	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1))
290	287, 289	ltned 11286	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≠ (𝑦 + 1))
291	290	neneqd 2930	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
292	291	intnand 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
293		nan 829	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) → ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))) ↔ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
294	292, 293	mpbir 231	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
295	294	alrimiv 1927	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ∀𝑓 ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
296		ab0 4339	. . . . . . . . . 10 ⊢ ({𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ∅ ↔ ∀𝑓 ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
297	295, 296	sylibr 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ∅)
298	284, 297	eqtrd 2764	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅)
299	298	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅)
300		hashun 14323	. . . . . . 7 ⊢ (({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin ∧ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin ∧ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
301	228, 282, 299, 300	syl3anc 1373	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
302		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆)))
303		simplr 768	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℕ0)
304		1nn0 12434	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
305	304	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℕ0)
306	303, 305	nn0addcld 12483	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (𝑦 + 1) ∈ ℕ0)
307	35	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑆 ∈ Fin)
308	63	ad2antrr 726	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑆 ≠ ∅)
309		eqid 2729	. . . . . . . . 9 ⊢ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}
310	306, 307, 308, 309	sticksstones21 42148	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
311	302, 310	oveq12d 7387	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))))
312	303	nn0cnd 12481	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℂ)
313		1cnd 11145	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℂ)
314	71	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℂ)
315	312, 313, 314	ppncand 11549	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + 1) + ((♯‘𝑆) − 1)) = (𝑦 + (♯‘𝑆)))
316	315	oveq1d 7384	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1)))
317	316	oveq2d 7385	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))))
318	82	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℕ0)
319	303, 318	nn0addcld 12483	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (𝑦 + (♯‘𝑆)) ∈ ℕ0)
320	318	nn0zd 12531	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℤ)
321		bcpasc 14262	. . . . . . . . . 10 ⊢ (((𝑦 + (♯‘𝑆)) ∈ ℕ0 ∧ (♯‘𝑆) ∈ ℤ) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
322	319, 320, 321	syl2anc 584	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
323	317, 322	eqtrd 2764	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
324	312, 314, 313	add32d 11378	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + (♯‘𝑆)) + 1) = ((𝑦 + 1) + (♯‘𝑆)))
325	324	oveq1d 7384	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
326	323, 325	eqtrd 2764	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
327	311, 326	eqtrd 2764	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
328	301, 327	eqtrd 2764	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
329	150, 328	eqtrd 2764	. . . 4 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
330	11, 18, 25, 32, 92, 329	nn0indd 12607	. . 3 ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
331	4, 330	mpdan 687	. 2 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
332	3, 331	eqtrd 2764	1 ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847  ∀wal 1538   = wceq 1540   ∈ wcel 2109  {cab 2707   ≠ wne 2925  ∀wral 3044   ∖ cdif 3908   ∪ cun 3909   ∩ cin 3910   ⊆ wss 3911  ∅c0 4292  𝒫 cpw 4559  {csn 4585   class class class wbr 5102   × cxp 5629   Fn wfn 6494  ⟶wf 6495  ‘cfv 6499  (class class class)co 7369  Fincfn 8895  ℂcc 11042  ℝcr 11043  0cc0 11044  1c1 11045   + caddc 11047   < clt 11184   ≤ cle 11185   − cmin 11381  ℕcn 12162  ℕ₀cn0 12418  ℤcz 12505  ...cfz 13444  Ccbc 14243  ♯chash 14271  Σcsu 15628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-rep 5229  ax-sep 5246  ax-nul 5256  ax-pow 5315  ax-pr 5382  ax-un 7691  ax-inf2 9570  ax-cnex 11100  ax-resscn 11101  ax-1cn 11102  ax-icn 11103  ax-addcl 11104  ax-addrcl 11105  ax-mulcl 11106  ax-mulrcl 11107  ax-mulcom 11108  ax-addass 11109  ax-mulass 11110  ax-distr 11111  ax-i2m1 11112  ax-1ne0 11113  ax-1rid 11114  ax-rnegex 11115  ax-rrecex 11116  ax-cnre 11117  ax-pre-lttri 11118  ax-pre-lttrn 11119  ax-pre-ltadd 11120  ax-pre-mulgt0 11121  ax-pre-sup 11122

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-nel 3030  df-ral 3045  df-rex 3054  df-rmo 3351  df-reu 3352  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4485  df-pw 4561  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-int 4907  df-iun 4953  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5526  df-eprel 5531  df-po 5539  df-so 5540  df-fr 5584  df-se 5585  df-we 5586  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6262  df-ord 6323  df-on 6324  df-lim 6325  df-suc 6326  df-iota 6452  df-fun 6501  df-fn 6502  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506  df-fv 6507  df-isom 6508  df-riota 7326  df-ov 7372  df-oprab 7373  df-mpo 7374  df-om 7823  df-1st 7947  df-2nd 7948  df-frecs 8237  df-wrecs 8268  df-recs 8317  df-rdg 8355  df-1o 8411  df-oadd 8415  df-er 8648  df-en 8896  df-dom 8897  df-sdom 8898  df-fin 8899  df-sup 9369  df-inf 9370  df-oi 9439  df-dju 9830  df-card 9868  df-pnf 11186  df-mnf 11187  df-xr 11188  df-ltxr 11189  df-le 11190  df-sub 11383  df-neg 11384  df-div 11812  df-nn 12163  df-2 12225  df-3 12226  df-n0 12419  df-z 12506  df-uz 12770  df-rp 12928  df-ico 13288  df-fz 13445  df-fzo 13592  df-seq 13943  df-exp 14003  df-fac 14215  df-bc 14244  df-hash 14272  df-cj 15041  df-re 15042  df-im 15043  df-sqrt 15177  df-abs 15178  df-clim 15430  df-sum 15629

This theorem is referenced by:  sticksstones23  42150