Theorem metakunt7

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt7.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt7.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt7.3	$$⊢\phi \to I\le M$$
4		metakunt7.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		metakunt7.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		metakunt7.6	$$⊢\phi \to X\in \left(1\dots M\right)$$
7	4	a1i	$$⊢\left(\phi \wedge I<X\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)$$
8		eqeq1	$$⊢x=X\to \left(x=I\leftrightarrow X=I\right)$$
9		breq1	$$⊢x=X\to \left(x<I\leftrightarrow X<I\right)$$
10		id	$$⊢x=X\to x=X$$
11		oveq1	$$⊢x=X\to x-1=X-1$$
12	9 10 11	ifbieq12d	$$⊢x=X\to if\left(x<I,x,x-1\right)=if\left(X<I,X,X-1\right)$$
13	8 12	ifbieq2d	$$⊢x=X\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=if\left(X=I,M,if\left(X<I,X,X-1\right)\right)$$
14	13	adantl	$$⊢\left(\left(\phi \wedge I<X\right)\wedge x=X\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=if\left(X=I,M,if\left(X<I,X,X-1\right)\right)$$
15	2	nnred	$$⊢\phi \to I\in ℝ$$
16	15	adantr	$$⊢\left(\phi \wedge I<X\right)\to I\in ℝ$$
17		simpr	$$⊢\left(\phi \wedge I<X\right)\to I<X$$
18	16 17	ltned	$$⊢\left(\phi \wedge I<X\right)\to I\ne X$$
19	18	necomd	$$⊢\left(\phi \wedge I<X\right)\to X\ne I$$
20		df-ne	$$⊢X\ne I\leftrightarrow \neg X=I$$
21	19 20	sylib	$$⊢\left(\phi \wedge I<X\right)\to \neg X=I$$
22		iffalse	$$⊢\neg X=I\to if\left(X=I,M,if\left(X<I,X,X-1\right)\right)=if\left(X<I,X,X-1\right)$$
23	21 22	syl	$$⊢\left(\phi \wedge I<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)$$
24		elfznn	$$⊢X\in \left(1\dots M\right)\to X\in \mathbb{N}$$
25	6 24	syl	$$⊢\phi \to X\in \mathbb{N}$$
26	25	nnred	$$⊢\phi \to X\in ℝ$$
27	26	adantr	$$⊢\left(\phi \wedge I<X\right)\to X\in ℝ$$
28	16 27 17	ltled	$$⊢\left(\phi \wedge I<X\right)\to I\le X$$
29	16 27	lenltd	$$⊢\left(\phi \wedge I<X\right)\to \left(I\le X\leftrightarrow \neg X<I\right)$$
30	28 29	mpbid	$$⊢\left(\phi \wedge I<X\right)\to \neg X<I$$
31		iffalse	$$⊢\neg X<I\to if\left(X<I,X,X-1\right)=X-1$$
32	30 31	syl	$$⊢\left(\phi \wedge I<X\right)\to if\left(X<I,X,X-1\right)=X-1$$
33	23 32	eqtrd	$$⊢\left(\phi \wedge I<X\right)\to if\left(X=I,M,if\left(X<I,X,X-1\right)\right)=X-1$$
34	33	adantr	$$⊢\left(\left(\phi \wedge I<X\right)\wedge x=X\right)\to if\left(X=I,M,if\left(X<I,X,X-1\right)\right)=X-1$$
35	14 34	eqtrd	$$⊢\left(\left(\phi \wedge I<X\right)\wedge x=X\right)\to if\left(x=I,M,if\left(x<I,x,x-1\right)\right)=X-1$$
36	6	adantr	$$⊢\left(\phi \wedge I<X\right)\to X\in \left(1\dots M\right)$$
37	36	elfzelzd	$$⊢\left(\phi \wedge I<X\right)\to X\in \mathbb{Z}$$
38		1zzd	$$⊢\left(\phi \wedge I<X\right)\to 1\in \mathbb{Z}$$
39	37 38	zsubcld	$$⊢\left(\phi \wedge I<X\right)\to X-1\in \mathbb{Z}$$
40	7 35 36 39	fvmptd	$$⊢\left(\phi \wedge I<X\right)\to A\left(X\right)=X-1$$
41		1red	$$⊢\phi \to 1\in ℝ$$
42	26 41	resubcld	$$⊢\phi \to X-1\in ℝ$$
43		elfzle2	$$⊢X\in \left(1\dots M\right)\to X\le M$$
44	6 43	syl	$$⊢\phi \to X\le M$$
45	6	elfzelzd	$$⊢\phi \to X\in \mathbb{Z}$$
46	1	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
47		zlem1lt	$$⊢\left(X\in \mathbb{Z}\wedge M\in \mathbb{Z}\right)\to \left(X\le M\leftrightarrow X-1<M\right)$$
48	45 46 47	syl2anc	$$⊢\phi \to \left(X\le M\leftrightarrow X-1<M\right)$$
49	44 48	mpbid	$$⊢\phi \to X-1<M$$
50	42 49	ltned	$$⊢\phi \to X-1\ne M$$
51	50	adantr	$$⊢\left(\phi \wedge I<X\right)\to X-1\ne M$$
52	40 51	eqnetrd	$$⊢\left(\phi \wedge I<X\right)\to A\left(X\right)\ne M$$
53	52	neneqd	$$⊢\left(\phi \wedge I<X\right)\to \neg A\left(X\right)=M$$
54	2	nnzd	$$⊢\phi \to I\in \mathbb{Z}$$
55		zltlem1	$$⊢\left(I\in \mathbb{Z}\wedge X\in \mathbb{Z}\right)\to \left(I<X\leftrightarrow I\le X-1\right)$$
56	55	biimpd	$$⊢\left(I\in \mathbb{Z}\wedge X\in \mathbb{Z}\right)\to \left(I<X\to I\le X-1\right)$$
57	54 45 56	syl2anc	$$⊢\phi \to \left(I<X\to I\le X-1\right)$$
58	57	imp	$$⊢\left(\phi \wedge I<X\right)\to I\le X-1$$
59	58 40	breqtrrd	$$⊢\left(\phi \wedge I<X\right)\to I\le A\left(X\right)$$
60	39	zred	$$⊢\left(\phi \wedge I<X\right)\to X-1\in ℝ$$
61	40 60	eqeltrd	$$⊢\left(\phi \wedge I<X\right)\to A\left(X\right)\in ℝ$$
62	16 61	lenltd	$$⊢\left(\phi \wedge I<X\right)\to \left(I\le A\left(X\right)\leftrightarrow \neg A\left(X\right)<I\right)$$
63	59 62	mpbid	$$⊢\left(\phi \wedge I<X\right)\to \neg A\left(X\right)<I$$
64	40 53 63	3jca	$$⊢\left(\phi \wedge I<X\right)\to \left(A\left(X\right)=X-1\wedge \neg A\left(X\right)=M\wedge \neg A\left(X\right)<I\right)$$