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	⊢ ( 𝐵 ∈ ℚ → ( ( 𝐴 ∈ ℂ ∧ ( 𝐴 + 𝐵 ) ∈ ℚ ) ↔ 𝐴 ∈ ℚ ) )