Metamath Proof Explorer

Theorem hashdvds

Description: The number of numbers in a given residue class in a finite set of integers. (Contributed by Mario Carneiro, 12-Mar-2014) (Proof shortened by Mario Carneiro, 7-Jun-2016)

Ref Expression
Hypotheses hashdvds.1 
|- ( ph -> N e. NN )
hashdvds.2 
|- ( ph -> A e. ZZ )
hashdvds.3 
|- ( ph -> B e. ( ZZ>= ` ( A - 1 ) ) )
hashdvds.4 
|- ( ph -> C e. ZZ )
Assertion hashdvds 
|- ( ph -> ( # ` { x e. ( A ... B ) | N || ( x - C ) } ) = ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) )

Proof

Step Hyp Ref Expression
1 hashdvds.1 
 |-  ( ph -> N e. NN )
2 hashdvds.2 
 |-  ( ph -> A e. ZZ )
3 hashdvds.3 
 |-  ( ph -> B e. ( ZZ>= ` ( A - 1 ) ) )
4 hashdvds.4 
 |-  ( ph -> C e. ZZ )
5 1zzd 
 |-  ( ph -> 1 e. ZZ )
6 eluzelz 
 |-  ( B e. ( ZZ>= ` ( A - 1 ) ) -> B e. ZZ )
7 3 6 syl 
 |-  ( ph -> B e. ZZ )
8 7 4 zsubcld 
 |-  ( ph -> ( B - C ) e. ZZ )
9 8 zred 
 |-  ( ph -> ( B - C ) e. RR )
10 9 1 nndivred 
 |-  ( ph -> ( ( B - C ) / N ) e. RR )
11 10 flcld 
 |-  ( ph -> ( |_ ` ( ( B - C ) / N ) ) e. ZZ )
12 peano2zm 
 |-  ( A e. ZZ -> ( A - 1 ) e. ZZ )
13 2 12 syl 
 |-  ( ph -> ( A - 1 ) e. ZZ )
14 13 4 zsubcld 
 |-  ( ph -> ( ( A - 1 ) - C ) e. ZZ )
15 14 zred 
 |-  ( ph -> ( ( A - 1 ) - C ) e. RR )
16 15 1 nndivred 
 |-  ( ph -> ( ( ( A - 1 ) - C ) / N ) e. RR )
17 16 flcld 
 |-  ( ph -> ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) e. ZZ )
18 11 17 zsubcld 
 |-  ( ph -> ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) e. ZZ )
19 fzen 
 |-  ( ( 1 e. ZZ /\ ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) e. ZZ /\ ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) e. ZZ ) -> ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ~~ ( ( 1 + ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ... ( ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) + ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) )
20 5 18 17 19 syl3anc 
 |-  ( ph -> ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ~~ ( ( 1 + ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ... ( ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) + ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) )
21 ax-1cn 
 |-  1 e. CC
22 17 zcnd 
 |-  ( ph -> ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) e. CC )
23 addcom 
 |-  ( ( 1 e. CC /\ ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) e. CC ) -> ( 1 + ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) = ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) )
24 21 22 23 sylancr 
 |-  ( ph -> ( 1 + ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) = ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) )
25 11 zcnd 
 |-  ( ph -> ( |_ ` ( ( B - C ) / N ) ) e. CC )
26 25 22 npcand 
 |-  ( ph -> ( ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) + ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) = ( |_ ` ( ( B - C ) / N ) ) )
27 24 26 oveq12d 
 |-  ( ph -> ( ( 1 + ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ... ( ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) + ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) = ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) )
28 20 27 breqtrd 
 |-  ( ph -> ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ~~ ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) )
29 ovexd 
 |-  ( ph -> ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) e. _V )
30 fzfi 
 |-  ( A ... B ) e. Fin
31 rabexg 
 |-  ( ( A ... B ) e. Fin -> { x e. ( A ... B ) | N || ( x - C ) } e. _V )
32 30 31 mp1i 
 |-  ( ph -> { x e. ( A ... B ) | N || ( x - C ) } e. _V )
33 oveq1 
 |-  ( x = ( ( z x. N ) + C ) -> ( x - C ) = ( ( ( z x. N ) + C ) - C ) )
34 33 breq2d 
 |-  ( x = ( ( z x. N ) + C ) -> ( N || ( x - C ) <-> N || ( ( ( z x. N ) + C ) - C ) ) )
35 2 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> A e. ZZ )
36 7 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> B e. ZZ )
37 elfzelz 
 |-  ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) -> z e. ZZ )
38 37 adantl 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> z e. ZZ )
39 1 nnzd 
 |-  ( ph -> N e. ZZ )
40 39 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> N e. ZZ )
41 38 40 zmulcld 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( z x. N ) e. ZZ )
42 4 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> C e. ZZ )
43 41 42 zaddcld 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( z x. N ) + C ) e. ZZ )
44 elfzle1 
 |-  ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) -> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) <_ z )
45 44 adantl 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) <_ z )
46 zltp1le 
 |-  ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) e. ZZ /\ z e. ZZ ) -> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) < z <-> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) <_ z ) )
47 17 37 46 syl2an 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) < z <-> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) <_ z ) )
48 45 47 mpbird 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) < z )
49 fllt 
 |-  ( ( ( ( ( A - 1 ) - C ) / N ) e. RR /\ z e. ZZ ) -> ( ( ( ( A - 1 ) - C ) / N ) < z <-> ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) < z ) )
50 16 37 49 syl2an 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( ( ( A - 1 ) - C ) / N ) < z <-> ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) < z ) )
51 48 50 mpbird 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( ( A - 1 ) - C ) / N ) < z )
52 15 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( A - 1 ) - C ) e. RR )
53 38 zred 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> z e. RR )
54 1 nnred 
 |-  ( ph -> N e. RR )
55 1 nngt0d 
 |-  ( ph -> 0 < N )
56 54 55 jca 
 |-  ( ph -> ( N e. RR /\ 0 < N ) )
57 56 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( N e. RR /\ 0 < N ) )
58 ltdivmul2 
 |-  ( ( ( ( A - 1 ) - C ) e. RR /\ z e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( ( ( A - 1 ) - C ) / N ) < z <-> ( ( A - 1 ) - C ) < ( z x. N ) ) )
59 52 53 57 58 syl3anc 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( ( ( A - 1 ) - C ) / N ) < z <-> ( ( A - 1 ) - C ) < ( z x. N ) ) )
60 51 59 mpbid 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( A - 1 ) - C ) < ( z x. N ) )
61 13 zred 
 |-  ( ph -> ( A - 1 ) e. RR )
62 61 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( A - 1 ) e. RR )
63 4 zred 
 |-  ( ph -> C e. RR )
64 63 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> C e. RR )
65 41 zred 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( z x. N ) e. RR )
66 62 64 65 ltsubaddd 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( ( A - 1 ) - C ) < ( z x. N ) <-> ( A - 1 ) < ( ( z x. N ) + C ) ) )
67 60 66 mpbid 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( A - 1 ) < ( ( z x. N ) + C ) )
68 zlem1lt 
 |-  ( ( A e. ZZ /\ ( ( z x. N ) + C ) e. ZZ ) -> ( A <_ ( ( z x. N ) + C ) <-> ( A - 1 ) < ( ( z x. N ) + C ) ) )
69 2 43 68 syl2an2r 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( A <_ ( ( z x. N ) + C ) <-> ( A - 1 ) < ( ( z x. N ) + C ) ) )
70 67 69 mpbird 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> A <_ ( ( z x. N ) + C ) )
71 elfzle2 
 |-  ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) -> z <_ ( |_ ` ( ( B - C ) / N ) ) )
72 71 adantl 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> z <_ ( |_ ` ( ( B - C ) / N ) ) )
73 flge 
 |-  ( ( ( ( B - C ) / N ) e. RR /\ z e. ZZ ) -> ( z <_ ( ( B - C ) / N ) <-> z <_ ( |_ ` ( ( B - C ) / N ) ) ) )
74 10 37 73 syl2an 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( z <_ ( ( B - C ) / N ) <-> z <_ ( |_ ` ( ( B - C ) / N ) ) ) )
75 72 74 mpbird 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> z <_ ( ( B - C ) / N ) )
76 9 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( B - C ) e. RR )
77 lemuldiv 
 |-  ( ( z e. RR /\ ( B - C ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( z x. N ) <_ ( B - C ) <-> z <_ ( ( B - C ) / N ) ) )
78 53 76 57 77 syl3anc 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( z x. N ) <_ ( B - C ) <-> z <_ ( ( B - C ) / N ) ) )
79 75 78 mpbird 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( z x. N ) <_ ( B - C ) )
80 7 zred 
 |-  ( ph -> B e. RR )
81 80 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> B e. RR )
82 leaddsub 
 |-  ( ( ( z x. N ) e. RR /\ C e. RR /\ B e. RR ) -> ( ( ( z x. N ) + C ) <_ B <-> ( z x. N ) <_ ( B - C ) ) )
83 65 64 81 82 syl3anc 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( ( z x. N ) + C ) <_ B <-> ( z x. N ) <_ ( B - C ) ) )
84 79 83 mpbird 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( z x. N ) + C ) <_ B )
85 35 36 43 70 84 elfzd 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( z x. N ) + C ) e. ( A ... B ) )
86 dvdsmul2 
 |-  ( ( z e. ZZ /\ N e. ZZ ) -> N || ( z x. N ) )
87 38 40 86 syl2anc 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> N || ( z x. N ) )
88 41 zcnd 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( z x. N ) e. CC )
89 4 zcnd 
 |-  ( ph -> C e. CC )
90 89 adantr 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> C e. CC )
91 88 90 pncand 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( ( z x. N ) + C ) - C ) = ( z x. N ) )
92 87 91 breqtrrd 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> N || ( ( ( z x. N ) + C ) - C ) )
93 34 85 92 elrabd 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> ( ( z x. N ) + C ) e. { x e. ( A ... B ) | N || ( x - C ) } )
94 93 ex 
 |-  ( ph -> ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) -> ( ( z x. N ) + C ) e. { x e. ( A ... B ) | N || ( x - C ) } ) )
95 oveq1 
 |-  ( x = y -> ( x - C ) = ( y - C ) )
96 95 breq2d 
 |-  ( x = y -> ( N || ( x - C ) <-> N || ( y - C ) ) )
97 96 elrab 
 |-  ( y e. { x e. ( A ... B ) | N || ( x - C ) } <-> ( y e. ( A ... B ) /\ N || ( y - C ) ) )
98 17 peano2zd 
 |-  ( ph -> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) e. ZZ )
99 98 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) e. ZZ )
100 11 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( |_ ` ( ( B - C ) / N ) ) e. ZZ )
101 simprr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> N || ( y - C ) )
102 39 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> N e. ZZ )
103 1 nnne0d 
 |-  ( ph -> N =/= 0 )
104 103 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> N =/= 0 )
105 elfzelz 
 |-  ( y e. ( A ... B ) -> y e. ZZ )
106 105 ad2antrl 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> y e. ZZ )
107 4 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> C e. ZZ )
108 106 107 zsubcld 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( y - C ) e. ZZ )
109 dvdsval2 
 |-  ( ( N e. ZZ /\ N =/= 0 /\ ( y - C ) e. ZZ ) -> ( N || ( y - C ) <-> ( ( y - C ) / N ) e. ZZ ) )
110 102 104 108 109 syl3anc 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( N || ( y - C ) <-> ( ( y - C ) / N ) e. ZZ ) )
111 101 110 mpbid 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( y - C ) / N ) e. ZZ )
112 61 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( A - 1 ) e. RR )
113 106 zred 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> y e. RR )
114 63 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> C e. RR )
115 elfzle1 
 |-  ( y e. ( A ... B ) -> A <_ y )
116 115 ad2antrl 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> A <_ y )
117 zlem1lt 
 |-  ( ( A e. ZZ /\ y e. ZZ ) -> ( A <_ y <-> ( A - 1 ) < y ) )
118 2 106 117 syl2an2r 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( A <_ y <-> ( A - 1 ) < y ) )
119 116 118 mpbid 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( A - 1 ) < y )
120 112 113 114 119 ltsub1dd 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( A - 1 ) - C ) < ( y - C ) )
121 15 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( A - 1 ) - C ) e. RR )
122 108 zred 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( y - C ) e. RR )
123 56 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( N e. RR /\ 0 < N ) )
124 ltdiv1 
 |-  ( ( ( ( A - 1 ) - C ) e. RR /\ ( y - C ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( ( A - 1 ) - C ) < ( y - C ) <-> ( ( ( A - 1 ) - C ) / N ) < ( ( y - C ) / N ) ) )
125 121 122 123 124 syl3anc 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( ( A - 1 ) - C ) < ( y - C ) <-> ( ( ( A - 1 ) - C ) / N ) < ( ( y - C ) / N ) ) )
126 120 125 mpbid 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( ( A - 1 ) - C ) / N ) < ( ( y - C ) / N ) )
127 fllt 
 |-  ( ( ( ( ( A - 1 ) - C ) / N ) e. RR /\ ( ( y - C ) / N ) e. ZZ ) -> ( ( ( ( A - 1 ) - C ) / N ) < ( ( y - C ) / N ) <-> ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) < ( ( y - C ) / N ) ) )
128 16 111 127 syl2an2r 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( ( ( A - 1 ) - C ) / N ) < ( ( y - C ) / N ) <-> ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) < ( ( y - C ) / N ) ) )
129 126 128 mpbid 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) < ( ( y - C ) / N ) )
130 zltp1le 
 |-  ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) e. ZZ /\ ( ( y - C ) / N ) e. ZZ ) -> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) < ( ( y - C ) / N ) <-> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) <_ ( ( y - C ) / N ) ) )
131 17 111 130 syl2an2r 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) < ( ( y - C ) / N ) <-> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) <_ ( ( y - C ) / N ) ) )
132 129 131 mpbid 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) <_ ( ( y - C ) / N ) )
133 80 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> B e. RR )
134 elfzle2 
 |-  ( y e. ( A ... B ) -> y <_ B )
135 134 ad2antrl 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> y <_ B )
136 113 133 114 135 lesub1dd 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( y - C ) <_ ( B - C ) )
137 9 adantr 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( B - C ) e. RR )
138 lediv1 
 |-  ( ( ( y - C ) e. RR /\ ( B - C ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( y - C ) <_ ( B - C ) <-> ( ( y - C ) / N ) <_ ( ( B - C ) / N ) ) )
139 122 137 123 138 syl3anc 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( y - C ) <_ ( B - C ) <-> ( ( y - C ) / N ) <_ ( ( B - C ) / N ) ) )
140 136 139 mpbid 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( y - C ) / N ) <_ ( ( B - C ) / N ) )
141 flge 
 |-  ( ( ( ( B - C ) / N ) e. RR /\ ( ( y - C ) / N ) e. ZZ ) -> ( ( ( y - C ) / N ) <_ ( ( B - C ) / N ) <-> ( ( y - C ) / N ) <_ ( |_ ` ( ( B - C ) / N ) ) ) )
142 10 111 141 syl2an2r 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( ( y - C ) / N ) <_ ( ( B - C ) / N ) <-> ( ( y - C ) / N ) <_ ( |_ ` ( ( B - C ) / N ) ) ) )
143 140 142 mpbid 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( y - C ) / N ) <_ ( |_ ` ( ( B - C ) / N ) ) )
144 99 100 111 132 143 elfzd 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( ( y - C ) / N ) e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) )
145 144 ex 
 |-  ( ph -> ( ( y e. ( A ... B ) /\ N || ( y - C ) ) -> ( ( y - C ) / N ) e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) )
146 97 145 syl5bi 
 |-  ( ph -> ( y e. { x e. ( A ... B ) | N || ( x - C ) } -> ( ( y - C ) / N ) e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) )
147 97 anbi2i 
 |-  ( ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ y e. { x e. ( A ... B ) | N || ( x - C ) } ) <-> ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) )
148 108 zcnd 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> ( y - C ) e. CC )
149 148 adantrl 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> ( y - C ) e. CC )
150 38 zcnd 
 |-  ( ( ph /\ z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ) -> z e. CC )
151 150 adantrr 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> z e. CC )
152 1 nncnd 
 |-  ( ph -> N e. CC )
153 152 adantr 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> N e. CC )
154 103 adantr 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> N =/= 0 )
155 149 151 153 154 divmul3d 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> ( ( ( y - C ) / N ) = z <-> ( y - C ) = ( z x. N ) ) )
156 106 zcnd 
 |-  ( ( ph /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) -> y e. CC )
157 156 adantrl 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> y e. CC )
158 89 adantr 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> C e. CC )
159 88 adantrr 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> ( z x. N ) e. CC )
160 157 158 159 subadd2d 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> ( ( y - C ) = ( z x. N ) <-> ( ( z x. N ) + C ) = y ) )
161 155 160 bitrd 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> ( ( ( y - C ) / N ) = z <-> ( ( z x. N ) + C ) = y ) )
162 eqcom 
 |-  ( z = ( ( y - C ) / N ) <-> ( ( y - C ) / N ) = z )
163 eqcom 
 |-  ( y = ( ( z x. N ) + C ) <-> ( ( z x. N ) + C ) = y )
164 161 162 163 3bitr4g 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( y e. ( A ... B ) /\ N || ( y - C ) ) ) ) -> ( z = ( ( y - C ) / N ) <-> y = ( ( z x. N ) + C ) ) )
165 147 164 sylan2b 
 |-  ( ( ph /\ ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ y e. { x e. ( A ... B ) | N || ( x - C ) } ) ) -> ( z = ( ( y - C ) / N ) <-> y = ( ( z x. N ) + C ) ) )
166 165 ex 
 |-  ( ph -> ( ( z e. ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ y e. { x e. ( A ... B ) | N || ( x - C ) } ) -> ( z = ( ( y - C ) / N ) <-> y = ( ( z x. N ) + C ) ) ) )
167 29 32 94 146 166 en3d 
 |-  ( ph -> ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ~~ { x e. ( A ... B ) | N || ( x - C ) } )
168 entr 
 |-  ( ( ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ~~ ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) /\ ( ( ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) + 1 ) ... ( |_ ` ( ( B - C ) / N ) ) ) ~~ { x e. ( A ... B ) | N || ( x - C ) } ) -> ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ~~ { x e. ( A ... B ) | N || ( x - C ) } )
169 28 167 168 syl2anc 
 |-  ( ph -> ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ~~ { x e. ( A ... B ) | N || ( x - C ) } )
170 fzfi 
 |-  ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) e. Fin
171 ssrab2 
 |-  { x e. ( A ... B ) | N || ( x - C ) } C_ ( A ... B )
172 ssfi 
 |-  ( ( ( A ... B ) e. Fin /\ { x e. ( A ... B ) | N || ( x - C ) } C_ ( A ... B ) ) -> { x e. ( A ... B ) | N || ( x - C ) } e. Fin )
173 30 171 172 mp2an 
 |-  { x e. ( A ... B ) | N || ( x - C ) } e. Fin
174 hashen 
 |-  ( ( ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) e. Fin /\ { x e. ( A ... B ) | N || ( x - C ) } e. Fin ) -> ( ( # ` ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ) = ( # ` { x e. ( A ... B ) | N || ( x - C ) } ) <-> ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ~~ { x e. ( A ... B ) | N || ( x - C ) } ) )
175 170 173 174 mp2an 
 |-  ( ( # ` ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ) = ( # ` { x e. ( A ... B ) | N || ( x - C ) } ) <-> ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ~~ { x e. ( A ... B ) | N || ( x - C ) } )
176 169 175 sylibr 
 |-  ( ph -> ( # ` ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ) = ( # ` { x e. ( A ... B ) | N || ( x - C ) } ) )
177 eluzle 
 |-  ( B e. ( ZZ>= ` ( A - 1 ) ) -> ( A - 1 ) <_ B )
178 3 177 syl 
 |-  ( ph -> ( A - 1 ) <_ B )
179 zre 
 |-  ( ( A - 1 ) e. ZZ -> ( A - 1 ) e. RR )
180 zre 
 |-  ( B e. ZZ -> B e. RR )
181 zre 
 |-  ( C e. ZZ -> C e. RR )
182 lesub1 
 |-  ( ( ( A - 1 ) e. RR /\ B e. RR /\ C e. RR ) -> ( ( A - 1 ) <_ B <-> ( ( A - 1 ) - C ) <_ ( B - C ) ) )
183 179 180 181 182 syl3an 
 |-  ( ( ( A - 1 ) e. ZZ /\ B e. ZZ /\ C e. ZZ ) -> ( ( A - 1 ) <_ B <-> ( ( A - 1 ) - C ) <_ ( B - C ) ) )
184 13 7 4 183 syl3anc 
 |-  ( ph -> ( ( A - 1 ) <_ B <-> ( ( A - 1 ) - C ) <_ ( B - C ) ) )
185 178 184 mpbid 
 |-  ( ph -> ( ( A - 1 ) - C ) <_ ( B - C ) )
186 lediv1 
 |-  ( ( ( ( A - 1 ) - C ) e. RR /\ ( B - C ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( ( A - 1 ) - C ) <_ ( B - C ) <-> ( ( ( A - 1 ) - C ) / N ) <_ ( ( B - C ) / N ) ) )
187 15 9 56 186 syl3anc 
 |-  ( ph -> ( ( ( A - 1 ) - C ) <_ ( B - C ) <-> ( ( ( A - 1 ) - C ) / N ) <_ ( ( B - C ) / N ) ) )
188 185 187 mpbid 
 |-  ( ph -> ( ( ( A - 1 ) - C ) / N ) <_ ( ( B - C ) / N ) )
189 flword2 
 |-  ( ( ( ( ( A - 1 ) - C ) / N ) e. RR /\ ( ( B - C ) / N ) e. RR /\ ( ( ( A - 1 ) - C ) / N ) <_ ( ( B - C ) / N ) ) -> ( |_ ` ( ( B - C ) / N ) ) e. ( ZZ>= ` ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) )
190 16 10 188 189 syl3anc 
 |-  ( ph -> ( |_ ` ( ( B - C ) / N ) ) e. ( ZZ>= ` ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) )
191 uznn0sub 
 |-  ( ( |_ ` ( ( B - C ) / N ) ) e. ( ZZ>= ` ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) -> ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) e. NN0 )
192 hashfz1 
 |-  ( ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) e. NN0 -> ( # ` ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ) = ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) )
193 190 191 192 3syl 
 |-  ( ph -> ( # ` ( 1 ... ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) ) ) = ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) )
194 176 193 eqtr3d 
 |-  ( ph -> ( # ` { x e. ( A ... B ) | N || ( x - C ) } ) = ( ( |_ ` ( ( B - C ) / N ) ) - ( |_ ` ( ( ( A - 1 ) - C ) / N ) ) ) )