Step |
Hyp |
Ref |
Expression |
1 |
|
addclpr |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( 𝐴 +P 𝐵 ) ∈ P ) |
2 |
|
eleq1 |
⊢ ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) → ( ( 𝐴 +P 𝐵 ) ∈ P ↔ ( 𝐴 +P 𝐶 ) ∈ P ) ) |
3 |
|
dmplp |
⊢ dom +P = ( P × P ) |
4 |
|
0npr |
⊢ ¬ ∅ ∈ P |
5 |
3 4
|
ndmovrcl |
⊢ ( ( 𝐴 +P 𝐶 ) ∈ P → ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ) |
6 |
2 5
|
syl6bi |
⊢ ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) → ( ( 𝐴 +P 𝐵 ) ∈ P → ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ) ) |
7 |
1 6
|
syl5com |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) → ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ) ) |
8 |
|
ltapr |
⊢ ( 𝐴 ∈ P → ( 𝐵 <P 𝐶 ↔ ( 𝐴 +P 𝐵 ) <P ( 𝐴 +P 𝐶 ) ) ) |
9 |
|
ltapr |
⊢ ( 𝐴 ∈ P → ( 𝐶 <P 𝐵 ↔ ( 𝐴 +P 𝐶 ) <P ( 𝐴 +P 𝐵 ) ) ) |
10 |
8 9
|
orbi12d |
⊢ ( 𝐴 ∈ P → ( ( 𝐵 <P 𝐶 ∨ 𝐶 <P 𝐵 ) ↔ ( ( 𝐴 +P 𝐵 ) <P ( 𝐴 +P 𝐶 ) ∨ ( 𝐴 +P 𝐶 ) <P ( 𝐴 +P 𝐵 ) ) ) ) |
11 |
10
|
notbid |
⊢ ( 𝐴 ∈ P → ( ¬ ( 𝐵 <P 𝐶 ∨ 𝐶 <P 𝐵 ) ↔ ¬ ( ( 𝐴 +P 𝐵 ) <P ( 𝐴 +P 𝐶 ) ∨ ( 𝐴 +P 𝐶 ) <P ( 𝐴 +P 𝐵 ) ) ) ) |
12 |
11
|
ad2antrr |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ) → ( ¬ ( 𝐵 <P 𝐶 ∨ 𝐶 <P 𝐵 ) ↔ ¬ ( ( 𝐴 +P 𝐵 ) <P ( 𝐴 +P 𝐶 ) ∨ ( 𝐴 +P 𝐶 ) <P ( 𝐴 +P 𝐵 ) ) ) ) |
13 |
|
ltsopr |
⊢ <P Or P |
14 |
|
sotrieq |
⊢ ( ( <P Or P ∧ ( 𝐵 ∈ P ∧ 𝐶 ∈ P ) ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 <P 𝐶 ∨ 𝐶 <P 𝐵 ) ) ) |
15 |
13 14
|
mpan |
⊢ ( ( 𝐵 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 <P 𝐶 ∨ 𝐶 <P 𝐵 ) ) ) |
16 |
15
|
ad2ant2l |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ) → ( 𝐵 = 𝐶 ↔ ¬ ( 𝐵 <P 𝐶 ∨ 𝐶 <P 𝐵 ) ) ) |
17 |
|
addclpr |
⊢ ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( 𝐴 +P 𝐶 ) ∈ P ) |
18 |
|
sotrieq |
⊢ ( ( <P Or P ∧ ( ( 𝐴 +P 𝐵 ) ∈ P ∧ ( 𝐴 +P 𝐶 ) ∈ P ) ) → ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) ↔ ¬ ( ( 𝐴 +P 𝐵 ) <P ( 𝐴 +P 𝐶 ) ∨ ( 𝐴 +P 𝐶 ) <P ( 𝐴 +P 𝐵 ) ) ) ) |
19 |
13 18
|
mpan |
⊢ ( ( ( 𝐴 +P 𝐵 ) ∈ P ∧ ( 𝐴 +P 𝐶 ) ∈ P ) → ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) ↔ ¬ ( ( 𝐴 +P 𝐵 ) <P ( 𝐴 +P 𝐶 ) ∨ ( 𝐴 +P 𝐶 ) <P ( 𝐴 +P 𝐵 ) ) ) ) |
20 |
1 17 19
|
syl2an |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ) → ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) ↔ ¬ ( ( 𝐴 +P 𝐵 ) <P ( 𝐴 +P 𝐶 ) ∨ ( 𝐴 +P 𝐶 ) <P ( 𝐴 +P 𝐵 ) ) ) ) |
21 |
12 16 20
|
3bitr4d |
⊢ ( ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) ∧ ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) ) → ( 𝐵 = 𝐶 ↔ ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) ) ) |
22 |
21
|
exbiri |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐴 ∈ P ∧ 𝐶 ∈ P ) → ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) → 𝐵 = 𝐶 ) ) ) |
23 |
7 22
|
syld |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) → ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) → 𝐵 = 𝐶 ) ) ) |
24 |
23
|
pm2.43d |
⊢ ( ( 𝐴 ∈ P ∧ 𝐵 ∈ P ) → ( ( 𝐴 +P 𝐵 ) = ( 𝐴 +P 𝐶 ) → 𝐵 = 𝐶 ) ) |