Metamath Proof Explorer

Theorem irrdifflemf

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

Ref Expression
Hypotheses irrdifflemf.a 
|- ( ph -> A e. RR )
irrdifflemf.irr 
|- ( ph -> -. A e. QQ )
irrdifflemf.q 
|- ( ph -> Q e. QQ )
irrdifflemf.r 
|- ( ph -> R e. QQ )
irrdifflemf.qr 
|- ( ph -> Q =/= R )
Assertion irrdifflemf 
|- ( ph -> ( abs ` ( A - Q ) ) =/= ( abs ` ( A - R ) ) )

Proof

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