Metamath Proof Explorer

Theorem irrmul

Description: The product of an irrational with a nonzero rational is irrational. (Contributed by NM, 7-Nov-2008)

Ref Expression
Assertion irrmul 
|- ( ( A e. ( RR \ QQ ) /\ B e. QQ /\ B =/= 0 ) -> ( A x. 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 remulcl 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
4 2 3 sylan2 
 |-  ( ( A e. RR /\ B e. QQ ) -> ( A x. B ) e. RR )
5 4 ad2ant2r 
 |-  ( ( ( A e. RR /\ -. A e. QQ ) /\ ( B e. QQ /\ B =/= 0 ) ) -> ( A x. B ) e. RR )
6 qdivcl 
 |-  ( ( ( A x. B ) e. QQ /\ B e. QQ /\ B =/= 0 ) -> ( ( A x. B ) / B ) e. QQ )
7 6 3expb 
 |-  ( ( ( A x. B ) e. QQ /\ ( B e. QQ /\ B =/= 0 ) ) -> ( ( A x. B ) / B ) e. QQ )
8 7 expcom 
 |-  ( ( B e. QQ /\ B =/= 0 ) -> ( ( A x. B ) e. QQ -> ( ( A x. B ) / B ) e. QQ ) )
9 8 adantl 
 |-  ( ( A e. RR /\ ( B e. QQ /\ B =/= 0 ) ) -> ( ( A x. B ) e. QQ -> ( ( A x. B ) / B ) e. QQ ) )
10 qcn 
 |-  ( B e. QQ -> B e. CC )
11 recn 
 |-  ( A e. RR -> A e. CC )
12 divcan4 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A x. B ) / B ) = A )
13 11 12 syl3an1 
 |-  ( ( A e. RR /\ B e. CC /\ B =/= 0 ) -> ( ( A x. B ) / B ) = A )
14 10 13 syl3an2 
 |-  ( ( A e. RR /\ B e. QQ /\ B =/= 0 ) -> ( ( A x. B ) / B ) = A )
15 14 3expb 
 |-  ( ( A e. RR /\ ( B e. QQ /\ B =/= 0 ) ) -> ( ( A x. B ) / B ) = A )
16 15 eleq1d 
 |-  ( ( A e. RR /\ ( B e. QQ /\ B =/= 0 ) ) -> ( ( ( A x. B ) / B ) e. QQ <-> A e. QQ ) )
17 9 16 sylibd 
 |-  ( ( A e. RR /\ ( B e. QQ /\ B =/= 0 ) ) -> ( ( A x. B ) e. QQ -> A e. QQ ) )
18 17 con3d 
 |-  ( ( A e. RR /\ ( B e. QQ /\ B =/= 0 ) ) -> ( -. A e. QQ -> -. ( A x. B ) e. QQ ) )
19 18 ex 
 |-  ( A e. RR -> ( ( B e. QQ /\ B =/= 0 ) -> ( -. A e. QQ -> -. ( A x. B ) e. QQ ) ) )
20 19 com23 
 |-  ( A e. RR -> ( -. A e. QQ -> ( ( B e. QQ /\ B =/= 0 ) -> -. ( A x. B ) e. QQ ) ) )
21 20 imp31 
 |-  ( ( ( A e. RR /\ -. A e. QQ ) /\ ( B e. QQ /\ B =/= 0 ) ) -> -. ( A x. B ) e. QQ )
22 5 21 jca 
 |-  ( ( ( A e. RR /\ -. A e. QQ ) /\ ( B e. QQ /\ B =/= 0 ) ) -> ( ( A x. B ) e. RR /\ -. ( A x. B ) e. QQ ) )
23 22 3impb 
 |-  ( ( ( A e. RR /\ -. A e. QQ ) /\ B e. QQ /\ B =/= 0 ) -> ( ( A x. B ) e. RR /\ -. ( A x. B ) e. QQ ) )
24 1 23 syl3an1b 
 |-  ( ( A e. ( RR \ QQ ) /\ B e. QQ /\ B =/= 0 ) -> ( ( A x. B ) e. RR /\ -. ( A x. B ) e. QQ ) )
25 eldif 
 |-  ( ( A x. B ) e. ( RR \ QQ ) <-> ( ( A x. B ) e. RR /\ -. ( A x. B ) e. QQ ) )
26 24 25 sylibr 
 |-  ( ( A e. ( RR \ QQ ) /\ B e. QQ /\ B =/= 0 ) -> ( A x. B ) e. ( RR \ QQ ) )