Metamath Proof Explorer

Theorem modirr

Description: A number modulo an irrational multiple of it is nonzero. (Contributed by NM, 11-Nov-2008)

Ref Expression
Assertion modirr 
|- ( ( A e. RR /\ B e. RR+ /\ ( A / B ) e. ( RR \ QQ ) ) -> ( A mod B ) =/= 0 )

Proof

Step Hyp Ref Expression
1 eldif 
 |-  ( ( A / B ) e. ( RR \ QQ ) <-> ( ( A / B ) e. RR /\ -. ( A / B ) e. QQ ) )
2 modval 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) = ( A - ( B x. ( |_ ` ( A / B ) ) ) ) )
3 2 eqeq1d 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( A - ( B x. ( |_ ` ( A / B ) ) ) ) = 0 ) )
4 recn 
 |-  ( A e. RR -> A e. CC )
5 4 adantr 
 |-  ( ( A e. RR /\ B e. RR+ ) -> A e. CC )
6 rpre 
 |-  ( B e. RR+ -> B e. RR )
7 6 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> B e. RR )
8 refldivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. RR )
9 7 8 remulcld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( |_ ` ( A / B ) ) ) e. RR )
10 9 recnd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B x. ( |_ ` ( A / B ) ) ) e. CC )
11 5 10 subeq0ad 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A - ( B x. ( |_ ` ( A / B ) ) ) ) = 0 <-> A = ( B x. ( |_ ` ( A / B ) ) ) ) )
12 rerpdivcl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A / B ) e. RR )
13 reflcl 
 |-  ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) e. RR )
14 13 recnd 
 |-  ( ( A / B ) e. RR -> ( |_ ` ( A / B ) ) e. CC )
15 12 14 syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( |_ ` ( A / B ) ) e. CC )
16 rpcnne0 
 |-  ( B e. RR+ -> ( B e. CC /\ B =/= 0 ) )
17 16 adantl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( B e. CC /\ B =/= 0 ) )
18 divmul2 
 |-  ( ( A e. CC /\ ( |_ ` ( A / B ) ) e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) = ( |_ ` ( A / B ) ) <-> A = ( B x. ( |_ ` ( A / B ) ) ) ) )
19 5 15 17 18 syl3anc 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) = ( |_ ` ( A / B ) ) <-> A = ( B x. ( |_ ` ( A / B ) ) ) ) )
20 eqcom 
 |-  ( ( A / B ) = ( |_ ` ( A / B ) ) <-> ( |_ ` ( A / B ) ) = ( A / B ) )
21 19 20 bitr3di 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( A = ( B x. ( |_ ` ( A / B ) ) ) <-> ( |_ ` ( A / B ) ) = ( A / B ) ) )
22 3 11 21 3bitrd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 <-> ( |_ ` ( A / B ) ) = ( A / B ) ) )
23 flidz 
 |-  ( ( A / B ) e. RR -> ( ( |_ ` ( A / B ) ) = ( A / B ) <-> ( A / B ) e. ZZ ) )
24 zq 
 |-  ( ( A / B ) e. ZZ -> ( A / B ) e. QQ )
25 23 24 syl6bi 
 |-  ( ( A / B ) e. RR -> ( ( |_ ` ( A / B ) ) = ( A / B ) -> ( A / B ) e. QQ ) )
26 12 25 syl 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( |_ ` ( A / B ) ) = ( A / B ) -> ( A / B ) e. QQ ) )
27 22 26 sylbid 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A mod B ) = 0 -> ( A / B ) e. QQ ) )
28 27 necon3bd 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( -. ( A / B ) e. QQ -> ( A mod B ) =/= 0 ) )
29 28 adantld 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( ( A / B ) e. RR /\ -. ( A / B ) e. QQ ) -> ( A mod B ) =/= 0 ) )
30 1 29 syl5bi 
 |-  ( ( A e. RR /\ B e. RR+ ) -> ( ( A / B ) e. ( RR \ QQ ) -> ( A mod B ) =/= 0 ) )
31 30 3impia 
 |-  ( ( A e. RR /\ B e. RR+ /\ ( A / B ) e. ( RR \ QQ ) ) -> ( A mod B ) =/= 0 )