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 ABA+B

Proof

Step Hyp Ref Expression
1 eldif AA¬A
2 qre BB
3 readdcl ABA+B
4 2 3 sylan2 ABA+B
5 4 adantlr A¬ABA+B
6 qsubcl A+BBA+B-B
7 6 expcom BA+BA+B-B
8 7 adantl ABA+BA+B-B
9 recn AA
10 qcn BB
11 pncan ABA+B-B=A
12 9 10 11 syl2an ABA+B-B=A
13 12 eleq1d ABA+B-BA
14 8 13 sylibd ABA+BA
15 14 con3d AB¬A¬A+B
16 15 ex AB¬A¬A+B
17 16 com23 A¬AB¬A+B
18 17 imp31 A¬AB¬A+B
19 5 18 jca A¬ABA+B¬A+B
20 1 19 sylanb ABA+B¬A+B
21 eldif A+BA+B¬A+B
22 20 21 sylibr ABA+B