Theorem irrdifflemf

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

	Ref	Expression
Hypotheses	irrdifflemf.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	irrdifflemf.irr	⊢ ( 𝜑 → ¬ 𝐴 ∈ ℚ )
	irrdifflemf.q	⊢ ( 𝜑 → 𝑄 ∈ ℚ )
	irrdifflemf.r	⊢ ( 𝜑 → 𝑅 ∈ ℚ )
	irrdifflemf.qr	⊢ ( 𝜑 → 𝑄 ≠ 𝑅 )
Assertion	irrdifflemf	⊢ ( 𝜑 → ( abs ‘ ( 𝐴 − 𝑄 ) ) ≠ ( abs ‘ ( 𝐴 − 𝑅 ) ) )

Proof

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