# 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 ${⊢}\left({A}\in \left(ℂ\setminus ℚ\right)\wedge \left({B}\in ℚ\wedge {C}\in ℚ\right)\wedge \left({D}\in ℚ\wedge {E}\in ℚ\right)\right)\to \left({B}+{A}{C}={D}+{A}{E}↔\left({B}={D}\wedge {C}={E}\right)\right)$

### Proof

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