Theorem divalglem9 13935

Description: Lemma for divalg 13937. (Contributed by Paul Chapman, 21-Mar-2011.)

Hypotheses

Ref	Expression
divalglem8.1	|- N e. ZZ
divalglem8.2	|- D e. ZZ
divalglem8.3	|- D =/= 0
divalglem8.4	|- S = { r e. NN0 | D || ( N - r ) }
divalglem9.5	|- R = sup ( S , RR , `' < )

Assertion

Ref	Expression
divalglem9	|- E! x e. S x < ( abs ` D )

Distinct variable groups:   D, r, x   N, r, x   x, S   x, R

Allowed substitution hints:   R( r)   S( r)

Proof of Theorem divalglem9

Dummy variables k y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		divalglem9.5	. . . 4 |- R = sup ( S , RR , `' < )
2		divalglem8.1	. . . . 5 |- N e. ZZ
3		divalglem8.2	. . . . 5 |- D e. ZZ
4		divalglem8.3	. . . . 5 |- D =/= 0
5		divalglem8.4	. . . . 5 |- S = { r e. NN0 | D || ( N - r ) }
6	2, 3, 4, 5	divalglem2 13929	. . . 4 |- sup ( S , RR , `' < ) e. S
7	1, 6	eqeltri 2551	. . 3 |- R e. S
8	2, 3, 4, 5, 1	divalglem5 13931	. . . 4 |- ( 0 <_ R /\ R < ( abs ` D ) )
9	8	simpri 462	. . 3 |- R < ( abs ` D )
10		breq1 4456	. . . 4 |- ( x = R -> ( x < ( abs ` D ) <-> R < ( abs ` D ) ) )
11	10	rspcev 3219	. . 3 |- ( ( R e. S /\ R < ( abs ` D ) ) -> E. x e. S x < ( abs ` D ) )
12	7, 9, 11	mp2an 672	. 2 |- E. x e. S x < ( abs ` D )
13		oveq2 6303	. . . . . . . . . . . . . . 15 |- ( r = x -> ( N - r ) = ( N - x ) )
14	13	breq2d 4465	. . . . . . . . . . . . . 14 |- ( r = x -> ( D || ( N - r ) <-> D || ( N - x ) ) )
15	14, 5	elrab2 3268	. . . . . . . . . . . . 13 |- ( x e. S <-> ( x e. NN0 /\ D || ( N - x ) ) )
16	15	simplbi 460	. . . . . . . . . . . 12 |- ( x e. S -> x e. NN0 )
17	16	nn0zd 10976	. . . . . . . . . . 11 |- ( x e. S -> x e. ZZ )
18		oveq2 6303	. . . . . . . . . . . . . . 15 |- ( r = y -> ( N - r ) = ( N - y ) )
19	18	breq2d 4465	. . . . . . . . . . . . . 14 |- ( r = y -> ( D || ( N - r ) <-> D || ( N - y ) ) )
20	19, 5	elrab2 3268	. . . . . . . . . . . . 13 |- ( y e. S <-> ( y e. NN0 /\ D || ( N - y ) ) )
21	20	simplbi 460	. . . . . . . . . . . 12 |- ( y e. S -> y e. NN0 )
22	21	nn0zd 10976	. . . . . . . . . . 11 |- ( y e. S -> y e. ZZ )
23		zsubcl 10917	. . . . . . . . . . . . 13 |- ( ( N e. ZZ /\ x e. ZZ ) -> ( N - x ) e. ZZ )
24	2, 23	mpan 670	. . . . . . . . . . . 12 |- ( x e. ZZ -> ( N - x ) e. ZZ )
25		zsubcl 10917	. . . . . . . . . . . . 13 |- ( ( N e. ZZ /\ y e. ZZ ) -> ( N - y ) e. ZZ )
26	2, 25	mpan 670	. . . . . . . . . . . 12 |- ( y e. ZZ -> ( N - y ) e. ZZ )
27	24, 26	anim12i 566	. . . . . . . . . . 11 |- ( ( x e. ZZ /\ y e. ZZ ) -> ( ( N - x ) e. ZZ /\ ( N - y ) e. ZZ ) )
28	17, 22, 27	syl2an 477	. . . . . . . . . 10 |- ( ( x e. S /\ y e. S ) -> ( ( N - x ) e. ZZ /\ ( N - y ) e. ZZ ) )
29	15	simprbi 464	. . . . . . . . . . 11 |- ( x e. S -> D || ( N - x ) )
30	20	simprbi 464	. . . . . . . . . . 11 |- ( y e. S -> D || ( N - y ) )
31	29, 30	anim12i 566	. . . . . . . . . 10 |- ( ( x e. S /\ y e. S ) -> ( D || ( N - x ) /\ D || ( N - y ) ) )
32		dvds2sub 13894	. . . . . . . . . . 11 |- ( ( D e. ZZ /\ ( N - x ) e. ZZ /\ ( N - y ) e. ZZ ) -> ( ( D || ( N - x ) /\ D || ( N - y ) ) -> D || ( ( N - x ) - ( N - y ) ) ) )
33	3, 32	mp3an1 1311	. . . . . . . . . 10 |- ( ( ( N - x ) e. ZZ /\ ( N - y ) e. ZZ ) -> ( ( D || ( N - x ) /\ D || ( N - y ) ) -> D || ( ( N - x ) - ( N - y ) ) ) )
34	28, 31, 33	sylc 60	. . . . . . . . 9 |- ( ( x e. S /\ y e. S ) -> D || ( ( N - x ) - ( N - y ) ) )
35		zcn 10881	. . . . . . . . . . . 12 |- ( x e. ZZ -> x e. CC )
36		zcn 10881	. . . . . . . . . . . 12 |- ( y e. ZZ -> y e. CC )
37	2	zrei 10882	. . . . . . . . . . . . . . . . 17 |- N e. RR
38	37	recni 9620	. . . . . . . . . . . . . . . 16 |- N e. CC
39	38	subidi 9902	. . . . . . . . . . . . . . 15 |- ( N - N ) = 0
40	39	oveq1i 6305	. . . . . . . . . . . . . 14 |- ( ( N - N ) - ( x - y ) ) = ( 0 - ( x - y ) )
41		0cn 9600	. . . . . . . . . . . . . . 15 |- 0 e. CC
42		subsub2 9859	. . . . . . . . . . . . . . 15 |- ( ( 0 e. CC /\ x e. CC /\ y e. CC ) -> ( 0 - ( x - y ) ) = ( 0 + ( y - x ) ) )
43	41, 42	mp3an1 1311	. . . . . . . . . . . . . 14 |- ( ( x e. CC /\ y e. CC ) -> ( 0 - ( x - y ) ) = ( 0 + ( y - x ) ) )
44	40, 43	syl5eq 2520	. . . . . . . . . . . . 13 |- ( ( x e. CC /\ y e. CC ) -> ( ( N - N ) - ( x - y ) ) = ( 0 + ( y - x ) ) )
45		sub4 9876	. . . . . . . . . . . . . 14 |- ( ( ( N e. CC /\ N e. CC ) /\ ( x e. CC /\ y e. CC ) ) -> ( ( N - N ) - ( x - y ) ) = ( ( N - x ) - ( N - y ) ) )
46	38, 38, 45	mpanl12 682	. . . . . . . . . . . . 13 |- ( ( x e. CC /\ y e. CC ) -> ( ( N - N ) - ( x - y ) ) = ( ( N - x ) - ( N - y ) ) )
47		subcl 9831	. . . . . . . . . . . . . . 15 |- ( ( y e. CC /\ x e. CC ) -> ( y - x ) e. CC )
48	47	ancoms 453	. . . . . . . . . . . . . 14 |- ( ( x e. CC /\ y e. CC ) -> ( y - x ) e. CC )
49	48	addid2d 9792	. . . . . . . . . . . . 13 |- ( ( x e. CC /\ y e. CC ) -> ( 0 + ( y - x ) ) = ( y - x ) )
50	44, 46, 49	3eqtr3d 2516	. . . . . . . . . . . 12 |- ( ( x e. CC /\ y e. CC ) -> ( ( N - x ) - ( N - y ) ) = ( y - x ) )
51	35, 36, 50	syl2an 477	. . . . . . . . . . 11 |- ( ( x e. ZZ /\ y e. ZZ ) -> ( ( N - x ) - ( N - y ) ) = ( y - x ) )
52	17, 22, 51	syl2an 477	. . . . . . . . . 10 |- ( ( x e. S /\ y e. S ) -> ( ( N - x ) - ( N - y ) ) = ( y - x ) )
53	52	breq2d 4465	. . . . . . . . 9 |- ( ( x e. S /\ y e. S ) -> ( D || ( ( N - x ) - ( N - y ) ) <-> D || ( y - x ) ) )
54	34, 53	mpbid 210	. . . . . . . 8 |- ( ( x e. S /\ y e. S ) -> D || ( y - x ) )
55		zsubcl 10917	. . . . . . . . . . 11 |- ( ( y e. ZZ /\ x e. ZZ ) -> ( y - x ) e. ZZ )
56	55	ancoms 453	. . . . . . . . . 10 |- ( ( x e. ZZ /\ y e. ZZ ) -> ( y - x ) e. ZZ )
57		absdvdsb 13880	. . . . . . . . . 10 |- ( ( D e. ZZ /\ ( y - x ) e. ZZ ) -> ( D || ( y - x ) <-> ( abs ` D ) || ( y - x ) ) )
58	3, 56, 57	sylancr 663	. . . . . . . . 9 |- ( ( x e. ZZ /\ y e. ZZ ) -> ( D || ( y - x ) <-> ( abs ` D ) || ( y - x ) ) )
59	17, 22, 58	syl2an 477	. . . . . . . 8 |- ( ( x e. S /\ y e. S ) -> ( D || ( y - x ) <-> ( abs ` D ) || ( y - x ) ) )
60	54, 59	mpbid 210	. . . . . . 7 |- ( ( x e. S /\ y e. S ) -> ( abs ` D ) || ( y - x ) )
61		nnabscl 13138	. . . . . . . . . . 11 |- ( ( D e. ZZ /\ D =/= 0 ) -> ( abs ` D ) e. NN )
62	3, 4, 61	mp2an 672	. . . . . . . . . 10 |- ( abs ` D ) e. NN
63	62	nnzi 10900	. . . . . . . . 9 |- ( abs ` D ) e. ZZ
64		divides 13866	. . . . . . . . 9 |- ( ( ( abs ` D ) e. ZZ /\ ( y - x ) e. ZZ ) -> ( ( abs ` D ) || ( y - x ) <-> E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) ) )
65	63, 56, 64	sylancr 663	. . . . . . . 8 |- ( ( x e. ZZ /\ y e. ZZ ) -> ( ( abs ` D ) || ( y - x ) <-> E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) ) )
66	17, 22, 65	syl2an 477	. . . . . . 7 |- ( ( x e. S /\ y e. S ) -> ( ( abs ` D ) || ( y - x ) <-> E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) ) )
67	60, 66	mpbid 210	. . . . . 6 |- ( ( x e. S /\ y e. S ) -> E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) )
68	67	adantr 465	. . . . 5 |- ( ( ( x e. S /\ y e. S ) /\ ( x < ( abs ` D ) /\ y < ( abs ` D ) ) ) -> E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) )
69	2, 3, 4, 5	divalglem8 13934	. . . . . 6 |- ( ( ( x e. S /\ y e. S ) /\ ( x < ( abs ` D ) /\ y < ( abs ` D ) ) ) -> ( k e. ZZ -> ( ( k x. ( abs ` D ) ) = ( y - x ) -> x = y ) ) )
70	69	rexlimdv 2957	. . . . 5 |- ( ( ( x e. S /\ y e. S ) /\ ( x < ( abs ` D ) /\ y < ( abs ` D ) ) ) -> ( E. k e. ZZ ( k x. ( abs ` D ) ) = ( y - x ) -> x = y ) )
71	68, 70	mpd 15	. . . 4 |- ( ( ( x e. S /\ y e. S ) /\ ( x < ( abs ` D ) /\ y < ( abs ` D ) ) ) -> x = y )
72	71	ex 434	. . 3 |- ( ( x e. S /\ y e. S ) -> ( ( x < ( abs ` D ) /\ y < ( abs ` D ) ) -> x = y ) )
73	72	rgen2a 2894	. 2 |- A. x e. S A. y e. S ( ( x < ( abs ` D ) /\ y < ( abs ` D ) ) -> x = y )
74		breq1 4456	. . 3 |- ( x = y -> ( x < ( abs ` D ) <-> y < ( abs ` D ) ) )
75	74	reu4 3302	. 2 |- ( E! x e. S x < ( abs ` D ) <-> ( E. x e. S x < ( abs ` D ) /\ A. x e. S A. y e. S ( ( x < ( abs ` D ) /\ y < ( abs ` D ) ) -> x = y ) ) )
76	12, 73, 75	mpbir2an 918	1 |- E! x e. S x < ( abs ` D )

Syntax hints:   -> wi 4   <-> wb 184   /\ wa 369   = wceq 1379   e. wcel 1767   =/= wne 2662   A.wral 2817   E.wrex 2818   E!wreu 2819   {crab 2821   class class class wbr 4453   `'ccnv 5004   ` cfv 5594  (class class class)co 6295   supcsup 7912   CCcc 9502   RRcr 9503   0cc0 9504   + caddc 9507   x. cmul 9509   < clt 9640   <_ cle 9641   - cmin 9817   NNcn 10548   NN0cn0 10807   ZZcz 10876   abscabs 13047   || cdivides 13864

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4574  ax-nul 4582  ax-pow 4631  ax-pr 4692  ax-un 6587  ax-cnex 9560  ax-resscn 9561  ax-1cn 9562  ax-icn 9563  ax-addcl 9564  ax-addrcl 9565  ax-mulcl 9566  ax-mulrcl 9567  ax-mulcom 9568  ax-addass 9569  ax-mulass 9570  ax-distr 9571  ax-i2m1 9572  ax-1ne0 9573  ax-1rid 9574  ax-rnegex 9575  ax-rrecex 9576  ax-cnre 9577  ax-pre-lttri 9578  ax-pre-lttrn 9579  ax-pre-ltadd 9580  ax-pre-mulgt0 9581  ax-pre-sup 9582

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-nel 2665  df-ral 2822  df-rex 2823  df-reu 2824  df-rmo 2825  df-rab 2826  df-v 3120  df-sbc 3337  df-csb 3441  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-pss 3497  df-nul 3791  df-if 3946  df-pw 4018  df-sn 4034  df-pr 4036  df-tp 4038  df-op 4040  df-uni 4252  df-iun 4333  df-br 4454  df-opab 4512  df-mpt 4513  df-tr 4547  df-eprel 4797  df-id 4801  df-po 4806  df-so 4807  df-fr 4844  df-we 4846  df-ord 4887  df-on 4888  df-lim 4889  df-suc 4890  df-xp 5011  df-rel 5012  df-cnv 5013  df-co 5014  df-dm 5015  df-rn 5016  df-res 5017  df-ima 5018  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6256  df-ov 6298  df-oprab 6299  df-mpt2 6300  df-om 6696  df-1st 6795  df-2nd 6796  df-recs 7054  df-rdg 7088  df-er 7323  df-en 7529  df-dom 7530  df-sdom 7531  df-sup 7913  df-pnf 9642  df-mnf 9643  df-xr 9644  df-ltxr 9645  df-le 9646  df-sub 9819  df-neg 9820  df-div 10219  df-nn 10549  df-2 10606  df-3 10607  df-n0 10808  df-z 10877  df-uz 11095  df-rp 11233  df-fz 11685  df-seq 12088  df-exp 12147  df-cj 12912  df-re 12913  df-im 12914  df-sqrt 13048  df-abs 13049  df-dvds 13865

This theorem is referenced by:  divalglem10  13936