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 addid1d ( ( 𝜑 ∧ ( 𝑋 + ( 𝑀𝐼 ) ) < 𝐼 ) → ( ( 𝑋 + ( 𝑀𝐼 ) ) + 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 ( 𝜑 → ( 𝐶 ‘ ( 𝐵 ‘ ( 𝐴𝑋 ) ) ) = ( ( 𝑋 + ( 𝑀𝐼 ) ) + 𝐻 ) )