Theorem metakunt30

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt30.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt30.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt30.3	$$⊢\phi \to I\le M$$
4		metakunt30.4	$$⊢\phi \to X\in \left(1\dots M\right)$$
5		metakunt30.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		metakunt30.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		metakunt30.7	$$⊢\phi \to \neg X=I$$
8		metakunt30.8	$$⊢\phi \to \neg X<I$$
9		metakunt30.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		metakunt30.10	$$⊢H=if\left(I\le X-I,1,0\right)$$
11	1 2 3 4 5 6 7 8	metakunt28	$$⊢\phi \to B\left(A\left(X\right)\right)=X-I$$
12	11	fveq2d	$$⊢\phi \to C\left(B\left(A\left(X\right)\right)\right)=C\left(X-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	2	nnred	$$⊢\phi \to I\in ℝ$$
19	17 18	resubcld	$$⊢\phi \to X-I\in ℝ$$
20	1	nnred	$$⊢\phi \to M\in ℝ$$
21	20 18	resubcld	$$⊢\phi \to M-I\in ℝ$$
22		elfzle2	$$⊢X\in \left(1\dots M\right)\to X\le M$$
23	4 22	syl	$$⊢\phi \to X\le M$$
24	17 20 18 23	lesub1dd	$$⊢\phi \to X-I\le M-I$$
25	2	nnrpd	$$⊢\phi \to I\in {ℝ}^{+}$$
26	20 25	ltsubrpd	$$⊢\phi \to M-I<M$$
27	19 21 20 24 26	lelttrd	$$⊢\phi \to X-I<M$$
28	19 27	ltned	$$⊢\phi \to X-I\ne M$$
29	28	adantr	$$⊢\left(\phi \wedge y=X-I\right)\to X-I\ne M$$
30		neeq1	$$⊢y=X-I\to \left(y\ne M\leftrightarrow X-I\ne M\right)$$
31	30	adantl	$$⊢\left(\phi \wedge y=X-I\right)\to \left(y\ne M\leftrightarrow X-I\ne M\right)$$
32	29 31	mpbird	$$⊢\left(\phi \wedge y=X-I\right)\to y\ne M$$
33	32	neneqd	$$⊢\left(\phi \wedge y=X-I\right)\to \neg y=M$$
34	33	iffalsed	$$⊢\left(\phi \wedge y=X-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)$$
35	18 19	lenltd	$$⊢\phi \to \left(I\le X-I\leftrightarrow \neg X-I<I\right)$$
36	35	biimpa	$$⊢\left(\phi \wedge I\le X-I\right)\to \neg X-I<I$$
37	36	3adant2	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to \neg X-I<I$$
38		breq1	$$⊢y=X-I\to \left(y<I\leftrightarrow X-I<I\right)$$
39	38	3ad2ant2	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to \left(y<I\leftrightarrow X-I<I\right)$$
40	37 39	mtbird	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to \neg y<I$$
41	40	iffalsed	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to if\left(y<I,y,y+1\right)=y+1$$
42		simp2	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to y=X-I$$
43	42	oveq1d	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to y+1=X-I+1$$
44		simp3	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to I\le X-I$$
45	44	iftrued	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to if\left(I\le X-I,1,0\right)=1$$
46	45	eqcomd	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to 1=if\left(I\le X-I,1,0\right)$$
47	10	a1i	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to H=if\left(I\le X-I,1,0\right)$$
48	47	eqcomd	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to if\left(I\le X-I,1,0\right)=H$$
49	46 48	eqtrd	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to 1=H$$
50	49	oveq2d	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to X-I+1=X-I+H$$
51	43 50	eqtrd	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to y+1=X-I+H$$
52	41 51	eqtrd	$$⊢\left(\phi \wedge y=X-I\wedge I\le X-I\right)\to if\left(y<I,y,y+1\right)=X-I+H$$
53	52	3expa	$$⊢\left(\left(\phi \wedge y=X-I\right)\wedge I\le X-I\right)\to if\left(y<I,y,y+1\right)=X-I+H$$
54		simpr	$$⊢\left(\phi \wedge \neg I\le X-I\right)\to \neg I\le X-I$$
55	19	adantr	$$⊢\left(\phi \wedge \neg I\le X-I\right)\to X-I\in ℝ$$
56	18	adantr	$$⊢\left(\phi \wedge \neg I\le X-I\right)\to I\in ℝ$$
57	55 56	ltnled	$$⊢\left(\phi \wedge \neg I\le X-I\right)\to \left(X-I<I\leftrightarrow \neg I\le X-I\right)$$
58	54 57	mpbird	$$⊢\left(\phi \wedge \neg I\le X-I\right)\to X-I<I$$
59	58	3adant2	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to X-I<I$$
60	38	3ad2ant2	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to \left(y<I\leftrightarrow X-I<I\right)$$
61	59 60	mpbird	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to y<I$$
62	61	iftrued	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to if\left(y<I,y,y+1\right)=y$$
63		simp2	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to y=X-I$$
64		nncn	$$⊢X\in \mathbb{N}\to X\in ℂ$$
65	15 64	syl	$$⊢\phi \to X\in ℂ$$
66	65	3ad2ant1	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to X\in ℂ$$
67	2	nncnd	$$⊢\phi \to I\in ℂ$$
68	67	3ad2ant1	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to I\in ℂ$$
69	66 68	subcld	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to X-I\in ℂ$$
70	69	addid1d	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to X-I+0=X-I$$
71	70	eqcomd	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to X-I=X-I+0$$
72	10	a1i	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to H=if\left(I\le X-I,1,0\right)$$
73		simp3	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to \neg I\le X-I$$
74	73	iffalsed	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to if\left(I\le X-I,1,0\right)=0$$
75	72 74	eqtrd	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to H=0$$
76	75	eqcomd	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to 0=H$$
77	76	oveq2d	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to X-I+0=X-I+H$$
78	71 77	eqtrd	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to X-I=X-I+H$$
79	63 78	eqtrd	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to y=X-I+H$$
80	62 79	eqtrd	$$⊢\left(\phi \wedge y=X-I\wedge \neg I\le X-I\right)\to if\left(y<I,y,y+1\right)=X-I+H$$
81	80	3expa	$$⊢\left(\left(\phi \wedge y=X-I\right)\wedge \neg I\le X-I\right)\to if\left(y<I,y,y+1\right)=X-I+H$$
82	53 81	pm2.61dan	$$⊢\left(\phi \wedge y=X-I\right)\to if\left(y<I,y,y+1\right)=X-I+H$$
83	34 82	eqtrd	$$⊢\left(\phi \wedge y=X-I\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=X-I+H$$
84		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
85	1	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
86	15	nnzd	$$⊢\phi \to X\in \mathbb{Z}$$
87	2	nnzd	$$⊢\phi \to I\in \mathbb{Z}$$
88	86 87	zsubcld	$$⊢\phi \to X-I\in \mathbb{Z}$$
89		1m1e0	$$⊢1-1=0$$
90	18 17 8	nltled	$$⊢\phi \to I\le X$$
91	7	neqned	$$⊢\phi \to X\ne I$$
92	90 91	jca	$$⊢\phi \to \left(I\le X\wedge X\ne I\right)$$
93	18 17	ltlend	$$⊢\phi \to \left(I<X\leftrightarrow \left(I\le X\wedge X\ne I\right)\right)$$
94	92 93	mpbird	$$⊢\phi \to I<X$$
95	18 17	posdifd	$$⊢\phi \to \left(I<X\leftrightarrow 0<X-I\right)$$
96	94 95	mpbid	$$⊢\phi \to 0<X-I$$
97	89 96	eqbrtrid	$$⊢\phi \to 1-1<X-I$$
98		zlem1lt	$$⊢\left(1\in \mathbb{Z}\wedge X-I\in \mathbb{Z}\right)\to \left(1\le X-I\leftrightarrow 1-1<X-I\right)$$
99	84 88 98	syl2anc	$$⊢\phi \to \left(1\le X-I\leftrightarrow 1-1<X-I\right)$$
100	97 99	mpbird	$$⊢\phi \to 1\le X-I$$
101	19 20 27	ltled	$$⊢\phi \to X-I\le M$$
102	84 85 88 100 101	elfzd	$$⊢\phi \to X-I\in \left(1\dots M\right)$$
103		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
104	84 103	ifcld	$$⊢\phi \to if\left(I\le X-I,1,0\right)\in \mathbb{Z}$$
105	10	a1i	$$⊢\phi \to H=if\left(I\le X-I,1,0\right)$$
106	105	eleq1d	$$⊢\phi \to \left(H\in \mathbb{Z}\leftrightarrow if\left(I\le X-I,1,0\right)\in \mathbb{Z}\right)$$
107	104 106	mpbird	$$⊢\phi \to H\in \mathbb{Z}$$
108	88 107	zaddcld	$$⊢\phi \to X-I+H\in \mathbb{Z}$$
109	13 83 102 108	fvmptd	$$⊢\phi \to C\left(X-I\right)=X-I+H$$
110	12 109	eqtrd	$$⊢\phi \to C\left(B\left(A\left(X\right)\right)\right)=X-I+H$$