sticksstones7

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

	Ref	Expression
Hypotheses	sticksstones7.1	$⊢ φ \to N \in ℕ_{0}$
	sticksstones7.2	$⊢ φ \to K \in ℕ_{0}$
	sticksstones7.3	$⊢ φ \to G : (1 \dots K + 1) ⟶ ℕ_{0}$
	sticksstones7.4	$⊢ φ \to X \in (1 \dots K)$
	sticksstones7.5	$⊢ F = (x \in (1 \dots K) ⟼ x + \sum_{i = 1}^{x} G (i))$
	sticksstones7.6	$⊢ φ \to \sum_{i = 1}^{K + 1} G (i) = N$
Assertion	sticksstones7	$⊢ φ \to F (X) \in (1 \dots N + K)$

Proof

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

Metamath Proof Explorer

Theorem sticksstones7

Proof