Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Stefan O'Rear
X and Y sequences 2: Order properties
rmyeq
Next ⟩
lermy
Metamath Proof Explorer
Ascii
Unicode
Theorem
rmyeq
Description:
Y is one-to-one.
(Contributed by
Stefan O'Rear
, 3-Oct-2014)
Ref
Expression
Assertion
rmyeq
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
∧
N
∈
ℤ
→
M
=
N
↔
A
Y
rm
M
=
A
Y
rm
N
Proof
Step
Hyp
Ref
Expression
1
oveq2
⊢
a
=
b
→
A
Y
rm
a
=
A
Y
rm
b
2
oveq2
⊢
a
=
M
→
A
Y
rm
a
=
A
Y
rm
M
3
oveq2
⊢
a
=
N
→
A
Y
rm
a
=
A
Y
rm
N
4
zssre
⊢
ℤ
⊆
ℝ
5
frmy
⊢
Y
rm
:
ℤ
≥
2
×
ℤ
⟶
ℤ
6
5
fovcl
⊢
A
∈
ℤ
≥
2
∧
a
∈
ℤ
→
A
Y
rm
a
∈
ℤ
7
6
zred
⊢
A
∈
ℤ
≥
2
∧
a
∈
ℤ
→
A
Y
rm
a
∈
ℝ
8
ltrmy
⊢
A
∈
ℤ
≥
2
∧
a
∈
ℤ
∧
b
∈
ℤ
→
a
<
b
↔
A
Y
rm
a
<
A
Y
rm
b
9
8
biimpd
⊢
A
∈
ℤ
≥
2
∧
a
∈
ℤ
∧
b
∈
ℤ
→
a
<
b
→
A
Y
rm
a
<
A
Y
rm
b
10
9
3expb
⊢
A
∈
ℤ
≥
2
∧
a
∈
ℤ
∧
b
∈
ℤ
→
a
<
b
→
A
Y
rm
a
<
A
Y
rm
b
11
1
2
3
4
7
10
eqord1
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
∧
N
∈
ℤ
→
M
=
N
↔
A
Y
rm
M
=
A
Y
rm
N
12
11
3impb
⊢
A
∈
ℤ
≥
2
∧
M
∈
ℤ
∧
N
∈
ℤ
→
M
=
N
↔
A
Y
rm
M
=
A
Y
rm
N