Theorem metakunt27

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

	Ref	Expression
Hypotheses	metakunt27.1	$$⊢\phi \to M\in \mathbb{N}$$
	metakunt27.2	$$⊢\phi \to I\in \mathbb{N}$$
	metakunt27.3	$$⊢\phi \to I\le M$$
	metakunt27.4	$$⊢\phi \to X\in \left(1\dots M\right)$$
	metakunt27.5	$$⊢A=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
	metakunt27.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)$$
	metakunt27.7	$$⊢\phi \to \neg X=I$$
	metakunt27.8	$$⊢\phi \to X<I$$
Assertion	metakunt27	$$⊢\phi \to B\left(A\left(X\right)\right)=X+M-I$$

Proof

Step	Hyp	Ref	Expression
1		metakunt27.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt27.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt27.3	$$⊢\phi \to I\le M$$
4		metakunt27.4	$$⊢\phi \to X\in \left(1\dots M\right)$$
5		metakunt27.5	$$⊢A=\left(x\in \left(1\dots M\right)⟼if\left(x=I,M,if\left(x<I,x,x-1\right)\right)\right)$$
6		metakunt27.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		metakunt27.7	$$⊢\phi \to \neg X=I$$
8		metakunt27.8	$$⊢\phi \to X<I$$
9	5	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)$$
10	7	adantr	$$⊢\left(\phi \wedge x=X\right)\to \neg X=I$$
11		simpr	$$⊢\left(\phi \wedge x=X\right)\to x=X$$
12	11	eqeq1d	$$⊢\left(\phi \wedge x=X\right)\to \left(x=I\leftrightarrow X=I\right)$$
13	12	notbid	$$⊢\left(\phi \wedge x=X\right)\to \left(\neg x=I\leftrightarrow \neg X=I\right)$$
14	10 13	mpbird	$$⊢\left(\phi \wedge x=X\right)\to \neg x=I$$
15	14	iffalsed	$$⊢\left(\phi \wedge x=X\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=if\left(x<I,x,x-1\right)$$
16	8	adantr	$$⊢\left(\phi \wedge x=X\right)\to X<I$$
17	11	breq1d	$$⊢\left(\phi \wedge x=X\right)\to \left(x<I\leftrightarrow X<I\right)$$
18	16 17	mpbird	$$⊢\left(\phi \wedge x=X\right)\to x<I$$
19	18	iftrued	$$⊢\left(\phi \wedge x=X\right)\to if\left(x<I,x,x-1\right)=x$$
20	19 11	eqtrd	$$⊢\left(\phi \wedge x=X\right)\to if\left(x<I,x,x-1\right)=X$$
21	15 20	eqtrd	$$⊢\left(\phi \wedge x=X\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=X$$
22	9 21 4 4	fvmptd	$$⊢\phi \to A\left(X\right)=X$$
23	22	fveq2d	$$⊢\phi \to B\left(A\left(X\right)\right)=B\left(X\right)$$
24	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)$$
25		elfznn	$$⊢X\in \left(1\dots M\right)\to X\in \mathbb{N}$$
26	4 25	syl	$$⊢\phi \to X\in \mathbb{N}$$
27	26	nnred	$$⊢\phi \to X\in ℝ$$
28	2	nnred	$$⊢\phi \to I\in ℝ$$
29	1	nnred	$$⊢\phi \to M\in ℝ$$
30	27 28 29 8 3	ltletrd	$$⊢\phi \to X<M$$
31	27 30	ltned	$$⊢\phi \to X\ne M$$
32	31	neneqd	$$⊢\phi \to \neg X=M$$
33	32	adantr	$$⊢\left(\phi \wedge z=X\right)\to \neg X=M$$
34		simpr	$$⊢\left(\phi \wedge z=X\right)\to z=X$$
35	34	eqeq1d	$$⊢\left(\phi \wedge z=X\right)\to \left(z=M\leftrightarrow X=M\right)$$
36	35	notbid	$$⊢\left(\phi \wedge z=X\right)\to \left(\neg z=M\leftrightarrow \neg X=M\right)$$
37	33 36	mpbird	$$⊢\left(\phi \wedge z=X\right)\to \neg z=M$$
38	37	iffalsed	$$⊢\left(\phi \wedge z=X\right)\to if\left(z=M,M,if\left(z<I,z+M-I,z+1-I\right)\right)=if\left(z<I,z+M-I,z+1-I\right)$$
39	8	adantr	$$⊢\left(\phi \wedge z=X\right)\to X<I$$
40	34	breq1d	$$⊢\left(\phi \wedge z=X\right)\to \left(z<I\leftrightarrow X<I\right)$$
41	39 40	mpbird	$$⊢\left(\phi \wedge z=X\right)\to z<I$$
42	41	iftrued	$$⊢\left(\phi \wedge z=X\right)\to if\left(z<I,z+M-I,z+1-I\right)=z+M-I$$
43	34	oveq1d	$$⊢\left(\phi \wedge z=X\right)\to z+M-I=X+M-I$$
44	42 43	eqtrd	$$⊢\left(\phi \wedge z=X\right)\to if\left(z<I,z+M-I,z+1-I\right)=X+M-I$$
45	38 44	eqtrd	$$⊢\left(\phi \wedge z=X\right)\to if\left(z=M,M,if\left(z<I,z+M-I,z+1-I\right)\right)=X+M-I$$
46	4	elfzelzd	$$⊢\phi \to X\in \mathbb{Z}$$
47	1	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
48	2	nnzd	$$⊢\phi \to I\in \mathbb{Z}$$
49	47 48	zsubcld	$$⊢\phi \to M-I\in \mathbb{Z}$$
50	46 49	zaddcld	$$⊢\phi \to X+M-I\in \mathbb{Z}$$
51	24 45 4 50	fvmptd	$$⊢\phi \to B\left(X\right)=X+M-I$$
52	23 51	eqtrd	$$⊢\phi \to B\left(A\left(X\right)\right)=X+M-I$$