Theorem acongrep 30886

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

Assertion

Ref	Expression
acongrep	|- ( ( A e. NN /\ N e. ZZ ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )

Distinct variable groups:   A, a   N, a

Proof of Theorem acongrep

Dummy variable b is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2nn 10694	. . . 4 |- 2 e. NN
2		simpl 457	. . . 4 |- ( ( A e. NN /\ N e. ZZ ) -> A e. NN )
3		nnmulcl 10560	. . . 4 |- ( ( 2 e. NN /\ A e. NN ) -> ( 2 x. A ) e. NN )
4	1, 2, 3	sylancr 663	. . 3 |- ( ( A e. NN /\ N e. ZZ ) -> ( 2 x. A ) e. NN )
5		simpr 461	. . 3 |- ( ( A e. NN /\ N e. ZZ ) -> N e. ZZ )
6		congrep 30879	. . 3 |- ( ( ( 2 x. A ) e. NN /\ N e. ZZ ) -> E. b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) ( 2 x. A ) || ( b - N ) )
7	4, 5, 6	syl2anc 661	. 2 |- ( ( A e. NN /\ N e. ZZ ) -> E. b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) ( 2 x. A ) || ( b - N ) )
8		elfzelz 11692	. . . . 5 |- ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) -> b e. ZZ )
9	8	zred 10969	. . . 4 |- ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) -> b e. RR )
10	9	ad2antrl 727	. . 3 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> b e. RR )
11		nnre 10544	. . . 4 |- ( A e. NN -> A e. RR )
12	11	ad2antrr 725	. . 3 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> A e. RR )
13		elfzle1 11693	. . . . . . 7 |- ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) -> 0 <_ b )
14	13	ad2antrl 727	. . . . . 6 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> 0 <_ b )
15	14	anim1i 568	. . . . 5 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> ( 0 <_ b /\ b <_ A ) )
16	8	ad2antrl 727	. . . . . . 7 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> b e. ZZ )
17		0zd 10877	. . . . . . 7 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> 0 e. ZZ )
18		nnz 10887	. . . . . . . 8 |- ( A e. NN -> A e. ZZ )
19	18	ad2antrr 725	. . . . . . 7 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> A e. ZZ )
20		elfz 11682	. . . . . . 7 |- ( ( b e. ZZ /\ 0 e. ZZ /\ A e. ZZ ) -> ( b e. ( 0 ... A ) <-> ( 0 <_ b /\ b <_ A ) ) )
21	16, 17, 19, 20	syl3anc 1227	. . . . . 6 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( b e. ( 0 ... A ) <-> ( 0 <_ b /\ b <_ A ) ) )
22	21	adantr 465	. . . . 5 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> ( b e. ( 0 ... A ) <-> ( 0 <_ b /\ b <_ A ) ) )
23	15, 22	mpbird 232	. . . 4 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> b e. ( 0 ... A ) )
24		simplrr 760	. . . . 5 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> ( 2 x. A ) || ( b - N ) )
25	24	orcd 392	. . . 4 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> ( ( 2 x. A ) || ( b - N ) \/ ( 2 x. A ) || ( b - -u N ) ) )
26		id 22	. . . . . 6 |- ( a = b -> a = b )
27		eqidd 2442	. . . . . 6 |- ( a = b -> N = N )
28	26, 27	acongeq12d 30885	. . . . 5 |- ( a = b -> ( ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) <-> ( ( 2 x. A ) || ( b - N ) \/ ( 2 x. A ) || ( b - -u N ) ) ) )
29	28	rspcev 3194	. . . 4 |- ( ( b e. ( 0 ... A ) /\ ( ( 2 x. A ) || ( b - N ) \/ ( 2 x. A ) || ( b - -u N ) ) ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
30	23, 25, 29	syl2anc 661	. . 3 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ b <_ A ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
31		simplll 757	. . . . . 6 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> A e. NN )
32		simplrl 759	. . . . . 6 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) )
33		simpr 461	. . . . . 6 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> A <_ b )
34	9	3ad2ant2 1017	. . . . . . . . 9 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b e. RR )
35		2re 10606	. . . . . . . . . . 11 |- 2 e. RR
36		remulcl 9575	. . . . . . . . . . 11 |- ( ( 2 e. RR /\ A e. RR ) -> ( 2 x. A ) e. RR )
37	35, 11, 36	sylancr 663	. . . . . . . . . 10 |- ( A e. NN -> ( 2 x. A ) e. RR )
38	37	3ad2ant1 1016	. . . . . . . . 9 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( 2 x. A ) e. RR )
39		0zd 10877	. . . . . . . . . . 11 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> 0 e. ZZ )
40		2z 10897	. . . . . . . . . . . . 13 |- 2 e. ZZ
41		zmulcl 10913	. . . . . . . . . . . . 13 |- ( ( 2 e. ZZ /\ A e. ZZ ) -> ( 2 x. A ) e. ZZ )
42	40, 18, 41	sylancr 663	. . . . . . . . . . . 12 |- ( A e. NN -> ( 2 x. A ) e. ZZ )
43	42	3ad2ant1 1016	. . . . . . . . . . 11 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( 2 x. A ) e. ZZ )
44		simp2 996	. . . . . . . . . . 11 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) )
45		elfzm11 11753	. . . . . . . . . . . 12 |- ( ( 0 e. ZZ /\ ( 2 x. A ) e. ZZ ) -> ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) <-> ( b e. ZZ /\ 0 <_ b /\ b < ( 2 x. A ) ) ) )
46	45	biimpa 484	. . . . . . . . . . 11 |- ( ( ( 0 e. ZZ /\ ( 2 x. A ) e. ZZ ) /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) ) -> ( b e. ZZ /\ 0 <_ b /\ b < ( 2 x. A ) ) )
47	39, 43, 44, 46	syl21anc 1226	. . . . . . . . . 10 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( b e. ZZ /\ 0 <_ b /\ b < ( 2 x. A ) ) )
48	47	simp3d 1009	. . . . . . . . 9 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b < ( 2 x. A ) )
49	34, 38, 48	ltled 9731	. . . . . . . 8 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b <_ ( 2 x. A ) )
50	38, 34	subge0d 10143	. . . . . . . 8 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( 0 <_ ( ( 2 x. A ) - b ) <-> b <_ ( 2 x. A ) ) )
51	49, 50	mpbird 232	. . . . . . 7 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> 0 <_ ( ( 2 x. A ) - b ) )
52	11	3ad2ant1 1016	. . . . . . . 8 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> A e. RR )
53		nncn 10545	. . . . . . . . . . 11 |- ( A e. NN -> A e. CC )
54		2times 10655	. . . . . . . . . . . . 13 |- ( A e. CC -> ( 2 x. A ) = ( A + A ) )
55	54	oveq1d 6292	. . . . . . . . . . . 12 |- ( A e. CC -> ( ( 2 x. A ) - A ) = ( ( A + A ) - A ) )
56		pncan2 9827	. . . . . . . . . . . . 13 |- ( ( A e. CC /\ A e. CC ) -> ( ( A + A ) - A ) = A )
57	56	anidms 645	. . . . . . . . . . . 12 |- ( A e. CC -> ( ( A + A ) - A ) = A )
58	55, 57	eqtrd 2482	. . . . . . . . . . 11 |- ( A e. CC -> ( ( 2 x. A ) - A ) = A )
59	53, 58	syl 16	. . . . . . . . . 10 |- ( A e. NN -> ( ( 2 x. A ) - A ) = A )
60	59	3ad2ant1 1016	. . . . . . . . 9 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( ( 2 x. A ) - A ) = A )
61		simp3 997	. . . . . . . . 9 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> A <_ b )
62	60, 61	eqbrtrd 4453	. . . . . . . 8 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( ( 2 x. A ) - A ) <_ b )
63	38, 52, 34, 62	subled 10156	. . . . . . 7 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( ( 2 x. A ) - b ) <_ A )
64	51, 63	jca 532	. . . . . 6 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( 0 <_ ( ( 2 x. A ) - b ) /\ ( ( 2 x. A ) - b ) <_ A ) )
65	31, 32, 33, 64	syl3anc 1227	. . . . 5 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> ( 0 <_ ( ( 2 x. A ) - b ) /\ ( ( 2 x. A ) - b ) <_ A ) )
66	40, 19, 41	sylancr 663	. . . . . . . 8 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) e. ZZ )
67	66, 16	zsubcld 10974	. . . . . . 7 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( 2 x. A ) - b ) e. ZZ )
68		elfz 11682	. . . . . . 7 |- ( ( ( ( 2 x. A ) - b ) e. ZZ /\ 0 e. ZZ /\ A e. ZZ ) -> ( ( ( 2 x. A ) - b ) e. ( 0 ... A ) <-> ( 0 <_ ( ( 2 x. A ) - b ) /\ ( ( 2 x. A ) - b ) <_ A ) ) )
69	67, 17, 19, 68	syl3anc 1227	. . . . . 6 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( ( 2 x. A ) - b ) e. ( 0 ... A ) <-> ( 0 <_ ( ( 2 x. A ) - b ) /\ ( ( 2 x. A ) - b ) <_ A ) ) )
70	69	adantr 465	. . . . 5 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> ( ( ( 2 x. A ) - b ) e. ( 0 ... A ) <-> ( 0 <_ ( ( 2 x. A ) - b ) /\ ( ( 2 x. A ) - b ) <_ A ) ) )
71	65, 70	mpbird 232	. . . 4 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> ( ( 2 x. A ) - b ) e. ( 0 ... A ) )
72		simplr 754	. . . . . . . . 9 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> N e. ZZ )
73		simprr 756	. . . . . . . . 9 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) || ( b - N ) )
74		congsym 30874	. . . . . . . . 9 |- ( ( ( ( 2 x. A ) e. ZZ /\ b e. ZZ ) /\ ( N e. ZZ /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) || ( N - b ) )
75	66, 16, 72, 73, 74	syl22anc 1228	. . . . . . . 8 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) || ( N - b ) )
76	72, 16	zsubcld 10974	. . . . . . . . 9 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( N - b ) e. ZZ )
77		dvdsadd 13896	. . . . . . . . 9 |- ( ( ( 2 x. A ) e. ZZ /\ ( N - b ) e. ZZ ) -> ( ( 2 x. A ) || ( N - b ) <-> ( 2 x. A ) || ( ( 2 x. A ) + ( N - b ) ) ) )
78	66, 76, 77	syl2anc 661	. . . . . . . 8 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( 2 x. A ) || ( N - b ) <-> ( 2 x. A ) || ( ( 2 x. A ) + ( N - b ) ) ) )
79	75, 78	mpbid 210	. . . . . . 7 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) || ( ( 2 x. A ) + ( N - b ) ) )
80	67	zcnd 10970	. . . . . . . . 9 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( 2 x. A ) - b ) e. CC )
81		zcn 10870	. . . . . . . . . 10 |- ( N e. ZZ -> N e. CC )
82	81	ad2antlr 726	. . . . . . . . 9 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> N e. CC )
83	80, 82	subnegd 9938	. . . . . . . 8 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( ( 2 x. A ) - b ) - -u N ) = ( ( ( 2 x. A ) - b ) + N ) )
84	66	zcnd 10970	. . . . . . . . 9 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) e. CC )
85	10	recnd 9620	. . . . . . . . 9 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> b e. CC )
86	84, 85, 82	subadd23d 9953	. . . . . . . 8 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( ( 2 x. A ) - b ) + N ) = ( ( 2 x. A ) + ( N - b ) ) )
87	83, 86	eqtrd 2482	. . . . . . 7 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( ( ( 2 x. A ) - b ) - -u N ) = ( ( 2 x. A ) + ( N - b ) ) )
88	79, 87	breqtrrd 4459	. . . . . 6 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - -u N ) )
89	88	adantr 465	. . . . 5 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - -u N ) )
90	89	olcd 393	. . . 4 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> ( ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - N ) \/ ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - -u N ) ) )
91		id 22	. . . . . 6 |- ( a = ( ( 2 x. A ) - b ) -> a = ( ( 2 x. A ) - b ) )
92		eqidd 2442	. . . . . 6 |- ( a = ( ( 2 x. A ) - b ) -> N = N )
93	91, 92	acongeq12d 30885	. . . . 5 |- ( a = ( ( 2 x. A ) - b ) -> ( ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) <-> ( ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - N ) \/ ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - -u N ) ) ) )
94	93	rspcev 3194	. . . 4 |- ( ( ( ( 2 x. A ) - b ) e. ( 0 ... A ) /\ ( ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - N ) \/ ( 2 x. A ) || ( ( ( 2 x. A ) - b ) - -u N ) ) ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
95	71, 90, 94	syl2anc 661	. . 3 |- ( ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) /\ A <_ b ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
96	10, 12, 30, 95	lecasei 9688	. 2 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )
97	7, 96	rexlimddv 2937	1 |- ( ( A e. NN /\ N e. ZZ ) -> E. a e. ( 0 ... A ) ( ( 2 x. A ) || ( a - N ) \/ ( 2 x. A ) || ( a - -u N ) ) )

Syntax hints:   -> wi 4   <-> wb 184   \/ wo 368   /\ wa 369   /\ w3a 972   = wceq 1381   e. wcel 1802   E.wrex 2792   class class class wbr 4433  (class class class)co 6277   CCcc 9488   RRcr 9489   0cc0 9490   1c1 9491   + caddc 9493   x. cmul 9495   < clt 9626   <_ cle 9627   - cmin 9805   -ucneg 9806   NNcn 10537   2c2 10586   ZZcz 10865   ...cfz 11676   || cdvds 13858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-pre-sup 9568

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-iun 4313  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-om 6682  df-1st 6781  df-2nd 6782  df-recs 7040  df-rdg 7074  df-er 7309  df-en 7515  df-dom 7516  df-sdom 7517  df-sup 7899  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9807  df-neg 9808  df-div 10208  df-nn 10538  df-2 10595  df-n0 10797  df-z 10866  df-uz 11086  df-rp 11225  df-fz 11677  df-fl 11903  df-mod 11971  df-dvds 13859

This theorem is referenced by:  jm2.26  30912