Theorem metakunt26

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

	Ref	Expression
Hypotheses	metakunt26.1	$$⊢\phi \to M\in \mathbb{N}$$
	metakunt26.2	$$⊢\phi \to I\in \mathbb{N}$$
	metakunt26.3	$$⊢\phi \to I\le M$$
	metakunt26.4	$$⊢A=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
	metakunt26.5	$$⊢C=\left(y\in \left(1\dots M\right)⟼if\left(y=M,I,if\left(y<I,y,y+1\right)\right)\right)$$
	metakunt26.6	$$⊢B=\left(z\in \left(1\dots M\right)⟼if\left(z=M,M,if\left(z<I,z+M-I,z+1-I\right)\right)\right)$$
	metakunt26.7	$$⊢\phi \to X=I$$
Assertion	metakunt26	$$⊢\phi \to C\left(B\left(A\left(X\right)\right)\right)=X$$

Proof

Step	Hyp	Ref	Expression
1		metakunt26.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt26.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt26.3	$$⊢\phi \to I\le M$$
4		metakunt26.4	$$⊢A=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
5		metakunt26.5	$$⊢C=\left(y\in \left(1\dots M\right)⟼if\left(y=M,I,if\left(y<I,y,y+1\right)\right)\right)$$
6		metakunt26.6	$$⊢B=\left(z\in \left(1\dots M\right)⟼if\left(z=M,M,if\left(z<I,z+M-I,z+1-I\right)\right)\right)$$
7		metakunt26.7	$$⊢\phi \to X=I$$
8	4	a1i	$$⊢\phi \to A=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
9	7	eqeq2d	$$⊢\phi \to \left(x=X\leftrightarrow x=I\right)$$
10		simpr	$$⊢\left(\phi \wedge x=I\right)\to x=I$$
11	10	iftrued	$$⊢\left(\phi \wedge x=I\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=M$$
12	11	ex	$$⊢\phi \to \left(x=I\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=M\right)$$
13	9 12	sylbid	$$⊢\phi \to \left(x=X\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=M\right)$$
14	13	imp	$$⊢\left(\phi \wedge x=X\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=M$$
15		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
16		nnz	$$⊢M\in \mathbb{N}\to M\in \mathbb{Z}$$
17	1 16	syl	$$⊢\phi \to M\in \mathbb{Z}$$
18	2	nnzd	$$⊢\phi \to I\in \mathbb{Z}$$
19	2	nnge1d	$$⊢\phi \to 1\le I$$
20	15 17 18 19 3	elfzd	$$⊢\phi \to I\in \left(1\dots M\right)$$
21	7	eleq1d	$$⊢\phi \to \left(X\in \left(1\dots M\right)\leftrightarrow I\in \left(1\dots M\right)\right)$$
22	20 21	mpbird	$$⊢\phi \to X\in \left(1\dots M\right)$$
23	8 14 22 1	fvmptd	$$⊢\phi \to A\left(X\right)=M$$
24	23	fveq2d	$$⊢\phi \to B\left(A\left(X\right)\right)=B\left(M\right)$$
25	6	a1i	$$⊢\phi \to B=\left(z\in \left(1\dots M\right)⟼if\left(z=M,M,if\left(z<I,z+M-I,z+1-I\right)\right)\right)$$
26		simpr	$$⊢\left(\phi \wedge z=M\right)\to z=M$$
27	26	iftrued	$$⊢\left(\phi \wedge z=M\right)\to if\left(z=M,M,if\left(z<I,z+M-I,z+1-I\right)\right)=M$$
28		1zzd	$$⊢M\in \mathbb{N}\to 1\in \mathbb{Z}$$
29		nnge1	$$⊢M\in \mathbb{N}\to 1\le M$$
30		nnre	$$⊢M\in \mathbb{N}\to M\in ℝ$$
31	30	leidd	$$⊢M\in \mathbb{N}\to M\le M$$
32	28 16 16 29 31	elfzd	$$⊢M\in \mathbb{N}\to M\in \left(1\dots M\right)$$
33	1 32	syl	$$⊢\phi \to M\in \left(1\dots M\right)$$
34	25 27 33 1	fvmptd	$$⊢\phi \to B\left(M\right)=M$$
35	24 34	eqtrd	$$⊢\phi \to B\left(A\left(X\right)\right)=M$$
36	35	fveq2d	$$⊢\phi \to C\left(B\left(A\left(X\right)\right)\right)=C\left(M\right)$$
37	5	a1i	$$⊢\phi \to C=\left(y\in \left(1\dots M\right)⟼if\left(y=M,I,if\left(y<I,y,y+1\right)\right)\right)$$
38		simpr	$$⊢\left(\phi \wedge y=M\right)\to y=M$$
39	38	iftrued	$$⊢\left(\phi \wedge y=M\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=I$$
40	37 39 33 2	fvmptd	$$⊢\phi \to C\left(M\right)=I$$
41	36 40	eqtrd	$$⊢\phi \to C\left(B\left(A\left(X\right)\right)\right)=I$$
42	7	eqcomd	$$⊢\phi \to I=X$$
43	41 42	eqtrd	$$⊢\phi \to C\left(B\left(A\left(X\right)\right)\right)=X$$