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∈ℚ