Theorem metakunt12

Description: C is the right inverse for A. (Contributed by metakunt, 25-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		metakunt12.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt12.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt12.3	$$⊢\phi \to I\le M$$
4		metakunt12.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		metakunt12.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		metakunt12.6	$$⊢\phi \to X\in \left(1\dots M\right)$$
7		ioran	$$⊢\neg \left(X=M\vee X<I\right)\leftrightarrow \left(\neg X=M\wedge \neg X<I\right)$$
8	4	a1i	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\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		eqeq1	$$⊢x=C\left(X\right)\to \left(x=I\leftrightarrow C\left(X\right)=I\right)$$
10		breq1	$$⊢x=C\left(X\right)\to \left(x<I\leftrightarrow C\left(X\right)<I\right)$$
11		id	$$⊢x=C\left(X\right)\to x=C\left(X\right)$$
12		oveq1	$$⊢x=C\left(X\right)\to x-1=C\left(X\right)-1$$
13	10 11 12	ifbieq12d	$$⊢x=C\left(X\right)\to if\left(x<I,x,x-1\right)=if\left(C\left(X\right)<I,C\left(X\right),C\left(X\right)-1\right)$$
14	9 13	ifbieq2d	$$⊢x=C\left(X\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=if\left(C\left(X\right)=I,M,if\left(C\left(X\right)<I,C\left(X\right),C\left(X\right)-1\right)\right)$$
15	14	adantl	$$⊢\left(\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\wedge x=C\left(X\right)\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=if\left(C\left(X\right)=I,M,if\left(C\left(X\right)<I,C\left(X\right),C\left(X\right)-1\right)\right)$$
16	5	a1i	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\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)$$
17		eqeq1	$$⊢y=X\to \left(y=M\leftrightarrow X=M\right)$$
18		breq1	$$⊢y=X\to \left(y<I\leftrightarrow X<I\right)$$
19		id	$$⊢y=X\to y=X$$
20		oveq1	$$⊢y=X\to y+1=X+1$$
21	18 19 20	ifbieq12d	$$⊢y=X\to if\left(y<I,y,y+1\right)=if\left(X<I,X,X+1\right)$$
22	17 21	ifbieq2d	$$⊢y=X\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=if\left(X=M,I,if\left(X<I,X,X+1\right)\right)$$
23	22	adantl	$$⊢\left(\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\wedge y=X\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=if\left(X=M,I,if\left(X<I,X,X+1\right)\right)$$
24		simp2	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to \neg X=M$$
25		iffalse	$$⊢\neg X=M\to if\left(X=M,I,if\left(X<I,X,X+1\right)\right)=if\left(X<I,X,X+1\right)$$
26	24 25	syl	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to if\left(X=M,I,if\left(X<I,X,X+1\right)\right)=if\left(X<I,X,X+1\right)$$
27		simp3	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to \neg X<I$$
28		iffalse	$$⊢\neg X<I\to if\left(X<I,X,X+1\right)=X+1$$
29	27 28	syl	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to if\left(X<I,X,X+1\right)=X+1$$
30	26 29	eqtrd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to if\left(X=M,I,if\left(X<I,X,X+1\right)\right)=X+1$$
31	30	adantr	$$⊢\left(\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\wedge y=X\right)\to if\left(X=M,I,if\left(X<I,X,X+1\right)\right)=X+1$$
32	23 31	eqtrd	$$⊢\left(\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\wedge y=X\right)\to if\left(y=M,I,if\left(y<I,y,y+1\right)\right)=X+1$$
33	6	3ad2ant1	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to X\in \left(1\dots M\right)$$
34		elfznn	$$⊢X\in \left(1\dots M\right)\to X\in \mathbb{N}$$
35	6 34	syl	$$⊢\phi \to X\in \mathbb{N}$$
36	35	nnzd	$$⊢\phi \to X\in \mathbb{Z}$$
37	36	3ad2ant1	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to X\in \mathbb{Z}$$
38	37	peano2zd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to X+1\in \mathbb{Z}$$
39	16 32 33 38	fvmptd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to C\left(X\right)=X+1$$
40		eqeq1	$$⊢C\left(X\right)=X+1\to \left(C\left(X\right)=I\leftrightarrow X+1=I\right)$$
41		breq1	$$⊢C\left(X\right)=X+1\to \left(C\left(X\right)<I\leftrightarrow X+1<I\right)$$
42		id	$$⊢C\left(X\right)=X+1\to C\left(X\right)=X+1$$
43		oveq1	$$⊢C\left(X\right)=X+1\to C\left(X\right)-1=X+1-1$$
44	41 42 43	ifbieq12d	$$⊢C\left(X\right)=X+1\to if\left(C\left(X\right)<I,C\left(X\right),C\left(X\right)-1\right)=if\left(X+1<I,X+1,X+1-1\right)$$
45	40 44	ifbieq2d	$$⊢C\left(X\right)=X+1\to if\left(C\left(X\right)=I,M,if\left(C\left(X\right)<I,C\left(X\right),C\left(X\right)-1\right)\right)=if\left(X+1=I,M,if\left(X+1<I,X+1,X+1-1\right)\right)$$
46	39 45	syl	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to if\left(C\left(X\right)=I,M,if\left(C\left(X\right)<I,C\left(X\right),C\left(X\right)-1\right)\right)=if\left(X+1=I,M,if\left(X+1<I,X+1,X+1-1\right)\right)$$
47	2	nnred	$$⊢\phi \to I\in ℝ$$
48	47	3ad2ant1	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to I\in ℝ$$
49	37	zred	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to X\in ℝ$$
50	38	zred	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to X+1\in ℝ$$
51	48 49	lenltd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to \left(I\le X\leftrightarrow \neg X<I\right)$$
52	27 51	mpbird	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to I\le X$$
53	49	ltp1d	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to X<X+1$$
54	48 49 50 52 53	lelttrd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to I<X+1$$
55	48 54	ltned	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to I\ne X+1$$
56	55	necomd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to X+1\ne I$$
57	56	neneqd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to \neg X+1=I$$
58		iffalse	$$⊢\neg X+1=I\to if\left(X+1=I,M,if\left(X+1<I,X+1,X+1-1\right)\right)=if\left(X+1<I,X+1,X+1-1\right)$$
59	57 58	syl	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to if\left(X+1=I,M,if\left(X+1<I,X+1,X+1-1\right)\right)=if\left(X+1<I,X+1,X+1-1\right)$$
60	49	lep1d	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to X\le X+1$$
61	48 49 50 52 60	letrd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to I\le X+1$$
62	48 50	lenltd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to \left(I\le X+1\leftrightarrow \neg X+1<I\right)$$
63	61 62	mpbid	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to \neg X+1<I$$
64		iffalse	$$⊢\neg X+1<I\to if\left(X+1<I,X+1,X+1-1\right)=X+1-1$$
65	63 64	syl	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to if\left(X+1<I,X+1,X+1-1\right)=X+1-1$$
66	37	zcnd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to X\in ℂ$$
67		1cnd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to 1\in ℂ$$
68	66 67	pncand	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to X+1-1=X$$
69	59 65 68	3eqtrd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to if\left(X+1=I,M,if\left(X+1<I,X+1,X+1-1\right)\right)=X$$
70	46 69	eqtrd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to if\left(C\left(X\right)=I,M,if\left(C\left(X\right)<I,C\left(X\right),C\left(X\right)-1\right)\right)=X$$
71	70	adantr	$$⊢\left(\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\wedge x=C\left(X\right)\right)\to if\left(C\left(X\right)=I,M,if\left(C\left(X\right)<I,C\left(X\right),C\left(X\right)-1\right)\right)=X$$
72	15 71	eqtrd	$$⊢\left(\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\wedge x=C\left(X\right)\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=X$$
73	1 2 3 5	metakunt2	$$⊢\phi \to C:\left(1\dots M\right)⟶\left(1\dots M\right)$$
74	73	3ad2ant1	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to C:\left(1\dots M\right)⟶\left(1\dots M\right)$$
75	74 33	ffvelrnd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to C\left(X\right)\in \left(1\dots M\right)$$
76	8 72 75 33	fvmptd	$$⊢\left(\phi \wedge \neg X=M\wedge \neg X<I\right)\to A\left(C\left(X\right)\right)=X$$
77	76	3expb	$$⊢\left(\phi \wedge \left(\neg X=M\wedge \neg X<I\right)\right)\to A\left(C\left(X\right)\right)=X$$
78	7 77	sylan2b	$$⊢\left(\phi \wedge \neg \left(X=M\vee X<I\right)\right)\to A\left(C\left(X\right)\right)=X$$