This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )