Step |
Hyp |
Ref |
Expression |
1 |
|
breq1 |
⊢ ( ( abs ‘ 𝑀 ) = 𝑀 → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ 𝑀 ∥ 𝑁 ) ) |
2 |
1
|
bicomd |
⊢ ( ( abs ‘ 𝑀 ) = 𝑀 → ( 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ 𝑁 ) ) |
3 |
2
|
a1i |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) = 𝑀 → ( 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ 𝑁 ) ) ) |
4 |
|
negdvdsb |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ - 𝑀 ∥ 𝑁 ) ) |
5 |
|
breq1 |
⊢ ( ( abs ‘ 𝑀 ) = - 𝑀 → ( ( abs ‘ 𝑀 ) ∥ 𝑁 ↔ - 𝑀 ∥ 𝑁 ) ) |
6 |
5
|
bicomd |
⊢ ( ( abs ‘ 𝑀 ) = - 𝑀 → ( - 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ 𝑁 ) ) |
7 |
4 6
|
sylan9bb |
⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ ( abs ‘ 𝑀 ) = - 𝑀 ) → ( 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ 𝑁 ) ) |
8 |
7
|
ex |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) = - 𝑀 → ( 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ 𝑁 ) ) ) |
9 |
|
zre |
⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℝ ) |
10 |
9
|
absord |
⊢ ( 𝑀 ∈ ℤ → ( ( abs ‘ 𝑀 ) = 𝑀 ∨ ( abs ‘ 𝑀 ) = - 𝑀 ) ) |
11 |
10
|
adantr |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( abs ‘ 𝑀 ) = 𝑀 ∨ ( abs ‘ 𝑀 ) = - 𝑀 ) ) |
12 |
3 8 11
|
mpjaod |
⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 ∥ 𝑁 ↔ ( abs ‘ 𝑀 ) ∥ 𝑁 ) ) |