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∈ℂ∖ℚ∧B∈ℚ∧C∈ℚ∧D∈ℚ∧E∈ℚ→B+A⁢C=D+A⁢E↔B=D∧C=E

Proof

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