Metamath Proof Explorer

Theorem mulp1mod1

Description: The product of an integer and an integer greater than 1 increased by 1 is 1 modulo the integer greater than 1. (Contributed by AV, 15-Jul-2021)

Ref Expression
Assertion mulp1mod1 
|- ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( N x. A ) + 1 ) mod N ) = 1 )

Proof

Step Hyp Ref Expression
1 eluzelcn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. CC )
2 1 adantl 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> N e. CC )
3 zcn 
 |-  ( A e. ZZ -> A e. CC )
4 3 adantr 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> A e. CC )
5 2 4 mulcomd 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( N x. A ) = ( A x. N ) )
6 5 oveq1d 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( N x. A ) mod N ) = ( ( A x. N ) mod N ) )
7 eluz2nn 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. NN )
8 7 nnrpd 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR+ )
9 mulmod0 
 |-  ( ( A e. ZZ /\ N e. RR+ ) -> ( ( A x. N ) mod N ) = 0 )
10 8 9 sylan2 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( A x. N ) mod N ) = 0 )
11 6 10 eqtrd 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( N x. A ) mod N ) = 0 )
12 11 oveq1d 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( N x. A ) mod N ) + 1 ) = ( 0 + 1 ) )
13 0p1e1 
 |-  ( 0 + 1 ) = 1
14 12 13 eqtrdi 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( N x. A ) mod N ) + 1 ) = 1 )
15 14 oveq1d 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( ( N x. A ) mod N ) + 1 ) mod N ) = ( 1 mod N ) )
16 eluzelre 
 |-  ( N e. ( ZZ>= ` 2 ) -> N e. RR )
17 16 adantl 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> N e. RR )
18 zre 
 |-  ( A e. ZZ -> A e. RR )
19 18 adantr 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> A e. RR )
20 17 19 remulcld 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( N x. A ) e. RR )
21 1red 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> 1 e. RR )
22 8 adantl 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> N e. RR+ )
23 modaddmod 
 |-  ( ( ( N x. A ) e. RR /\ 1 e. RR /\ N e. RR+ ) -> ( ( ( ( N x. A ) mod N ) + 1 ) mod N ) = ( ( ( N x. A ) + 1 ) mod N ) )
24 20 21 22 23 syl3anc 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( ( N x. A ) mod N ) + 1 ) mod N ) = ( ( ( N x. A ) + 1 ) mod N ) )
25 eluz2gt1 
 |-  ( N e. ( ZZ>= ` 2 ) -> 1 < N )
26 16 25 jca 
 |-  ( N e. ( ZZ>= ` 2 ) -> ( N e. RR /\ 1 < N ) )
27 26 adantl 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( N e. RR /\ 1 < N ) )
28 1mod 
 |-  ( ( N e. RR /\ 1 < N ) -> ( 1 mod N ) = 1 )
29 27 28 syl 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( 1 mod N ) = 1 )
30 15 24 29 3eqtr3d 
 |-  ( ( A e. ZZ /\ N e. ( ZZ>= ` 2 ) ) -> ( ( ( N x. A ) + 1 ) mod N ) = 1 )