irrdifflemf

Description: Lemma for irrdiff . The forward direction. (Contributed by Jim Kingdon, 20-May-2024)

	Ref	Expression
Hypotheses	irrdifflemf.a	$⊢ φ \to A \in ℝ$
	irrdifflemf.irr	$⊢ φ \to \neg A \in ℚ$
	irrdifflemf.q	$⊢ φ \to Q \in ℚ$
	irrdifflemf.r	$⊢ φ \to R \in ℚ$
	irrdifflemf.qr	$⊢ φ \to Q \neq R$
Assertion	irrdifflemf	$⊢ φ \to \|A - Q\| \neq \|A - R\|$

Proof

Step	Hyp	Ref	Expression
1		irrdifflemf.a	$⊢ φ \to A \in ℝ$
2		irrdifflemf.irr	$⊢ φ \to \neg A \in ℚ$
3		irrdifflemf.q	$⊢ φ \to Q \in ℚ$
4		irrdifflemf.r	$⊢ φ \to R \in ℚ$
5		irrdifflemf.qr	$⊢ φ \to Q \neq R$
6		simplll	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = A - R) \to φ$
7		simpllr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = A - R) \to \|A - Q\| = \|A - R\|$
8		simplr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = A - R) \to \|A - Q\| = A - Q$
9		simpr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = A - R) \to \|A - R\| = A - R$
10	7 8 9	3eqtr3d	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = A - R) \to A - Q = A - R$
11	1	recnd	$⊢ φ \to A \in ℂ$
12	11	adantr	$⊢ (φ \land A - Q = A - R) \to A \in ℂ$
13		qre	$⊢ Q \in ℚ \to Q \in ℝ$
14	3 13	syl	$⊢ φ \to Q \in ℝ$
15	14	recnd	$⊢ φ \to Q \in ℂ$
16	15	adantr	$⊢ (φ \land A - Q = A - R) \to Q \in ℂ$
17		qre	$⊢ R \in ℚ \to R \in ℝ$
18	4 17	syl	$⊢ φ \to R \in ℝ$
19	18	recnd	$⊢ φ \to R \in ℂ$
20	19	adantr	$⊢ (φ \land A - Q = A - R) \to R \in ℂ$
21		simpr	$⊢ (φ \land A - Q = A - R) \to A - Q = A - R$
22	12 16 20 21	subcand	$⊢ (φ \land A - Q = A - R) \to Q = R$
23	5	adantr	$⊢ (φ \land A - Q = A - R) \to Q \neq R$
24	22 23	pm2.21ddne	$⊢ (φ \land A - Q = A - R) \to ⊥$
25	6 10 24	syl2anc	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = A - R) \to ⊥$
26		simplll	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = - (A - R)) \to φ$
27		simpllr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = - (A - R)) \to \|A - Q\| = \|A - R\|$
28		simplr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = - (A - R)) \to \|A - Q\| = A - Q$
29		simpr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = - (A - R)) \to \|A - R\| = - (A - R)$
30	27 28 29	3eqtr3d	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = - (A - R)) \to A - Q = - (A - R)$
31		2cnd	$⊢ (φ \land A - Q = - (A - R)) \to 2 \in ℂ$
32	11	adantr	$⊢ (φ \land A - Q = - (A - R)) \to A \in ℂ$
33		2ne0	$⊢ 2 \neq 0$
34	33	a1i	$⊢ (φ \land A - Q = - (A - R)) \to 2 \neq 0$
35	32	2timesd	$⊢ (φ \land A - Q = - (A - R)) \to 2 A = A + A$
36		simpr	$⊢ (φ \land A - Q = - (A - R)) \to A - Q = - (A - R)$
37	19	adantr	$⊢ (φ \land A - Q = - (A - R)) \to R \in ℂ$
38	32 37	negsubdi2d	$⊢ (φ \land A - Q = - (A - R)) \to - (A - R) = R - A$
39	36 38	eqtrd	$⊢ (φ \land A - Q = - (A - R)) \to A - Q = R - A$
40	15	adantr	$⊢ (φ \land A - Q = - (A - R)) \to Q \in ℂ$
41	40 37 32 32	addsubeq4d	$⊢ (φ \land A - Q = - (A - R)) \to (Q + R = A + A \leftrightarrow A - Q = R - A)$
42	39 41	mpbird	$⊢ (φ \land A - Q = - (A - R)) \to Q + R = A + A$
43	35 42	eqtr4d	$⊢ (φ \land A - Q = - (A - R)) \to 2 A = Q + R$
44	31 32 34 43	mvllmuld	$⊢ (φ \land A - Q = - (A - R)) \to A = \frac{Q + R}{2}$
45	3	adantr	$⊢ (φ \land A - Q = - (A - R)) \to Q \in ℚ$
46	4	adantr	$⊢ (φ \land A - Q = - (A - R)) \to R \in ℚ$
47		qaddcl	$⊢ (Q \in ℚ \land R \in ℚ) \to Q + R \in ℚ$
48	45 46 47	syl2anc	$⊢ (φ \land A - Q = - (A - R)) \to Q + R \in ℚ$
49		2z	$⊢ 2 \in ℤ$
50		zq	$⊢ 2 \in ℤ \to 2 \in ℚ$
51	49 50	mp1i	$⊢ (φ \land A - Q = - (A - R)) \to 2 \in ℚ$
52		qdivcl	$⊢ (Q + R \in ℚ \land 2 \in ℚ \land 2 \neq 0) \to \frac{Q + R}{2} \in ℚ$
53	48 51 34 52	syl3anc	$⊢ (φ \land A - Q = - (A - R)) \to \frac{Q + R}{2} \in ℚ$
54	44 53	eqeltrd	$⊢ (φ \land A - Q = - (A - R)) \to A \in ℚ$
55	2	adantr	$⊢ (φ \land A - Q = - (A - R)) \to \neg A \in ℚ$
56	54 55	pm2.21fal	$⊢ (φ \land A - Q = - (A - R)) \to ⊥$
57	26 30 56	syl2anc	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \land \|A - R\| = - (A - R)) \to ⊥$
58	1 18	resubcld	$⊢ φ \to A - R \in ℝ$
59	58	absord	$⊢ φ \to (\|A - R\| = A - R \lor \|A - R\| = - (A - R))$
60	59	ad2antrr	$⊢ ((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \to (\|A - R\| = A - R \lor \|A - R\| = - (A - R))$
61	25 57 60	mpjaodan	$⊢ ((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = A - Q) \to ⊥$
62		simplll	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = A - R) \to φ$
63		simpllr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = A - R) \to \|A - Q\| = \|A - R\|$
64		simplr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = A - R) \to \|A - Q\| = - (A - Q)$
65		simpr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = A - R) \to \|A - R\| = A - R$
66	63 64 65	3eqtr3rd	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = A - R) \to A - R = - (A - Q)$
67	58	recnd	$⊢ φ \to A - R \in ℂ$
68	67	ad3antrrr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = A - R) \to A - R \in ℂ$
69	1 14	resubcld	$⊢ φ \to A - Q \in ℝ$
70	69	recnd	$⊢ φ \to A - Q \in ℂ$
71	70	ad3antrrr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = A - R) \to A - Q \in ℂ$
72		negcon2	$⊢ (A - R \in ℂ \land A - Q \in ℂ) \to (A - R = - (A - Q) \leftrightarrow A - Q = - (A - R))$
73	68 71 72	syl2anc	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = A - R) \to (A - R = - (A - Q) \leftrightarrow A - Q = - (A - R))$
74	66 73	mpbid	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = A - R) \to A - Q = - (A - R)$
75	62 74 56	syl2anc	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = A - R) \to ⊥$
76		simplll	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = - (A - R)) \to φ$
77	70	ad3antrrr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = - (A - R)) \to A - Q \in ℂ$
78	67	ad3antrrr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = - (A - R)) \to A - R \in ℂ$
79		simpllr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = - (A - R)) \to \|A - Q\| = \|A - R\|$
80		simplr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = - (A - R)) \to \|A - Q\| = - (A - Q)$
81		simpr	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = - (A - R)) \to \|A - R\| = - (A - R)$
82	79 80 81	3eqtr3d	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = - (A - R)) \to - (A - Q) = - (A - R)$
83	77 78 82	neg11d	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = - (A - R)) \to A - Q = A - R$
84	76 83 24	syl2anc	$⊢ (((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \land \|A - R\| = - (A - R)) \to ⊥$
85	59	ad2antrr	$⊢ ((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \to (\|A - R\| = A - R \lor \|A - R\| = - (A - R))$
86	75 84 85	mpjaodan	$⊢ ((φ \land \|A - Q\| = \|A - R\|) \land \|A - Q\| = - (A - Q)) \to ⊥$
87	69	absord	$⊢ φ \to (\|A - Q\| = A - Q \lor \|A - Q\| = - (A - Q))$
88	87	adantr	$⊢ (φ \land \|A - Q\| = \|A - R\|) \to (\|A - Q\| = A - Q \lor \|A - Q\| = - (A - Q))$
89	61 86 88	mpjaodan	$⊢ (φ \land \|A - Q\| = \|A - R\|) \to ⊥$
90	89	ex	$⊢ φ \to (\|A - Q\| = \|A - R\| \to ⊥)$
91		df-ne	$⊢ \|A - Q\| \neq \|A - R\| \leftrightarrow \neg \|A - Q\| = \|A - R\|$
92		dfnot	$⊢ \neg \|A - Q\| = \|A - R\| \leftrightarrow (\|A - Q\| = \|A - R\| \to ⊥)$
93	91 92	bitri	$⊢ \|A - Q\| \neq \|A - R\| \leftrightarrow (\|A - Q\| = \|A - R\| \to ⊥)$
94	90 93	sylibr	$⊢ φ \to \|A - Q\| \neq \|A - R\|$

Metamath Proof Explorer

Theorem irrdifflemf

Proof