Theorem irradd

Description: The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008)

	Ref	Expression
Assertion	irradd	|- ( ( A e. ( RR \ QQ ) /\ B e. QQ ) -> ( A + B ) e. ( RR \ QQ ) )

Proof

Step	Hyp	Ref	Expression
1		eldif	|- ( A e. ( RR \ QQ ) <-> ( A e. RR /\ -. A e. QQ ) )
2		qre	|- ( B e. QQ -> B e. RR )
3		readdcl	|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
4	2 3	sylan2	|- ( ( A e. RR /\ B e. QQ ) -> ( A + B ) e. RR )
5	4	adantlr	|- ( ( ( A e. RR /\ -. A e. QQ ) /\ B e. QQ ) -> ( A + B ) e. RR )
6		qsubcl	|- ( ( ( A + B ) e. QQ /\ B e. QQ ) -> ( ( A + B ) - B ) e. QQ )
7	6	expcom	|- ( B e. QQ -> ( ( A + B ) e. QQ -> ( ( A + B ) - B ) e. QQ ) )
8	7	adantl	|- ( ( A e. RR /\ B e. QQ ) -> ( ( A + B ) e. QQ -> ( ( A + B ) - B ) e. QQ ) )
9		recn	|- ( A e. RR -> A e. CC )
10		qcn	|- ( B e. QQ -> B e. CC )
11		pncan	|- ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) - B ) = A )
12	9 10 11	syl2an	|- ( ( A e. RR /\ B e. QQ ) -> ( ( A + B ) - B ) = A )
13	12	eleq1d	|- ( ( A e. RR /\ B e. QQ ) -> ( ( ( A + B ) - B ) e. QQ <-> A e. QQ ) )
14	8 13	sylibd	|- ( ( A e. RR /\ B e. QQ ) -> ( ( A + B ) e. QQ -> A e. QQ ) )
15	14	con3d	|- ( ( A e. RR /\ B e. QQ ) -> ( -. A e. QQ -> -. ( A + B ) e. QQ ) )
16	15	ex	|- ( A e. RR -> ( B e. QQ -> ( -. A e. QQ -> -. ( A + B ) e. QQ ) ) )
17	16	com23	|- ( A e. RR -> ( -. A e. QQ -> ( B e. QQ -> -. ( A + B ) e. QQ ) ) )
18	17	imp31	|- ( ( ( A e. RR /\ -. A e. QQ ) /\ B e. QQ ) -> -. ( A + B ) e. QQ )
19	5 18	jca	|- ( ( ( A e. RR /\ -. A e. QQ ) /\ B e. QQ ) -> ( ( A + B ) e. RR /\ -. ( A + B ) e. QQ ) )
20	1 19	sylanb	|- ( ( A e. ( RR \ QQ ) /\ B e. QQ ) -> ( ( A + B ) e. RR /\ -. ( A + B ) e. QQ ) )
21		eldif	|- ( ( A + B ) e. ( RR \ QQ ) <-> ( ( A + B ) e. RR /\ -. ( A + B ) e. QQ ) )
22	20 21	sylibr	|- ( ( A e. ( RR \ QQ ) /\ B e. QQ ) -> ( A + B ) e. ( RR \ QQ ) )