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 − B C − 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 − B C − E = A
45 qdivcl ⊢ D − B ∈ ℚ ∧ C − E ∈ ℚ ∧ C − E ≠ 0 → D − B C − E ∈ ℚ
46 35 16 42 45 syl3anc ⊢ A ∈ ℂ ∖ ℚ ∧ B ∈ ℚ ∧ C ∈ ℚ ∧ D ∈ ℚ ∧ E ∈ ℚ ∧ B + A ⁢ C = D + A ⁢ E ∧ ¬ C = E → D − B C − 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