Theorem metakunt3

Description: Value of A. (Contributed by metakunt, 23-May-2024)

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

Proof

Step	Hyp	Ref	Expression
1		metakunt3.1	$$⊢\phi \to M\in \mathbb{N}$$
2		metakunt3.2	$$⊢\phi \to I\in \mathbb{N}$$
3		metakunt3.3	$$⊢\phi \to I\le M$$
4		metakunt3.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		metakunt3.5	$$⊢\phi \to X\in \left(1\dots M\right)$$
6	4	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)$$
7		eqeq1	$$⊢x=X\to \left(x=I\leftrightarrow X=I\right)$$
8		breq1	$$⊢x=X\to \left(x<I\leftrightarrow X<I\right)$$
9		id	$$⊢x=X\to x=X$$
10		oveq1	$$⊢x=X\to x-1=X-1$$
11	8 9 10	ifbieq12d	$$⊢x=X\to if\left(x<I,x,x-1\right)=if\left(X<I,X,X-1\right)$$
12	7 11	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)$$
13	12	adantl	$$⊢\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,M,if\left(X<I,X,X-1\right)\right)$$
14	1	nnzd	$$⊢\phi \to M\in \mathbb{Z}$$
15	5	elfzelzd	$$⊢\phi \to X\in \mathbb{Z}$$
16		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
17	15 16	zsubcld	$$⊢\phi \to X-1\in \mathbb{Z}$$
18	15 17	ifcld	$$⊢\phi \to if\left(X<I,X,X-1\right)\in \mathbb{Z}$$
19	14 18	ifcld	$$⊢\phi \to if\left(X=I,M,if\left(X<I,X,X-1\right)\right)\in \mathbb{Z}$$
20	6 13 5 19	fvmptd	$$⊢\phi \to A\left(X\right)=if\left(X=I,M,if\left(X<I,X,X-1\right)\right)$$