Metamath Proof Explorer

Theorem sticksstones7

Description: Closure property of sticks and stones function. (Contributed by metakunt, 1-Oct-2024)

Ref Expression
Hypotheses sticksstones7.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones7.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
sticksstones7.3 ⊢ ( 𝜑 → 𝐺 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
sticksstones7.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝐾 ) )
sticksstones7.5 ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑥 + Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) ) )
sticksstones7.6 ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) = 𝑁 )
Assertion sticksstones7 ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 sticksstones7.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones7.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 sticksstones7.3 ⊢ ( 𝜑 → 𝐺 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
4 sticksstones7.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝐾 ) )
5 sticksstones7.5 ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑥 + Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) ) )
6 sticksstones7.6 ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) = 𝑁 )
7 5 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑥 + Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) ) ) )
8 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
9 8 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 1 ... 𝑥 ) = ( 1 ... 𝑋 ) )
10 9 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) )
11 8 10 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 + Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) ) = ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) )
12 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝐾 ) → 𝑋 ∈ ℕ )
13 4 12 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
14 13 nnnn0d ⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
15 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑋 ) ∈ Fin )
16 1zzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 1 ∈ ℤ )
17 2 nn0zd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
18 17 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝐾 ∈ ℤ )
19 18 peano2zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → ( 𝐾 + 1 ) ∈ ℤ )
20 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... 𝑋 ) → 𝑖 ∈ ℤ )
21 20 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ∈ ℤ )
22 elfzle1 ⊢ ( 𝑖 ∈ ( 1 ... 𝑋 ) → 1 ≤ 𝑖 )
23 22 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 1 ≤ 𝑖 )
24 21 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ∈ ℝ )
25 13 nnred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑋 ∈ ℝ )
27 19 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → ( 𝐾 + 1 ) ∈ ℝ )
28 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑋 ) → 𝑖 ≤ 𝑋 )
29 28 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ≤ 𝑋 )
30 2 nn0red ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
31 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
32 30 31 readdcld ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℝ )
33 elfzle2 ⊢ ( 𝑋 ∈ ( 1 ... 𝐾 ) → 𝑋 ≤ 𝐾 )
34 4 33 syl ⊢ ( 𝜑 → 𝑋 ≤ 𝐾 )
35 30 lep1d ⊢ ( 𝜑 → 𝐾 ≤ ( 𝐾 + 1 ) )
36 25 30 32 34 35 letrd ⊢ ( 𝜑 → 𝑋 ≤ ( 𝐾 + 1 ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑋 ≤ ( 𝐾 + 1 ) )
38 24 26 27 29 37 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ≤ ( 𝐾 + 1 ) )
39 16 19 21 23 38 elfzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) )
40 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝐺 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
41 40 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
42 39 41 mpdan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
43 15 42 fsumnn0cl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
44 14 43 nn0addcld ⊢ ( 𝜑 → ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) ∈ ℕ0 )
45 7 11 4 44 fvmptd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) )
46 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
47 1 nn0zd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
48 47 17 zaddcld ⊢ ( 𝜑 → ( 𝑁 + 𝐾 ) ∈ ℤ )
49 44 nn0zd ⊢ ( 𝜑 → ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) ∈ ℤ )
50 eqid ⊢ 1 = 1
51 1p0e1 ⊢ ( 1 + 0 ) = 1
52 50 51 eqtr4i ⊢ 1 = ( 1 + 0 )
53 52 a1i ⊢ ( 𝜑 → 1 = ( 1 + 0 ) )
54 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
55 43 nn0red ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ∈ ℝ )
56 13 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑋 )
57 43 nn0ge0d ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) )
58 31 54 25 55 56 57 le2addd ⊢ ( 𝜑 → ( 1 + 0 ) ≤ ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) )
59 53 58 eqbrtrd ⊢ ( 𝜑 → 1 ≤ ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) )
60 1 nn0red ⊢ ( 𝜑 → 𝑁 ∈ ℝ )
61 fzfid ⊢ ( 𝜑 → ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ∈ Fin )
62 46 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 1 ∈ ℤ )
63 17 peano2zd ⊢ ( 𝜑 → ( 𝐾 + 1 ) ∈ ℤ )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → ( 𝐾 + 1 ) ∈ ℤ )
65 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) → 𝑖 ∈ ℤ )
66 65 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 𝑖 ∈ ℤ )
67 31 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 1 ∈ ℝ )
68 25 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 𝑋 ∈ ℝ )
69 68 67 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → ( 𝑋 + 1 ) ∈ ℝ )
70 66 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 𝑖 ∈ ℝ )
71 56 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 1 ≤ 𝑋 )
72 68 lep1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 𝑋 ≤ ( 𝑋 + 1 ) )
73 67 68 69 71 72 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 1 ≤ ( 𝑋 + 1 ) )
74 elfzle1 ⊢ ( 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) → ( 𝑋 + 1 ) ≤ 𝑖 )
75 74 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → ( 𝑋 + 1 ) ≤ 𝑖 )
76 67 69 70 73 75 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 1 ≤ 𝑖 )
77 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) → 𝑖 ≤ ( 𝐾 + 1 ) )
78 77 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 𝑖 ≤ ( 𝐾 + 1 ) )
79 62 64 66 76 78 elfzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) )
80 3 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
81 80 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
82 79 81 mpdan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
83 61 82 fsumnn0cl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
84 83 nn0ge0d ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) )
85 83 nn0red ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ∈ ℝ )
86 55 85 addge01d ⊢ ( 𝜑 → ( 0 ≤ Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ≤ ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ) ) )
87 84 86 mpbid ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ≤ ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ) )
88 25 ltp1d ⊢ ( 𝜑 → 𝑋 < ( 𝑋 + 1 ) )
89 fzdisj ⊢ ( 𝑋 < ( 𝑋 + 1 ) → ( ( 1 ... 𝑋 ) ∩ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) = ∅ )
90 88 89 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑋 ) ∩ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) = ∅ )
91 14 nn0zd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
92 46 63 91 56 36 elfzd ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... ( 𝐾 + 1 ) ) )
93 fzsplit ⊢ ( 𝑋 ∈ ( 1 ... ( 𝐾 + 1 ) ) → ( 1 ... ( 𝐾 + 1 ) ) = ( ( 1 ... 𝑋 ) ∪ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) )
94 92 93 syl ⊢ ( 𝜑 → ( 1 ... ( 𝐾 + 1 ) ) = ( ( 1 ... 𝑋 ) ∪ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ) )
95 fzfid ⊢ ( 𝜑 → ( 1 ... ( 𝐾 + 1 ) ) ∈ Fin )
96 nn0cn ⊢ ( ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 → ( 𝐺 ‘ 𝑖 ) ∈ ℂ )
97 80 96 syl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℂ )
98 90 94 95 97 fsumsplit ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) ) )
99 87 98 breqtrrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ≤ Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) )
100 6 eqcomd ⊢ ( 𝜑 → 𝑁 = Σ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ( 𝐺 ‘ 𝑖 ) )
101 99 100 breqtrrd ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ≤ 𝑁 )
102 25 55 30 60 34 101 le2addd ⊢ ( 𝜑 → ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) ≤ ( 𝐾 + 𝑁 ) )
103 2 nn0cnd ⊢ ( 𝜑 → 𝐾 ∈ ℂ )
104 1 nn0cnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
105 103 104 addcomd ⊢ ( 𝜑 → ( 𝐾 + 𝑁 ) = ( 𝑁 + 𝐾 ) )
106 102 105 breqtrd ⊢ ( 𝜑 → ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) ≤ ( 𝑁 + 𝐾 ) )
107 46 48 49 59 106 elfzd ⊢ ( 𝜑 → ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )
108 45 107 eqeltrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ( 1 ... ( 𝑁 + 𝐾 ) ) )