Theorem sticksstones22 42169

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 6910	. 2 ⊢ (𝜑 → (♯‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}))
4		sticksstones22.1	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
5		breq2 5147	. . . . . . . 8 ⊢ (𝑥 = 0 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0))
6	5	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)))
7	6	abbidv 2808	. . . . . 6 ⊢ (𝑥 = 0 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)})
8	7	fveq2d 6910	. . . . 5 ⊢ (𝑥 = 0 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}))
9		oveq1 7438	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 + (♯‘𝑆)) = (0 + (♯‘𝑆)))
10	9	oveq1d 7446	. . . . 5 ⊢ (𝑥 = 0 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
11	8, 10	eqeq12d 2753	. . . 4 ⊢ (𝑥 = 0 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆))))
12		breq2 5147	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
13	12	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)))
14	13	abbidv 2808	. . . . . 6 ⊢ (𝑥 = 𝑦 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)})
15	14	fveq2d 6910	. . . . 5 ⊢ (𝑥 = 𝑦 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}))
16		oveq1 7438	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 + (♯‘𝑆)) = (𝑦 + (♯‘𝑆)))
17	16	oveq1d 7446	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆)))
18	15, 17	eqeq12d 2753	. . . 4 ⊢ (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))))
19		breq2 5147	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)))
20	19	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
21	20	abbidv 2808	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))})
22	21	fveq2d 6910	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}))
23		oveq1 7438	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 + (♯‘𝑆)) = ((𝑦 + 1) + (♯‘𝑆)))
24	23	oveq1d 7446	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
25	22, 24	eqeq12d 2753	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆))))
26		breq2 5147	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁))
27	26	anbi2d 630	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)))
28	27	abbidv 2808	. . . . . 6 ⊢ (𝑥 = 𝑁 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)})
29	28	fveq2d 6910	. . . . 5 ⊢ (𝑥 = 𝑁 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}))
30		oveq1 7438	. . . . . 6 ⊢ (𝑥 = 𝑁 → (𝑥 + (♯‘𝑆)) = (𝑁 + (♯‘𝑆)))
31	30	oveq1d 7446	. . . . 5 ⊢ (𝑥 = 𝑁 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
32	29, 31	eqeq12d 2753	. . . 4 ⊢ (𝑥 = 𝑁 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆))))
33		simprl 771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 𝑓:𝑆⟶ℕ0)
34		simprr 773	. . . . . . . . . . . 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 7104	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
39	36, 38	fsumnn0cl 15772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
40	33, 39	syldan 591	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
41	40	nn0ge0d 12590	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 0 ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
42		0red 11264	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 0 ∈ ℝ)
43	40	nn0red 12588	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
44	42, 43	lenltd 11407	. . . . . . . . . . . . 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 11405	. . . . . . . . . . 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 771	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 𝑓:𝑆⟶ℕ0)
52		simprr 773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)
53		0red 11264	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 0 ∈ ℝ)
54	53	leidd 11829	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 0 ≤ 0)
55	52, 54	eqbrtrd 5165	. . . . . . . . . 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 2808	. . . . . 6 ⊢ (𝜑 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)})
60	59	fveq2d 6910	. . . . 5 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}))
61		0nn0 12541	. . . . . . . 8 ⊢ 0 ∈ ℕ0
62	61	a1i 11	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℕ0)
63		sticksstones22.3	. . . . . . 7 ⊢ (𝜑 → 𝑆 ≠ ∅)
64		eqid 2737	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}
65	62, 35, 63, 64	sticksstones21 42168	. . . . . 6 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}) = ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
66		hashnncl 14405	. . . . . . . . . . . . . . . 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 12282	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑆) ∈ ℂ)
72		1cnd 11256	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
73	71, 72	subcld 11620	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑆) − 1) ∈ ℂ)
74	73	addlidd 11462	. . . . . . . . 9 ⊢ (𝜑 → (0 + ((♯‘𝑆) − 1)) = ((♯‘𝑆) − 1))
75	74	oveq1d 7446	. . . . . . . 8 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)))
76		nnm1nn0 12567	. . . . . . . . . 10 ⊢ ((♯‘𝑆) ∈ ℕ → ((♯‘𝑆) − 1) ∈ ℕ0)
77	70, 76	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑆) − 1) ∈ ℕ0)
78		bcnn 14351	. . . . . . . . 9 ⊢ (((♯‘𝑆) − 1) ∈ ℕ0 → (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)) = 1)
79	77, 78	syl 17	. . . . . . . 8 ⊢ (𝜑 → (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)) = 1)
80	75, 79	eqtrd 2777	. . . . . . 7 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = 1)
81		eqidd 2738	. . . . . . 7 ⊢ (𝜑 → 1 = 1)
82	70	nnnn0d 12587	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ0)
83		bcnn 14351	. . . . . . . . . 10 ⊢ ((♯‘𝑆) ∈ ℕ0 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
84	82, 83	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
85	84	eqcomd 2743	. . . . . . . 8 ⊢ (𝜑 → 1 = ((♯‘𝑆)C(♯‘𝑆)))
86	71	addlidd 11462	. . . . . . . . . 10 ⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
87	86	eqcomd 2743	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑆) = (0 + (♯‘𝑆)))
88	87	oveq1d 7446	. . . . . . . 8 ⊢ (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
89	85, 88	eqtrd 2777	. . . . . . 7 ⊢ (𝜑 → 1 = ((0 + (♯‘𝑆))C(♯‘𝑆)))
90	80, 81, 89	3eqtrd 2781	. . . . . 6 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
91	65, 90	eqtrd 2777	. . . . 5 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
92	60, 91	eqtrd 2777	. . . 4 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
93		simprl 771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑓:𝑆⟶ℕ0)
94		simprr 773	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))
95	35	ad2antrr 726	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → 𝑆 ∈ Fin)
96		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → 𝑓:𝑆⟶ℕ0)
97	96	ffvelcdmda 7104	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
98	95, 97	fsumnn0cl 15772	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
99	93, 98	syldan 591	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
100	99	nn0red 12588	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
101		nn0re 12535	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℝ)
102	101	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℝ)
103	102	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℝ)
104		1red 11262	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 1 ∈ ℝ)
105	103, 104	readdcld 11290	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
106	100, 105	leloed 11404	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1) ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
107	94, 106	mpbid 232	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
108	99	nn0zd 12639	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ)
109		nn0z 12638	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℤ)
110	109	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℤ)
111	110	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℤ)
112		zleltp1 12668	. . . . . . . . . . . . . . . . 17 ⊢ ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1)))
113	112	bicomd 223	. . . . . . . . . . . . . . . 16 ⊢ ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
114	108, 111, 113	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
115	114	orbi1d 917	. . . . . . . . . . . . . 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 1010	. . . . . . . . . . . . 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 771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶ℕ0)
123	122, 98	syldan 591	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
124	123	nn0red 12588	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
125	102	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℝ)
126		1red 11262	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 1 ∈ ℝ)
127	125, 126	readdcld 11290	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑦 + 1) ∈ ℝ)
128		simprr 773	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
129	125	lep1d 12199	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ≤ (𝑦 + 1))
130	124, 125, 127, 128, 129	letrd 11418	. . . . . . . . . . . . 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 771	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓:𝑆⟶ℕ0)
134		simprr 773	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
135	102	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑦 ∈ ℝ)
136		1red 11262	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 1 ∈ ℝ)
137	135, 136	readdcld 11290	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
138	137	leidd 11829	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑦 + 1) ≤ (𝑦 + 1))
139	134, 138	eqbrtrd 5165	. . . . . . . . . . . . 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 860	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
143	121, 142	impbid 212	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)) ↔ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))))
144	143	abbidv 2808	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
145		unab 4308	. . . . . . . . . 10 ⊢ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))}
146	145	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
147	146	eqcomd 2743	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
148	144, 147	eqtrd 2777	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
149	148	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
150	149	fveq2d 6910	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
151	35	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑆 ∈ Fin)
152		fzfid 14014	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (0...𝑦) ∈ Fin)
153	151, 152	jca 511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin))
154		xpfi 9358	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin) → (𝑆 × (0...𝑦)) ∈ Fin)
155	153, 154	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 × (0...𝑦)) ∈ Fin)
156		pwfi 9357	. . . . . . . . . . 11 ⊢ ((𝑆 × (0...𝑦)) ∈ Fin ↔ 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
157	155, 156	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
158		fsetsspwxp 8893	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦))
159	158	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦)))
160	157, 159	ssfid 9301	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ∈ Fin)
161		ffn 6736	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝑆⟶ℕ0 → 𝑓 Fn 𝑆)
162	122, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓 Fn 𝑆)
163		0zd 12625	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ∈ ℤ)
164	110	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℤ)
165	164	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℤ)
166	122	ffvelcdmda 7104	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℕ0)
167	166	nn0zd 12639	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℤ)
168	166	nn0ge0d 12590	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ≤ (𝑓‘𝑠))
169	128	ad2antrr 726	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
170	125	ad2antrr 726	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 ∈ ℝ)
171	166	nn0red 12588	. . . . . . . . . . . . . . . . . . . . 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 775	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝜑)
177		simpllr 776	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℕ0)
178		simplrl 777	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑓:𝑆⟶ℕ0)
179	176, 177, 178	jca31 514	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0))
180		difssd 4137	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
181	35, 180	ssfid 9301	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑆 ∖ {𝑠}) ∈ Fin)
182	181	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
183	182	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
184		eldifi 4131	. . . . . . . . . . . . . . . . . . . . . . . . . . . 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 15772	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
189	179, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
190	189	nn0ge0d 12590	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))
191		difssd 4137	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
192	95, 191	ssfid 9301	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
193	192, 187	fsumnn0cl 15772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
194	179, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
195	194	nn0red 12588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℝ)
196	171, 195	addge01d 11851	. . . . . . . . . . . . . . . . . . . . . . 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 2905	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑖(𝑓‘𝑠)
202	95	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → 𝑆 ∈ Fin)
203	97	adantlr 715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
204	203	nn0cnd 12589	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℂ)
205		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
206		fveq2 6906	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑠 → (𝑓‘𝑖) = (𝑓‘𝑠))
207	200, 201, 202, 204, 205, 206	fsumsplit1 15781	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
208	199, 207	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
209	208	eqcomd 2743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)) = Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
210	197, 209	breqtrd 5169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
211	210	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
212	170, 172, 174, 175, 211	ltletrd 11421	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
213	170, 174	ltnled 11408	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑦 < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ↔ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
214	212, 213	mpbid 232	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
215	169, 214	pm2.21dd 195	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → ¬ 𝑦 < (𝑓‘𝑠))
216	215	pm2.01da 799	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ¬ 𝑦 < (𝑓‘𝑠))
217	177, 101	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℝ)
218	171, 217	lenltd 11407	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) ≤ 𝑦 ↔ ¬ 𝑦 < (𝑓‘𝑠)))
219	216, 218	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ 𝑦)
220	163, 165, 167, 168, 219	elfzd 13555	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ (0...𝑦))
221	220	ralrimiva 3146	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦))
222	162, 221	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦)))
223		ffnfv 7139	. . . . . . . . . . . 12 ⊢ (𝑓:𝑆⟶(0...𝑦) ↔ (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦)))
224	222, 223	sylibr 234	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶(0...𝑦))
225	224	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) → 𝑓:𝑆⟶(0...𝑦)))
226	225	ss2abdv 4066	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ⊆ {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)})
227	160, 226	ssfid 9301	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin)
228	227	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin)
229		fzfid 14014	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (0...(𝑦 + 1)) ∈ Fin)
230	151, 229	jca 511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin))
231		xpfi 9358	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
232	230, 231	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
233		pwfi 9357	. . . . . . . . . . 11 ⊢ ((𝑆 × (0...(𝑦 + 1))) ∈ Fin ↔ 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
234	232, 233	sylib 218	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
235		fsetsspwxp 8893	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1)))
236	235	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1))))
237	234, 236	ssfid 9301	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ∈ Fin)
238	161	ad2antrl 728	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓 Fn 𝑆)
239		0zd 12625	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 0 ∈ ℤ)
240		simpllr 776	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℕ0)
241	240	nn0zd 12639	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℤ)
242	241	peano2zd 12725	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑦 + 1) ∈ ℤ)
243	133	ffvelcdmda 7104	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℕ0)
244	243	nn0zd 12639	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℤ)
245	243	nn0ge0d 12590	. . . . . . . . . . . . . . 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 769	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 𝑠 ∈ 𝑆)
250	248, 249	ffvelcdmd 7105	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℕ0)
251	250	nn0red 12588	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℝ)
252	246, 247	eqeltrd 2841	. . . . . . . . . . . . . . . . . . . . 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 12590	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))
258	256	nn0red 12588	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℝ)
259	251, 258	addge01d 11851	. . . . . . . . . . . . . . . . . . . . . . 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 2743	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)) = Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
264	260, 263	breqtrd 5169	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
265	247, 251, 252, 253, 264	ltletrd 11421	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
266	247, 265	ltned 11397	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) ≠ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
267	266	necomd 2996	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≠ (𝑦 + 1))
268	246, 267	pm2.21ddne 3026	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → ¬ (𝑦 + 1) < (𝑓‘𝑠))
269	268	pm2.01da 799	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → ¬ (𝑦 + 1) < (𝑓‘𝑠))
270	243	nn0red 12588	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℝ)
271	137	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑦 + 1) ∈ ℝ)
272	270, 271	lenltd 11407	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) ≤ (𝑦 + 1) ↔ ¬ (𝑦 + 1) < (𝑓‘𝑠)))
273	269, 272	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ (𝑦 + 1))
274	239, 242, 244, 245, 273	elfzd 13555	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ (0...(𝑦 + 1)))
275	274	ralrimiva 3146	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1)))
276	238, 275	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1))))
277		ffnfv 7139	. . . . . . . . . . . 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 4066	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ⊆ {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))})
281	237, 280	ssfid 9301	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin)
282	281	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin)
283		inab 4309	. . . . . . . . . 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 12639	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ)
287	286	zred 12722	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
288	125	ltp1d 12198	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 < (𝑦 + 1))
289	287, 125, 127, 128, 288	lelttrd 11419	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1))
290	287, 289	ltned 11397	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≠ (𝑦 + 1))
291	290	neneqd 2945	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
292	291	intnand 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
293		nan 830	. . . . . . . . . . . 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 4380	. . . . . . . . . 10 ⊢ ({𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ∅ ↔ ∀𝑓 ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
297	295, 296	sylibr 234	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ∅)
298	284, 297	eqtrd 2777	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅)
299	298	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅)
300		hashun 14421	. . . . . . 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 769	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℕ0)
304		1nn0 12542	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
305	304	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℕ0)
306	303, 305	nn0addcld 12591	. . . . . . . . 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 2737	. . . . . . . . 9 ⊢ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}
310	306, 307, 308, 309	sticksstones21 42168	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
311	302, 310	oveq12d 7449	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))))
312	303	nn0cnd 12589	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℂ)
313		1cnd 11256	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℂ)
314	71	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℂ)
315	312, 313, 314	ppncand 11660	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + 1) + ((♯‘𝑆) − 1)) = (𝑦 + (♯‘𝑆)))
316	315	oveq1d 7446	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1)))
317	316	oveq2d 7447	. . . . . . . . 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 12591	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (𝑦 + (♯‘𝑆)) ∈ ℕ0)
320	318	nn0zd 12639	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℤ)
321		bcpasc 14360	. . . . . . . . . 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 2777	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
324	312, 314, 313	add32d 11489	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + (♯‘𝑆)) + 1) = ((𝑦 + 1) + (♯‘𝑆)))
325	324	oveq1d 7446	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
326	323, 325	eqtrd 2777	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
327	311, 326	eqtrd 2777	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
328	301, 327	eqtrd 2777	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
329	150, 328	eqtrd 2777	. . . 4 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
330	11, 18, 25, 32, 92, 329	nn0indd 12715	. . 3 ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
331	4, 330	mpdan 687	. 2 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
332	3, 331	eqtrd 2777	1 ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848  ∀wal 1538   = wceq 1540   ∈ wcel 2108  {cab 2714   ≠ wne 2940  ∀wral 3061   ∖ cdif 3948   ∪ cun 3949   ∩ cin 3950   ⊆ wss 3951  ∅c0 4333  𝒫 cpw 4600  {csn 4626   class class class wbr 5143   × cxp 5683   Fn wfn 6556  ⟶wf 6557  ‘cfv 6561  (class class class)co 7431  Fincfn 8985  ℂcc 11153  ℝcr 11154  0cc0 11155  1c1 11156   + caddc 11158   < clt 11295   ≤ cle 11296   − cmin 11492  ℕcn 12266  ℕ₀cn0 12526  ℤcz 12613  ...cfz 13547  Ccbc 14341  ♯chash 14369  Σcsu 15722

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-er 8745  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-sup 9482  df-inf 9483  df-oi 9550  df-dju 9941  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-n0 12527  df-z 12614  df-uz 12879  df-rp 13035  df-ico 13393  df-fz 13548  df-fzo 13695  df-seq 14043  df-exp 14103  df-fac 14313  df-bc 14342  df-hash 14370  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-clim 15524  df-sum 15723

This theorem is referenced by:  sticksstones23  42170