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 ) |