Theorem metakunt29

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt29.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt29.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt29.3	$$⊢\phi \to I\le M$$
4		metakunt29.4	$$⊢\phi \to X\in \left(1\dots M\right)$$
5		metakunt29.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		metakunt29.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		metakunt29.7	$$⊢\phi \to \neg X=I$$
8		metakunt29.8	$$⊢\phi \to X<I$$
9		metakunt29.9	$$⊢C=\left(y\in \left(1\dots M\right)⟼if\left(y=M,I,if\left(y<I,y,y+1\right)\right)\right)$$
10		metakunt29.10	$$⊢H=if\left(I\le X+M-I,1,0\right)$$
11	1 2 3 4 5 6 7 8	metakunt27	$$⊢\phi \to B\left(A\left(X\right)\right)=X+M-I$$
12	11	fveq2d	$$⊢\phi \to C\left(B\left(A\left(X\right)\right)\right)=C\left(X+M-I\right)$$
13	9	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)$$
14		elfznn	$$⊢X\in \left(1\dots M\right)\to X\in \mathbb{N}$$
15	4 14	syl	$$⊢\phi \to X\in \mathbb{N}$$
16		nnre	$$⊢X\in \mathbb{N}\to X\in ℝ$$
17	15 16	syl	$$⊢\phi \to X\in ℝ$$
18	1	nnred	$$⊢\phi \to M\in ℝ$$
19	2	nnred	$$⊢\phi \to I\in ℝ$$
20	18 19	resubcld	$$⊢\phi \to M-I\in ℝ$$
21	17 20	readdcld	$$⊢\phi \to X+M-I\in ℝ$$
22	17	recnd	$$⊢\phi \to X\in ℂ$$
23	18	recnd	$$⊢\phi \to M\in ℂ$$
24	19	recnd	$$⊢\phi \to I\in ℂ$$
25	22 23 24	addsub12d	$$⊢\phi \to X+M-I=M+X-I$$
26	23 24 22	subsub2d	$$⊢\phi \to M-\left(I-X\right)=M+X-I$$
27	19 17	resubcld	$$⊢\phi \to I-X\in ℝ$$
28	17 19	posdifd	$$⊢\phi \to \left(X<I\leftrightarrow 0<I-X\right)$$
29	8 28	mpbid	$$⊢\phi \to 0<I-X$$
30	27 29	elrpd	$$⊢\phi \to I-X\in {ℝ}^{+}$$
31	18 30	ltsubrpd	$$⊢\phi \to M-\left(I-X\right)<M$$
32	26 31	eqbrtrrd	$$⊢\phi \to M+X-I<M$$
33	25 32	eqbrtrd	$$⊢\phi \to X+M-I<M$$
34	21 33	ltned	$$⊢\phi \to X+M-I\ne M$$
35	34	adantr	$$⊢\left(\phi \wedge y=X+M-I\right)\to X+M-I\ne M$$
36		simpr	$$⊢\left(\phi \wedge y=X+M-I\right)\to y=X+M-I$$
37	36	neeq1d	$$⊢\left(\phi \wedge y=X+M-I\right)\to \left(y\ne M\leftrightarrow X+M-I\ne M\right)$$
38	35 37	mpbird	$$⊢\left(\phi \wedge y=X+M-I\right)\to y\ne M$$
39	38	neneqd	$$⊢\left(\phi \wedge y=X+M-I\right)\to \neg y=M$$
40	39	iffalsed	$$⊢\left(\phi \wedge y=X+M-I\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=if\left(y<I,y,y+1\right)$$
41		simpr	$$⊢\left(\phi \wedge I\le X+M-I\right)\to I\le X+M-I$$
42	19	adantr	$$⊢\left(\phi \wedge I\le X+M-I\right)\to I\in ℝ$$
43	17	adantr	$$⊢\left(\phi \wedge I\le X+M-I\right)\to X\in ℝ$$
44	18	adantr	$$⊢\left(\phi \wedge I\le X+M-I\right)\to M\in ℝ$$
45	44 42	resubcld	$$⊢\left(\phi \wedge I\le X+M-I\right)\to M-I\in ℝ$$
46	43 45	readdcld	$$⊢\left(\phi \wedge I\le X+M-I\right)\to X+M-I\in ℝ$$
47	42 46	lenltd	$$⊢\left(\phi \wedge I\le X+M-I\right)\to \left(I\le X+M-I\leftrightarrow \neg X+M-I<I\right)$$
48	41 47	mpbid	$$⊢\left(\phi \wedge I\le X+M-I\right)\to \neg X+M-I<I$$
49	48	3adant2	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to \neg X+M-I<I$$
50		simp2	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to y=X+M-I$$
51	50	breq1d	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to \left(y<I\leftrightarrow X+M-I<I\right)$$
52	51	notbid	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to \left(\neg y<I\leftrightarrow \neg X+M-I<I\right)$$
53	49 52	mpbird	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to \neg y<I$$
54	53	iffalsed	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to if\left(y<I,y,y+1\right)=y+1$$
55	50	oveq1d	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to y+1=X+\left(M-I\right)+1$$
56	54 55	eqtrd	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to if\left(y<I,y,y+1\right)=X+\left(M-I\right)+1$$
57		simp3	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to I\le X+M-I$$
58	57	iftrued	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to if\left(I\le X+M-I,1,0\right)=1$$
59	58	eqcomd	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to 1=if\left(I\le X+M-I,1,0\right)$$
60	59 10	eqtr4di	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to 1=H$$
61	60	oveq2d	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to X+\left(M-I\right)+1=X+\left(M-I\right)+H$$
62	56 61	eqtrd	$$⊢\left(\phi \wedge y=X+M-I\wedge I\le X+M-I\right)\to if\left(y<I,y,y+1\right)=X+\left(M-I\right)+H$$
63	62	3expa	$$⊢\left(\left(\phi \wedge y=X+M-I\right)\wedge I\le X+M-I\right)\to if\left(y<I,y,y+1\right)=X+\left(M-I\right)+H$$
64	21 19	ltnled	$$⊢\phi \to \left(X+M-I<I\leftrightarrow \neg I\le X+M-I\right)$$
65	64	biimprd	$$⊢\phi \to \left(\neg I\le X+M-I\to X+M-I<I\right)$$
66	65	imp	$$⊢\left(\phi \wedge \neg I\le X+M-I\right)\to X+M-I<I$$
67	66	3adant2	$$⊢\left(\phi \wedge y=X+M-I\wedge \neg I\le X+M-I\right)\to X+M-I<I$$
68		simp2	$$⊢\left(\phi \wedge y=X+M-I\wedge \neg I\le X+M-I\right)\to y=X+M-I$$
69	68	breq1d	$$⊢\left(\phi \wedge y=X+M-I\wedge \neg I\le X+M-I\right)\to \left(y<I\leftrightarrow X+M-I<I\right)$$
70	67 69	mpbird	$$⊢\left(\phi \wedge y=X+M-I\wedge \neg I\le X+M-I\right)\to y<I$$
71	70	iftrued	$$⊢\left(\phi \wedge y=X+M-I\wedge \neg I\le X+M-I\right)\to if\left(y<I,y,y+1\right)=y$$
72	22	adantr	$$⊢\left(\phi \wedge X+M-I<I\right)\to X\in ℂ$$
73	23	adantr	$$⊢\left(\phi \wedge X+M-I<I\right)\to M\in ℂ$$
74	24	adantr	$$⊢\left(\phi \wedge X+M-I<I\right)\to I\in ℂ$$
75	73 74	subcld	$$⊢\left(\phi \wedge X+M-I<I\right)\to M-I\in ℂ$$
76	72 75	addcld	$$⊢\left(\phi \wedge X+M-I<I\right)\to X+M-I\in ℂ$$
77	76	addid1d	$$⊢\left(\phi \wedge X+M-I<I\right)\to X+\left(M-I\right)+0=X+M-I$$
78	77	eqcomd	$$⊢\left(\phi \wedge X+M-I<I\right)\to X+M-I=X+\left(M-I\right)+0$$
79	64	biimpa	$$⊢\left(\phi \wedge X+M-I<I\right)\to \neg I\le X+M-I$$
80	79	iffalsed	$$⊢\left(\phi \wedge X+M-I<I\right)\to if\left(I\le X+M-I,1,0\right)=0$$
81	80	eqcomd	$$⊢\left(\phi \wedge X+M-I<I\right)\to 0=if\left(I\le X+M-I,1,0\right)$$
82	10	a1i	$$⊢\left(\phi \wedge X+M-I<I\right)\to H=if\left(I\le X+M-I,1,0\right)$$
83	82	eqcomd	$$⊢\left(\phi \wedge X+M-I<I\right)\to if\left(I\le X+M-I,1,0\right)=H$$
84	81 83	eqtrd	$$⊢\left(\phi \wedge X+M-I<I\right)\to 0=H$$
85	84	oveq2d	$$⊢\left(\phi \wedge X+M-I<I\right)\to X+\left(M-I\right)+0=X+\left(M-I\right)+H$$
86	78 85	eqtrd	$$⊢\left(\phi \wedge X+M-I<I\right)\to X+M-I=X+\left(M-I\right)+H$$
87	86	ex	$$⊢\phi \to \left(X+M-I<I\to X+M-I=X+\left(M-I\right)+H\right)$$
88	65 87	syld	$$⊢\phi \to \left(\neg I\le X+M-I\to X+M-I=X+\left(M-I\right)+H\right)$$
89	88	imp	$$⊢\left(\phi \wedge \neg I\le X+M-I\right)\to X+M-I=X+\left(M-I\right)+H$$
90	89	3adant2	$$⊢\left(\phi \wedge y=X+M-I\wedge \neg I\le X+M-I\right)\to X+M-I=X+\left(M-I\right)+H$$
91	68 90	eqtrd	$$⊢\left(\phi \wedge y=X+M-I\wedge \neg I\le X+M-I\right)\to y=X+\left(M-I\right)+H$$
92	71 91	eqtrd	$$⊢\left(\phi \wedge y=X+M-I\wedge \neg I\le X+M-I\right)\to if\left(y<I,y,y+1\right)=X+\left(M-I\right)+H$$
93	92	3expa	$$⊢\left(\left(\phi \wedge y=X+M-I\right)\wedge \neg I\le X+M-I\right)\to if\left(y<I,y,y+1\right)=X+\left(M-I\right)+H$$
94	63 93	pm2.61dan	$$⊢\left(\phi \wedge y=X+M-I\right)\to if\left(y<I,y,y+1\right)=X+\left(M-I\right)+H$$
95	40 94	eqtrd	$$⊢\left(\phi \wedge y=X+M-I\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=X+\left(M-I\right)+H$$
96		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
97	1	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
98	15	nnzd	$$⊢\phi \to X\in \mathbb{Z}$$
99	2	nnzd	$$⊢\phi \to I\in \mathbb{Z}$$
100	97 99	zsubcld	$$⊢\phi \to M-I\in \mathbb{Z}$$
101	98 100	zaddcld	$$⊢\phi \to X+M-I\in \mathbb{Z}$$
102		1p0e1	$$⊢1+0=1$$
103		1red	$$⊢\phi \to 1\in ℝ$$
104		0red	$$⊢\phi \to 0\in ℝ$$
105	15	nnge1d	$$⊢\phi \to 1\le X$$
106	18 19	subge0d	$$⊢\phi \to \left(0\le M-I\leftrightarrow I\le M\right)$$
107	3 106	mpbird	$$⊢\phi \to 0\le M-I$$
108	103 104 17 20 105 107	le2addd	$$⊢\phi \to 1+0\le X+M-I$$
109	102 108	eqbrtrrid	$$⊢\phi \to 1\le X+M-I$$
110	21 18 33	ltled	$$⊢\phi \to X+M-I\le M$$
111	96 97 101 109 110	elfzd	$$⊢\phi \to X+M-I\in \left(1\dots M\right)$$
112	111	elfzelzd	$$⊢\phi \to X+M-I\in \mathbb{Z}$$
113		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
114	96 113	ifcld	$$⊢\phi \to if\left(I\le X+M-I,1,0\right)\in \mathbb{Z}$$
115	10	a1i	$$⊢\phi \to H=if\left(I\le X+M-I,1,0\right)$$
116	115	eleq1d	$$⊢\phi \to \left(H\in \mathbb{Z}\leftrightarrow if\left(I\le X+M-I,1,0\right)\in \mathbb{Z}\right)$$
117	114 116	mpbird	$$⊢\phi \to H\in \mathbb{Z}$$
118	112 117	zaddcld	$$⊢\phi \to X+\left(M-I\right)+H\in \mathbb{Z}$$
119	13 95 111 118	fvmptd	$$⊢\phi \to C\left(X+M-I\right)=X+\left(M-I\right)+H$$
120	12 119	eqtrd	$$⊢\phi \to C\left(B\left(A\left(X\right)\right)\right)=X+\left(M-I\right)+H$$