Metamath Proof Explorer

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 ‘ ( 𝐴 − 𝑅 ) ) )