Metamath Proof Explorer

Theorem sticksstones7

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

Ref Expression
Hypotheses sticksstones7.1 
|- ( ph -> N e. NN0 )
sticksstones7.2 
|- ( ph -> K e. NN0 )
sticksstones7.3 
|- ( ph -> G : ( 1 ... ( K + 1 ) ) --> NN0 )
sticksstones7.4 
|- ( ph -> X e. ( 1 ... K ) )
sticksstones7.5 
|- F = ( x e. ( 1 ... K ) |-> ( x + sum_ i e. ( 1 ... x ) ( G ` i ) ) )
sticksstones7.6 
|- ( ph -> sum_ i e. ( 1 ... ( K + 1 ) ) ( G ` i ) = N )
Assertion sticksstones7 
|- ( ph -> ( F ` X ) e. ( 1 ... ( N + K ) ) )

Proof

Step Hyp Ref Expression
1 sticksstones7.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones7.2 
 |-  ( ph -> K e. NN0 )
3 sticksstones7.3 
 |-  ( ph -> G : ( 1 ... ( K + 1 ) ) --> NN0 )
4 sticksstones7.4 
 |-  ( ph -> X e. ( 1 ... K ) )
5 sticksstones7.5 
 |-  F = ( x e. ( 1 ... K ) |-> ( x + sum_ i e. ( 1 ... x ) ( G ` i ) ) )
6 sticksstones7.6 
 |-  ( ph -> sum_ i e. ( 1 ... ( K + 1 ) ) ( G ` i ) = N )
7 5 a1i 
 |-  ( ph -> F = ( x e. ( 1 ... K ) |-> ( x + sum_ i e. ( 1 ... x ) ( G ` i ) ) ) )
8 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
9 8 oveq2d 
 |-  ( ( ph /\ x = X ) -> ( 1 ... x ) = ( 1 ... X ) )
10 9 sumeq1d 
 |-  ( ( ph /\ x = X ) -> sum_ i e. ( 1 ... x ) ( G ` i ) = sum_ i e. ( 1 ... X ) ( G ` i ) )
11 8 10 oveq12d 
 |-  ( ( ph /\ x = X ) -> ( x + sum_ i e. ( 1 ... x ) ( G ` i ) ) = ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) )
12 elfznn 
 |-  ( X e. ( 1 ... K ) -> X e. NN )
13 4 12 syl 
 |-  ( ph -> X e. NN )
14 13 nnnn0d 
 |-  ( ph -> X e. NN0 )
15 fzfid 
 |-  ( ph -> ( 1 ... X ) e. Fin )
16 1zzd 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> 1 e. ZZ )
17 2 nn0zd 
 |-  ( ph -> K e. ZZ )
18 17 adantr 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> K e. ZZ )
19 18 peano2zd 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> ( K + 1 ) e. ZZ )
20 elfzelz 
 |-  ( i e. ( 1 ... X ) -> i e. ZZ )
21 20 adantl 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i e. ZZ )
22 elfzle1 
 |-  ( i e. ( 1 ... X ) -> 1 <_ i )
23 22 adantl 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> 1 <_ i )
24 21 zred 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i e. RR )
25 13 nnred 
 |-  ( ph -> X e. RR )
26 25 adantr 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> X e. RR )
27 19 zred 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> ( K + 1 ) e. RR )
28 elfzle2 
 |-  ( i e. ( 1 ... X ) -> i <_ X )
29 28 adantl 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i <_ X )
30 2 nn0red 
 |-  ( ph -> K e. RR )
31 1red 
 |-  ( ph -> 1 e. RR )
32 30 31 readdcld 
 |-  ( ph -> ( K + 1 ) e. RR )
33 elfzle2 
 |-  ( X e. ( 1 ... K ) -> X <_ K )
34 4 33 syl 
 |-  ( ph -> X <_ K )
35 30 lep1d 
 |-  ( ph -> K <_ ( K + 1 ) )
36 25 30 32 34 35 letrd 
 |-  ( ph -> X <_ ( K + 1 ) )
37 36 adantr 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> X <_ ( K + 1 ) )
38 24 26 27 29 37 letrd 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i <_ ( K + 1 ) )
39 16 19 21 23 38 elfzd 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i e. ( 1 ... ( K + 1 ) ) )
40 3 adantr 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> G : ( 1 ... ( K + 1 ) ) --> NN0 )
41 40 ffvelrnda 
 |-  ( ( ( ph /\ i e. ( 1 ... X ) ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( G ` i ) e. NN0 )
42 39 41 mpdan 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> ( G ` i ) e. NN0 )
43 15 42 fsumnn0cl 
 |-  ( ph -> sum_ i e. ( 1 ... X ) ( G ` i ) e. NN0 )
44 14 43 nn0addcld 
 |-  ( ph -> ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) e. NN0 )
45 7 11 4 44 fvmptd 
 |-  ( ph -> ( F ` X ) = ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) )
46 1zzd 
 |-  ( ph -> 1 e. ZZ )
47 1 nn0zd 
 |-  ( ph -> N e. ZZ )
48 47 17 zaddcld 
 |-  ( ph -> ( N + K ) e. ZZ )
49 44 nn0zd 
 |-  ( ph -> ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) e. ZZ )
50 eqid 
 |-  1 = 1
51 1p0e1 
 |-  ( 1 + 0 ) = 1
52 50 51 eqtr4i 
 |-  1 = ( 1 + 0 )
53 52 a1i 
 |-  ( ph -> 1 = ( 1 + 0 ) )
54 0red 
 |-  ( ph -> 0 e. RR )
55 43 nn0red 
 |-  ( ph -> sum_ i e. ( 1 ... X ) ( G ` i ) e. RR )
56 13 nnge1d 
 |-  ( ph -> 1 <_ X )
57 43 nn0ge0d 
 |-  ( ph -> 0 <_ sum_ i e. ( 1 ... X ) ( G ` i ) )
58 31 54 25 55 56 57 le2addd 
 |-  ( ph -> ( 1 + 0 ) <_ ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) )
59 53 58 eqbrtrd 
 |-  ( ph -> 1 <_ ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) )
60 1 nn0red 
 |-  ( ph -> N e. RR )
61 fzfid 
 |-  ( ph -> ( ( X + 1 ) ... ( K + 1 ) ) e. Fin )
62 46 adantr 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> 1 e. ZZ )
63 17 peano2zd 
 |-  ( ph -> ( K + 1 ) e. ZZ )
64 63 adantr 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> ( K + 1 ) e. ZZ )
65 elfzelz 
 |-  ( i e. ( ( X + 1 ) ... ( K + 1 ) ) -> i e. ZZ )
66 65 adantl 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> i e. ZZ )
67 31 adantr 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> 1 e. RR )
68 25 adantr 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> X e. RR )
69 68 67 readdcld 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> ( X + 1 ) e. RR )
70 66 zred 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> i e. RR )
71 56 adantr 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> 1 <_ X )
72 68 lep1d 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> X <_ ( X + 1 ) )
73 67 68 69 71 72 letrd 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> 1 <_ ( X + 1 ) )
74 elfzle1 
 |-  ( i e. ( ( X + 1 ) ... ( K + 1 ) ) -> ( X + 1 ) <_ i )
75 74 adantl 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> ( X + 1 ) <_ i )
76 67 69 70 73 75 letrd 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> 1 <_ i )
77 elfzle2 
 |-  ( i e. ( ( X + 1 ) ... ( K + 1 ) ) -> i <_ ( K + 1 ) )
78 77 adantl 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> i <_ ( K + 1 ) )
79 62 64 66 76 78 elfzd 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> i e. ( 1 ... ( K + 1 ) ) )
80 3 ffvelrnda 
 |-  ( ( ph /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( G ` i ) e. NN0 )
81 80 adantlr 
 |-  ( ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( G ` i ) e. NN0 )
82 79 81 mpdan 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... ( K + 1 ) ) ) -> ( G ` i ) e. NN0 )
83 61 82 fsumnn0cl 
 |-  ( ph -> sum_ i e. ( ( X + 1 ) ... ( K + 1 ) ) ( G ` i ) e. NN0 )
84 83 nn0ge0d 
 |-  ( ph -> 0 <_ sum_ i e. ( ( X + 1 ) ... ( K + 1 ) ) ( G ` i ) )
85 83 nn0red 
 |-  ( ph -> sum_ i e. ( ( X + 1 ) ... ( K + 1 ) ) ( G ` i ) e. RR )
86 55 85 addge01d 
 |-  ( ph -> ( 0 <_ sum_ i e. ( ( X + 1 ) ... ( K + 1 ) ) ( G ` i ) <-> sum_ i e. ( 1 ... X ) ( G ` i ) <_ ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... ( K + 1 ) ) ( G ` i ) ) ) )
87 84 86 mpbid 
 |-  ( ph -> sum_ i e. ( 1 ... X ) ( G ` i ) <_ ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... ( K + 1 ) ) ( G ` i ) ) )
88 25 ltp1d 
 |-  ( ph -> X < ( X + 1 ) )
89 fzdisj 
 |-  ( X < ( X + 1 ) -> ( ( 1 ... X ) i^i ( ( X + 1 ) ... ( K + 1 ) ) ) = (/) )
90 88 89 syl 
 |-  ( ph -> ( ( 1 ... X ) i^i ( ( X + 1 ) ... ( K + 1 ) ) ) = (/) )
91 14 nn0zd 
 |-  ( ph -> X e. ZZ )
92 46 63 91 56 36 elfzd 
 |-  ( ph -> X e. ( 1 ... ( K + 1 ) ) )
93 fzsplit 
 |-  ( X e. ( 1 ... ( K + 1 ) ) -> ( 1 ... ( K + 1 ) ) = ( ( 1 ... X ) u. ( ( X + 1 ) ... ( K + 1 ) ) ) )
94 92 93 syl 
 |-  ( ph -> ( 1 ... ( K + 1 ) ) = ( ( 1 ... X ) u. ( ( X + 1 ) ... ( K + 1 ) ) ) )
95 fzfid 
 |-  ( ph -> ( 1 ... ( K + 1 ) ) e. Fin )
96 nn0cn 
 |-  ( ( G ` i ) e. NN0 -> ( G ` i ) e. CC )
97 80 96 syl 
 |-  ( ( ph /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( G ` i ) e. CC )
98 90 94 95 97 fsumsplit 
 |-  ( ph -> sum_ i e. ( 1 ... ( K + 1 ) ) ( G ` i ) = ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... ( K + 1 ) ) ( G ` i ) ) )
99 87 98 breqtrrd 
 |-  ( ph -> sum_ i e. ( 1 ... X ) ( G ` i ) <_ sum_ i e. ( 1 ... ( K + 1 ) ) ( G ` i ) )
100 6 eqcomd 
 |-  ( ph -> N = sum_ i e. ( 1 ... ( K + 1 ) ) ( G ` i ) )
101 99 100 breqtrrd 
 |-  ( ph -> sum_ i e. ( 1 ... X ) ( G ` i ) <_ N )
102 25 55 30 60 34 101 le2addd 
 |-  ( ph -> ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) <_ ( K + N ) )
103 2 nn0cnd 
 |-  ( ph -> K e. CC )
104 1 nn0cnd 
 |-  ( ph -> N e. CC )
105 103 104 addcomd 
 |-  ( ph -> ( K + N ) = ( N + K ) )
106 102 105 breqtrd 
 |-  ( ph -> ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) <_ ( N + K ) )
107 46 48 49 59 106 elfzd 
 |-  ( ph -> ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) e. ( 1 ... ( N + K ) ) )
108 45 107 eqeltrd 
 |-  ( ph -> ( F ` X ) e. ( 1 ... ( N + K ) ) )