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