Theorem metakunt4

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

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

Proof

Step	Hyp	Ref	Expression
1		metakunt4.1	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2		metakunt4.2	⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3		metakunt4.3	⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4		metakunt4.4	⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝑀 , 𝐼 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 + 1 ) ) ) )
5		metakunt4.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	2	nnzd	⊢ ( 𝜑 → 𝐼 ∈ ℤ )
15	5	elfzelzd	⊢ ( 𝜑 → 𝑋 ∈ ℤ )
16	15	peano2zd	⊢ ( 𝜑 → ( 𝑋 + 1 ) ∈ ℤ )
17	15 16	ifcld	⊢ ( 𝜑 → if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ∈ ℤ )
18	14 17	ifcld	⊢ ( 𝜑 → if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) ∈ ℤ )
19	6 13 5 18	fvmptd	⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = if ( 𝑋 = 𝑀 , 𝐼 , if ( 𝑋 < 𝐼 , 𝑋 , ( 𝑋 + 1 ) ) ) )