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