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

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