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 ( ( 𝐴 ∈ ( ℂ ∖ ℚ ) ∧ ( 𝐵 ∈ ℚ ∧ 𝐶 ∈ ℚ ) ∧ ( 𝐷 ∈ ℚ ∧ 𝐸 ∈ ℚ ) ) → ( ( 𝐵 + ( 𝐴 · 𝐶 ) ) = ( 𝐷 + ( 𝐴 · 𝐸 ) ) ↔ ( 𝐵 = 𝐷 ∧ 𝐶 = 𝐸 ) ) )

Proof

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