Metamath Proof Explorer

Theorem metakunt29

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

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

Proof

Step Hyp Ref Expression
1 metakunt29.1 ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 metakunt29.2 ⊢ ( 𝜑 → 𝐼 ∈ ℕ )
3 metakunt29.3 ⊢ ( 𝜑 → 𝐼 ≤ 𝑀 )
4 metakunt29.4 ⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) )
5 metakunt29.5 ⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) )
6 metakunt29.6 ⊢ 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) )
7 metakunt29.7 ⊢ ( 𝜑 → ¬ 𝑋 = 𝐼 )
8 metakunt29.8 ⊢ ( 𝜑 → 𝑋 < 𝐼 )
9 metakunt29.9 ⊢ 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) )
10 metakunt29.10 ⊢ 𝐻 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 )
11 1 2 3 4 5 6 7 8 metakunt27 ⊢ ( 𝜑 → ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
12 11 fveq2d ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( 𝐶 ‘ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) )
13 9 a1i ⊢ ( 𝜑 → 𝐶 = ( 𝑦 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) ) )
14 elfznn ⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ∈ ℕ )
15 4 14 syl ⊢ ( 𝜑 → 𝑋 ∈ ℕ )
16 nnre ⊢ ( 𝑋 ∈ ℕ → 𝑋 ∈ ℝ )
17 15 16 syl ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
18 1 nnred ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
19 2 nnred ⊢ ( 𝜑 → 𝐼 ∈ ℝ )
20 18 19 resubcld ⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) ∈ ℝ )
21 17 20 readdcld ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∈ ℝ )
22 17 recnd ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
23 18 recnd ⊢ ( 𝜑 → 𝑀 ∈ ℂ )
24 19 recnd ⊢ ( 𝜑 → 𝐼 ∈ ℂ )
25 22 23 24 addsub12d ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) = ( 𝑀 + ( 𝑋 − 𝐼 ) ) )
26 23 24 22 subsub2d ⊢ ( 𝜑 → ( 𝑀 − ( 𝐼 − 𝑋 ) ) = ( 𝑀 + ( 𝑋 − 𝐼 ) ) )
27 19 17 resubcld ⊢ ( 𝜑 → ( 𝐼 − 𝑋 ) ∈ ℝ )
28 17 19 posdifd ⊢ ( 𝜑 → ( 𝑋 < 𝐼 ↔ 0 < ( 𝐼 − 𝑋 ) ) )
29 8 28 mpbid ⊢ ( 𝜑 → 0 < ( 𝐼 − 𝑋 ) )
30 27 29 elrpd ⊢ ( 𝜑 → ( 𝐼 − 𝑋 ) ∈ ℝ+ )
31 18 30 ltsubrpd ⊢ ( 𝜑 → ( 𝑀 − ( 𝐼 − 𝑋 ) ) < 𝑀 )
32 26 31 eqbrtrrd ⊢ ( 𝜑 → ( 𝑀 + ( 𝑋 − 𝐼 ) ) < 𝑀 )
33 25 32 eqbrtrd ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝑀 )
34 21 33 ltned ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ≠ 𝑀 )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ≠ 𝑀 )
36 simpr ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
37 36 neeq1d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑦 ≠ 𝑀 ↔ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ≠ 𝑀 ) )
38 35 37 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝑦 ≠ 𝑀 )
39 38 neneqd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ¬ 𝑦 = 𝑀 )
40 39 iffalsed ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) )
41 simpr ⊢ ( ( 𝜑 ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
42 19 adantr ⊢ ( ( 𝜑 ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝐼 ∈ ℝ )
43 17 adantr ⊢ ( ( 𝜑 ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝑋 ∈ ℝ )
44 18 adantr ⊢ ( ( 𝜑 ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝑀 ∈ ℝ )
45 44 42 resubcld ⊢ ( ( 𝜑 ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑀 − 𝐼 ) ∈ ℝ )
46 43 45 readdcld ⊢ ( ( 𝜑 ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∈ ℝ )
47 42 46 lenltd ⊢ ( ( 𝜑 ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ↔ ¬ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) )
48 41 47 mpbid ⊢ ( ( 𝜑 ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ¬ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 )
49 48 3adant2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ¬ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 )
50 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
51 50 breq1d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑦 < 𝐼 ↔ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) )
52 51 notbid ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( ¬ 𝑦 < 𝐼 ↔ ¬ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) )
53 49 52 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ¬ 𝑦 < 𝐼 )
54 53 iffalsed ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( 𝑦 + 1 ) )
55 50 oveq1d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑦 + 1 ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 1 ) )
56 54 55 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 1 ) )
57 simp3 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
58 57 iftrued ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) = 1 )
59 58 eqcomd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 1 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) )
60 59 10 eqtr4di ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 1 = 𝐻 )
61 60 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 1 ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
62 56 61 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
63 62 3expa ⊢ ( ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) ∧ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
64 21 19 ltnled ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ↔ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) )
65 64 biimprd ⊢ ( 𝜑 → ( ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) )
66 65 imp ⊢ ( ( 𝜑 ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 )
67 66 3adant2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 )
68 simp2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
69 68 breq1d ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑦 < 𝐼 ↔ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) )
70 67 69 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝑦 < 𝐼 )
71 70 iftrued ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = 𝑦 )
72 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → 𝑋 ∈ ℂ )
73 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → 𝑀 ∈ ℂ )
74 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → 𝐼 ∈ ℂ )
75 73 74 subcld ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → ( 𝑀 − 𝐼 ) ∈ ℂ )
76 72 75 addcld ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∈ ℂ )
77 76 addridd ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 0 ) = ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
78 77 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 0 ) )
79 64 biimpa ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
80 79 iffalsed ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) = 0 )
81 80 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → 0 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) )
82 10 a1i ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → 𝐻 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) )
83 82 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) = 𝐻 )
84 81 83 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → 0 = 𝐻 )
85 84 oveq2d ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 0 ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
86 78 85 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
87 86 ex ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) < 𝐼 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) ) )
88 65 87 syld ⊢ ( 𝜑 → ( ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) ) )
89 88 imp ⊢ ( ( 𝜑 ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
90 89 3adant2 ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → ( 𝑋 + ( 𝑀 − 𝐼 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
91 68 90 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → 𝑦 = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
92 71 91 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
93 92 3expa ⊢ ( ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) ∧ ¬ 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
94 63 93 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
95 40 94 eqtrd ⊢ ( ( 𝜑 ∧ 𝑦 = ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) → if ( 𝑦 = 𝑀 , 𝐼 , if ( 𝑦 < 𝐼 , 𝑦 , ( 𝑦 + 1 ) ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
96 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
97 1 nnzd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
98 15 nnzd ⊢ ( 𝜑 → 𝑋 ∈ ℤ )
99 2 nnzd ⊢ ( 𝜑 → 𝐼 ∈ ℤ )
100 97 99 zsubcld ⊢ ( 𝜑 → ( 𝑀 − 𝐼 ) ∈ ℤ )
101 98 100 zaddcld ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∈ ℤ )
102 1p0e1 ⊢ ( 1 + 0 ) = 1
103 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
104 0red ⊢ ( 𝜑 → 0 ∈ ℝ )
105 15 nnge1d ⊢ ( 𝜑 → 1 ≤ 𝑋 )
106 18 19 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( 𝑀 − 𝐼 ) ↔ 𝐼 ≤ 𝑀 ) )
107 3 106 mpbird ⊢ ( 𝜑 → 0 ≤ ( 𝑀 − 𝐼 ) )
108 103 104 17 20 105 107 le2addd ⊢ ( 𝜑 → ( 1 + 0 ) ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
109 102 108 eqbrtrrid ⊢ ( 𝜑 → 1 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) )
110 21 18 33 ltled ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ≤ 𝑀 )
111 96 97 101 109 110 elfzd ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∈ ( 1 ... 𝑀 ) )
112 111 elfzelzd ⊢ ( 𝜑 → ( 𝑋 + ( 𝑀 − 𝐼 ) ) ∈ ℤ )
113 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
114 96 113 ifcld ⊢ ( 𝜑 → if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ∈ ℤ )
115 10 a1i ⊢ ( 𝜑 → 𝐻 = if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) )
116 115 eleq1d ⊢ ( 𝜑 → ( 𝐻 ∈ ℤ ↔ if ( 𝐼 ≤ ( 𝑋 + ( 𝑀 − 𝐼 ) ) , 1 , 0 ) ∈ ℤ ) )
117 114 116 mpbird ⊢ ( 𝜑 → 𝐻 ∈ ℤ )
118 112 117 zaddcld ⊢ ( 𝜑 → ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) ∈ ℤ )
119 13 95 111 118 fvmptd ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝑋 + ( 𝑀 − 𝐼 ) ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )
120 12 119 eqtrd ⊢ ( 𝜑 → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) ) = ( ( 𝑋 + ( 𝑀 − 𝐼 ) ) + 𝐻 ) )