Metamath Proof Explorer

Theorem sticksstones16

Description: Sticks and stones with collapsed definitions for positive integers. (Contributed by metakunt, 20-Oct-2024)

Ref Expression
Hypotheses sticksstones16.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones16.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
sticksstones16.3 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
Assertion sticksstones16 ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + ( 𝐾 − 1 ) ) C ( 𝐾 − 1 ) ) )

Proof

Step Hyp Ref Expression
1 sticksstones16.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones16.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ )
3 sticksstones16.3 ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
4 fveq2 ⊢ ( 𝑖 = 𝑗 → ( 𝑔 ‘ 𝑖 ) = ( 𝑔 ‘ 𝑗 ) )
5 4 cbvsumv ⊢ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = Σ 𝑗 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑗 )
6 5 eqeq1i ⊢ ( Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ↔ Σ 𝑗 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑗 ) = 𝑁 )
7 6 anbi2i ⊢ ( ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) ↔ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) )
8 7 abbii ⊢ { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) } = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) }
9 3 8 eqtri ⊢ 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) }
10 9 a1i ⊢ ( 𝜑 → 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) } )
11 nfv ⊢ Ⅎ 𝑔 𝜑
12 2 nncnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
13 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
14 12 13 npcand ⊢ ( 𝜑 → ( ( 𝐾 − 1 ) + 1 ) = 𝐾 )
15 14 eqcomd ⊢ ( 𝜑 → 𝐾 = ( ( 𝐾 − 1 ) + 1 ) )
16 15 oveq2d ⊢ ( 𝜑 → ( 1 ... 𝐾 ) = ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) )
17 16 feq2d ⊢ ( 𝜑 → ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ↔ 𝑔 : ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ⟶ ℕ0 ) )
18 16 sumeq1d ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑗 ) = Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) )
19 18 eqeq1d ⊢ ( 𝜑 → ( Σ 𝑗 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ↔ Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) )
20 17 19 anbi12d ⊢ ( 𝜑 → ( ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) ↔ ( 𝑔 : ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) ) )
21 11 20 abbid ⊢ ( 𝜑 → { 𝑔 ∣ ( 𝑔 : ( 1 ... 𝐾 ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... 𝐾 ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) } = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) } )
22 10 21 eqtrd ⊢ ( 𝜑 → 𝐴 = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) } )
23 22 fveq2d ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) } ) )
24 nnm1nn0 ⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
25 2 24 syl ⊢ ( 𝜑 → ( 𝐾 − 1 ) ∈ ℕ0 )
26 fveq2 ⊢ ( 𝑗 = 𝑖 → ( 𝑔 ‘ 𝑗 ) = ( 𝑔 ‘ 𝑖 ) )
27 26 cbvsumv ⊢ Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) = Σ 𝑖 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑖 )
28 27 eqeq1i ⊢ ( Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ↔ Σ 𝑖 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 )
29 28 anbi2i ⊢ ( ( 𝑔 : ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) ↔ ( 𝑔 : ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) )
30 29 abbii ⊢ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) } = { 𝑔 ∣ ( 𝑔 : ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑖 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑖 ) = 𝑁 ) }
31 1 25 30 sticksstones15 ⊢ ( 𝜑 → ( ♯ ‘ { 𝑔 ∣ ( 𝑔 : ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ⟶ ℕ0 ∧ Σ 𝑗 ∈ ( 1 ... ( ( 𝐾 − 1 ) + 1 ) ) ( 𝑔 ‘ 𝑗 ) = 𝑁 ) } ) = ( ( 𝑁 + ( 𝐾 − 1 ) ) C ( 𝐾 − 1 ) ) )
32 23 31 eqtrd ⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + ( 𝐾 − 1 ) ) C ( 𝐾 − 1 ) ) )