rrx2pnedifcoorneor

Description: If two different points X and Y in a real Euclidean space of dimension 2 are different, then at least one difference of two corresponding coordinates is not 0. (Contributed by AV, 26-Feb-2023)

	Ref	Expression
Hypotheses	rrx2pnecoorneor.i	$⊢ I = \{1, 2\}$
	rrx2pnecoorneor.b	$⊢ P = ℝ^{I}$
	rrx2pnedifcoorneor.a	$⊢ A = Y (1) - X (1)$
	rrx2pnedifcoorneor.b	$⊢ B = Y (2) - X (2)$
Assertion	rrx2pnedifcoorneor	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (A \neq 0 \lor B \neq 0)$

Proof

Step	Hyp	Ref	Expression
1		rrx2pnecoorneor.i	$⊢ I = \{1, 2\}$
2		rrx2pnecoorneor.b	$⊢ P = ℝ^{I}$
3		rrx2pnedifcoorneor.a	$⊢ A = Y (1) - X (1)$
4		rrx2pnedifcoorneor.b	$⊢ B = Y (2) - X (2)$
5	1 2	rrx2pnecoorneor	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (X (1) \neq Y (1) \lor X (2) \neq Y (2))$
6	3	neeq1i	$⊢ A \neq 0 \leftrightarrow Y (1) - X (1) \neq 0$
7	4	neeq1i	$⊢ B \neq 0 \leftrightarrow Y (2) - X (2) \neq 0$
8	6 7	orbi12i	$⊢ (A \neq 0 \lor B \neq 0) \leftrightarrow (Y (1) - X (1) \neq 0 \lor Y (2) - X (2) \neq 0)$
9	1 2	rrx2pxel	$⊢ Y \in P \to Y (1) \in ℝ$
10	9	recnd	$⊢ Y \in P \to Y (1) \in ℂ$
11	1 2	rrx2pxel	$⊢ X \in P \to X (1) \in ℝ$
12	11	recnd	$⊢ X \in P \to X (1) \in ℂ$
13		subeq0	$⊢ (Y (1) \in ℂ \land X (1) \in ℂ) \to (Y (1) - X (1) = 0 \leftrightarrow Y (1) = X (1))$
14	10 12 13	syl2anr	$⊢ (X \in P \land Y \in P) \to (Y (1) - X (1) = 0 \leftrightarrow Y (1) = X (1))$
15	14	necon3bid	$⊢ (X \in P \land Y \in P) \to (Y (1) - X (1) \neq 0 \leftrightarrow Y (1) \neq X (1))$
16	1 2	rrx2pyel	$⊢ Y \in P \to Y (2) \in ℝ$
17	16	recnd	$⊢ Y \in P \to Y (2) \in ℂ$
18	1 2	rrx2pyel	$⊢ X \in P \to X (2) \in ℝ$
19	18	recnd	$⊢ X \in P \to X (2) \in ℂ$
20		subeq0	$⊢ (Y (2) \in ℂ \land X (2) \in ℂ) \to (Y (2) - X (2) = 0 \leftrightarrow Y (2) = X (2))$
21	17 19 20	syl2anr	$⊢ (X \in P \land Y \in P) \to (Y (2) - X (2) = 0 \leftrightarrow Y (2) = X (2))$
22	21	necon3bid	$⊢ (X \in P \land Y \in P) \to (Y (2) - X (2) \neq 0 \leftrightarrow Y (2) \neq X (2))$
23	15 22	orbi12d	$⊢ (X \in P \land Y \in P) \to ((Y (1) - X (1) \neq 0 \lor Y (2) - X (2) \neq 0) \leftrightarrow (Y (1) \neq X (1) \lor Y (2) \neq X (2)))$
24		necom	$⊢ Y (1) \neq X (1) \leftrightarrow X (1) \neq Y (1)$
25		necom	$⊢ Y (2) \neq X (2) \leftrightarrow X (2) \neq Y (2)$
26	24 25	orbi12i	$⊢ (Y (1) \neq X (1) \lor Y (2) \neq X (2)) \leftrightarrow (X (1) \neq Y (1) \lor X (2) \neq Y (2))$
27	23 26	bitrdi	$⊢ (X \in P \land Y \in P) \to ((Y (1) - X (1) \neq 0 \lor Y (2) - X (2) \neq 0) \leftrightarrow (X (1) \neq Y (1) \lor X (2) \neq Y (2)))$
28	8 27	syl5bb	$⊢ (X \in P \land Y \in P) \to ((A \neq 0 \lor B \neq 0) \leftrightarrow (X (1) \neq Y (1) \lor X (2) \neq Y (2)))$
29	28	3adant3	$⊢ (X \in P \land Y \in P \land X \neq Y) \to ((A \neq 0 \lor B \neq 0) \leftrightarrow (X (1) \neq Y (1) \lor X (2) \neq Y (2)))$
30	5 29	mpbird	$⊢ (X \in P \land Y \in P \land X \neq Y) \to (A \neq 0 \lor B \neq 0)$

Metamath Proof Explorer

Theorem rrx2pnedifcoorneor

Proof