Theorem metakunt3

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

	Ref	Expression
Hypotheses	metakunt3.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
	metakunt3.2	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
	metakunt3.3	⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
	metakunt3.4	⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
	metakunt3.5	⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
Assertion	metakunt3	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		metakunt3.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		metakunt3.2	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3		metakunt3.3	⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4		metakunt3.4	⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
5		metakunt3.5	⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
6	4	a1i	⊢ ( 𝜑 → 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) )
7		eqeq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 = 𝐼 ↔ 𝑋 = 𝐼 ) )
8		breq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 < 𝐼 ↔ 𝑋 < 𝐼 ) )
9		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
10		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 − 1 ) = ( 𝑋 − 1 ) )
11	8 9 10	ifbieq12d	⊢ ( 𝑥 = 𝑋 → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) )
12	7 11	ifbieq2d	⊢ ( 𝑥 = 𝑋 → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) )
14	1	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
15	5	elfzelzd	⊢ ( 𝜑 → 𝑋 ∈ ℤ )
16		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
17	15 16	zsubcld	⊢ ( 𝜑 → ( 𝑋 − 1 ) ∈ ℤ )
18	15 17	ifcld	⊢ ( 𝜑 → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ∈ ℤ )
19	14 18	ifcld	⊢ ( 𝜑 → if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) ∈ ℤ )
20	6 13 5 19	fvmptd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = if ( 𝑋 = 𝐼 , 𝑀 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 − 1 ) ) ) )