Metamath Proof Explorer


Theorem 1mod

Description: Special case: 1 modulo a real number greater than 1 is 1. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Assertion 1mod
|- ( ( N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )

Proof

Step Hyp Ref Expression
1 0lt1
 |-  0 < 1
2 0re
 |-  0 e. RR
3 1re
 |-  1 e. RR
4 lttr
 |-  ( ( 0 e. RR /\ 1 e. RR /\ N e. RR ) -> ( ( 0 < 1 /\ 1 < N ) -> 0 < N ) )
5 2 3 4 mp3an12
 |-  ( N e. RR -> ( ( 0 < 1 /\ 1 < N ) -> 0 < N ) )
6 1 5 mpani
 |-  ( N e. RR -> ( 1 < N -> 0 < N ) )
7 6 imdistani
 |-  ( ( N e. RR /\ 1 < N ) -> ( N e. RR /\ 0 < N ) )
8 elrp
 |-  ( N e. RR+ <-> ( N e. RR /\ 0 < N ) )
9 7 8 sylibr
 |-  ( ( N e. RR /\ 1 < N ) -> N e. RR+ )
10 9 3 jctil
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 e. RR /\ N e. RR+ ) )
11 simpr
 |-  ( ( N e. RR /\ 1 < N ) -> 1 < N )
12 0le1
 |-  0 <_ 1
13 11 12 jctil
 |-  ( ( N e. RR /\ 1 < N ) -> ( 0 <_ 1 /\ 1 < N ) )
14 modid
 |-  ( ( ( 1 e. RR /\ N e. RR+ ) /\ ( 0 <_ 1 /\ 1 < N ) ) -> ( 1 mod N ) = 1 )
15 10 13 14 syl2anc
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )