Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for metakunt
Permutation results
metakunt13
Next ⟩
metakunt14
Metamath Proof Explorer
Ascii
Unicode
Theorem
metakunt13
Description:
C is the right inverse for A.
(Contributed by
metakunt
, 25-May-2024)
Ref
Expression
Hypotheses
metakunt13.1
⊢
φ
→
M
∈
ℕ
metakunt13.2
⊢
φ
→
I
∈
ℕ
metakunt13.3
⊢
φ
→
I
≤
M
metakunt13.4
⊢
A
=
x
∈
1
…
M
⟼
if
x
=
I
M
if
x
<
I
x
x
−
1
metakunt13.5
⊢
C
=
y
∈
1
…
M
⟼
if
y
=
M
I
if
y
<
I
y
y
+
1
metakunt13.6
⊢
φ
→
X
∈
1
…
M
Assertion
metakunt13
⊢
φ
→
A
⁡
C
⁡
X
=
X
Proof
Step
Hyp
Ref
Expression
1
metakunt13.1
⊢
φ
→
M
∈
ℕ
2
metakunt13.2
⊢
φ
→
I
∈
ℕ
3
metakunt13.3
⊢
φ
→
I
≤
M
4
metakunt13.4
⊢
A
=
x
∈
1
…
M
⟼
if
x
=
I
M
if
x
<
I
x
x
−
1
5
metakunt13.5
⊢
C
=
y
∈
1
…
M
⟼
if
y
=
M
I
if
y
<
I
y
y
+
1
6
metakunt13.6
⊢
φ
→
X
∈
1
…
M
7
1
2
3
4
5
6
metakunt10
⊢
φ
∧
X
=
M
→
A
⁡
C
⁡
X
=
X
8
7
ex
⊢
φ
→
X
=
M
→
A
⁡
C
⁡
X
=
X
9
1
2
3
4
5
6
metakunt11
⊢
φ
∧
X
<
I
→
A
⁡
C
⁡
X
=
X
10
9
ex
⊢
φ
→
X
<
I
→
A
⁡
C
⁡
X
=
X
11
1
2
3
4
5
6
metakunt12
⊢
φ
∧
¬
X
=
M
∨
X
<
I
→
A
⁡
C
⁡
X
=
X
12
11
ex
⊢
φ
→
¬
X
=
M
∨
X
<
I
→
A
⁡
C
⁡
X
=
X
13
8
10
12
ecase3d
⊢
φ
→
A
⁡
C
⁡
X
=
X