Theorem sticksstones22 40052

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 6760	. 2 ⊢ (𝜑 → (♯‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}))
4		sticksstones22.1	. . 3 ⊢ (𝜑 → 𝑁 ∈ ℕ0)
5		breq2 5074	. . . . . . . 8 ⊢ (𝑥 = 0 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0))
6	5	anbi2d 628	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)))
7	6	abbidv 2808	. . . . . 6 ⊢ (𝑥 = 0 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)})
8	7	fveq2d 6760	. . . . 5 ⊢ (𝑥 = 0 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}))
9		oveq1 7262	. . . . . 6 ⊢ (𝑥 = 0 → (𝑥 + (♯‘𝑆)) = (0 + (♯‘𝑆)))
10	9	oveq1d 7270	. . . . 5 ⊢ (𝑥 = 0 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
11	8, 10	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 0 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆))))
12		breq2 5074	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
13	12	anbi2d 628	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)))
14	13	abbidv 2808	. . . . . 6 ⊢ (𝑥 = 𝑦 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)})
15	14	fveq2d 6760	. . . . 5 ⊢ (𝑥 = 𝑦 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}))
16		oveq1 7262	. . . . . 6 ⊢ (𝑥 = 𝑦 → (𝑥 + (♯‘𝑆)) = (𝑦 + (♯‘𝑆)))
17	16	oveq1d 7270	. . . . 5 ⊢ (𝑥 = 𝑦 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆)))
18	15, 17	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))))
19		breq2 5074	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)))
20	19	anbi2d 628	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
21	20	abbidv 2808	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))})
22	21	fveq2d 6760	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}))
23		oveq1 7262	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 + (♯‘𝑆)) = ((𝑦 + 1) + (♯‘𝑆)))
24	23	oveq1d 7270	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
25	22, 24	eqeq12d 2754	. . . 4 ⊢ (𝑥 = (𝑦 + 1) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆))))
26		breq2 5074	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁))
27	26	anbi2d 628	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)))
28	27	abbidv 2808	. . . . . 6 ⊢ (𝑥 = 𝑁 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)})
29	28	fveq2d 6760	. . . . 5 ⊢ (𝑥 = 𝑁 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}))
30		oveq1 7262	. . . . . 6 ⊢ (𝑥 = 𝑁 → (𝑥 + (♯‘𝑆)) = (𝑁 + (♯‘𝑆)))
31	30	oveq1d 7270	. . . . 5 ⊢ (𝑥 = 𝑁 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
32	29, 31	eqeq12d 2754	. . . 4 ⊢ (𝑥 = 𝑁 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆))))
33		simprl 767	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 𝑓:𝑆⟶ℕ0)
34		simprr 769	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)
35		sticksstones22.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑆 ∈ Fin)
36	35	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → 𝑆 ∈ Fin)
37		simpr 484	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → 𝑓:𝑆⟶ℕ0)
38	37	ffvelrnda 6943	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
39	36, 38	fsumnn0cl 15376	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
40	33, 39	syldan 590	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
41	40	nn0ge0d 12226	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 0 ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
42		0red 10909	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → 0 ∈ ℝ)
43	40	nn0red 12224	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
44	42, 43	lenltd 11051	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (0 ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ↔ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0))
45	41, 44	mpbid 231	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0)
46	34, 45	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0 ∧ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0))
47	43, 42	eqleltd 11049	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0 ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0 ∧ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < 0)))
48	46, 47	mpbird 256	. . . . . . . . . 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 767	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 𝑓:𝑆⟶ℕ0)
52		simprr 769	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)
53		0red 10909	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 0 ∈ ℝ)
54	53	leidd 11471	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)) → 0 ≤ 0)
55	52, 54	eqbrtrd 5092	. . . . . . . . . 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 211	. . . . . . 7 ⊢ (𝜑 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)))
59	58	abbidv 2808	. . . . . 6 ⊢ (𝜑 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)})
60	59	fveq2d 6760	. . . . 5 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}))
61		0nn0 12178	. . . . . . . 8 ⊢ 0 ∈ ℕ0
62	61	a1i 11	. . . . . . 7 ⊢ (𝜑 → 0 ∈ ℕ0)
63		sticksstones22.3	. . . . . . 7 ⊢ (𝜑 → 𝑆 ≠ ∅)
64		eqid 2738	. . . . . . 7 ⊢ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}
65	62, 35, 63, 64	sticksstones21 40051	. . . . . 6 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}) = ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
66		hashnncl 14009	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∈ Fin → ((♯‘𝑆) ∈ ℕ ↔ 𝑆 ≠ ∅))
67	35, 66	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((♯‘𝑆) ∈ ℕ ↔ 𝑆 ≠ ∅))
68	67	bicomd 222	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑆 ≠ ∅ ↔ (♯‘𝑆) ∈ ℕ))
69	68	biimpd 228	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆 ≠ ∅ → (♯‘𝑆) ∈ ℕ))
70	63, 69	mpd 15	. . . . . . . . . . . 12 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ)
71	70	nncnd 11919	. . . . . . . . . . 11 ⊢ (𝜑 → (♯‘𝑆) ∈ ℂ)
72		1cnd 10901	. . . . . . . . . . 11 ⊢ (𝜑 → 1 ∈ ℂ)
73	71, 72	subcld 11262	. . . . . . . . . 10 ⊢ (𝜑 → ((♯‘𝑆) − 1) ∈ ℂ)
74	73	addid2d 11106	. . . . . . . . 9 ⊢ (𝜑 → (0 + ((♯‘𝑆) − 1)) = ((♯‘𝑆) − 1))
75	74	oveq1d 7270	. . . . . . . 8 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)))
76		nnm1nn0 12204	. . . . . . . . . 10 ⊢ ((♯‘𝑆) ∈ ℕ → ((♯‘𝑆) − 1) ∈ ℕ0)
77	70, 76	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑆) − 1) ∈ ℕ0)
78		bcnn 13954	. . . . . . . . 9 ⊢ (((♯‘𝑆) − 1) ∈ ℕ0 → (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)) = 1)
79	77, 78	syl 17	. . . . . . . 8 ⊢ (𝜑 → (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)) = 1)
80	75, 79	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = 1)
81		eqidd 2739	. . . . . . 7 ⊢ (𝜑 → 1 = 1)
82	70	nnnn0d 12223	. . . . . . . . . 10 ⊢ (𝜑 → (♯‘𝑆) ∈ ℕ0)
83		bcnn 13954	. . . . . . . . . 10 ⊢ ((♯‘𝑆) ∈ ℕ0 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
84	82, 83	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
85	84	eqcomd 2744	. . . . . . . 8 ⊢ (𝜑 → 1 = ((♯‘𝑆)C(♯‘𝑆)))
86	71	addid2d 11106	. . . . . . . . . 10 ⊢ (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
87	86	eqcomd 2744	. . . . . . . . 9 ⊢ (𝜑 → (♯‘𝑆) = (0 + (♯‘𝑆)))
88	87	oveq1d 7270	. . . . . . . 8 ⊢ (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
89	85, 88	eqtrd 2778	. . . . . . 7 ⊢ (𝜑 → 1 = ((0 + (♯‘𝑆))C(♯‘𝑆)))
90	80, 81, 89	3eqtrd 2782	. . . . . 6 ⊢ (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
91	65, 90	eqtrd 2778	. . . . 5 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
92	60, 91	eqtrd 2778	. . . 4 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
93		simprl 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑓:𝑆⟶ℕ0)
94		simprr 769	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))
95	35	ad2antrr 722	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → 𝑆 ∈ Fin)
96		simpr 484	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → 𝑓:𝑆⟶ℕ0)
97	96	ffvelrnda 6943	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
98	95, 97	fsumnn0cl 15376	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
99	93, 98	syldan 590	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
100	99	nn0red 12224	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
101		nn0re 12172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℝ)
102	101	adantl 481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℝ)
103	102	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℝ)
104		1red 10907	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 1 ∈ ℝ)
105	103, 104	readdcld 10935	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
106	100, 105	leloed 11048	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1) ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
107	94, 106	mpbid 231	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
108	99	nn0zd 12353	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ)
109		nn0z 12273	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ ℕ0 → 𝑦 ∈ ℤ)
110	109	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑦 ∈ ℤ)
111	110	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℤ)
112		zleltp1 12301	. . . . . . . . . . . . . . . . 17 ⊢ ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1)))
113	112	bicomd 222	. . . . . . . . . . . . . . . 16 ⊢ ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
114	108, 111, 113	syl2anc 583	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ↔ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
115	114	orbi1d 913	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → ((Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1) ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)) ↔ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
116	107, 115	mpbid 231	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
117	93, 116	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
118		andi 1004	. . . . . . . . . . . . 13 ⊢ ((𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ↔ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
119	118	bicomi 223	. . . . . . . . . . . 12 ⊢ (((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ↔ (𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦 ∨ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
120	117, 119	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
121	120	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))))
122		simprl 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶ℕ0)
123	122, 98	syldan 590	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
124	123	nn0red 12224	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
125	102	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℝ)
126		1red 10907	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 1 ∈ ℝ)
127	125, 126	readdcld 10935	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑦 + 1) ∈ ℝ)
128		simprr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
129	125	lep1d 11836	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ≤ (𝑦 + 1))
130	124, 125, 127, 128, 129	letrd 11062	. . . . . . . . . . . . 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 767	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓:𝑆⟶ℕ0)
134		simprr 769	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
135	102	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑦 ∈ ℝ)
136		1red 10907	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 1 ∈ ℝ)
137	135, 136	readdcld 10935	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
138	137	leidd 11471	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑦 + 1) ≤ (𝑦 + 1))
139	134, 138	eqbrtrd 5092	. . . . . . . . . . . . 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 855	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))))
143	121, 142	impbid 211	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1)) ↔ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))))
144	143	abbidv 2808	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
145		unab 4229	. . . . . . . . . 10 ⊢ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))}
146	145	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
147	146	eqcomd 2744	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
148	144, 147	eqtrd 2778	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
149	148	adantr 480	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}))
150	149	fveq2d 6760	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
151	35	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝑆 ∈ Fin)
152		fzfid 13621	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (0...𝑦) ∈ Fin)
153	151, 152	jca 511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin))
154		xpfi 9015	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin) → (𝑆 × (0...𝑦)) ∈ Fin)
155	153, 154	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 × (0...𝑦)) ∈ Fin)
156		pwfi 8923	. . . . . . . . . . 11 ⊢ ((𝑆 × (0...𝑦)) ∈ Fin ↔ 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
157	155, 156	sylib 217	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
158		fsetsspwxp 8599	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦))
159	158	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦)))
160	157, 159	ssfid 8971	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)} ∈ Fin)
161		ffn 6584	. . . . . . . . . . . . . 14 ⊢ (𝑓:𝑆⟶ℕ0 → 𝑓 Fn 𝑆)
162	122, 161	syl 17	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓 Fn 𝑆)
163		0zd 12261	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ∈ ℤ)
164	110	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 ∈ ℤ)
165	164	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℤ)
166	122	ffvelrnda 6943	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℕ0)
167	166	nn0zd 12353	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℤ)
168	166	nn0ge0d 12226	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ≤ (𝑓‘𝑠))
169	128	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
170	125	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 ∈ ℝ)
171	166	nn0red 12224	. . . . . . . . . . . . . . . . . . . . 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 771	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝜑)
177		simpllr 772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℕ0)
178		simplrl 773	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑓:𝑆⟶ℕ0)
179	176, 177, 178	jca31 514	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0))
180		difssd 4063	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝜑 → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
181	35, 180	ssfid 8971	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝜑 → (𝑆 ∖ {𝑠}) ∈ Fin)
182	181	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
183	182	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
184		eldifi 4057	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑖 ∈ (𝑆 ∖ {𝑠}) → 𝑖 ∈ 𝑆)
185	184	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) → 𝑖 ∈ 𝑆)
186	97	adantlr 711	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
187	185, 186	mpdan 683	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) → (𝑓‘𝑖) ∈ ℕ0)
188	183, 187	fsumnn0cl 15376	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
189	179, 188	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
190	189	nn0ge0d 12226	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))
191		difssd 4063	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
192	95, 191	ssfid 8971	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
193	192, 187	fsumnn0cl 15376	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
194	179, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℕ0)
195	194	nn0red 12224	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℝ)
196	171, 195	addge01d 11493	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ↔ (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))))
197	190, 196	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
198		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
199	179, 198	jca 511	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆))
200		nfv 1918	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑖(((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆)
201		nfcv 2906	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ Ⅎ𝑖(𝑓‘𝑠)
202	95	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → 𝑆 ∈ Fin)
203	97	adantlr 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℕ0)
204	203	nn0cnd 12225	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) ∧ 𝑖 ∈ 𝑆) → (𝑓‘𝑖) ∈ ℂ)
205		simpr 484	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑆)
206		fveq2 6756	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 = 𝑠 → (𝑓‘𝑖) = (𝑓‘𝑠))
207	200, 201, 202, 204, 205, 206	fsumsplit1 15385	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
208	199, 207	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
209	208	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)) = Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
210	197, 209	breqtrd 5096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
211	210	adantr 480	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
212	170, 172, 174, 175, 211	ltletrd 11065	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → 𝑦 < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
213	170, 174	ltnled 11052	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → (𝑦 < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ↔ ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦))
214	212, 213	mpbid 231	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)
215	169, 214	pm2.21dd 194	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) ∧ 𝑦 < (𝑓‘𝑠)) → ¬ 𝑦 < (𝑓‘𝑠))
216	215	pm2.01da 795	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ¬ 𝑦 < (𝑓‘𝑠))
217	177, 101	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℝ)
218	171, 217	lenltd 11051	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) ≤ 𝑦 ↔ ¬ 𝑦 < (𝑓‘𝑠)))
219	216, 218	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ 𝑦)
220	163, 165, 167, 168, 219	elfzd 13176	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ (0...𝑦))
221	220	ralrimiva 3107	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦))
222	162, 221	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦)))
223		ffnfv 6974	. . . . . . . . . . . 12 ⊢ (𝑓:𝑆⟶(0...𝑦) ↔ (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...𝑦)))
224	222, 223	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶(0...𝑦))
225	224	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) → 𝑓:𝑆⟶(0...𝑦)))
226	225	ss2abdv 3993	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ⊆ {𝑓 ∣ 𝑓:𝑆⟶(0...𝑦)})
227	160, 226	ssfid 8971	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin)
228	227	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin)
229		fzfid 13621	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (0...(𝑦 + 1)) ∈ Fin)
230	151, 229	jca 511	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin))
231		xpfi 9015	. . . . . . . . . . . 12 ⊢ ((𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
232	230, 231	syl 17	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
233		pwfi 8923	. . . . . . . . . . 11 ⊢ ((𝑆 × (0...(𝑦 + 1))) ∈ Fin ↔ 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
234	232, 233	sylib 217	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
235		fsetsspwxp 8599	. . . . . . . . . . 11 ⊢ {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1)))
236	235	a1i 11	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1))))
237	234, 236	ssfid 8971	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))} ∈ Fin)
238	161	ad2antrl 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓 Fn 𝑆)
239		0zd 12261	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 0 ∈ ℤ)
240		simpllr 772	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℕ0)
241	240	nn0zd 12353	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 𝑦 ∈ ℤ)
242	241	peano2zd 12358	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑦 + 1) ∈ ℤ)
243	133	ffvelrnda 6943	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℕ0)
244	243	nn0zd 12353	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℤ)
245	243	nn0ge0d 12226	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → 0 ≤ (𝑓‘𝑠))
246	134	ad2antrr 722	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
247	137	ad2antrr 722	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) ∈ ℝ)
248	133	ad2antrr 722	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 𝑓:𝑆⟶ℕ0)
249		simplr 765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 𝑠 ∈ 𝑆)
250	248, 249	ffvelrnd 6944	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℕ0)
251	250	nn0red 12224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ∈ ℝ)
252	246, 247	eqeltrd 2839	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
253		simpr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) < (𝑓‘𝑠))
254	133, 188	syldan 590	. . . . . . . . . . . . . . . . . . . . . . . . . 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 12226	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))
258	256	nn0red 12224	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ∈ ℝ)
259	251, 258	addge01d 11493	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖) ↔ (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖))))
260	257, 259	mpbid 231	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
261	133, 207	syldanl 601	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
262	261	adantr 480	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)))
263	262	eqcomd 2744	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → ((𝑓‘𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓‘𝑖)) = Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
264	260, 263	breqtrd 5096	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑓‘𝑠) ≤ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
265	247, 251, 252, 253, 264	ltletrd 11065	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) < Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
266	247, 265	ltned 11041	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → (𝑦 + 1) ≠ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖))
267	266	necomd 2998	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≠ (𝑦 + 1))
268	246, 267	pm2.21ddne 3028	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) ∧ (𝑦 + 1) < (𝑓‘𝑠)) → ¬ (𝑦 + 1) < (𝑓‘𝑠))
269	268	pm2.01da 795	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → ¬ (𝑦 + 1) < (𝑓‘𝑠))
270	243	nn0red 12224	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ ℝ)
271	137	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑦 + 1) ∈ ℝ)
272	270, 271	lenltd 11051	. . . . . . . . . . . . . . . 16 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → ((𝑓‘𝑠) ≤ (𝑦 + 1) ↔ ¬ (𝑦 + 1) < (𝑓‘𝑠)))
273	269, 272	mpbird 256	. . . . . . . . . . . . . . 15 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ≤ (𝑦 + 1))
274	239, 242, 244, 245, 273	elfzd 13176	. . . . . . . . . . . . . 14 ⊢ ((((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) ∧ 𝑠 ∈ 𝑆) → (𝑓‘𝑠) ∈ (0...(𝑦 + 1)))
275	274	ralrimiva 3107	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1)))
276	238, 275	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1))))
277		ffnfv 6974	. . . . . . . . . . . 12 ⊢ (𝑓:𝑆⟶(0...(𝑦 + 1)) ↔ (𝑓 Fn 𝑆 ∧ ∀𝑠 ∈ 𝑆 (𝑓‘𝑠) ∈ (0...(𝑦 + 1))))
278	276, 277	sylibr 233	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))) → 𝑓:𝑆⟶(0...(𝑦 + 1)))
279	278	ex 412	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)) → 𝑓:𝑆⟶(0...(𝑦 + 1))))
280	279	ss2abdv 3993	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ⊆ {𝑓 ∣ 𝑓:𝑆⟶(0...(𝑦 + 1))})
281	237, 280	ssfid 8971	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin)
282	281	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin)
283		inab 4230	. . . . . . . . . 10 ⊢ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))}
284	283	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))})
285	98	adantrr 713	. . . . . . . . . . . . . . . . 17 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℕ0)
286	285	nn0zd 12353	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℤ)
287	286	zred 12355	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ∈ ℝ)
288	125	ltp1d 11835	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → 𝑦 < (𝑦 + 1))
289	287, 125, 127, 128, 288	lelttrd 11063	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) < (𝑦 + 1))
290	287, 289	ltned 11041	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≠ (𝑦 + 1))
291	290	neneqd 2947	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))
292	291	intnand 488	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))
293		nan 826	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) → ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))) ↔ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)) → ¬ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
294	292, 293	mpbir 230	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
295	294	alrimiv 1931	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ∀𝑓 ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
296		ab0 4305	. . . . . . . . . 10 ⊢ ({𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ∅ ↔ ∀𝑓 ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))))
297	295, 296	sylibr 233	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1)))} = ∅)
298	284, 297	eqtrd 2778	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅)
299	298	adantr 480	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅)
300		hashun 14025	. . . . . . 7 ⊢ (({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∈ Fin ∧ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} ∈ Fin ∧ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = ∅) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
301	228, 282, 299, 300	syl3anc 1369	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})))
302		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆)))
303		simplr 765	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℕ0)
304		1nn0 12179	. . . . . . . . . . 11 ⊢ 1 ∈ ℕ0
305	304	a1i 11	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℕ0)
306	303, 305	nn0addcld 12227	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (𝑦 + 1) ∈ ℕ0)
307	35	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑆 ∈ Fin)
308	63	ad2antrr 722	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑆 ≠ ∅)
309		eqid 2738	. . . . . . . . 9 ⊢ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}
310	306, 307, 308, 309	sticksstones21 40051	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))}) = (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
311	302, 310	oveq12d 7273	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))))
312	303	nn0cnd 12225	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℂ)
313		1cnd 10901	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℂ)
314	71	ad2antrr 722	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℂ)
315	312, 313, 314	ppncand 11302	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + 1) + ((♯‘𝑆) − 1)) = (𝑦 + (♯‘𝑆)))
316	315	oveq1d 7270	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1)))
317	316	oveq2d 7271	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))))
318	82	ad2antrr 722	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℕ0)
319	303, 318	nn0addcld 12227	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (𝑦 + (♯‘𝑆)) ∈ ℕ0)
320	318	nn0zd 12353	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℤ)
321		bcpasc 13963	. . . . . . . . . 10 ⊢ (((𝑦 + (♯‘𝑆)) ∈ ℕ0 ∧ (♯‘𝑆) ∈ ℤ) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
322	319, 320, 321	syl2anc 583	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
323	317, 322	eqtrd 2778	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
324	312, 314, 313	add32d 11132	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + (♯‘𝑆)) + 1) = ((𝑦 + 1) + (♯‘𝑆)))
325	324	oveq1d 7270	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
326	323, 325	eqtrd 2778	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
327	311, 326	eqtrd 2778	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
328	301, 327	eqtrd 2778	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) = (𝑦 + 1))})) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
329	150, 328	eqtrd 2778	. . . 4 ⊢ (((𝜑 ∧ 𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
330	11, 18, 25, 32, 92, 329	nn0indd 12347	. . 3 ⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
331	4, 330	mpdan 683	. 2 ⊢ (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖 ∈ 𝑆 (𝑓‘𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
332	3, 331	eqtrd 2778	1 ⊢ (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∨ wo 843  ∀wal 1537   = wceq 1539   ∈ wcel 2108  {cab 2715   ≠ wne 2942  ∀wral 3063   ∖ cdif 3880   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530  {csn 4558   class class class wbr 5070   × cxp 5578   Fn wfn 6413  ⟶wf 6414  ‘cfv 6418  (class class class)co 7255  Fincfn 8691  ℂcc 10800  ℝcr 10801  0cc0 10802  1c1 10803   + caddc 10805   < clt 10940   ≤ cle 10941   − cmin 11135  ℕcn 11903  ℕ₀cn0 12163  ℤcz 12249  ...cfz 13168  Ccbc 13944  ♯chash 13972  Σcsu 15325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-rep 5205  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-inf2 9329  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879  ax-pre-sup 10880

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-int 4877  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-se 5536  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-isom 6427  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-1o 8267  df-oadd 8271  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-fin 8695  df-sup 9131  df-inf 9132  df-oi 9199  df-dju 9590  df-card 9628  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-div 11563  df-nn 11904  df-2 11966  df-3 11967  df-n0 12164  df-z 12250  df-uz 12512  df-rp 12660  df-ico 13014  df-fz 13169  df-fzo 13312  df-seq 13650  df-exp 13711  df-fac 13916  df-bc 13945  df-hash 13973  df-cj 14738  df-re 14739  df-im 14740  df-sqrt 14874  df-abs 14875  df-clim 15125  df-sum 15326

This theorem is referenced by: (None)