Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sticksstones7 Structured version   Visualization version   GIF version

Theorem sticksstones7 39859
Description: Closure property of sticks and stones function. (Contributed by metakunt, 1-Oct-2024.)
Hypotheses
Ref Expression
sticksstones7.1 (𝜑𝑁 ∈ ℕ0)
sticksstones7.2 (𝜑𝐾 ∈ ℕ0)
sticksstones7.3 (𝜑𝐺:(1...(𝐾 + 1))⟶ℕ0)
sticksstones7.4 (𝜑𝑋 ∈ (1...𝐾))
sticksstones7.5 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺𝑖)))
sticksstones7.6 (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺𝑖) = 𝑁)
Assertion
Ref Expression
sticksstones7 (𝜑 → (𝐹𝑋) ∈ (1...(𝑁 + 𝐾)))
Distinct variable groups:   𝑥,𝐺   𝑖,𝐾,𝑥   𝑖,𝑋,𝑥   𝜑,𝑖,𝑥
Allowed substitution hints:   𝐹(𝑥,𝑖)   𝐺(𝑖)   𝑁(𝑥,𝑖)

Proof of Theorem sticksstones7
StepHypRef Expression
1 sticksstones7.5 . . . 4 𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺𝑖)))
21a1i 11 . . 3 (𝜑𝐹 = (𝑥 ∈ (1...𝐾) ↦ (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺𝑖))))
3 simpr 488 . . . 4 ((𝜑𝑥 = 𝑋) → 𝑥 = 𝑋)
43oveq2d 7247 . . . . 5 ((𝜑𝑥 = 𝑋) → (1...𝑥) = (1...𝑋))
54sumeq1d 15289 . . . 4 ((𝜑𝑥 = 𝑋) → Σ𝑖 ∈ (1...𝑥)(𝐺𝑖) = Σ𝑖 ∈ (1...𝑋)(𝐺𝑖))
63, 5oveq12d 7249 . . 3 ((𝜑𝑥 = 𝑋) → (𝑥 + Σ𝑖 ∈ (1...𝑥)(𝐺𝑖)) = (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺𝑖)))
7 sticksstones7.4 . . 3 (𝜑𝑋 ∈ (1...𝐾))
8 elfznn 13165 . . . . . 6 (𝑋 ∈ (1...𝐾) → 𝑋 ∈ ℕ)
97, 8syl 17 . . . . 5 (𝜑𝑋 ∈ ℕ)
109nnnn0d 12174 . . . 4 (𝜑𝑋 ∈ ℕ0)
11 fzfid 13570 . . . . 5 (𝜑 → (1...𝑋) ∈ Fin)
12 1zzd 12232 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑋)) → 1 ∈ ℤ)
13 sticksstones7.2 . . . . . . . . . 10 (𝜑𝐾 ∈ ℕ0)
1413nn0zd 12304 . . . . . . . . 9 (𝜑𝐾 ∈ ℤ)
1514adantr 484 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑋)) → 𝐾 ∈ ℤ)
1615peano2zd 12309 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑋)) → (𝐾 + 1) ∈ ℤ)
17 elfzelz 13136 . . . . . . . 8 (𝑖 ∈ (1...𝑋) → 𝑖 ∈ ℤ)
1817adantl 485 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑋)) → 𝑖 ∈ ℤ)
19 elfzle1 13139 . . . . . . . 8 (𝑖 ∈ (1...𝑋) → 1 ≤ 𝑖)
2019adantl 485 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑋)) → 1 ≤ 𝑖)
2118zred 12306 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑋)) → 𝑖 ∈ ℝ)
229nnred 11869 . . . . . . . . 9 (𝜑𝑋 ∈ ℝ)
2322adantr 484 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑋)) → 𝑋 ∈ ℝ)
2416zred 12306 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑋)) → (𝐾 + 1) ∈ ℝ)
25 elfzle2 13140 . . . . . . . . 9 (𝑖 ∈ (1...𝑋) → 𝑖𝑋)
2625adantl 485 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑋)) → 𝑖𝑋)
2713nn0red 12175 . . . . . . . . . 10 (𝜑𝐾 ∈ ℝ)
28 1red 10858 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℝ)
2927, 28readdcld 10886 . . . . . . . . . 10 (𝜑 → (𝐾 + 1) ∈ ℝ)
30 elfzle2 13140 . . . . . . . . . . 11 (𝑋 ∈ (1...𝐾) → 𝑋𝐾)
317, 30syl 17 . . . . . . . . . 10 (𝜑𝑋𝐾)
3227lep1d 11787 . . . . . . . . . 10 (𝜑𝐾 ≤ (𝐾 + 1))
3322, 27, 29, 31, 32letrd 11013 . . . . . . . . 9 (𝜑𝑋 ≤ (𝐾 + 1))
3433adantr 484 . . . . . . . 8 ((𝜑𝑖 ∈ (1...𝑋)) → 𝑋 ≤ (𝐾 + 1))
3521, 23, 24, 26, 34letrd 11013 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑋)) → 𝑖 ≤ (𝐾 + 1))
3612, 16, 18, 20, 35elfzd 13127 . . . . . 6 ((𝜑𝑖 ∈ (1...𝑋)) → 𝑖 ∈ (1...(𝐾 + 1)))
37 sticksstones7.3 . . . . . . . 8 (𝜑𝐺:(1...(𝐾 + 1))⟶ℕ0)
3837adantr 484 . . . . . . 7 ((𝜑𝑖 ∈ (1...𝑋)) → 𝐺:(1...(𝐾 + 1))⟶ℕ0)
3938ffvelrnda 6922 . . . . . 6 (((𝜑𝑖 ∈ (1...𝑋)) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝐺𝑖) ∈ ℕ0)
4036, 39mpdan 687 . . . . 5 ((𝜑𝑖 ∈ (1...𝑋)) → (𝐺𝑖) ∈ ℕ0)
4111, 40fsumnn0cl 15324 . . . 4 (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺𝑖) ∈ ℕ0)
4210, 41nn0addcld 12178 . . 3 (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺𝑖)) ∈ ℕ0)
432, 6, 7, 42fvmptd 6843 . 2 (𝜑 → (𝐹𝑋) = (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺𝑖)))
44 1zzd 12232 . . 3 (𝜑 → 1 ∈ ℤ)
45 sticksstones7.1 . . . . 5 (𝜑𝑁 ∈ ℕ0)
4645nn0zd 12304 . . . 4 (𝜑𝑁 ∈ ℤ)
4746, 14zaddcld 12310 . . 3 (𝜑 → (𝑁 + 𝐾) ∈ ℤ)
4842nn0zd 12304 . . 3 (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺𝑖)) ∈ ℤ)
49 eqid 2738 . . . . . 6 1 = 1
50 1p0e1 11978 . . . . . 6 (1 + 0) = 1
5149, 50eqtr4i 2769 . . . . 5 1 = (1 + 0)
5251a1i 11 . . . 4 (𝜑 → 1 = (1 + 0))
53 0red 10860 . . . . 5 (𝜑 → 0 ∈ ℝ)
5441nn0red 12175 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺𝑖) ∈ ℝ)
559nnge1d 11902 . . . . 5 (𝜑 → 1 ≤ 𝑋)
5641nn0ge0d 12177 . . . . 5 (𝜑 → 0 ≤ Σ𝑖 ∈ (1...𝑋)(𝐺𝑖))
5728, 53, 22, 54, 55, 56le2addd 11475 . . . 4 (𝜑 → (1 + 0) ≤ (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺𝑖)))
5852, 57eqbrtrd 5089 . . 3 (𝜑 → 1 ≤ (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺𝑖)))
5945nn0red 12175 . . . . 5 (𝜑𝑁 ∈ ℝ)
60 fzfid 13570 . . . . . . . . . 10 (𝜑 → ((𝑋 + 1)...(𝐾 + 1)) ∈ Fin)
6144adantr 484 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ∈ ℤ)
6214peano2zd 12309 . . . . . . . . . . . . 13 (𝜑 → (𝐾 + 1) ∈ ℤ)
6362adantr 484 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝐾 + 1) ∈ ℤ)
64 elfzelz 13136 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1)) → 𝑖 ∈ ℤ)
6564adantl 485 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ∈ ℤ)
6628adantr 484 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ∈ ℝ)
6722adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑋 ∈ ℝ)
6867, 66readdcld 10886 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝑋 + 1) ∈ ℝ)
6965zred 12306 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ∈ ℝ)
7055adantr 484 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ≤ 𝑋)
7167lep1d 11787 . . . . . . . . . . . . . 14 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑋 ≤ (𝑋 + 1))
7266, 67, 68, 70, 71letrd 11013 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ≤ (𝑋 + 1))
73 elfzle1 13139 . . . . . . . . . . . . . 14 (𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1)) → (𝑋 + 1) ≤ 𝑖)
7473adantl 485 . . . . . . . . . . . . 13 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝑋 + 1) ≤ 𝑖)
7566, 68, 69, 72, 74letrd 11013 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 1 ≤ 𝑖)
76 elfzle2 13140 . . . . . . . . . . . . 13 (𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1)) → 𝑖 ≤ (𝐾 + 1))
7776adantl 485 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ≤ (𝐾 + 1))
7861, 63, 65, 75, 77elfzd 13127 . . . . . . . . . . 11 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → 𝑖 ∈ (1...(𝐾 + 1)))
7937ffvelrnda 6922 . . . . . . . . . . . 12 ((𝜑𝑖 ∈ (1...(𝐾 + 1))) → (𝐺𝑖) ∈ ℕ0)
8079adantlr 715 . . . . . . . . . . 11 (((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) ∧ 𝑖 ∈ (1...(𝐾 + 1))) → (𝐺𝑖) ∈ ℕ0)
8178, 80mpdan 687 . . . . . . . . . 10 ((𝜑𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))) → (𝐺𝑖) ∈ ℕ0)
8260, 81fsumnn0cl 15324 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺𝑖) ∈ ℕ0)
8382nn0ge0d 12177 . . . . . . . 8 (𝜑 → 0 ≤ Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺𝑖))
8482nn0red 12175 . . . . . . . . 9 (𝜑 → Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺𝑖) ∈ ℝ)
8554, 84addge01d 11444 . . . . . . . 8 (𝜑 → (0 ≤ Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺𝑖) ↔ Σ𝑖 ∈ (1...𝑋)(𝐺𝑖) ≤ (Σ𝑖 ∈ (1...𝑋)(𝐺𝑖) + Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺𝑖))))
8683, 85mpbid 235 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺𝑖) ≤ (Σ𝑖 ∈ (1...𝑋)(𝐺𝑖) + Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺𝑖)))
8722ltp1d 11786 . . . . . . . . 9 (𝜑𝑋 < (𝑋 + 1))
88 fzdisj 13163 . . . . . . . . 9 (𝑋 < (𝑋 + 1) → ((1...𝑋) ∩ ((𝑋 + 1)...(𝐾 + 1))) = ∅)
8987, 88syl 17 . . . . . . . 8 (𝜑 → ((1...𝑋) ∩ ((𝑋 + 1)...(𝐾 + 1))) = ∅)
9010nn0zd 12304 . . . . . . . . . 10 (𝜑𝑋 ∈ ℤ)
9144, 62, 90, 55, 33elfzd 13127 . . . . . . . . 9 (𝜑𝑋 ∈ (1...(𝐾 + 1)))
92 fzsplit 13162 . . . . . . . . 9 (𝑋 ∈ (1...(𝐾 + 1)) → (1...(𝐾 + 1)) = ((1...𝑋) ∪ ((𝑋 + 1)...(𝐾 + 1))))
9391, 92syl 17 . . . . . . . 8 (𝜑 → (1...(𝐾 + 1)) = ((1...𝑋) ∪ ((𝑋 + 1)...(𝐾 + 1))))
94 fzfid 13570 . . . . . . . 8 (𝜑 → (1...(𝐾 + 1)) ∈ Fin)
95 nn0cn 12124 . . . . . . . . 9 ((𝐺𝑖) ∈ ℕ0 → (𝐺𝑖) ∈ ℂ)
9679, 95syl 17 . . . . . . . 8 ((𝜑𝑖 ∈ (1...(𝐾 + 1))) → (𝐺𝑖) ∈ ℂ)
9789, 93, 94, 96fsumsplit 15329 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺𝑖) = (Σ𝑖 ∈ (1...𝑋)(𝐺𝑖) + Σ𝑖 ∈ ((𝑋 + 1)...(𝐾 + 1))(𝐺𝑖)))
9886, 97breqtrrd 5095 . . . . . 6 (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺𝑖) ≤ Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺𝑖))
99 sticksstones7.6 . . . . . . 7 (𝜑 → Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺𝑖) = 𝑁)
10099eqcomd 2744 . . . . . 6 (𝜑𝑁 = Σ𝑖 ∈ (1...(𝐾 + 1))(𝐺𝑖))
10198, 100breqtrrd 5095 . . . . 5 (𝜑 → Σ𝑖 ∈ (1...𝑋)(𝐺𝑖) ≤ 𝑁)
10222, 54, 27, 59, 31, 101le2addd 11475 . . . 4 (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺𝑖)) ≤ (𝐾 + 𝑁))
10313nn0cnd 12176 . . . . 5 (𝜑𝐾 ∈ ℂ)
10445nn0cnd 12176 . . . . 5 (𝜑𝑁 ∈ ℂ)
105103, 104addcomd 11058 . . . 4 (𝜑 → (𝐾 + 𝑁) = (𝑁 + 𝐾))
106102, 105breqtrd 5093 . . 3 (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺𝑖)) ≤ (𝑁 + 𝐾))
10744, 47, 48, 58, 106elfzd 13127 . 2 (𝜑 → (𝑋 + Σ𝑖 ∈ (1...𝑋)(𝐺𝑖)) ∈ (1...(𝑁 + 𝐾)))
10843, 107eqeltrd 2839 1 (𝜑 → (𝐹𝑋) ∈ (1...(𝑁 + 𝐾)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1543  wcel 2111  cun 3878  cin 3879  c0 4251   class class class wbr 5067  cmpt 5149  wf 6393  cfv 6397  (class class class)co 7231  cc 10751  cr 10752  0cc0 10753  1c1 10754   + caddc 10756   < clt 10891  cle 10892  cn 11854  0cn0 12114  cz 12200  ...cfz 13119  Σcsu 15273
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5272  ax-pr 5336  ax-un 7541  ax-inf2 9280  ax-cnex 10809  ax-resscn 10810  ax-1cn 10811  ax-icn 10812  ax-addcl 10813  ax-addrcl 10814  ax-mulcl 10815  ax-mulrcl 10816  ax-mulcom 10817  ax-addass 10818  ax-mulass 10819  ax-distr 10820  ax-i2m1 10821  ax-1ne0 10822  ax-1rid 10823  ax-rnegex 10824  ax-rrecex 10825  ax-cnre 10826  ax-pre-lttri 10827  ax-pre-lttrn 10828  ax-pre-ltadd 10829  ax-pre-mulgt0 10830  ax-pre-sup 10831
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2072  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3067  df-rex 3068  df-reu 3069  df-rmo 3070  df-rab 3071  df-v 3422  df-sbc 3709  df-csb 3826  df-dif 3883  df-un 3885  df-in 3887  df-ss 3897  df-pss 3899  df-nul 4252  df-if 4454  df-pw 4529  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4834  df-int 4874  df-iun 4920  df-br 5068  df-opab 5130  df-mpt 5150  df-tr 5176  df-id 5469  df-eprel 5474  df-po 5482  df-so 5483  df-fr 5523  df-se 5524  df-we 5525  df-xp 5571  df-rel 5572  df-cnv 5573  df-co 5574  df-dm 5575  df-rn 5576  df-res 5577  df-ima 5578  df-pred 6175  df-ord 6233  df-on 6234  df-lim 6235  df-suc 6236  df-iota 6355  df-fun 6399  df-fn 6400  df-f 6401  df-f1 6402  df-fo 6403  df-f1o 6404  df-fv 6405  df-isom 6406  df-riota 7188  df-ov 7234  df-oprab 7235  df-mpo 7236  df-om 7663  df-1st 7779  df-2nd 7780  df-wrecs 8067  df-recs 8128  df-rdg 8166  df-1o 8222  df-er 8411  df-en 8647  df-dom 8648  df-sdom 8649  df-fin 8650  df-sup 9082  df-oi 9150  df-card 9579  df-pnf 10893  df-mnf 10894  df-xr 10895  df-ltxr 10896  df-le 10897  df-sub 11088  df-neg 11089  df-div 11514  df-nn 11855  df-2 11917  df-3 11918  df-n0 12115  df-z 12201  df-uz 12463  df-rp 12611  df-fz 13120  df-fzo 13263  df-seq 13599  df-exp 13660  df-hash 13921  df-cj 14686  df-re 14687  df-im 14688  df-sqrt 14822  df-abs 14823  df-clim 15073  df-sum 15274
This theorem is referenced by:  sticksstones8  39860
  Copyright terms: Public domain W3C validator