Step |
Hyp |
Ref |
Expression |
1 |
|
metakunt28.1 |
⊢ ( 𝜑 → 𝑀 ∈ ℕ ) |
2 |
|
metakunt28.2 |
⊢ ( 𝜑 → 𝐼 ∈ ℕ ) |
3 |
|
metakunt28.3 |
⊢ ( 𝜑 → 𝐼 ≤ 𝑀 ) |
4 |
|
metakunt28.4 |
⊢ ( 𝜑 → 𝑋 ∈ ( 1 ... 𝑀 ) ) |
5 |
|
metakunt28.5 |
⊢ 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) |
6 |
|
metakunt28.6 |
⊢ 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) ) |
7 |
|
metakunt28.7 |
⊢ ( 𝜑 → ¬ 𝑋 = 𝐼 ) |
8 |
|
metakunt28.8 |
⊢ ( 𝜑 → ¬ 𝑋 < 𝐼 ) |
9 |
5
|
a1i |
⊢ ( 𝜑 → 𝐴 = ( 𝑥 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) ) ) |
10 |
7
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ¬ 𝑋 = 𝐼 ) |
11 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 ) |
12 |
11
|
eqeq1d |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 = 𝐼 ↔ 𝑋 = 𝐼 ) ) |
13 |
12
|
notbid |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ¬ 𝑥 = 𝐼 ↔ ¬ 𝑋 = 𝐼 ) ) |
14 |
10 13
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ¬ 𝑥 = 𝐼 ) |
15 |
14
|
iffalsed |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) |
16 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ¬ 𝑋 < 𝐼 ) |
17 |
11
|
breq1d |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 < 𝐼 ↔ 𝑋 < 𝐼 ) ) |
18 |
17
|
notbid |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ¬ 𝑥 < 𝐼 ↔ ¬ 𝑋 < 𝐼 ) ) |
19 |
16 18
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ¬ 𝑥 < 𝐼 ) |
20 |
19
|
iffalsed |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = ( 𝑥 − 1 ) ) |
21 |
11
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 − 1 ) = ( 𝑋 − 1 ) ) |
22 |
20 21
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) = ( 𝑋 − 1 ) ) |
23 |
15 22
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → if ( 𝑥 = 𝐼 , 𝑀 , if ( 𝑥 < 𝐼 , 𝑥 , ( 𝑥 − 1 ) ) ) = ( 𝑋 − 1 ) ) |
24 |
4
|
elfzelzd |
⊢ ( 𝜑 → 𝑋 ∈ ℤ ) |
25 |
|
1zzd |
⊢ ( 𝜑 → 1 ∈ ℤ ) |
26 |
24 25
|
zsubcld |
⊢ ( 𝜑 → ( 𝑋 − 1 ) ∈ ℤ ) |
27 |
9 23 4 26
|
fvmptd |
⊢ ( 𝜑 → ( 𝐴 ‘ 𝑋 ) = ( 𝑋 − 1 ) ) |
28 |
27
|
fveq2d |
⊢ ( 𝜑 → ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝐵 ‘ ( 𝑋 − 1 ) ) ) |
29 |
6
|
a1i |
⊢ ( 𝜑 → 𝐵 = ( 𝑧 ∈ ( 1 ... 𝑀 ) ↦ if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) ) ) |
30 |
26
|
zred |
⊢ ( 𝜑 → ( 𝑋 − 1 ) ∈ ℝ ) |
31 |
24
|
zred |
⊢ ( 𝜑 → 𝑋 ∈ ℝ ) |
32 |
1
|
nnred |
⊢ ( 𝜑 → 𝑀 ∈ ℝ ) |
33 |
|
1rp |
⊢ 1 ∈ ℝ+ |
34 |
33
|
a1i |
⊢ ( 𝜑 → 1 ∈ ℝ+ ) |
35 |
31 34
|
ltsubrpd |
⊢ ( 𝜑 → ( 𝑋 − 1 ) < 𝑋 ) |
36 |
|
elfzle2 |
⊢ ( 𝑋 ∈ ( 1 ... 𝑀 ) → 𝑋 ≤ 𝑀 ) |
37 |
4 36
|
syl |
⊢ ( 𝜑 → 𝑋 ≤ 𝑀 ) |
38 |
30 31 32 35 37
|
ltletrd |
⊢ ( 𝜑 → ( 𝑋 − 1 ) < 𝑀 ) |
39 |
30 38
|
ltned |
⊢ ( 𝜑 → ( 𝑋 − 1 ) ≠ 𝑀 ) |
40 |
39
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( 𝑋 − 1 ) ≠ 𝑀 ) |
41 |
40
|
neneqd |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ¬ ( 𝑋 − 1 ) = 𝑀 ) |
42 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → 𝑧 = ( 𝑋 − 1 ) ) |
43 |
42
|
eqeq1d |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( 𝑧 = 𝑀 ↔ ( 𝑋 − 1 ) = 𝑀 ) ) |
44 |
43
|
notbid |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( ¬ 𝑧 = 𝑀 ↔ ¬ ( 𝑋 − 1 ) = 𝑀 ) ) |
45 |
41 44
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ¬ 𝑧 = 𝑀 ) |
46 |
45
|
iffalsed |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) = if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) |
47 |
7
|
neqned |
⊢ ( 𝜑 → 𝑋 ≠ 𝐼 ) |
48 |
2
|
nnred |
⊢ ( 𝜑 → 𝐼 ∈ ℝ ) |
49 |
48 31 8
|
nltled |
⊢ ( 𝜑 → 𝐼 ≤ 𝑋 ) |
50 |
48 31 49
|
leltned |
⊢ ( 𝜑 → ( 𝐼 < 𝑋 ↔ 𝑋 ≠ 𝐼 ) ) |
51 |
47 50
|
mpbird |
⊢ ( 𝜑 → 𝐼 < 𝑋 ) |
52 |
2
|
nnzd |
⊢ ( 𝜑 → 𝐼 ∈ ℤ ) |
53 |
52 24
|
zltlem1d |
⊢ ( 𝜑 → ( 𝐼 < 𝑋 ↔ 𝐼 ≤ ( 𝑋 − 1 ) ) ) |
54 |
51 53
|
mpbid |
⊢ ( 𝜑 → 𝐼 ≤ ( 𝑋 − 1 ) ) |
55 |
48 30
|
lenltd |
⊢ ( 𝜑 → ( 𝐼 ≤ ( 𝑋 − 1 ) ↔ ¬ ( 𝑋 − 1 ) < 𝐼 ) ) |
56 |
54 55
|
mpbid |
⊢ ( 𝜑 → ¬ ( 𝑋 − 1 ) < 𝐼 ) |
57 |
56
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ¬ ( 𝑋 − 1 ) < 𝐼 ) |
58 |
42
|
breq1d |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( 𝑧 < 𝐼 ↔ ( 𝑋 − 1 ) < 𝐼 ) ) |
59 |
58
|
notbid |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( ¬ 𝑧 < 𝐼 ↔ ¬ ( 𝑋 − 1 ) < 𝐼 ) ) |
60 |
57 59
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ¬ 𝑧 < 𝐼 ) |
61 |
60
|
iffalsed |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) = ( 𝑧 + ( 1 − 𝐼 ) ) ) |
62 |
42
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( 𝑧 + ( 1 − 𝐼 ) ) = ( ( 𝑋 − 1 ) + ( 1 − 𝐼 ) ) ) |
63 |
24
|
zcnd |
⊢ ( 𝜑 → 𝑋 ∈ ℂ ) |
64 |
|
1cnd |
⊢ ( 𝜑 → 1 ∈ ℂ ) |
65 |
2
|
nncnd |
⊢ ( 𝜑 → 𝐼 ∈ ℂ ) |
66 |
63 64 65
|
npncand |
⊢ ( 𝜑 → ( ( 𝑋 − 1 ) + ( 1 − 𝐼 ) ) = ( 𝑋 − 𝐼 ) ) |
67 |
66
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( ( 𝑋 − 1 ) + ( 1 − 𝐼 ) ) = ( 𝑋 − 𝐼 ) ) |
68 |
62 67
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → ( 𝑧 + ( 1 − 𝐼 ) ) = ( 𝑋 − 𝐼 ) ) |
69 |
61 68
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) = ( 𝑋 − 𝐼 ) ) |
70 |
46 69
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑧 = ( 𝑋 − 1 ) ) → if ( 𝑧 = 𝑀 , 𝑀 , if ( 𝑧 < 𝐼 , ( 𝑧 + ( 𝑀 − 𝐼 ) ) , ( 𝑧 + ( 1 − 𝐼 ) ) ) ) = ( 𝑋 − 𝐼 ) ) |
71 |
1
|
nnzd |
⊢ ( 𝜑 → 𝑀 ∈ ℤ ) |
72 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
73 |
2
|
nnge1d |
⊢ ( 𝜑 → 1 ≤ 𝐼 ) |
74 |
72 48 31 73 51
|
lelttrd |
⊢ ( 𝜑 → 1 < 𝑋 ) |
75 |
25 24
|
zltlem1d |
⊢ ( 𝜑 → ( 1 < 𝑋 ↔ 1 ≤ ( 𝑋 − 1 ) ) ) |
76 |
74 75
|
mpbid |
⊢ ( 𝜑 → 1 ≤ ( 𝑋 − 1 ) ) |
77 |
31 72
|
resubcld |
⊢ ( 𝜑 → ( 𝑋 − 1 ) ∈ ℝ ) |
78 |
|
0le1 |
⊢ 0 ≤ 1 |
79 |
78
|
a1i |
⊢ ( 𝜑 → 0 ≤ 1 ) |
80 |
31 72
|
subge02d |
⊢ ( 𝜑 → ( 0 ≤ 1 ↔ ( 𝑋 − 1 ) ≤ 𝑋 ) ) |
81 |
79 80
|
mpbid |
⊢ ( 𝜑 → ( 𝑋 − 1 ) ≤ 𝑋 ) |
82 |
77 31 32 81 37
|
letrd |
⊢ ( 𝜑 → ( 𝑋 − 1 ) ≤ 𝑀 ) |
83 |
25 71 26 76 82
|
elfzd |
⊢ ( 𝜑 → ( 𝑋 − 1 ) ∈ ( 1 ... 𝑀 ) ) |
84 |
24 52
|
zsubcld |
⊢ ( 𝜑 → ( 𝑋 − 𝐼 ) ∈ ℤ ) |
85 |
29 70 83 84
|
fvmptd |
⊢ ( 𝜑 → ( 𝐵 ‘ ( 𝑋 − 1 ) ) = ( 𝑋 − 𝐼 ) ) |
86 |
28 85
|
eqtrd |
⊢ ( 𝜑 → ( 𝐵 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑋 − 𝐼 ) ) |