Metamath Proof Explorer

Theorem congrep

Description: Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014)

Ref Expression
Assertion congrep 
|- ( ( A e. NN /\ N e. ZZ ) -> E. a e. ( 0 ... ( A - 1 ) ) A || ( a - N ) )

Proof

Step Hyp Ref Expression
1 zmodfz 
 |-  ( ( N e. ZZ /\ A e. NN ) -> ( N mod A ) e. ( 0 ... ( A - 1 ) ) )
2 1 ancoms 
 |-  ( ( A e. NN /\ N e. ZZ ) -> ( N mod A ) e. ( 0 ... ( A - 1 ) ) )
3 nnz 
 |-  ( A e. NN -> A e. ZZ )
4 3 adantr 
 |-  ( ( A e. NN /\ N e. ZZ ) -> A e. ZZ )
5 simpr 
 |-  ( ( A e. NN /\ N e. ZZ ) -> N e. ZZ )
6 zmodcl 
 |-  ( ( N e. ZZ /\ A e. NN ) -> ( N mod A ) e. NN0 )
7 6 ancoms 
 |-  ( ( A e. NN /\ N e. ZZ ) -> ( N mod A ) e. NN0 )
8 7 nn0zd 
 |-  ( ( A e. NN /\ N e. ZZ ) -> ( N mod A ) e. ZZ )
9 zre 
 |-  ( N e. ZZ -> N e. RR )
10 nnrp 
 |-  ( A e. NN -> A e. RR+ )
11 moddifz 
 |-  ( ( N e. RR /\ A e. RR+ ) -> ( ( N - ( N mod A ) ) / A ) e. ZZ )
12 9 10 11 syl2anr 
 |-  ( ( A e. NN /\ N e. ZZ ) -> ( ( N - ( N mod A ) ) / A ) e. ZZ )
13 nnne0 
 |-  ( A e. NN -> A =/= 0 )
14 13 adantr 
 |-  ( ( A e. NN /\ N e. ZZ ) -> A =/= 0 )
15 5 8 zsubcld 
 |-  ( ( A e. NN /\ N e. ZZ ) -> ( N - ( N mod A ) ) e. ZZ )
16 dvdsval2 
 |-  ( ( A e. ZZ /\ A =/= 0 /\ ( N - ( N mod A ) ) e. ZZ ) -> ( A || ( N - ( N mod A ) ) <-> ( ( N - ( N mod A ) ) / A ) e. ZZ ) )
17 4 14 15 16 syl3anc 
 |-  ( ( A e. NN /\ N e. ZZ ) -> ( A || ( N - ( N mod A ) ) <-> ( ( N - ( N mod A ) ) / A ) e. ZZ ) )
18 12 17 mpbird 
 |-  ( ( A e. NN /\ N e. ZZ ) -> A || ( N - ( N mod A ) ) )
19 congsym 
 |-  ( ( ( A e. ZZ /\ N e. ZZ ) /\ ( ( N mod A ) e. ZZ /\ A || ( N - ( N mod A ) ) ) ) -> A || ( ( N mod A ) - N ) )
20 4 5 8 18 19 syl22anc 
 |-  ( ( A e. NN /\ N e. ZZ ) -> A || ( ( N mod A ) - N ) )
21 oveq1 
 |-  ( a = ( N mod A ) -> ( a - N ) = ( ( N mod A ) - N ) )
22 21 breq2d 
 |-  ( a = ( N mod A ) -> ( A || ( a - N ) <-> A || ( ( N mod A ) - N ) ) )
23 22 rspcev 
 |-  ( ( ( N mod A ) e. ( 0 ... ( A - 1 ) ) /\ A || ( ( N mod A ) - N ) ) -> E. a e. ( 0 ... ( A - 1 ) ) A || ( a - N ) )
24 2 20 23 syl2anc 
 |-  ( ( A e. NN /\ N e. ZZ ) -> E. a e. ( 0 ... ( A - 1 ) ) A || ( a - N ) )