Metamath Proof Explorer

Theorem metakunt32

Description: Construction of one solution of the increment equation system. (Contributed by metakunt, 18-Jul-2024)

Ref Expression
Hypotheses metakunt32.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt32.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt32.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt32.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
metakunt32.5 ⊢ 𝐷 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑥 , if ( 𝑥 < 𝐼 , ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑥 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) , ( ( 𝑥 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑥 − 𝐼 ) , 1 , 0 ) ) ) ) )
metakunt32.6 ⊢ 𝐺 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 )
metakunt32.7 ⊢ 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 )
metakunt32.8 ⊢ 𝑅 = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) )
Assertion metakunt32 ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = 𝑅 )

Proof

Step Hyp Ref Expression
1 metakunt32.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt32.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt32.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt32.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
5 metakunt32.5 ⊢ 𝐷 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑥 , if ( 𝑥 < 𝐼 , ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑥 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) , ( ( 𝑥 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑥 − 𝐼 ) , 1 , 0 ) ) ) ) )
6 metakunt32.6 ⊢ 𝐺 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 )
7 metakunt32.7 ⊢ 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 )
8 metakunt32.8 ⊢ 𝑅 = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) )
9 5 a1i ⊢ ( 𝜑 → 𝐷 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑥 , if ( 𝑥 < 𝐼 , ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑥 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) , ( ( 𝑥 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑥 − 𝐼 ) , 1 , 0 ) ) ) ) ) )
10 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
11 10 eqeq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 = 𝐼 ↔ 𝑋 = 𝐼 ) )
12 10 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 < 𝐼 ↔ 𝑋 < 𝐼 ) )
13 oveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( 𝑀 − 𝐼 ) ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
14 13 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 + ( 𝑀 − 𝐼 ) ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
15 14 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐼 ≤ ( 𝑥 + ( 𝑀 − 𝐼 ) ) ↔ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) )
16 15 ifbid ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝐼 ≤ ( 𝑥 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) )
17 14 16 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑥 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) )
18 6 a1i ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝐺 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) )
19 18 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) = 𝐺 )
20 19 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) )
21 17 20 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑥 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) )
22 10 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 − 𝐼 ) = ( 𝑋 − 𝐼 ) )
23 22 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝐼 ≤ ( 𝑥 − 𝐼 ) ↔ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) )
24 23 ifbid ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝐼 ≤ ( 𝑥 − 𝐼 ) , 1 , 0 ) = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) )
25 22 24 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑥 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑥 − 𝐼 ) , 1 , 0 ) ) = ( ( 𝑋 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) ) )
26 7 a1i ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) )
27 26 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) = 𝐻 )
28 27 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑋 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
29 25 28 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑥 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑥 − 𝐼 ) , 1 , 0 ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
30 12 21 29 ifbieq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 < 𝐼 , ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑥 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) , ( ( 𝑥 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑥 − 𝐼 ) , 1 , 0 ) ) ) = if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) )
31 11 10 30 ifbieq12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑥 , if ( 𝑥 < 𝐼 , ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑥 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) , ( ( 𝑥 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑥 − 𝐼 ) , 1 , 0 ) ) ) ) = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) )
32 8 a1i ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑅 = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) )
33 32 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) = 𝑅 )
34 31 33 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑥 , if ( 𝑥 < 𝐼 , ( ( 𝑥 + ( 𝑀 − 𝐼 ) ) + if ( 𝐼 ≤ ( 𝑥 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ) , ( ( 𝑥 − 𝐼 ) + if ( 𝐼 ≤ ( 𝑥 − 𝐼 ) , 1 , 0 ) ) ) ) = 𝑅 )
35 4 elfzelzd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
36 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
37 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
38 36 37 zsubcld ⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) ∈ ℤ )
39 35 38 zaddcld ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∈ ℤ )
40 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
41 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
42 40 41 ifcld ⊢ ( 𝜑 → if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ∈ ℤ )
43 6 a1i ⊢ ( 𝜑 → 𝐺 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) )
44 43 eleq1d ⊢ ( 𝜑 → ( 𝐺 ∈ ℤ ↔ if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ∈ ℤ ) )
45 42 44 mpbird ⊢ ( 𝜑 → 𝐺 ∈ ℤ )
46 39 45 zaddcld ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) ∈ ℤ )
47 35 37 zsubcld ⊢ ( 𝜑 → ( 𝑋 − 𝐼 ) ∈ ℤ )
48 40 41 ifcld ⊢ ( 𝜑 → if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) ∈ ℤ )
49 7 a1i ⊢ ( 𝜑 → 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) )
50 49 eleq1d ⊢ ( 𝜑 → ( 𝐻 ∈ ℤ ↔ if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) ∈ ℤ ) )
51 48 50 mpbird ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
52 47 51 zaddcld ⊢ ( 𝜑 → ( ( 𝑋 − 𝐼 ) + 𝐻 ) ∈ ℤ )
53 46 52 ifcld ⊢ ( 𝜑 → if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ∈ ℤ )
54 35 53 ifcld ⊢ ( 𝜑 → if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) ∈ ℤ )
55 8 a1i ⊢ ( 𝜑 → 𝑅 = if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) )
56 55 eleq1d ⊢ ( 𝜑 → ( 𝑅 ∈ ℤ ↔ if ( 𝑋 = 𝐼 , 𝑋 , if ( 𝑋 < 𝐼 , ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐺 ) , ( ( 𝑋 − 𝐼 ) + 𝐻 ) ) ) ∈ ℤ ) )
57 54 56 mpbird ⊢ ( 𝜑 → 𝑅 ∈ ℤ )
58 9 34 4 57 fvmptd ⊢ ( 𝜑 → ( 𝐷 ‘ 𝑋 ) = 𝑅 )