Theorem metakunt3

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt3.1	|- ( ph -> M e. NN )
2		metakunt3.2	|- ( ph -> I e. NN )
3		metakunt3.3	|- ( ph -> I <_ M )
4		metakunt3.4	|- A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) )
5		metakunt3.5	|- ( ph -> X e. ( 1 ... M ) )
6	4	a1i	|- ( ph -> A = ( x e. ( 1 ... M ) |-> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) ) )
7		eqeq1	|- ( x = X -> ( x = I <-> X = I ) )
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 = I , M , if ( x < I , x , ( x - 1 ) ) ) = if ( X = I , M , if ( X < I , X , ( X - 1 ) ) ) )
13	12	adantl	|- ( ( ph /\ x = X ) -> if ( x = I , M , if ( x < I , x , ( x - 1 ) ) ) = if ( X = I , M , if ( X < I , X , ( X - 1 ) ) ) )
14	1	nnzd	|- ( ph -> M e. ZZ )
15	5	elfzelzd	|- ( ph -> X e. ZZ )
16		1zzd	|- ( ph -> 1 e. ZZ )
17	15 16	zsubcld	|- ( ph -> ( X - 1 ) e. ZZ )
18	15 17	ifcld	|- ( ph -> if ( X < I , X , ( X - 1 ) ) e. ZZ )
19	14 18	ifcld	|- ( ph -> if ( X = I , M , if ( X < I , X , ( X - 1 ) ) ) e. ZZ )
20	6 13 5 19	fvmptd	|- ( ph -> ( A ` X ) = if ( X = I , M , if ( X < I , X , ( X - 1 ) ) ) )