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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones6.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
sticksstones6.3 ⊢ ( 𝜑 → 𝐺 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
sticksstones6.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝐾 ) )
sticksstones6.5 ⊢ ( 𝜑 → 𝑌 ∈ ( 1 ... 𝐾 ) )
sticksstones6.6 ⊢ ( 𝜑 → 𝑋 < 𝑌 )
sticksstones6.7 ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑥 + Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) ) )
Assertion sticksstones6 ( 𝜑 → ( 𝐹 ‘ 𝑋 ) < ( 𝐹 ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 sticksstones6.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 sticksstones6.2 ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 sticksstones6.3 ⊢ ( 𝜑 → 𝐺 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
4 sticksstones6.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝐾 ) )
5 sticksstones6.5 ⊢ ( 𝜑 → 𝑌 ∈ ( 1 ... 𝐾 ) )
6 sticksstones6.6 ⊢ ( 𝜑 → 𝑋 < 𝑌 )
7 sticksstones6.7 ⊢ 𝐹 = ( 𝑥 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑥 + Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) ) )
8 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝐾 ) → 𝑋 ∈ ℕ )
9 4 8 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
10 9 nnred ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
11 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑋 ) ∈ Fin )
12 1zzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 1 ∈ ℤ )
13 2 nn0zd ⊢ ( 𝜑 → 𝐾 ∈ ℤ )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝐾 ∈ ℤ )
15 14 peano2zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → ( 𝐾 + 1 ) ∈ ℤ )
16 elfznn ⊢ ( 𝑖 ∈ ( 1 ... 𝑋 ) → 𝑖 ∈ ℕ )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ∈ ℕ )
18 17 nnzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ∈ ℤ )
19 17 nnge1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 1 ≤ 𝑖 )
20 17 nnred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ∈ ℝ )
21 14 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝐾 ∈ ℝ )
22 15 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → ( 𝐾 + 1 ) ∈ ℝ )
23 9 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑋 ∈ ℕ )
24 23 nnred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑋 ∈ ℝ )
25 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑋 ) → 𝑖 ≤ 𝑋 )
26 25 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ≤ 𝑋 )
27 elfzle2 ⊢ ( 𝑋 ∈ ( 1 ... 𝐾 ) → 𝑋 ≤ 𝐾 )
28 4 27 syl ⊢ ( 𝜑 → 𝑋 ≤ 𝐾 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑋 ≤ 𝐾 )
30 20 24 21 26 29 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ≤ 𝐾 )
31 21 lep1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝐾 ≤ ( 𝐾 + 1 ) )
32 20 21 22 30 31 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ≤ ( 𝐾 + 1 ) )
33 12 15 18 19 32 elfzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) )
34 3 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝐺 : ( 1 ... ( 𝐾 + 1 ) ) ⟶ ℕ0 )
35 simpr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) )
36 34 35 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
37 36 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
38 33 37 mpdan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑋 ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
39 11 38 fsumnn0cl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
40 39 nn0red ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ∈ ℝ )
41 elfznn ⊢ ( 𝑌 ∈ ( 1 ... 𝐾 ) → 𝑌 ∈ ℕ )
42 5 41 syl ⊢ ( 𝜑 → 𝑌 ∈ ℕ )
43 42 nnred ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
44 fzfid ⊢ ( 𝜑 → ( ( 𝑋 + 1 ) ... 𝑌 ) ∈ Fin )
45 1zzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 1 ∈ ℤ )
46 13 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝐾 ∈ ℤ )
47 46 peano2zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → ( 𝐾 + 1 ) ∈ ℤ )
48 elfzelz ⊢ ( 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) → 𝑖 ∈ ℤ )
49 48 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝑖 ∈ ℤ )
50 1red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 1 ∈ ℝ )
51 10 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝑋 ∈ ℝ )
52 51 50 readdcld ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → ( 𝑋 + 1 ) ∈ ℝ )
53 49 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝑖 ∈ ℝ )
54 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
55 10 54 readdcld ⊢ ( 𝜑 → ( 𝑋 + 1 ) ∈ ℝ )
56 9 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑋 )
57 10 ltp1d ⊢ ( 𝜑 → 𝑋 < ( 𝑋 + 1 ) )
58 10 55 57 ltled ⊢ ( 𝜑 → 𝑋 ≤ ( 𝑋 + 1 ) )
59 54 10 55 56 58 letrd ⊢ ( 𝜑 → 1 ≤ ( 𝑋 + 1 ) )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 1 ≤ ( 𝑋 + 1 ) )
61 elfzle1 ⊢ ( 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) → ( 𝑋 + 1 ) ≤ 𝑖 )
62 61 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → ( 𝑋 + 1 ) ≤ 𝑖 )
63 50 52 53 60 62 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 1 ≤ 𝑖 )
64 43 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝑌 ∈ ℝ )
65 47 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → ( 𝐾 + 1 ) ∈ ℝ )
66 elfzle2 ⊢ ( 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) → 𝑖 ≤ 𝑌 )
67 66 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝑖 ≤ 𝑌 )
68 46 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝐾 ∈ ℝ )
69 elfzle2 ⊢ ( 𝑌 ∈ ( 1 ... 𝐾 ) → 𝑌 ≤ 𝐾 )
70 5 69 syl ⊢ ( 𝜑 → 𝑌 ≤ 𝐾 )
71 70 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝑌 ≤ 𝐾 )
72 68 lep1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝐾 ≤ ( 𝐾 + 1 ) )
73 64 68 65 71 72 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝑌 ≤ ( 𝐾 + 1 ) )
74 53 64 65 67 73 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝑖 ≤ ( 𝐾 + 1 ) )
75 45 47 49 63 74 elfzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) )
76 36 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
77 75 76 mpdan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
78 77 nn0red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℝ )
79 44 78 fsumrecl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ∈ ℝ )
80 40 79 readdcld ⊢ ( 𝜑 → ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) ∈ ℝ )
81 77 nn0ge0d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ) → 0 ≤ ( 𝐺 ‘ 𝑖 ) )
82 44 78 81 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) )
83 40 79 addge01d ⊢ ( 𝜑 → ( 0 ≤ Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ↔ Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ≤ ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) ) )
84 82 83 mpbid ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ≤ ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) )
85 10 40 43 80 6 84 ltleaddd ⊢ ( 𝜑 → ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) < ( 𝑌 + ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) ) )
86 7 a1i ⊢ ( 𝜑 → 𝐹 = ( 𝑥 ∈ ( 1 ... 𝐾 ) ↦ ( 𝑥 + Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) ) ) )
87 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
88 87 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 1 ... 𝑥 ) = ( 1 ... 𝑋 ) )
89 88 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) )
90 87 89 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 + Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) ) = ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) )
91 9 nnnn0d ⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
92 91 39 nn0addcld ⊢ ( 𝜑 → ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) ∈ ℕ0 )
93 86 90 4 92 fvmptd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) )
94 93 eqcomd ⊢ ( 𝜑 → ( 𝑋 + Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) ) = ( 𝐹 ‘ 𝑋 ) )
95 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → 𝑥 = 𝑌 )
96 95 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 1 ... 𝑥 ) = ( 1 ... 𝑌 ) )
97 96 sumeq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) )
98 95 97 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → ( 𝑥 + Σ 𝑖 ∈ ( 1 ... 𝑥 ) ( 𝐺 ‘ 𝑖 ) ) = ( 𝑌 + Σ 𝑖 ∈ ( 1 ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) )
99 42 nnnn0d ⊢ ( 𝜑 → 𝑌 ∈ ℕ0 )
100 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑌 ) ∈ Fin )
101 1zzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 1 ∈ ℤ )
102 13 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝐾 ∈ ℤ )
103 102 peano2zd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → ( 𝐾 + 1 ) ∈ ℤ )
104 elfzelz ⊢ ( 𝑖 ∈ ( 1 ... 𝑌 ) → 𝑖 ∈ ℤ )
105 104 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝑖 ∈ ℤ )
106 elfzle1 ⊢ ( 𝑖 ∈ ( 1 ... 𝑌 ) → 1 ≤ 𝑖 )
107 106 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 1 ≤ 𝑖 )
108 105 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝑖 ∈ ℝ )
109 43 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝑌 ∈ ℝ )
110 103 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → ( 𝐾 + 1 ) ∈ ℝ )
111 elfzle2 ⊢ ( 𝑖 ∈ ( 1 ... 𝑌 ) → 𝑖 ≤ 𝑌 )
112 111 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝑖 ≤ 𝑌 )
113 102 zred ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝐾 ∈ ℝ )
114 70 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝑌 ≤ 𝐾 )
115 113 lep1d ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝐾 ≤ ( 𝐾 + 1 ) )
116 109 113 110 114 115 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝑌 ≤ ( 𝐾 + 1 ) )
117 108 109 110 112 116 letrd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝑖 ≤ ( 𝐾 + 1 ) )
118 101 103 105 107 117 elfzd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) )
119 36 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) ∧ 𝑖 ∈ ( 1 ... ( 𝐾 + 1 ) ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
120 118 119 mpdan ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
121 100 120 fsumnn0cl ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ∈ ℕ0 )
122 99 121 nn0addcld ⊢ ( 𝜑 → ( 𝑌 + Σ 𝑖 ∈ ( 1 ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) ∈ ℕ0 )
123 86 98 5 122 fvmptd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = ( 𝑌 + Σ 𝑖 ∈ ( 1 ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) )
124 fzdisj ⊢ ( 𝑋 < ( 𝑋 + 1 ) → ( ( 1 ... 𝑋 ) ∩ ( ( 𝑋 + 1 ) ... 𝑌 ) ) = ∅ )
125 57 124 syl ⊢ ( 𝜑 → ( ( 1 ... 𝑋 ) ∩ ( ( 𝑋 + 1 ) ... 𝑌 ) ) = ∅ )
126 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
127 99 nn0zd ⊢ ( 𝜑 → 𝑌 ∈ ℤ )
128 91 nn0zd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
129 10 43 6 ltled ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
130 126 127 128 56 129 elfzd ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑌 ) )
131 fzsplit ⊢ ( 𝑋 ∈ ( 1 ... 𝑌 ) → ( 1 ... 𝑌 ) = ( ( 1 ... 𝑋 ) ∪ ( ( 𝑋 + 1 ) ... 𝑌 ) ) )
132 130 131 syl ⊢ ( 𝜑 → ( 1 ... 𝑌 ) = ( ( 1 ... 𝑋 ) ∪ ( ( 𝑋 + 1 ) ... 𝑌 ) ) )
133 120 nn0red ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℝ )
134 133 recnd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 1 ... 𝑌 ) ) → ( 𝐺 ‘ 𝑖 ) ∈ ℂ )
135 125 132 100 134 fsumsplit ⊢ ( 𝜑 → Σ 𝑖 ∈ ( 1 ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) = ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) )
136 135 oveq2d ⊢ ( 𝜑 → ( 𝑌 + Σ 𝑖 ∈ ( 1 ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) = ( 𝑌 + ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) ) )
137 123 136 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑌 ) = ( 𝑌 + ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) ) )
138 137 eqcomd ⊢ ( 𝜑 → ( 𝑌 + ( Σ 𝑖 ∈ ( 1 ... 𝑋 ) ( 𝐺 ‘ 𝑖 ) + Σ 𝑖 ∈ ( ( 𝑋 + 1 ) ... 𝑌 ) ( 𝐺 ‘ 𝑖 ) ) ) = ( 𝐹 ‘ 𝑌 ) )
139 85 94 138 3brtr3d ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) < ( 𝐹 ‘ 𝑌 ) )