Metamath Proof Explorer

Theorem qrevaddcl

Description: Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion qrevaddcl ⊢ B ∈ ℚ → A ∈ ℂ ∧ A + B ∈ ℚ ↔ A ∈ ℚ

Proof

Step Hyp Ref Expression
1 qcn ⊢ B ∈ ℚ → B ∈ ℂ
2 pncan ⊢ A ∈ ℂ ∧ B ∈ ℂ → A + B - B = A
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℚ → A + B - B = A
4 3 ancoms ⊢ B ∈ ℚ ∧ A ∈ ℂ → A + B - B = A
5 4 adantr ⊢ B ∈ ℚ ∧ A ∈ ℂ ∧ A + B ∈ ℚ → A + B - B = A
6 qsubcl ⊢ A + B ∈ ℚ ∧ B ∈ ℚ → A + B - B ∈ ℚ
7 6 ancoms ⊢ B ∈ ℚ ∧ A + B ∈ ℚ → A + B - B ∈ ℚ
8 7 adantlr ⊢ B ∈ ℚ ∧ A ∈ ℂ ∧ A + B ∈ ℚ → A + B - B ∈ ℚ
9 5 8 eqeltrrd ⊢ B ∈ ℚ ∧ A ∈ ℂ ∧ A + B ∈ ℚ → A ∈ ℚ
10 9 ex ⊢ B ∈ ℚ ∧ A ∈ ℂ → A + B ∈ ℚ → A ∈ ℚ
11 qaddcl ⊢ A ∈ ℚ ∧ B ∈ ℚ → A + B ∈ ℚ
12 11 expcom ⊢ B ∈ ℚ → A ∈ ℚ → A + B ∈ ℚ
13 12 adantr ⊢ B ∈ ℚ ∧ A ∈ ℂ → A ∈ ℚ → A + B ∈ ℚ
14 10 13 impbid ⊢ B ∈ ℚ ∧ A ∈ ℂ → A + B ∈ ℚ ↔ A ∈ ℚ
15 14 pm5.32da ⊢ B ∈ ℚ → A ∈ ℂ ∧ A + B ∈ ℚ ↔ A ∈ ℂ ∧ A ∈ ℚ
16 qcn ⊢ A ∈ ℚ → A ∈ ℂ
17 16 pm4.71ri ⊢ A ∈ ℚ ↔ A ∈ ℂ ∧ A ∈ ℚ
18 15 17 bitr4di ⊢ B ∈ ℚ → A ∈ ℂ ∧ A + B ∈ ℚ ↔ A ∈ ℚ