Theorem metakunt28

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt28.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt28.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt28.3	$$⊢\phi \to I\le M$$
4		metakunt28.4	$$⊢\phi \to X\in \left(1\dots M\right)$$
5		metakunt28.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		metakunt28.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		metakunt28.7	$$⊢\phi \to \neg X=I$$
8		metakunt28.8	$$⊢\phi \to \neg 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 \neg X<I$$
17	11	breq1d	$$⊢\left(\phi \wedge x=X\right)\to \left(x<I\leftrightarrow X<I\right)$$
18	17	notbid	$$⊢\left(\phi \wedge x=X\right)\to \left(\neg x<I\leftrightarrow \neg X<I\right)$$
19	16 18	mpbird	$$⊢\left(\phi \wedge x=X\right)\to \neg x<I$$
20	19	iffalsed	$$⊢\left(\phi \wedge x=X\right)\to if\left(x<I,x,x-1\right)=x-1$$
21	11	oveq1d	$$⊢\left(\phi \wedge x=X\right)\to x-1=X-1$$
22	20 21	eqtrd	$$⊢\left(\phi \wedge x=X\right)\to if\left(x<I,x,x-1\right)=X-1$$
23	15 22	eqtrd	$$⊢\left(\phi \wedge x=X\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=X-1$$
24	4	elfzelzd	$$⊢\phi \to X\in \mathbb{Z}$$
25		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
26	24 25	zsubcld	$$⊢\phi \to X-1\in \mathbb{Z}$$
27	9 23 4 26	fvmptd	$$⊢\phi \to A\left(X\right)=X-1$$
28	27	fveq2d	$$⊢\phi \to B\left(A\left(X\right)\right)=B\left(X-1\right)$$
29	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)$$
30	26	zred	$$⊢\phi \to X-1\in ℝ$$
31	24	zred	$$⊢\phi \to X\in ℝ$$
32	1	nnred	$$⊢\phi \to M\in ℝ$$
33		1rp	$$⊢1\in {ℝ}^{+}$$
34	33	a1i	$$⊢\phi \to 1\in {ℝ}^{+}$$
35	31 34	ltsubrpd	$$⊢\phi \to X-1<X$$
36		elfzle2	$$⊢X\in \left(1\dots M\right)\to X\le M$$
37	4 36	syl	$$⊢\phi \to X\le M$$
38	30 31 32 35 37	ltletrd	$$⊢\phi \to X-1<M$$
39	30 38	ltned	$$⊢\phi \to X-1\ne M$$
40	39	adantr	$$⊢\left(\phi \wedge z=X-1\right)\to X-1\ne M$$
41	40	neneqd	$$⊢\left(\phi \wedge z=X-1\right)\to \neg X-1=M$$
42		simpr	$$⊢\left(\phi \wedge z=X-1\right)\to z=X-1$$
43	42	eqeq1d	$$⊢\left(\phi \wedge z=X-1\right)\to \left(z=M\leftrightarrow X-1=M\right)$$
44	43	notbid	$$⊢\left(\phi \wedge z=X-1\right)\to \left(\neg z=M\leftrightarrow \neg X-1=M\right)$$
45	41 44	mpbird	$$⊢\left(\phi \wedge z=X-1\right)\to \neg z=M$$
46	45	iffalsed	$$⊢\left(\phi \wedge z=X-1\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)$$
47	7	neqned	$$⊢\phi \to X\ne I$$
48	2	nnred	$$⊢\phi \to I\in ℝ$$
49	48 31 8	nltled	$$⊢\phi \to I\le X$$
50	48 31 49	leltned	$$⊢\phi \to \left(I<X\leftrightarrow X\ne I\right)$$
51	47 50	mpbird	$$⊢\phi \to I<X$$
52	2	nnzd	$$⊢\phi \to I\in \mathbb{Z}$$
53	52 24	zltlem1d	$$⊢\phi \to \left(I<X\leftrightarrow I\le X-1\right)$$
54	51 53	mpbid	$$⊢\phi \to I\le X-1$$
55	48 30	lenltd	$$⊢\phi \to \left(I\le X-1\leftrightarrow \neg X-1<I\right)$$
56	54 55	mpbid	$$⊢\phi \to \neg X-1<I$$
57	56	adantr	$$⊢\left(\phi \wedge z=X-1\right)\to \neg X-1<I$$
58	42	breq1d	$$⊢\left(\phi \wedge z=X-1\right)\to \left(z<I\leftrightarrow X-1<I\right)$$
59	58	notbid	$$⊢\left(\phi \wedge z=X-1\right)\to \left(\neg z<I\leftrightarrow \neg X-1<I\right)$$
60	57 59	mpbird	$$⊢\left(\phi \wedge z=X-1\right)\to \neg z<I$$
61	60	iffalsed	$$⊢\left(\phi \wedge z=X-1\right)\to if\left(z<I,z+M-I,z+1-I\right)=z+1-I$$
62	42	oveq1d	$$⊢\left(\phi \wedge z=X-1\right)\to z+1-I=\left(X-1\right)+1-I$$
63	24	zcnd	$$⊢\phi \to X\in ℂ$$
64		1cnd	$$⊢\phi \to 1\in ℂ$$
65	2	nncnd	$$⊢\phi \to I\in ℂ$$
66	63 64 65	npncand	$$⊢\phi \to \left(X-1\right)+1-I=X-I$$
67	66	adantr	$$⊢\left(\phi \wedge z=X-1\right)\to \left(X-1\right)+1-I=X-I$$
68	62 67	eqtrd	$$⊢\left(\phi \wedge z=X-1\right)\to z+1-I=X-I$$
69	61 68	eqtrd	$$⊢\left(\phi \wedge z=X-1\right)\to if\left(z<I,z+M-I,z+1-I\right)=X-I$$
70	46 69	eqtrd	$$⊢\left(\phi \wedge z=X-1\right)\to if\left(z=M,M,if\left(z<I,z+M-I,z+1-I\right)\right)=X-I$$
71	1	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
72		1red	$$⊢\phi \to 1\in ℝ$$
73	2	nnge1d	$$⊢\phi \to 1\le I$$
74	72 48 31 73 51	lelttrd	$$⊢\phi \to 1<X$$
75	25 24	zltlem1d	$$⊢\phi \to \left(1<X\leftrightarrow 1\le X-1\right)$$
76	74 75	mpbid	$$⊢\phi \to 1\le X-1$$
77	31 72	resubcld	$$⊢\phi \to X-1\in ℝ$$
78		0le1	$$⊢0\le 1$$
79	78	a1i	$$⊢\phi \to 0\le 1$$
80	31 72	subge02d	$$⊢\phi \to \left(0\le 1\leftrightarrow X-1\le X\right)$$
81	79 80	mpbid	$$⊢\phi \to X-1\le X$$
82	77 31 32 81 37	letrd	$$⊢\phi \to X-1\le M$$
83	25 71 26 76 82	elfzd	$$⊢\phi \to X-1\in \left(1\dots M\right)$$
84	24 52	zsubcld	$$⊢\phi \to X-I\in \mathbb{Z}$$
85	29 70 83 84	fvmptd	$$⊢\phi \to B\left(X-1\right)=X-I$$
86	28 85	eqtrd	$$⊢\phi \to B\left(A\left(X\right)\right)=X-I$$