Metamath Proof Explorer

Theorem qirropth

Description: This lemma implements the concept of "equate rational and irrational parts", used to prove many arithmetical properties of the X and Y sequences. (Contributed by Stefan O'Rear, 21-Sep-2014)

Ref Expression
Assertion qirropth 
|- ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) -> ( ( B + ( A x. C ) ) = ( D + ( A x. E ) ) <-> ( B = D /\ C = E ) ) )

Proof

Step Hyp Ref Expression
1 eldifn 
 |-  ( A e. ( CC \ QQ ) -> -. A e. QQ )
2 1 3ad2ant1 
 |-  ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) -> -. A e. QQ )
3 2 adantr 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> -. A e. QQ )
4 simpll1 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> A e. ( CC \ QQ ) )
5 4 eldifad 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> A e. CC )
6 simp2r 
 |-  ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) -> C e. QQ )
7 6 ad2antrr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> C e. QQ )
8 qcn 
 |-  ( C e. QQ -> C e. CC )
9 7 8 syl 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> C e. CC )
10 simp3r 
 |-  ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) -> E e. QQ )
11 10 ad2antrr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> E e. QQ )
12 qcn 
 |-  ( E e. QQ -> E e. CC )
13 11 12 syl 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> E e. CC )
14 5 9 13 subdid 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( A x. ( C - E ) ) = ( ( A x. C ) - ( A x. E ) ) )
15 qsubcl 
 |-  ( ( C e. QQ /\ E e. QQ ) -> ( C - E ) e. QQ )
16 7 11 15 syl2anc 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( C - E ) e. QQ )
17 qcn 
 |-  ( ( C - E ) e. QQ -> ( C - E ) e. CC )
18 16 17 syl 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( C - E ) e. CC )
19 18 5 mulcomd 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( ( C - E ) x. A ) = ( A x. ( C - E ) ) )
20 simplr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( B + ( A x. C ) ) = ( D + ( A x. E ) ) )
21 simp2l 
 |-  ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) -> B e. QQ )
22 21 ad2antrr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> B e. QQ )
23 qcn 
 |-  ( B e. QQ -> B e. CC )
24 22 23 syl 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> B e. CC )
25 5 9 mulcld 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( A x. C ) e. CC )
26 simp3l 
 |-  ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) -> D e. QQ )
27 26 ad2antrr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> D e. QQ )
28 qcn 
 |-  ( D e. QQ -> D e. CC )
29 27 28 syl 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> D e. CC )
30 5 13 mulcld 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( A x. E ) e. CC )
31 24 25 29 30 addsubeq4d 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( ( B + ( A x. C ) ) = ( D + ( A x. E ) ) <-> ( D - B ) = ( ( A x. C ) - ( A x. E ) ) ) )
32 20 31 mpbid 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( D - B ) = ( ( A x. C ) - ( A x. E ) ) )
33 14 19 32 3eqtr4d 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( ( C - E ) x. A ) = ( D - B ) )
34 qsubcl 
 |-  ( ( D e. QQ /\ B e. QQ ) -> ( D - B ) e. QQ )
35 27 22 34 syl2anc 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( D - B ) e. QQ )
36 qcn 
 |-  ( ( D - B ) e. QQ -> ( D - B ) e. CC )
37 35 36 syl 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( D - B ) e. CC )
38 simpr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> -. C = E )
39 subeq0 
 |-  ( ( C e. CC /\ E e. CC ) -> ( ( C - E ) = 0 <-> C = E ) )
40 39 necon3abid 
 |-  ( ( C e. CC /\ E e. CC ) -> ( ( C - E ) =/= 0 <-> -. C = E ) )
41 9 13 40 syl2anc 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( ( C - E ) =/= 0 <-> -. C = E ) )
42 38 41 mpbird 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( C - E ) =/= 0 )
43 37 18 5 42 divmuld 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( ( ( D - B ) / ( C - E ) ) = A <-> ( ( C - E ) x. A ) = ( D - B ) ) )
44 33 43 mpbird 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( ( D - B ) / ( C - E ) ) = A )
45 qdivcl 
 |-  ( ( ( D - B ) e. QQ /\ ( C - E ) e. QQ /\ ( C - E ) =/= 0 ) -> ( ( D - B ) / ( C - E ) ) e. QQ )
46 35 16 42 45 syl3anc 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> ( ( D - B ) / ( C - E ) ) e. QQ )
47 44 46 eqeltrrd 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ -. C = E ) -> A e. QQ )
48 47 ex 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> ( -. C = E -> A e. QQ ) )
49 3 48 mt3d 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> C = E )
50 simpl2l 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> B e. QQ )
51 50 23 syl 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> B e. CC )
52 51 adantr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ C = E ) -> B e. CC )
53 simpl3l 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> D e. QQ )
54 53 28 syl 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> D e. CC )
55 54 adantr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ C = E ) -> D e. CC )
56 simpl1 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> A e. ( CC \ QQ ) )
57 56 eldifad 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> A e. CC )
58 simpl3r 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> E e. QQ )
59 58 12 syl 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> E e. CC )
60 57 59 mulcld 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> ( A x. E ) e. CC )
61 60 adantr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ C = E ) -> ( A x. E ) e. CC )
62 simpr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ C = E ) -> C = E )
63 62 eqcomd 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ C = E ) -> E = C )
64 63 oveq2d 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ C = E ) -> ( A x. E ) = ( A x. C ) )
65 64 oveq2d 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ C = E ) -> ( B + ( A x. E ) ) = ( B + ( A x. C ) ) )
66 simplr 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ C = E ) -> ( B + ( A x. C ) ) = ( D + ( A x. E ) ) )
67 65 66 eqtrd 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ C = E ) -> ( B + ( A x. E ) ) = ( D + ( A x. E ) ) )
68 52 55 61 67 addcan2ad 
 |-  ( ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) /\ C = E ) -> B = D )
69 68 ex 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> ( C = E -> B = D ) )
70 49 69 jcai 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> ( C = E /\ B = D ) )
71 70 ancomd 
 |-  ( ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) /\ ( B + ( A x. C ) ) = ( D + ( A x. E ) ) ) -> ( B = D /\ C = E ) )
72 71 ex 
 |-  ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) -> ( ( B + ( A x. C ) ) = ( D + ( A x. E ) ) -> ( B = D /\ C = E ) ) )
73 id 
 |-  ( B = D -> B = D )
74 oveq2 
 |-  ( C = E -> ( A x. C ) = ( A x. E ) )
75 73 74 oveqan12d 
 |-  ( ( B = D /\ C = E ) -> ( B + ( A x. C ) ) = ( D + ( A x. E ) ) )
76 72 75 impbid1 
 |-  ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) -> ( ( B + ( A x. C ) ) = ( D + ( A x. E ) ) <-> ( B = D /\ C = E ) ) )