Metamath Proof Explorer


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 ) )