Step |
Hyp |
Ref |
Expression |
1 |
|
rrx2pnecoorneor.i |
⊢ 𝐼 = { 1 , 2 } |
2 |
|
rrx2pnecoorneor.b |
⊢ 𝑃 = ( ℝ ↑m 𝐼 ) |
3 |
|
rrx2pnedifcoorneor.a |
⊢ 𝐴 = ( ( 𝑌 ‘ 1 ) − ( 𝑋 ‘ 1 ) ) |
4 |
|
rrx2pnedifcoorneorr.b |
⊢ 𝐵 = ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) |
5 |
|
eqid |
⊢ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) |
6 |
1 2 3 5
|
rrx2pnedifcoorneor |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐴 ≠ 0 ∨ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 ) ) |
7 |
|
eqcom |
⊢ ( ( 𝑌 ‘ 2 ) = ( 𝑋 ‘ 2 ) ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) |
8 |
7
|
a1i |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑌 ‘ 2 ) = ( 𝑋 ‘ 2 ) ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) |
9 |
1 2
|
rrx2pyel |
⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℝ ) |
10 |
9
|
recnd |
⊢ ( 𝑋 ∈ 𝑃 → ( 𝑋 ‘ 2 ) ∈ ℂ ) |
11 |
1 2
|
rrx2pyel |
⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℝ ) |
12 |
11
|
recnd |
⊢ ( 𝑌 ∈ 𝑃 → ( 𝑌 ‘ 2 ) ∈ ℂ ) |
13 |
10 12
|
anim12i |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑋 ‘ 2 ) ∈ ℂ ∧ ( 𝑌 ‘ 2 ) ∈ ℂ ) ) |
14 |
13
|
ancomd |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ) → ( ( 𝑌 ‘ 2 ) ∈ ℂ ∧ ( 𝑋 ‘ 2 ) ∈ ℂ ) ) |
15 |
14
|
3adant3 |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑌 ‘ 2 ) ∈ ℂ ∧ ( 𝑋 ‘ 2 ) ∈ ℂ ) ) |
16 |
|
subeq0 |
⊢ ( ( ( 𝑌 ‘ 2 ) ∈ ℂ ∧ ( 𝑋 ‘ 2 ) ∈ ℂ ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 ↔ ( 𝑌 ‘ 2 ) = ( 𝑋 ‘ 2 ) ) ) |
17 |
15 16
|
syl |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 ↔ ( 𝑌 ‘ 2 ) = ( 𝑋 ‘ 2 ) ) ) |
18 |
13
|
3adant3 |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝑋 ‘ 2 ) ∈ ℂ ∧ ( 𝑌 ‘ 2 ) ∈ ℂ ) ) |
19 |
|
subeq0 |
⊢ ( ( ( 𝑋 ‘ 2 ) ∈ ℂ ∧ ( 𝑌 ‘ 2 ) ∈ ℂ ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = 0 ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) |
20 |
18 19
|
syl |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = 0 ↔ ( 𝑋 ‘ 2 ) = ( 𝑌 ‘ 2 ) ) ) |
21 |
8 17 20
|
3bitr4d |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 ↔ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = 0 ) ) |
22 |
4
|
eqcomi |
⊢ ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = 𝐵 |
23 |
22
|
eqeq1i |
⊢ ( ( ( 𝑋 ‘ 2 ) − ( 𝑌 ‘ 2 ) ) = 0 ↔ 𝐵 = 0 ) |
24 |
21 23
|
bitrdi |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) = 0 ↔ 𝐵 = 0 ) ) |
25 |
24
|
necon3bid |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 ↔ 𝐵 ≠ 0 ) ) |
26 |
25
|
orbi2d |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( ( 𝐴 ≠ 0 ∨ ( ( 𝑌 ‘ 2 ) − ( 𝑋 ‘ 2 ) ) ≠ 0 ) ↔ ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) ) |
27 |
6 26
|
mpbid |
⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑋 ≠ 𝑌 ) → ( 𝐴 ≠ 0 ∨ 𝐵 ≠ 0 ) ) |