sticksstones6

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

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

Proof

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

Metamath Proof Explorer

Theorem sticksstones6

Proof