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 )