Metamath Proof Explorer

Theorem sticksstones6

Description: Function induces an order isomorphism for sticks and stones theorem. (Contributed by metakunt, 1-Oct-2024)

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

Proof

Step Hyp Ref Expression
1 sticksstones6.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones6.2 
 |-  ( ph -> K e. NN0 )
3 sticksstones6.3 
 |-  ( ph -> G : ( 1 ... ( K + 1 ) ) --> NN0 )
4 sticksstones6.4 
 |-  ( ph -> X e. ( 1 ... K ) )
5 sticksstones6.5 
 |-  ( ph -> Y e. ( 1 ... K ) )
6 sticksstones6.6 
 |-  ( ph -> X < Y )
7 sticksstones6.7 
 |-  F = ( x e. ( 1 ... K ) |-> ( x + sum_ i e. ( 1 ... x ) ( G ` i ) ) )
8 elfznn 
 |-  ( X e. ( 1 ... K ) -> X e. NN )
9 4 8 syl 
 |-  ( ph -> X e. NN )
10 9 nnred 
 |-  ( ph -> X e. RR )
11 fzfid 
 |-  ( ph -> ( 1 ... X ) e. Fin )
12 1zzd 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> 1 e. ZZ )
13 2 nn0zd 
 |-  ( ph -> K e. ZZ )
14 13 adantr 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> K e. ZZ )
15 14 peano2zd 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> ( K + 1 ) e. ZZ )
16 elfznn 
 |-  ( i e. ( 1 ... X ) -> i e. NN )
17 16 adantl 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i e. NN )
18 17 nnzd 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i e. ZZ )
19 17 nnge1d 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> 1 <_ i )
20 17 nnred 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i e. RR )
21 14 zred 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> K e. RR )
22 15 zred 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> ( K + 1 ) e. RR )
23 9 adantr 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> X e. NN )
24 23 nnred 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> X e. RR )
25 elfzle2 
 |-  ( i e. ( 1 ... X ) -> i <_ X )
26 25 adantl 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i <_ X )
27 elfzle2 
 |-  ( X e. ( 1 ... K ) -> X <_ K )
28 4 27 syl 
 |-  ( ph -> X <_ K )
29 28 adantr 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> X <_ K )
30 20 24 21 26 29 letrd 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i <_ K )
31 21 lep1d 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> K <_ ( K + 1 ) )
32 20 21 22 30 31 letrd 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i <_ ( K + 1 ) )
33 12 15 18 19 32 elfzd 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> i e. ( 1 ... ( K + 1 ) ) )
34 3 adantr 
 |-  ( ( ph /\ i e. ( 1 ... ( K + 1 ) ) ) -> G : ( 1 ... ( K + 1 ) ) --> NN0 )
35 simpr 
 |-  ( ( ph /\ i e. ( 1 ... ( K + 1 ) ) ) -> i e. ( 1 ... ( K + 1 ) ) )
36 34 35 ffvelcdmd 
 |-  ( ( ph /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( G ` i ) e. NN0 )
37 36 adantlr 
 |-  ( ( ( ph /\ i e. ( 1 ... X ) ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( G ` i ) e. NN0 )
38 33 37 mpdan 
 |-  ( ( ph /\ i e. ( 1 ... X ) ) -> ( G ` i ) e. NN0 )
39 11 38 fsumnn0cl 
 |-  ( ph -> sum_ i e. ( 1 ... X ) ( G ` i ) e. NN0 )
40 39 nn0red 
 |-  ( ph -> sum_ i e. ( 1 ... X ) ( G ` i ) e. RR )
41 elfznn 
 |-  ( Y e. ( 1 ... K ) -> Y e. NN )
42 5 41 syl 
 |-  ( ph -> Y e. NN )
43 42 nnred 
 |-  ( ph -> Y e. RR )
44 fzfid 
 |-  ( ph -> ( ( X + 1 ) ... Y ) e. Fin )
45 1zzd 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> 1 e. ZZ )
46 13 adantr 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> K e. ZZ )
47 46 peano2zd 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> ( K + 1 ) e. ZZ )
48 elfzelz 
 |-  ( i e. ( ( X + 1 ) ... Y ) -> i e. ZZ )
49 48 adantl 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> i e. ZZ )
50 1red 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> 1 e. RR )
51 10 adantr 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> X e. RR )
52 51 50 readdcld 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> ( X + 1 ) e. RR )
53 49 zred 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> i e. RR )
54 1red 
 |-  ( ph -> 1 e. RR )
55 10 54 readdcld 
 |-  ( ph -> ( X + 1 ) e. RR )
56 9 nnge1d 
 |-  ( ph -> 1 <_ X )
57 10 ltp1d 
 |-  ( ph -> X < ( X + 1 ) )
58 10 55 57 ltled 
 |-  ( ph -> X <_ ( X + 1 ) )
59 54 10 55 56 58 letrd 
 |-  ( ph -> 1 <_ ( X + 1 ) )
60 59 adantr 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> 1 <_ ( X + 1 ) )
61 elfzle1 
 |-  ( i e. ( ( X + 1 ) ... Y ) -> ( X + 1 ) <_ i )
62 61 adantl 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> ( X + 1 ) <_ i )
63 50 52 53 60 62 letrd 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> 1 <_ i )
64 43 adantr 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> Y e. RR )
65 47 zred 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> ( K + 1 ) e. RR )
66 elfzle2 
 |-  ( i e. ( ( X + 1 ) ... Y ) -> i <_ Y )
67 66 adantl 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> i <_ Y )
68 46 zred 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> K e. RR )
69 elfzle2 
 |-  ( Y e. ( 1 ... K ) -> Y <_ K )
70 5 69 syl 
 |-  ( ph -> Y <_ K )
71 70 adantr 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> Y <_ K )
72 68 lep1d 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> K <_ ( K + 1 ) )
73 64 68 65 71 72 letrd 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> Y <_ ( K + 1 ) )
74 53 64 65 67 73 letrd 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> i <_ ( K + 1 ) )
75 45 47 49 63 74 elfzd 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> i e. ( 1 ... ( K + 1 ) ) )
76 36 adantlr 
 |-  ( ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( G ` i ) e. NN0 )
77 75 76 mpdan 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> ( G ` i ) e. NN0 )
78 77 nn0red 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> ( G ` i ) e. RR )
79 44 78 fsumrecl 
 |-  ( ph -> sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) e. RR )
80 40 79 readdcld 
 |-  ( ph -> ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) ) e. RR )
81 77 nn0ge0d 
 |-  ( ( ph /\ i e. ( ( X + 1 ) ... Y ) ) -> 0 <_ ( G ` i ) )
82 44 78 81 fsumge0 
 |-  ( ph -> 0 <_ sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) )
83 40 79 addge01d 
 |-  ( ph -> ( 0 <_ sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) <-> sum_ i e. ( 1 ... X ) ( G ` i ) <_ ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) ) ) )
84 82 83 mpbid 
 |-  ( ph -> sum_ i e. ( 1 ... X ) ( G ` i ) <_ ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) ) )
85 10 40 43 80 6 84 ltleaddd 
 |-  ( ph -> ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) < ( Y + ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) ) ) )
86 7 a1i 
 |-  ( ph -> F = ( x e. ( 1 ... K ) |-> ( x + sum_ i e. ( 1 ... x ) ( G ` i ) ) ) )
87 simpr 
 |-  ( ( ph /\ x = X ) -> x = X )
88 87 oveq2d 
 |-  ( ( ph /\ x = X ) -> ( 1 ... x ) = ( 1 ... X ) )
89 88 sumeq1d 
 |-  ( ( ph /\ x = X ) -> sum_ i e. ( 1 ... x ) ( G ` i ) = sum_ i e. ( 1 ... X ) ( G ` i ) )
90 87 89 oveq12d 
 |-  ( ( ph /\ x = X ) -> ( x + sum_ i e. ( 1 ... x ) ( G ` i ) ) = ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) )
91 9 nnnn0d 
 |-  ( ph -> X e. NN0 )
92 91 39 nn0addcld 
 |-  ( ph -> ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) e. NN0 )
93 86 90 4 92 fvmptd 
 |-  ( ph -> ( F ` X ) = ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) )
94 93 eqcomd 
 |-  ( ph -> ( X + sum_ i e. ( 1 ... X ) ( G ` i ) ) = ( F ` X ) )
95 simpr 
 |-  ( ( ph /\ x = Y ) -> x = Y )
96 95 oveq2d 
 |-  ( ( ph /\ x = Y ) -> ( 1 ... x ) = ( 1 ... Y ) )
97 96 sumeq1d 
 |-  ( ( ph /\ x = Y ) -> sum_ i e. ( 1 ... x ) ( G ` i ) = sum_ i e. ( 1 ... Y ) ( G ` i ) )
98 95 97 oveq12d 
 |-  ( ( ph /\ x = Y ) -> ( x + sum_ i e. ( 1 ... x ) ( G ` i ) ) = ( Y + sum_ i e. ( 1 ... Y ) ( G ` i ) ) )
99 42 nnnn0d 
 |-  ( ph -> Y e. NN0 )
100 fzfid 
 |-  ( ph -> ( 1 ... Y ) e. Fin )
101 1zzd 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> 1 e. ZZ )
102 13 adantr 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> K e. ZZ )
103 102 peano2zd 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> ( K + 1 ) e. ZZ )
104 elfzelz 
 |-  ( i e. ( 1 ... Y ) -> i e. ZZ )
105 104 adantl 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> i e. ZZ )
106 elfzle1 
 |-  ( i e. ( 1 ... Y ) -> 1 <_ i )
107 106 adantl 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> 1 <_ i )
108 105 zred 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> i e. RR )
109 43 adantr 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> Y e. RR )
110 103 zred 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> ( K + 1 ) e. RR )
111 elfzle2 
 |-  ( i e. ( 1 ... Y ) -> i <_ Y )
112 111 adantl 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> i <_ Y )
113 102 zred 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> K e. RR )
114 70 adantr 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> Y <_ K )
115 113 lep1d 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> K <_ ( K + 1 ) )
116 109 113 110 114 115 letrd 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> Y <_ ( K + 1 ) )
117 108 109 110 112 116 letrd 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> i <_ ( K + 1 ) )
118 101 103 105 107 117 elfzd 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> i e. ( 1 ... ( K + 1 ) ) )
119 36 adantlr 
 |-  ( ( ( ph /\ i e. ( 1 ... Y ) ) /\ i e. ( 1 ... ( K + 1 ) ) ) -> ( G ` i ) e. NN0 )
120 118 119 mpdan 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> ( G ` i ) e. NN0 )
121 100 120 fsumnn0cl 
 |-  ( ph -> sum_ i e. ( 1 ... Y ) ( G ` i ) e. NN0 )
122 99 121 nn0addcld 
 |-  ( ph -> ( Y + sum_ i e. ( 1 ... Y ) ( G ` i ) ) e. NN0 )
123 86 98 5 122 fvmptd 
 |-  ( ph -> ( F ` Y ) = ( Y + sum_ i e. ( 1 ... Y ) ( G ` i ) ) )
124 fzdisj 
 |-  ( X < ( X + 1 ) -> ( ( 1 ... X ) i^i ( ( X + 1 ) ... Y ) ) = (/) )
125 57 124 syl 
 |-  ( ph -> ( ( 1 ... X ) i^i ( ( X + 1 ) ... Y ) ) = (/) )
126 1zzd 
 |-  ( ph -> 1 e. ZZ )
127 99 nn0zd 
 |-  ( ph -> Y e. ZZ )
128 91 nn0zd 
 |-  ( ph -> X e. ZZ )
129 10 43 6 ltled 
 |-  ( ph -> X <_ Y )
130 126 127 128 56 129 elfzd 
 |-  ( ph -> X e. ( 1 ... Y ) )
131 fzsplit 
 |-  ( X e. ( 1 ... Y ) -> ( 1 ... Y ) = ( ( 1 ... X ) u. ( ( X + 1 ) ... Y ) ) )
132 130 131 syl 
 |-  ( ph -> ( 1 ... Y ) = ( ( 1 ... X ) u. ( ( X + 1 ) ... Y ) ) )
133 120 nn0red 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> ( G ` i ) e. RR )
134 133 recnd 
 |-  ( ( ph /\ i e. ( 1 ... Y ) ) -> ( G ` i ) e. CC )
135 125 132 100 134 fsumsplit 
 |-  ( ph -> sum_ i e. ( 1 ... Y ) ( G ` i ) = ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) ) )
136 135 oveq2d 
 |-  ( ph -> ( Y + sum_ i e. ( 1 ... Y ) ( G ` i ) ) = ( Y + ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) ) ) )
137 123 136 eqtrd 
 |-  ( ph -> ( F ` Y ) = ( Y + ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) ) ) )
138 137 eqcomd 
 |-  ( ph -> ( Y + ( sum_ i e. ( 1 ... X ) ( G ` i ) + sum_ i e. ( ( X + 1 ) ... Y ) ( G ` i ) ) ) = ( F ` Y ) )
139 85 94 138 3brtr3d 
 |-  ( ph -> ( F ` X ) < ( F ` Y ) )