# Metamath Proof Explorer

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

Ref Expression
Assertion qrevaddcl ${⊢}{B}\in ℚ\to \left(\left({A}\in ℂ\wedge {A}+{B}\in ℚ\right)↔{A}\in ℚ\right)$

### Proof

Step Hyp Ref Expression
1 qcn ${⊢}{B}\in ℚ\to {B}\in ℂ$
2 pncan ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}+{B}-{B}={A}$
3 1 2 sylan2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℚ\right)\to {A}+{B}-{B}={A}$
4 3 ancoms ${⊢}\left({B}\in ℚ\wedge {A}\in ℂ\right)\to {A}+{B}-{B}={A}$
5 4 adantr ${⊢}\left(\left({B}\in ℚ\wedge {A}\in ℂ\right)\wedge {A}+{B}\in ℚ\right)\to {A}+{B}-{B}={A}$
6 qsubcl ${⊢}\left({A}+{B}\in ℚ\wedge {B}\in ℚ\right)\to {A}+{B}-{B}\in ℚ$
7 6 ancoms ${⊢}\left({B}\in ℚ\wedge {A}+{B}\in ℚ\right)\to {A}+{B}-{B}\in ℚ$
8 7 adantlr ${⊢}\left(\left({B}\in ℚ\wedge {A}\in ℂ\right)\wedge {A}+{B}\in ℚ\right)\to {A}+{B}-{B}\in ℚ$
9 5 8 eqeltrrd ${⊢}\left(\left({B}\in ℚ\wedge {A}\in ℂ\right)\wedge {A}+{B}\in ℚ\right)\to {A}\in ℚ$
10 9 ex ${⊢}\left({B}\in ℚ\wedge {A}\in ℂ\right)\to \left({A}+{B}\in ℚ\to {A}\in ℚ\right)$
11 qaddcl ${⊢}\left({A}\in ℚ\wedge {B}\in ℚ\right)\to {A}+{B}\in ℚ$
12 11 expcom ${⊢}{B}\in ℚ\to \left({A}\in ℚ\to {A}+{B}\in ℚ\right)$
13 12 adantr ${⊢}\left({B}\in ℚ\wedge {A}\in ℂ\right)\to \left({A}\in ℚ\to {A}+{B}\in ℚ\right)$
14 10 13 impbid ${⊢}\left({B}\in ℚ\wedge {A}\in ℂ\right)\to \left({A}+{B}\in ℚ↔{A}\in ℚ\right)$
15 14 pm5.32da ${⊢}{B}\in ℚ\to \left(\left({A}\in ℂ\wedge {A}+{B}\in ℚ\right)↔\left({A}\in ℂ\wedge {A}\in ℚ\right)\right)$
16 qcn ${⊢}{A}\in ℚ\to {A}\in ℂ$
17 16 pm4.71ri ${⊢}{A}\in ℚ↔\left({A}\in ℂ\wedge {A}\in ℚ\right)$
18 15 17 syl6bbr ${⊢}{B}\in ℚ\to \left(\left({A}\in ℂ\wedge {A}+{B}\in ℚ\right)↔{A}\in ℚ\right)$