Theorem metakunt4

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

	Ref	Expression
Hypotheses	metakunt4.1	|- ( ph -> M e. NN )
	metakunt4.2	|- ( ph -> I e. NN )
	metakunt4.3	|- ( ph -> I <_ M )
	metakunt4.4	|- A = ( x e. ( 1 ... M ) |-> if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) )
	metakunt4.5	|- ( ph -> X e. ( 1 ... M ) )
Assertion	metakunt4	|- ( ph -> ( A ` X ) = if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		metakunt4.1	|- ( ph -> M e. NN )
2		metakunt4.2	|- ( ph -> I e. NN )
3		metakunt4.3	|- ( ph -> I <_ M )
4		metakunt4.4	|- A = ( x e. ( 1 ... M ) |-> if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) )
5		metakunt4.5	|- ( ph -> X e. ( 1 ... M ) )
6	4	a1i	|- ( ph -> A = ( x e. ( 1 ... M ) |-> if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) ) )
7		eqeq1	|- ( x = X -> ( x = M <-> X = M ) )
8		breq1	|- ( x = X -> ( x < I <-> X < I ) )
9		id	|- ( x = X -> x = X )
10		oveq1	|- ( x = X -> ( x + 1 ) = ( X + 1 ) )
11	8 9 10	ifbieq12d	|- ( x = X -> if ( x < I , x , ( x + 1 ) ) = if ( X < I , X , ( X + 1 ) ) )
12	7 11	ifbieq2d	|- ( x = X -> if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) = if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) )
13	12	adantl	|- ( ( ph /\ x = X ) -> if ( x = M , I , if ( x < I , x , ( x + 1 ) ) ) = if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) )
14	2	nnzd	|- ( ph -> I e. ZZ )
15	5	elfzelzd	|- ( ph -> X e. ZZ )
16	15	peano2zd	|- ( ph -> ( X + 1 ) e. ZZ )
17	15 16	ifcld	|- ( ph -> if ( X < I , X , ( X + 1 ) ) e. ZZ )
18	14 17	ifcld	|- ( ph -> if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) e. ZZ )
19	6 13 5 18	fvmptd	|- ( ph -> ( A ` X ) = if ( X = M , I , if ( X < I , X , ( X + 1 ) ) ) )