Metamath Proof Explorer

Theorem metakunt30

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

Ref Expression
Hypotheses metakunt30.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
metakunt30.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
metakunt30.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
metakunt30.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
metakunt30.5 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
metakunt30.6 ⊢ 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) )
metakunt30.7 ⊢ ( 𝜑 → ¬ 𝑋 = 𝐼 )
metakunt30.8 ⊢ ( 𝜑 → ¬ 𝑋 < 𝐼 )
metakunt30.9 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
metakunt30.10 ⊢ 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 )
Assertion metakunt30 ( 𝜑 → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )

Proof

Step Hyp Ref Expression
1 metakunt30.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt30.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt30.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt30.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
5 metakunt30.5 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
6 metakunt30.6 ⊢ 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) )
7 metakunt30.7 ⊢ ( 𝜑 → ¬ 𝑋 = 𝐼 )
8 metakunt30.8 ⊢ ( 𝜑 → ¬ 𝑋 < 𝐼 )
9 metakunt30.9 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
10 metakunt30.10 ⊢ 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 )
11 1 2 3 4 5 6 7 8 metakunt28 ⊢ ( 𝜑 → ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑋 − 𝐼 ) )
12 11 fveq2d ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( 𝐶 ‘ ( 𝑋 − 𝐼 ) ) )
13 9 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) ) )
14 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ∈ ℕ )
15 4 14 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
16 nnre ⊢ ( 𝑋 ∈ ℕ → 𝑋 ∈ ℝ )
17 15 16 syl ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
18 2 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
19 17 18 resubcld ⊢ ( 𝜑 → ( 𝑋 − 𝐼 ) ∈ ℝ )
20 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
21 20 18 resubcld ⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) ∈ ℝ )
22 elfzle2 ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ≤ 𝑀 )
23 4 22 syl ⊢ ( 𝜑 → 𝑋 ≤ 𝑀 )
24 17 20 18 23 lesub1dd ⊢ ( 𝜑 → ( 𝑋 − 𝐼 ) ≤ ( 𝑀 − 𝐼 ) )
25 2 nnrpd ⊢ ( 𝜑 → 𝐼 ∈ ℝ+ )
26 20 25 ltsubrpd ⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) < 𝑀 )
27 19 21 20 24 26 lelttrd ⊢ ( 𝜑 → ( 𝑋 − 𝐼 ) < 𝑀 )
28 19 27 ltned ⊢ ( 𝜑 → ( 𝑋 − 𝐼 ) ≠ 𝑀 )
29 28 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ) → ( 𝑋 − 𝐼 ) ≠ 𝑀 )
30 neeq1 ⊢ ( 𝑦 = ( 𝑋 − 𝐼 ) → ( 𝑦 ≠ 𝑀 ↔ ( 𝑋 − 𝐼 ) ≠ 𝑀 ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ) → ( 𝑦 ≠ 𝑀 ↔ ( 𝑋 − 𝐼 ) ≠ 𝑀 ) )
32 29 31 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ) → 𝑦 ≠ 𝑀 )
33 32 neneqd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ) → ¬ 𝑦 = 𝑀 )
34 33 iffalsed ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) )
35 18 19 lenltd ⊢ ( 𝜑 → ( 𝐼 ≤ ( 𝑋 − 𝐼 ) ↔ ¬ ( 𝑋 − 𝐼 ) < 𝐼 ) )
36 35 biimpa ⊢ ( ( 𝜑 ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ¬ ( 𝑋 − 𝐼 ) < 𝐼 )
37 36 3adant2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ¬ ( 𝑋 − 𝐼 ) < 𝐼 )
38 breq1 ⊢ ( 𝑦 = ( 𝑋 − 𝐼 ) → ( 𝑦 < 𝐼 ↔ ( 𝑋 − 𝐼 ) < 𝐼 ) )
39 38 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( 𝑦 < 𝐼 ↔ ( 𝑋 − 𝐼 ) < 𝐼 ) )
40 37 39 mtbird ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ¬ 𝑦 < 𝐼 )
41 40 iffalsed ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑦 + 1 ) )
42 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝑦 = ( 𝑋 − 𝐼 ) )
43 42 oveq1d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( 𝑦 + 1 ) = ( ( 𝑋 − 𝐼 ) + 1 ) )
44 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝐼 ≤ ( 𝑋 − 𝐼 ) )
45 44 iftrued ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) = 1 )
46 45 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 1 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) )
47 10 a1i ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) )
48 47 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) = 𝐻 )
49 46 48 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 1 = 𝐻 )
50 49 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( ( 𝑋 − 𝐼 ) + 1 ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
51 43 50 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( 𝑦 + 1 ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
52 41 51 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
53 52 3expa ⊢ ( ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
54 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) )
55 19 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( 𝑋 − 𝐼 ) ∈ ℝ )
56 18 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝐼 ∈ ℝ )
57 55 56 ltnled ⊢ ( ( 𝜑 ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( ( 𝑋 − 𝐼 ) < 𝐼 ↔ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) )
58 54 57 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( 𝑋 − 𝐼 ) < 𝐼 )
59 58 3adant2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( 𝑋 − 𝐼 ) < 𝐼 )
60 38 3ad2ant2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( 𝑦 < 𝐼 ↔ ( 𝑋 − 𝐼 ) < 𝐼 ) )
61 59 60 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝑦 < 𝐼 )
62 61 iftrued ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
63 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝑦 = ( 𝑋 − 𝐼 ) )
64 nncn ⊢ ( 𝑋 ∈ ℕ → 𝑋 ∈ ℂ )
65 15 64 syl ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
66 65 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝑋 ∈ ℂ )
67 2 nncnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
68 67 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝐼 ∈ ℂ )
69 66 68 subcld ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( 𝑋 − 𝐼 ) ∈ ℂ )
70 69 addid1d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( ( 𝑋 − 𝐼 ) + 0 ) = ( 𝑋 − 𝐼 ) )
71 70 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( 𝑋 − 𝐼 ) = ( ( 𝑋 − 𝐼 ) + 0 ) )
72 10 a1i ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) )
73 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) )
74 73 iffalsed ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) = 0 )
75 72 74 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝐻 = 0 )
76 75 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 0 = 𝐻 )
77 76 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( ( 𝑋 − 𝐼 ) + 0 ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
78 71 77 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → ( 𝑋 − 𝐼 ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
79 63 78 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → 𝑦 = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
80 62 79 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
81 80 3expa ⊢ ( ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ) ∧ ¬ 𝐼 ≤ ( 𝑋 − 𝐼 ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
82 53 81 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
83 34 82 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 − 𝐼 ) ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
84 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
85 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
86 15 nnzd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
87 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
88 86 87 zsubcld ⊢ ( 𝜑 → ( 𝑋 − 𝐼 ) ∈ ℤ )
89 1m1e0 ⊢ ( 1 − 1 ) = 0
90 18 17 8 nltled ⊢ ( 𝜑 → 𝐼 ≤ 𝑋 )
91 7 neqned ⊢ ( 𝜑 → 𝑋 ≠ 𝐼 )
92 90 91 jca ⊢ ( 𝜑 → ( 𝐼 ≤ 𝑋 ∧ 𝑋 ≠ 𝐼 ) )
93 18 17 ltlend ⊢ ( 𝜑 → ( 𝐼 < 𝑋 ↔ ( 𝐼 ≤ 𝑋 ∧ 𝑋 ≠ 𝐼 ) ) )
94 92 93 mpbird ⊢ ( 𝜑 → 𝐼 < 𝑋 )
95 18 17 posdifd ⊢ ( 𝜑 → ( 𝐼 < 𝑋 ↔ 0 < ( 𝑋 − 𝐼 ) ) )
96 94 95 mpbid ⊢ ( 𝜑 → 0 < ( 𝑋 − 𝐼 ) )
97 89 96 eqbrtrid ⊢ ( 𝜑 → ( 1 − 1 ) < ( 𝑋 − 𝐼 ) )
98 zlem1lt ⊢ ( ( 1 ∈ ℤ ∧ ( 𝑋 − 𝐼 ) ∈ ℤ ) → ( 1 ≤ ( 𝑋 − 𝐼 ) ↔ ( 1 − 1 ) < ( 𝑋 − 𝐼 ) ) )
99 84 88 98 syl2anc ⊢ ( 𝜑 → ( 1 ≤ ( 𝑋 − 𝐼 ) ↔ ( 1 − 1 ) < ( 𝑋 − 𝐼 ) ) )
100 97 99 mpbird ⊢ ( 𝜑 → 1 ≤ ( 𝑋 − 𝐼 ) )
101 19 20 27 ltled ⊢ ( 𝜑 → ( 𝑋 − 𝐼 ) ≤ 𝑀 )
102 84 85 88 100 101 elfzd ⊢ ( 𝜑 → ( 𝑋 − 𝐼 ) ∈ ( 1 ... 𝑀 ) )
103 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
104 84 103 ifcld ⊢ ( 𝜑 → if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) ∈ ℤ )
105 10 a1i ⊢ ( 𝜑 → 𝐻 = if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) )
106 105 eleq1d ⊢ ( 𝜑 → ( 𝐻 ∈ ℤ ↔ if ( 𝐼 ≤ ( 𝑋 − 𝐼 ) , 1 , 0 ) ∈ ℤ ) )
107 104 106 mpbird ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
108 88 107 zaddcld ⊢ ( 𝜑 → ( ( 𝑋 − 𝐼 ) + 𝐻 ) ∈ ℤ )
109 13 83 102 108 fvmptd ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑋 − 𝐼 ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )
110 12 109 eqtrd ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( 𝑋 − 𝐼 ) + 𝐻 ) )