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	biimtrid	\|- ( 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 ) ) ) )

Metamath Proof Explorer

Theorem hashdvds

Proof