Description: The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008)
Ref | Expression | ||
---|---|---|---|
Assertion | irradd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eldif | |
|
2 | qre | |
|
3 | readdcl | |
|
4 | 2 3 | sylan2 | |
5 | 4 | adantlr | |
6 | qsubcl | |
|
7 | 6 | expcom | |
8 | 7 | adantl | |
9 | recn | |
|
10 | qcn | |
|
11 | pncan | |
|
12 | 9 10 11 | syl2an | |
13 | 12 | eleq1d | |
14 | 8 13 | sylibd | |
15 | 14 | con3d | |
16 | 15 | ex | |
17 | 16 | com23 | |
18 | 17 | imp31 | |
19 | 5 18 | jca | |
20 | 1 19 | sylanb | |
21 | eldif | |
|
22 | 20 21 | sylibr | |