This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qrevaddcl

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

Ref Expression
Assertion qrevaddcl ( 𝐵 ∈ ℚ → ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) ∈ ℚ ) ↔ 𝐴 ∈ ℚ ) )

Proof

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