Theorem sticksstones22 42963

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 6885	. 2 ⊢ (𝜑 → (♯‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}))
4		sticksstones22.1	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
5		breq2 5113	. . . . . . . 8 ⊢ (𝑥 = 0 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0))
6	5	anbi2d 641	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)))
7	6	abbidv 2829	. . . . . 6 ⊢ (𝑥 = 0 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)})
8	7	fveq2d 6885	. . . . 5 ⊢ (𝑥 = 0 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}))
9		oveq1 7417	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 + (♯‘𝑆)) = (0 + (♯‘𝑆)))
10	9	oveq1d 7425	. . . . 5 ⊢ (𝑥 = 0 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
11	8, 10	eqeq12d 2779	. . . 4 ⊢ (𝑥 = 0 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆))))
12		breq2 5113	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
13	12	anbi2d 641	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)))
14	13	abbidv 2829	. . . . . 6 ⊢ (𝑥 = 𝑦 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)})
15	14	fveq2d 6885	. . . . 5 ⊢ (𝑥 = 𝑦 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}))
16		oveq1 7417	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 + (♯‘𝑆)) = (𝑦 + (♯‘𝑆)))
17	16	oveq1d 7425	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆)))
18	15, 17	eqeq12d 2779	. . . 4 ⊢ (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))))
19		breq2 5113	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)))
20	19	anbi2d 641	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
21	20	abbidv 2829	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))})
22	21	fveq2d 6885	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}))
23		oveq1 7417	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 + (♯‘𝑆)) = ((𝑦 + 1) + (♯‘𝑆)))
24	23	oveq1d 7425	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
25	22, 24	eqeq12d 2779	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆))))
26		breq2 5113	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁))
27	26	anbi2d 641	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)))
28	27	abbidv 2829	. . . . . 6 ⊢ (𝑥 = 𝑁 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)})
29	28	fveq2d 6885	. . . . 5 ⊢ (𝑥 = 𝑁 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}))
30		oveq1 7417	. . . . . 6 ⊢ (𝑥 = 𝑁 → (𝑥 + (♯‘𝑆)) = (𝑁 + (♯‘𝑆)))
31	30	oveq1d 7425	. . . . 5 ⊢ (𝑥 = 𝑁 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
32	29, 31	eqeq12d 2779	. . . 4 ⊢ (𝑥 = 𝑁 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆))))
33		simprl 782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 𝑓:𝑆⟶ℕ0)
34		simprr 784	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)
35		sticksstones22.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ∈ Fin)
36	35	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → 𝑆 ∈ Fin)
37		simpr 489	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → 𝑓:𝑆⟶ℕ0)
38	37	ffvelcdmda 7079	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
39	36, 38	fsumnn0cl 15792	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
40	33, 39	syldan 602	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
41	40	nn0ge0d 12572	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 0 ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
42		0red 11215	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 0 ∈ ℝ)
43	40	nn0red 12570	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
44	42, 43	lenltd 11360	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (0 ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ↔ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0))
45	41, 44	mpbid 235	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0)
46	34, 45	jca 520	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0 ∧ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0))
47	43, 42	eqleltd 11358	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0 ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0 ∧ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0)))
48	46, 47	mpbird 260	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)
49	33, 48	jca 520	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0))
50	49	ex 417	. . . . . . . 8 ⊢ (𝜑 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)))
51		simprl 782	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 𝑓:𝑆⟶ℕ0)
52		simprr 784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)
53		0red 11215	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 0 ∈ ℝ)
54	53	leidd 11784	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 0 ≤ 0)
55	52, 54	eqbrtrd 5133	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)
56	51, 55	jca 520	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0))
57	56	ex 417	. . . . . . . 8 ⊢ (𝜑 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)))
58	50, 57	impbid 215	. . . . . . 7 ⊢ (𝜑 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)))
59	58	abbidv 2829	. . . . . 6 ⊢ (𝜑 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)})
60	59	fveq2d 6885	. . . . 5 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}))
61		0nn0 12523	. . . . . . . 8 ⊢ 0 ∈ ℕ0
62	61	a1i 11	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℕ0)
63		sticksstones22.3	. . . . . . 7 ⊢ (𝜑 → 𝑆 ≠ ∅)
64		eqid 2763	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}
65	62, 35, 63, 64	sticksstones21 42962	. . . . . 6 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}) = ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
66		hashnncl 14407	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ Fin → ((♯‘𝑆) ∈ ℕ ↔ 𝑆 ≠ ∅))
67	35, 66	syl 18	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((♯‘𝑆) ∈ ℕ ↔ 𝑆 ≠ ∅))
68	67	bicomd 226	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆 ≠ ∅ ↔ (♯‘𝑆) ∈ ℕ))
69	68	biimpd 232	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ≠ ∅ → (♯‘𝑆) ∈ ℕ))
70	63, 69	mpd 16	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ)
71	70	nncnd 12253	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑆) ∈ ℂ)
72		1cnd 11206	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
73	71, 72	subcld 11573	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑆) − 1) ∈ ℂ)
74	73	addlidd 11415	. . . . . . . . 9 ⊢ (𝜑 → (0 + ((♯‘𝑆) − 1)) = ((♯‘𝑆) − 1))
75	74	oveq1d 7425	. . . . . . . 8 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)))
76		nnm1nn0 12549	. . . . . . . . . 10 ⊢ ((♯‘𝑆) ∈ ℕ → ((♯‘𝑆) − 1) ∈ ℕ0)
77	70, 76	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑆) − 1) ∈ ℕ0)
78		bcnn 14353	. . . . . . . . 9 ⊢ (((♯‘𝑆) − 1) ∈ ℕ0 → (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)) = 1)
79	77, 78	syl 18	. . . . . . . 8 ⊢ (𝜑 → (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)) = 1)
80	75, 79	eqtrd 2798	. . . . . . 7 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = 1)
81		eqidd 2764	. . . . . . 7 ⊢ (𝜑 → 1 = 1)
82	70	nnnn0d 12569	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ0)
83		bcnn 14353	. . . . . . . . . 10 ⊢ ((♯‘𝑆) ∈ ℕ0 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
84	82, 83	syl 18	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
85	84	eqcomd 2769	. . . . . . . 8 ⊢ (𝜑 → 1 = ((♯‘𝑆)C(♯‘𝑆)))
86	71	addlidd 11415	. . . . . . . . . 10 ⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
87	86	eqcomd 2769	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑆) = (0 + (♯‘𝑆)))
88	87	oveq1d 7425	. . . . . . . 8 ⊢ (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
89	85, 88	eqtrd 2798	. . . . . . 7 ⊢ (𝜑 → 1 = ((0 + (♯‘𝑆))C(♯‘𝑆)))
90	80, 81, 89	3eqtrd 2802	. . . . . 6 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
91	65, 90	eqtrd 2798	. . . . 5 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
92	60, 91	eqtrd 2798	. . . 4 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
93		simprl 782	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑓:𝑆⟶ℕ0)
94		simprr 784	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))
95	35	ad2antrr 738	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → 𝑆 ∈ Fin)
96		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → 𝑓:𝑆⟶ℕ0)
97	96	ffvelcdmda 7079	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
98	95, 97	fsumnn0cl 15792	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
99	93, 98	syldan 602	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
100	99	nn0red 12570	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
101		nn0re 12517	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℝ)
102	101	adantl 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℝ)
103	102	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℝ)
104		1red 11213	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 1 ∈ ℝ)
105	103, 104	readdcld 11242	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
106	100, 105	leloed 11357	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1) ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
107	94, 106	mpbid 235	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
108	99	nn0zd 12620	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ)
109		nn0z 12619	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℤ)
110	109	adantl 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℤ)
111	110	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℤ)
112		zleltp1 12649	. . . . . . . . . . . . . . . . 17 ⊢ ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1)))
113	112	bicomd 226	. . . . . . . . . . . . . . . 16 ⊢ ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
114	108, 111, 113	syl2anc 595	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
115	114	orbi1d 929	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)) ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
116	107, 115	mpbid 235	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
117	93, 116	jca 520	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
118		andi 1025	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ↔ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
119	118	bicomi 227	. . . . . . . . . . . 12 ⊢ (((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ↔ (𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
120	117, 119	sylibr 237	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
121	120	ex 417	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))))
122		simprl 782	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶ℕ0)
123	122, 98	syldan 602	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
124	123	nn0red 12570	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
125	102	adantr 485	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℝ)
126		1red 11213	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 1 ∈ ℝ)
127	125, 126	readdcld 11242	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑦 + 1) ∈ ℝ)
128		simprr 784	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
129	125	lep1d 12150	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ≤ (𝑦 + 1))
130	124, 125, 127, 128, 129	letrd 11371	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))
131	122, 130	jca 520	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)))
132	131	ex 417	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
133		simprl 782	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓:𝑆⟶ℕ0)
134		simprr 784	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
135	102	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑦 ∈ ℝ)
136		1red 11213	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 1 ∈ ℝ)
137	135, 136	readdcld 11242	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
138	137	leidd 11784	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑦 + 1) ≤ (𝑦 + 1))
139	134, 138	eqbrtrd 5133	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))
140	133, 139	jca 520	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)))
141	140	ex 417	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
142	132, 141	jaod 872	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
143	121, 142	impbid 215	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)) ↔ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))))
144	143	abbidv 2829	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
145		unab 4261	. . . . . . . . . 10 ⊢ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))}
146	145	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
147	146	eqcomd 2769	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
148	144, 147	eqtrd 2798	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
149	148	adantr 485	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
150	149	fveq2d 6885	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
151	35	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑆 ∈ Fin)
152		fzfid 14014	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (0...𝑦) ∈ Fin)
153	151, 152	jca 520	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin))
154		xpfi 9275	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin) → (𝑆 × (0...𝑦)) ∈ Fin)
155	153, 154	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 × (0...𝑦)) ∈ Fin)
156		pwfi 9274	. . . . . . . . . . 11 ⊢ ((𝑆 × (0...𝑦)) ∈ Fin ↔ 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
157	155, 156	sylib 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
158		fsetsspwxp 8846	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦))
159	158	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦)))
160	157, 159	ssfid 9225	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ∈ Fin)
161		ffn 6705	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝑆⟶ℕ0 → 𝑓 Fn 𝑆)
162	122, 161	syl 18	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓 Fn 𝑆)
163		0zd 12607	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ∈ ℤ)
164	110	adantr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℤ)
165	164	adantr 485	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℤ)
166	122	ffvelcdmda 7079	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℕ0)
167	166	nn0zd 12620	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℤ)
168	166	nn0ge0d 12572	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ≤ (𝑓‘𝑠))
169	128	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
170	125	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 ∈ ℝ)
171	166	nn0red 12570	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℝ)
172	171	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℝ)
173	124	adantr 485	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
174	173	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
175		simpr 489	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 < (𝑓‘𝑠))
176		simplll 786	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝜑)
177		simpllr 787	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℕ0)
178		simplrl 788	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑓:𝑆⟶ℕ0)
179	176, 177, 178	jca31 523	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0))
180		difssd 4091	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
181	35, 180	ssfid 9225	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑆 ∖ {𝑠}) ∈ Fin)
182	181	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
183	182	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
184		eldifi 4085	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 ∈ (𝑆 ∖ {𝑠}) → 𝑖 ∈ 𝑆)
185	184	adantl 486	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) → 𝑖 ∈ 𝑆)
186	97	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
187	185, 186	mpdan 699	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) → (𝑓‘𝑖) ∈ ℕ0)
188	183, 187	fsumnn0cl 15792	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
189	179, 188	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
190	189	nn0ge0d 12572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))
191		difssd 4091	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
192	95, 191	ssfid 9225	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
193	192, 187	fsumnn0cl 15792	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
194	179, 193	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
195	194	nn0red 12570	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℝ)
196	171, 195	addge01d 11806	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ↔ (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))))
197	190, 196	mpbid 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
198		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
199	179, 198	jca 520	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆))
200		nfv 1944	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑖(((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆)
201		nfcv 2925	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑖(𝑓‘𝑠)
202	95	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → 𝑆 ∈ Fin)
203	97	adantlr 727	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
204	203	nn0cnd 12571	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℂ)
205		simpr 489	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
206		fveq2 6881	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑠 → (𝑓‘𝑖) = (𝑓‘𝑠))
207	200, 201, 202, 204, 205, 206	fsumsplit1 15801	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
208	199, 207	syl 18	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
209	208	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)) = Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
210	197, 209	breqtrd 5137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
211	210	adantr 485	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
212	170, 172, 174, 175, 211	ltletrd 11374	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
213	170, 174	ltnled 11361	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑦 < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ↔ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
214	212, 213	mpbid 235	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
215	169, 214	pm2.21dd 198	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → ¬ 𝑦 < (𝑓‘𝑠))
216	215	pm2.01da 810	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ¬ 𝑦 < (𝑓‘𝑠))
217	177, 101	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℝ)
218	171, 217	lenltd 11360	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) ≤ 𝑦 ↔ ¬ 𝑦 < (𝑓‘𝑠)))
219	216, 218	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ 𝑦)
220	163, 165, 167, 168, 219	elfzd 13547	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ (0...𝑦))
221	220	ralrimiva 3157	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦))
222	162, 221	jca 520	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦)))
223		ffnfv 7114	. . . . . . . . . . . 12 ⊢ (𝑓:𝑆⟶(0...𝑦) ↔ (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦)))
224	222, 223	sylibr 237	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶(0...𝑦))
225	224	ex 417	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) → 𝑓:𝑆⟶(0...𝑦)))
226	225	ss2abdv 4019	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ⊆ {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)})
227	160, 226	ssfid 9225	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin)
228	227	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin)
229		fzfid 14014	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (0...(𝑦 + 1)) ∈ Fin)
230	151, 229	jca 520	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin))
231		xpfi 9275	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
232	230, 231	syl 18	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
233		pwfi 9274	. . . . . . . . . . 11 ⊢ ((𝑆 × (0...(𝑦 + 1))) ∈ Fin ↔ 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
234	232, 233	sylib 221	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
235		fsetsspwxp 8846	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1)))
236	235	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1))))
237	234, 236	ssfid 9225	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ∈ Fin)
238	161	ad2antrl 740	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓 Fn 𝑆)
239		0zd 12607	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 0 ∈ ℤ)
240		simpllr 787	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℕ0)
241	240	nn0zd 12620	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℤ)
242	241	peano2zd 12707	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑦 + 1) ∈ ℤ)
243	133	ffvelcdmda 7079	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℕ0)
244	243	nn0zd 12620	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℤ)
245	243	nn0ge0d 12572	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 0 ≤ (𝑓‘𝑠))
246	134	ad2antrr 738	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
247	137	ad2antrr 738	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) ∈ ℝ)
248	133	ad2antrr 738	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 𝑓:𝑆⟶ℕ0)
249		simplr 780	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 𝑠 ∈ 𝑆)
250	248, 249	ffvelcdmd 7080	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℕ0)
251	250	nn0red 12570	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℝ)
252	246, 247	eqeltrd 2863	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
253		simpr 489	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) < (𝑓‘𝑠))
254	133, 188	syldan 602	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
255	254	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
256	255	adantr 485	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
257	256	nn0ge0d 12572	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))
258	256	nn0red 12570	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℝ)
259	251, 258	addge01d 11806	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ↔ (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))))
260	257, 259	mpbid 235	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
261	133, 207	syldanl 613	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
262	261	adantr 485	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
263	262	eqcomd 2769	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)) = Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
264	260, 263	breqtrd 5137	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
265	247, 251, 252, 253, 264	ltletrd 11374	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
266	247, 265	ltned 11350	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) ≠ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
267	266	necomd 3013	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≠ (𝑦 + 1))
268	246, 267	pm2.21ddne 3042	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → ¬ (𝑦 + 1) < (𝑓‘𝑠))
269	268	pm2.01da 810	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → ¬ (𝑦 + 1) < (𝑓‘𝑠))
270	243	nn0red 12570	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℝ)
271	137	adantr 485	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑦 + 1) ∈ ℝ)
272	270, 271	lenltd 11360	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) ≤ (𝑦 + 1) ↔ ¬ (𝑦 + 1) < (𝑓‘𝑠)))
273	269, 272	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ (𝑦 + 1))
274	239, 242, 244, 245, 273	elfzd 13547	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ (0...(𝑦 + 1)))
275	274	ralrimiva 3157	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1)))
276	238, 275	jca 520	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1))))
277		ffnfv 7114	. . . . . . . . . . . 12 ⊢ (𝑓:𝑆⟶(0...(𝑦 + 1)) ↔ (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1))))
278	276, 277	sylibr 237	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓:𝑆⟶(0...(𝑦 + 1)))
279	278	ex 417	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)) → 𝑓:𝑆⟶(0...(𝑦 + 1))))
280	279	ss2abdv 4019	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ⊆ {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))})
281	237, 280	ssfid 9225	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin)
282	281	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin)
283		inab 4262	. . . . . . . . . 10 ⊢ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))}
284	283	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
285	98	adantrr 729	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
286	285	nn0zd 12620	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ)
287	286	zred 12704	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
288	125	ltp1d 12149	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 < (𝑦 + 1))
289	287, 125, 127, 128, 288	lelttrd 11372	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1))
290	287, 289	ltned 11350	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≠ (𝑦 + 1))
291	290	neneqd 2963	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
292	291	intnand 493	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
293		nan 842	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) → ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))) ↔ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
294	292, 293	mpbir 234	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
295	294	alrimiv 1957	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ∀𝑓 ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
296		ab0 4336	. . . . . . . . . 10 ⊢ ({𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ∅ ↔ ∀𝑓 ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
297	295, 296	sylibr 237	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ∅)
298	284, 297	eqtrd 2798	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅)
299	298	adantr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅)
300		hashun 14423	. . . . . . 7 ⊢ (({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin ∧ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin ∧ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
301	228, 282, 299, 300	syl3anc 1398	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
302		simpr 489	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆)))
303		simplr 780	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℕ0)
304		1nn0 12524	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
305	304	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℕ0)
306	303, 305	nn0addcld 12573	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (𝑦 + 1) ∈ ℕ0)
307	35	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑆 ∈ Fin)
308	63	ad2antrr 738	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑆 ≠ ∅)
309		eqid 2763	. . . . . . . . 9 ⊢ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}
310	306, 307, 308, 309	sticksstones21 42962	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
311	302, 310	oveq12d 7428	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))))
312	303	nn0cnd 12571	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℂ)
313		1cnd 11206	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℂ)
314	71	ad2antrr 738	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℂ)
315	312, 313, 314	ppncand 11613	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + 1) + ((♯‘𝑆) − 1)) = (𝑦 + (♯‘𝑆)))
316	315	oveq1d 7425	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1)))
317	316	oveq2d 7426	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))))
318	82	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℕ0)
319	303, 318	nn0addcld 12573	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (𝑦 + (♯‘𝑆)) ∈ ℕ0)
320	318	nn0zd 12620	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℤ)
321		bcpasc 14362	. . . . . . . . . 10 ⊢ (((𝑦 + (♯‘𝑆)) ∈ ℕ0 ∧ (♯‘𝑆) ∈ ℤ) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
322	319, 320, 321	syl2anc 595	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
323	317, 322	eqtrd 2798	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
324	312, 314, 313	add32d 11442	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + (♯‘𝑆)) + 1) = ((𝑦 + 1) + (♯‘𝑆)))
325	324	oveq1d 7425	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
326	323, 325	eqtrd 2798	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
327	311, 326	eqtrd 2798	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
328	301, 327	eqtrd 2798	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
329	150, 328	eqtrd 2798	. . . 4 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
330	11, 18, 25, 32, 92, 329	nn0indd 12697	. . 3 ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
331	4, 330	mpdan 699	. 2 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
332	3, 331	eqtrd 2798	1 ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860  ∀wal 1568   = wceq 1570   ∈ wcel 2143  {cab 2741   ≠ wne 2958  ∀wral 3079   ∖ cdif 3902   ∪ cun 3903   ∩ cin 3904   ⊆ wss 3905  ∅c0 4286  𝒫 cpw 4562  {csn 4589   class class class wbr 5109   × cxp 5659   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410  Fincfn 8939  ℂcc 11102  ℝcr 11103  0cc0 11104  1c1 11105   + caddc 11107   < clt 11247   ≤ cle 11248   − cmin 11445  ℕcn 12237  ℕ₀cn0 12508  ℤcz 12595  ...cfz 13539  Ccbc 14343  ♯chash 14371  Σcsu 15742

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5238  ax-sep 5257  ax-nul 5269  ax-pow 5336  ax-pr 5404  ax-un 7732  ax-inf2 9606  ax-cnex 11160  ax-resscn 11161  ax-1cn 11162  ax-icn 11163  ax-addcl 11164  ax-addrcl 11165  ax-mulcl 11166  ax-mulrcl 11167  ax-mulcom 11168  ax-addass 11169  ax-mulass 11170  ax-distr 11171  ax-i2m1 11172  ax-1ne0 11173  ax-1rid 11174  ax-rnegex 11175  ax-rrecex 11176  ax-cnre 11177  ax-pre-lttri 11178  ax-pre-lttrn 11179  ax-pre-ltadd 11180  ax-pre-mulgt0 11181  ax-pre-sup 11182

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-nel 3065  df-ral 3080  df-rex 3090  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4488  df-pw 4564  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-int 4913  df-iun 4958  df-br 5110  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5556  df-eprel 5561  df-po 5569  df-so 5570  df-fr 5614  df-se 5615  df-we 5616  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-pred 6302  df-ord 6363  df-on 6364  df-lim 6365  df-suc 6366  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544  df-isom 6545  df-riota 7367  df-ov 7413  df-oprab 7414  df-mpo 7415  df-om 7859  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8354  df-rdg 8393  df-1o 8449  df-oadd 8453  df-er 8690  df-en 8940  df-dom 8941  df-sdom 8942  df-fin 8943  df-sup 9398  df-inf 9399  df-oi 9468  df-dju 9892  df-card 9930  df-pnf 11249  df-mnf 11250  df-xr 11251  df-ltxr 11252  df-le 11253  df-sub 11447  df-neg 11448  df-div 11876  df-nn 12238  df-2 12307  df-3 12308  df-n0 12509  df-z 12596  df-uz 12867  df-rp 13021  df-ico 13382  df-fz 13540  df-fzo 13688  df-seq 14043  df-exp 14103  df-fac 14315  df-bc 14344  df-hash 14372  df-cj 15155  df-re 15156  df-im 15157  df-sqrt 15291  df-abs 15292  df-clim 15544  df-sum 15743

This theorem is used by:  sticksstones23  42964