Theorem metakunt32

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024)

	Ref	Expression
Hypotheses	metakunt32.1	$$⊢\phi \to M\in \mathbb{N}$$
	metakunt32.2	$$⊢\phi \to I\in \mathbb{N}$$
	metakunt32.3	$$⊢\phi \to I\le M$$
	metakunt32.4	$$⊢\phi \to X\in \left(1\dots M\right)$$
	metakunt32.5	$$⊢D=\left(x\in \left(1\dots M\right)⟼if\left(x=I,x,if\left(x<I,x+\left(M-I\right)+if\left(I\le x+M-I,1,0\right),x-I+if\left(I\le x-I,1,0\right)\right)\right)\right)$$
	metakunt32.6	$$⊢G=if\left(I\le X+M-I,1,0\right)$$
	metakunt32.7	$$⊢H=if\left(I\le X-I,1,0\right)$$
	metakunt32.8	$$⊢R=if\left(X=I,X,if\left(X<I,X+\left(M-I\right)+G,X-I+H\right)\right)$$
Assertion	metakunt32	$$⊢\phi \to D\left(X\right)=R$$

Proof

Step	Hyp	Ref	Expression
1		metakunt32.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt32.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt32.3	$$⊢\phi \to I\le M$$
4		metakunt32.4	$$⊢\phi \to X\in \left(1\dots M\right)$$
5		metakunt32.5	$$⊢D=\left(x\in \left(1\dots M\right)⟼if\left(x=I,x,if\left(x<I,x+\left(M-I\right)+if\left(I\le x+M-I,1,0\right),x-I+if\left(I\le x-I,1,0\right)\right)\right)\right)$$
6		metakunt32.6	$$⊢G=if\left(I\le X+M-I,1,0\right)$$
7		metakunt32.7	$$⊢H=if\left(I\le X-I,1,0\right)$$
8		metakunt32.8	$$⊢R=if\left(X=I,X,if\left(X<I,X+\left(M-I\right)+G,X-I+H\right)\right)$$
9	5	a1i	$$⊢\phi \to D=\left(x\in \left(1\dots M\right)⟼if\left(x=I,x,if\left(x<I,x+\left(M-I\right)+if\left(I\le x+M-I,1,0\right),x-I+if\left(I\le x-I,1,0\right)\right)\right)\right)$$
10		simpr	$$⊢\left(\phi \wedge x=X\right)\to x=X$$
11	10	eqeq1d	$$⊢\left(\phi \wedge x=X\right)\to \left(x=I\leftrightarrow X=I\right)$$
12	10	breq1d	$$⊢\left(\phi \wedge x=X\right)\to \left(x<I\leftrightarrow X<I\right)$$
13		oveq1	$$⊢x=X\to x+M-I=X+M-I$$
14	13	adantl	$$⊢\left(\phi \wedge x=X\right)\to x+M-I=X+M-I$$
15	14	breq2d	$$⊢\left(\phi \wedge x=X\right)\to \left(I\le x+M-I\leftrightarrow I\le X+M-I\right)$$
16	15	ifbid	$$⊢\left(\phi \wedge x=X\right)\to if\left(I\le x+M-I,1,0\right)=if\left(I\le X+M-I,1,0\right)$$
17	14 16	oveq12d	$$⊢\left(\phi \wedge x=X\right)\to x+\left(M-I\right)+if\left(I\le x+M-I,1,0\right)=X+\left(M-I\right)+if\left(I\le X+M-I,1,0\right)$$
18	6	a1i	$$⊢\left(\phi \wedge x=X\right)\to G=if\left(I\le X+M-I,1,0\right)$$
19	18	eqcomd	$$⊢\left(\phi \wedge x=X\right)\to if\left(I\le X+M-I,1,0\right)=G$$
20	19	oveq2d	$$⊢\left(\phi \wedge x=X\right)\to X+\left(M-I\right)+if\left(I\le X+M-I,1,0\right)=X+\left(M-I\right)+G$$
21	17 20	eqtrd	$$⊢\left(\phi \wedge x=X\right)\to x+\left(M-I\right)+if\left(I\le x+M-I,1,0\right)=X+\left(M-I\right)+G$$
22	10	oveq1d	$$⊢\left(\phi \wedge x=X\right)\to x-I=X-I$$
23	22	breq2d	$$⊢\left(\phi \wedge x=X\right)\to \left(I\le x-I\leftrightarrow I\le X-I\right)$$
24	23	ifbid	$$⊢\left(\phi \wedge x=X\right)\to if\left(I\le x-I,1,0\right)=if\left(I\le X-I,1,0\right)$$
25	22 24	oveq12d	$$⊢\left(\phi \wedge x=X\right)\to x-I+if\left(I\le x-I,1,0\right)=X-I+if\left(I\le X-I,1,0\right)$$
26	7	a1i	$$⊢\left(\phi \wedge x=X\right)\to H=if\left(I\le X-I,1,0\right)$$
27	26	eqcomd	$$⊢\left(\phi \wedge x=X\right)\to if\left(I\le X-I,1,0\right)=H$$
28	27	oveq2d	$$⊢\left(\phi \wedge x=X\right)\to X-I+if\left(I\le X-I,1,0\right)=X-I+H$$
29	25 28	eqtrd	$$⊢\left(\phi \wedge x=X\right)\to x-I+if\left(I\le x-I,1,0\right)=X-I+H$$
30	12 21 29	ifbieq12d	$$⊢\left(\phi \wedge x=X\right)\to if\left(x<I,x+\left(M-I\right)+if\left(I\le x+M-I,1,0\right),x-I+if\left(I\le x-I,1,0\right)\right)=if\left(X<I,X+\left(M-I\right)+G,X-I+H\right)$$
31	11 10 30	ifbieq12d	$$⊢\left(\phi \wedge x=X\right)\to if\left(x=I,x,if\left(x<I,x+\left(M-I\right)+if\left(I\le x+M-I,1,0\right),x-I+if\left(I\le x-I,1,0\right)\right)\right)=if\left(X=I,X,if\left(X<I,X+\left(M-I\right)+G,X-I+H\right)\right)$$
32	8	a1i	$$⊢\left(\phi \wedge x=X\right)\to R=if\left(X=I,X,if\left(X<I,X+\left(M-I\right)+G,X-I+H\right)\right)$$
33	32	eqcomd	$$⊢\left(\phi \wedge x=X\right)\to if\left(X=I,X,if\left(X<I,X+\left(M-I\right)+G,X-I+H\right)\right)=R$$
34	31 33	eqtrd	$$⊢\left(\phi \wedge x=X\right)\to if\left(x=I,x,if\left(x<I,x+\left(M-I\right)+if\left(I\le x+M-I,1,0\right),x-I+if\left(I\le x-I,1,0\right)\right)\right)=R$$
35	4	elfzelzd	$$⊢\phi \to X\in \mathbb{Z}$$
36	1	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
37	2	nnzd	$$⊢\phi \to I\in \mathbb{Z}$$
38	36 37	zsubcld	$$⊢\phi \to M-I\in \mathbb{Z}$$
39	35 38	zaddcld	$$⊢\phi \to X+M-I\in \mathbb{Z}$$
40		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
41		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
42	40 41	ifcld	$$⊢\phi \to if\left(I\le X+M-I,1,0\right)\in \mathbb{Z}$$
43	6	a1i	$$⊢\phi \to G=if\left(I\le X+M-I,1,0\right)$$
44	43	eleq1d	$$⊢\phi \to \left(G\in \mathbb{Z}\leftrightarrow if\left(I\le X+M-I,1,0\right)\in \mathbb{Z}\right)$$
45	42 44	mpbird	$$⊢\phi \to G\in \mathbb{Z}$$
46	39 45	zaddcld	$$⊢\phi \to X+\left(M-I\right)+G\in \mathbb{Z}$$
47	35 37	zsubcld	$$⊢\phi \to X-I\in \mathbb{Z}$$
48	40 41	ifcld	$$⊢\phi \to if\left(I\le X-I,1,0\right)\in \mathbb{Z}$$
49	7	a1i	$$⊢\phi \to H=if\left(I\le X-I,1,0\right)$$
50	49	eleq1d	$$⊢\phi \to \left(H\in \mathbb{Z}\leftrightarrow if\left(I\le X-I,1,0\right)\in \mathbb{Z}\right)$$
51	48 50	mpbird	$$⊢\phi \to H\in \mathbb{Z}$$
52	47 51	zaddcld	$$⊢\phi \to X-I+H\in \mathbb{Z}$$
53	46 52	ifcld	$$⊢\phi \to if\left(X<I,X+\left(M-I\right)+G,X-I+H\right)\in \mathbb{Z}$$
54	35 53	ifcld	$$⊢\phi \to if\left(X=I,X,if\left(X<I,X+\left(M-I\right)+G,X-I+H\right)\right)\in \mathbb{Z}$$
55	8	a1i	$$⊢\phi \to R=if\left(X=I,X,if\left(X<I,X+\left(M-I\right)+G,X-I+H\right)\right)$$
56	55	eleq1d	$$⊢\phi \to \left(R\in \mathbb{Z}\leftrightarrow if\left(X=I,X,if\left(X<I,X+\left(M-I\right)+G,X-I+H\right)\right)\in \mathbb{Z}\right)$$
57	54 56	mpbird	$$⊢\phi \to R\in \mathbb{Z}$$
58	9 34 4 57	fvmptd	$$⊢\phi \to D\left(X\right)=R$$