Theorem sticksstones22 42156

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 6862	. 2 ⊢ (𝜑 → (♯‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}))
4		sticksstones22.1	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
5		breq2 5111	. . . . . . . 8 ⊢ (𝑥 = 0 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0))
6	5	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)))
7	6	abbidv 2795	. . . . . 6 ⊢ (𝑥 = 0 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)})
8	7	fveq2d 6862	. . . . 5 ⊢ (𝑥 = 0 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}))
9		oveq1 7394	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 + (♯‘𝑆)) = (0 + (♯‘𝑆)))
10	9	oveq1d 7402	. . . . 5 ⊢ (𝑥 = 0 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
11	8, 10	eqeq12d 2745	. . . 4 ⊢ (𝑥 = 0 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆))))
12		breq2 5111	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
13	12	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)))
14	13	abbidv 2795	. . . . . 6 ⊢ (𝑥 = 𝑦 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)})
15	14	fveq2d 6862	. . . . 5 ⊢ (𝑥 = 𝑦 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}))
16		oveq1 7394	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 + (♯‘𝑆)) = (𝑦 + (♯‘𝑆)))
17	16	oveq1d 7402	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆)))
18	15, 17	eqeq12d 2745	. . . 4 ⊢ (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))))
19		breq2 5111	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)))
20	19	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
21	20	abbidv 2795	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))})
22	21	fveq2d 6862	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}))
23		oveq1 7394	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 + (♯‘𝑆)) = ((𝑦 + 1) + (♯‘𝑆)))
24	23	oveq1d 7402	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
25	22, 24	eqeq12d 2745	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆))))
26		breq2 5111	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁))
27	26	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)))
28	27	abbidv 2795	. . . . . 6 ⊢ (𝑥 = 𝑁 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)})
29	28	fveq2d 6862	. . . . 5 ⊢ (𝑥 = 𝑁 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}))
30		oveq1 7394	. . . . . 6 ⊢ (𝑥 = 𝑁 → (𝑥 + (♯‘𝑆)) = (𝑁 + (♯‘𝑆)))
31	30	oveq1d 7402	. . . . 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 7056	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
39	36, 38	fsumnn0cl 15702	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
40	33, 39	syldan 591	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
41	40	nn0ge0d 12506	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 0 ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
42		0red 11177	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 0 ∈ ℝ)
43	40	nn0red 12504	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
44	42, 43	lenltd 11320	. . . . . . . . . . . . 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 11318	. . . . . . . . . . 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 11177	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 0 ∈ ℝ)
54	53	leidd 11744	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 0 ≤ 0)
55	52, 54	eqbrtrd 5129	. . . . . . . . . 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 6862	. . . . 5 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}))
61		0nn0 12457	. . . . . . . 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 42155	. . . . . 6 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}) = ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
66		hashnncl 14331	. . . . . . . . . . . . . . . 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 12202	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑆) ∈ ℂ)
72		1cnd 11169	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
73	71, 72	subcld 11533	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑆) − 1) ∈ ℂ)
74	73	addlidd 11375	. . . . . . . . 9 ⊢ (𝜑 → (0 + ((♯‘𝑆) − 1)) = ((♯‘𝑆) − 1))
75	74	oveq1d 7402	. . . . . . . 8 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)))
76		nnm1nn0 12483	. . . . . . . . . 10 ⊢ ((♯‘𝑆) ∈ ℕ → ((♯‘𝑆) − 1) ∈ ℕ0)
77	70, 76	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑆) − 1) ∈ ℕ0)
78		bcnn 14277	. . . . . . . . 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 12503	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ0)
83		bcnn 14277	. . . . . . . . . 10 ⊢ ((♯‘𝑆) ∈ ℕ0 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
84	82, 83	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
85	84	eqcomd 2735	. . . . . . . 8 ⊢ (𝜑 → 1 = ((♯‘𝑆)C(♯‘𝑆)))
86	71	addlidd 11375	. . . . . . . . . 10 ⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
87	86	eqcomd 2735	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑆) = (0 + (♯‘𝑆)))
88	87	oveq1d 7402	. . . . . . . 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 7056	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
98	95, 97	fsumnn0cl 15702	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
99	93, 98	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
100	99	nn0red 12504	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
101		nn0re 12451	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℝ)
102	101	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℝ)
103	102	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℝ)
104		1red 11175	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 1 ∈ ℝ)
105	103, 104	readdcld 11203	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
106	100, 105	leloed 11317	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1) ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
107	94, 106	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
108	99	nn0zd 12555	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ)
109		nn0z 12554	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℤ)
110	109	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℤ)
111	110	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℤ)
112		zleltp1 12584	. . . . . . . . . . . . . . . . 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 12504	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
125	102	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℝ)
126		1red 11175	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 1 ∈ ℝ)
127	125, 126	readdcld 11203	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑦 + 1) ∈ ℝ)
128		simprr 772	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
129	125	lep1d 12114	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ≤ (𝑦 + 1))
130	124, 125, 127, 128, 129	letrd 11331	. . . . . . . . . . . . 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 11175	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 1 ∈ ℝ)
137	135, 136	readdcld 11203	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
138	137	leidd 11744	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑦 + 1) ≤ (𝑦 + 1))
139	134, 138	eqbrtrd 5129	. . . . . . . . . . . . 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 4271	. . . . . . . . . 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 6862	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
151	35	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑆 ∈ Fin)
152		fzfid 13938	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (0...𝑦) ∈ Fin)
153	151, 152	jca 511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin))
154		xpfi 9269	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin) → (𝑆 × (0...𝑦)) ∈ Fin)
155	153, 154	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 × (0...𝑦)) ∈ Fin)
156		pwfi 9268	. . . . . . . . . . 11 ⊢ ((𝑆 × (0...𝑦)) ∈ Fin ↔ 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
157	155, 156	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
158		fsetsspwxp 8826	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦))
159	158	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦)))
160	157, 159	ssfid 9212	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ∈ Fin)
161		ffn 6688	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝑆⟶ℕ0 → 𝑓 Fn 𝑆)
162	122, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓 Fn 𝑆)
163		0zd 12541	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ∈ ℤ)
164	110	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℤ)
165	164	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℤ)
166	122	ffvelcdmda 7056	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℕ0)
167	166	nn0zd 12555	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℤ)
168	166	nn0ge0d 12506	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ≤ (𝑓‘𝑠))
169	128	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
170	125	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 ∈ ℝ)
171	166	nn0red 12504	. . . . . . . . . . . . . . . . . . . . 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 4100	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
181	35, 180	ssfid 9212	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑆 ∖ {𝑠}) ∈ Fin)
182	181	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
183	182	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
184		eldifi 4094	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 15702	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
189	179, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
190	189	nn0ge0d 12506	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))
191		difssd 4100	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
192	95, 191	ssfid 9212	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
193	192, 187	fsumnn0cl 15702	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
194	179, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
195	194	nn0red 12504	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℝ)
196	171, 195	addge01d 11766	. . . . . . . . . . . . . . . . . . . . . . 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 12505	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℂ)
205		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
206		fveq2 6858	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑠 → (𝑓‘𝑖) = (𝑓‘𝑠))
207	200, 201, 202, 204, 205, 206	fsumsplit1 15711	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
208	199, 207	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
209	208	eqcomd 2735	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)) = Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
210	197, 209	breqtrd 5133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
211	210	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
212	170, 172, 174, 175, 211	ltletrd 11334	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
213	170, 174	ltnled 11321	. . . . . . . . . . . . . . . . . . 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 11320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) ≤ 𝑦 ↔ ¬ 𝑦 < (𝑓‘𝑠)))
219	216, 218	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ 𝑦)
220	163, 165, 167, 168, 219	elfzd 13476	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ (0...𝑦))
221	220	ralrimiva 3125	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦))
222	162, 221	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦)))
223		ffnfv 7091	. . . . . . . . . . . 12 ⊢ (𝑓:𝑆⟶(0...𝑦) ↔ (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦)))
224	222, 223	sylibr 234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶(0...𝑦))
225	224	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) → 𝑓:𝑆⟶(0...𝑦)))
226	225	ss2abdv 4029	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ⊆ {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)})
227	160, 226	ssfid 9212	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin)
228	227	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin)
229		fzfid 13938	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (0...(𝑦 + 1)) ∈ Fin)
230	151, 229	jca 511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin))
231		xpfi 9269	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
232	230, 231	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
233		pwfi 9268	. . . . . . . . . . 11 ⊢ ((𝑆 × (0...(𝑦 + 1))) ∈ Fin ↔ 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
234	232, 233	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
235		fsetsspwxp 8826	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1)))
236	235	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1))))
237	234, 236	ssfid 9212	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ∈ Fin)
238	161	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓 Fn 𝑆)
239		0zd 12541	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 0 ∈ ℤ)
240		simpllr 775	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℕ0)
241	240	nn0zd 12555	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℤ)
242	241	peano2zd 12641	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑦 + 1) ∈ ℤ)
243	133	ffvelcdmda 7056	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℕ0)
244	243	nn0zd 12555	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℤ)
245	243	nn0ge0d 12506	. . . . . . . . . . . . . . 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 7057	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℕ0)
251	250	nn0red 12504	. . . . . . . . . . . . . . . . . . . . 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 12506	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))
258	256	nn0red 12504	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℝ)
259	251, 258	addge01d 11766	. . . . . . . . . . . . . . . . . . . . . . 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 5133	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
265	247, 251, 252, 253, 264	ltletrd 11334	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
266	247, 265	ltned 11310	. . . . . . . . . . . . . . . . . . 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 12504	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℝ)
271	137	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑦 + 1) ∈ ℝ)
272	270, 271	lenltd 11320	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) ≤ (𝑦 + 1) ↔ ¬ (𝑦 + 1) < (𝑓‘𝑠)))
273	269, 272	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ (𝑦 + 1))
274	239, 242, 244, 245, 273	elfzd 13476	. . . . . . . . . . . . . 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 7091	. . . . . . . . . . . 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 4029	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ⊆ {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))})
281	237, 280	ssfid 9212	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin)
282	281	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin)
283		inab 4272	. . . . . . . . . 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 12555	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ)
287	286	zred 12638	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
288	125	ltp1d 12113	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 < (𝑦 + 1))
289	287, 125, 127, 128, 288	lelttrd 11332	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1))
290	287, 289	ltned 11310	. . . . . . . . . . . . . 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 4343	. . . . . . . . . 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 14347	. . . . . . 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 12458	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
305	304	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℕ0)
306	303, 305	nn0addcld 12507	. . . . . . . . 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 42155	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
311	302, 310	oveq12d 7405	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))))
312	303	nn0cnd 12505	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℂ)
313		1cnd 11169	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℂ)
314	71	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℂ)
315	312, 313, 314	ppncand 11573	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + 1) + ((♯‘𝑆) − 1)) = (𝑦 + (♯‘𝑆)))
316	315	oveq1d 7402	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1)))
317	316	oveq2d 7403	. . . . . . . . 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 12507	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (𝑦 + (♯‘𝑆)) ∈ ℕ0)
320	318	nn0zd 12555	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℤ)
321		bcpasc 14286	. . . . . . . . . 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 11402	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + (♯‘𝑆)) + 1) = ((𝑦 + 1) + (♯‘𝑆)))
325	324	oveq1d 7402	. . . . . . . 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 12631	. . 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 3911   ∪ cun 3912   ∩ cin 3913   ⊆ wss 3914  ∅c0 4296  𝒫 cpw 4563  {csn 4589   class class class wbr 5107   × cxp 5636   Fn wfn 6506  ⟶wf 6507  ‘cfv 6511  (class class class)co 7387  Fincfn 8918  ℂcc 11066  ℝcr 11067  0cc0 11068  1c1 11069   + caddc 11071   < clt 11208   ≤ cle 11209   − cmin 11405  ℕcn 12186  ℕ₀cn0 12442  ℤcz 12529  ...cfz 13468  Ccbc 14267  ♯chash 14295  Σcsu 15652

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 5234  ax-sep 5251  ax-nul 5261  ax-pow 5320  ax-pr 5387  ax-un 7711  ax-inf2 9594  ax-cnex 11124  ax-resscn 11125  ax-1cn 11126  ax-icn 11127  ax-addcl 11128  ax-addrcl 11129  ax-mulcl 11130  ax-mulrcl 11131  ax-mulcom 11132  ax-addass 11133  ax-mulass 11134  ax-distr 11135  ax-i2m1 11136  ax-1ne0 11137  ax-1rid 11138  ax-rnegex 11139  ax-rrecex 11140  ax-cnre 11141  ax-pre-lttri 11142  ax-pre-lttrn 11143  ax-pre-ltadd 11144  ax-pre-mulgt0 11145  ax-pre-sup 11146

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 3354  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-int 4911  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-se 5592  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-isom 6520  df-riota 7344  df-ov 7390  df-oprab 7391  df-mpo 7392  df-om 7843  df-1st 7968  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-1o 8434  df-oadd 8438  df-er 8671  df-en 8919  df-dom 8920  df-sdom 8921  df-fin 8922  df-sup 9393  df-inf 9394  df-oi 9463  df-dju 9854  df-card 9892  df-pnf 11210  df-mnf 11211  df-xr 11212  df-ltxr 11213  df-le 11214  df-sub 11407  df-neg 11408  df-div 11836  df-nn 12187  df-2 12249  df-3 12250  df-n0 12443  df-z 12530  df-uz 12794  df-rp 12952  df-ico 13312  df-fz 13469  df-fzo 13616  df-seq 13967  df-exp 14027  df-fac 14239  df-bc 14268  df-hash 14296  df-cj 15065  df-re 15066  df-im 15067  df-sqrt 15201  df-abs 15202  df-clim 15454  df-sum 15653

This theorem is referenced by:  sticksstones23  42157