Theorem acongrep 31123

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 10632	. . . 4 |- 2 e. NN
2		simpl 455	. . . 4 |- ( ( A e. NN /\ N e. ZZ ) -> A e. NN )
3		nnmulcl 10497	. . . 4 |- ( ( 2 e. NN /\ A e. NN ) -> ( 2 x. A ) e. NN )
4	1, 2, 3	sylancr 661	. . 3 |- ( ( A e. NN /\ N e. ZZ ) -> ( 2 x. A ) e. NN )
5		simpr 459	. . 3 |- ( ( A e. NN /\ N e. ZZ ) -> N e. ZZ )
6		congrep 31116	. . 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 659	. 2 |- ( ( A e. NN /\ N e. ZZ ) -> E. b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) ( 2 x. A ) || ( b - N ) )
8		elfzelz 11631	. . . . 5 |- ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) -> b e. ZZ )
9	8	zred 10906	. . . 4 |- ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) -> b e. RR )
10	9	ad2antrl 725	. . 3 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> b e. RR )
11		nnre 10481	. . . 4 |- ( A e. NN -> A e. RR )
12	11	ad2antrr 723	. . 3 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> A e. RR )
13		elfzle1 11632	. . . . . . 7 |- ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) -> 0 <_ b )
14	13	ad2antrl 725	. . . . . 6 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> 0 <_ b )
15	14	anim1i 566	. . . . 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 725	. . . . . . 7 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> b e. ZZ )
17		0zd 10815	. . . . . . 7 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> 0 e. ZZ )
18		nnz 10825	. . . . . . . 8 |- ( A e. NN -> A e. ZZ )
19	18	ad2antrr 723	. . . . . . 7 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> A e. ZZ )
20		elfz 11621	. . . . . . 7 |- ( ( b e. ZZ /\ 0 e. ZZ /\ A e. ZZ ) -> ( b e. ( 0 ... A ) <-> ( 0 <_ b /\ b <_ A ) ) )
21	16, 17, 19, 20	syl3anc 1226	. . . . . 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 463	. . . . 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 390	. . . 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 2397	. . . . . 6 |- ( a = b -> N = N )
28	26, 27	acongeq12d 31122	. . . . 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 3152	. . . 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 659	. . 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 459	. . . . . 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 1016	. . . . . . . . 9 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b e. RR )
35		2re 10544	. . . . . . . . . . 11 |- 2 e. RR
36		remulcl 9510	. . . . . . . . . . 11 |- ( ( 2 e. RR /\ A e. RR ) -> ( 2 x. A ) e. RR )
37	35, 11, 36	sylancr 661	. . . . . . . . . 10 |- ( A e. NN -> ( 2 x. A ) e. RR )
38	37	3ad2ant1 1015	. . . . . . . . 9 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( 2 x. A ) e. RR )
39		0zd 10815	. . . . . . . . . . 11 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> 0 e. ZZ )
40		2z 10835	. . . . . . . . . . . . 13 |- 2 e. ZZ
41		zmulcl 10851	. . . . . . . . . . . . 13 |- ( ( 2 e. ZZ /\ A e. ZZ ) -> ( 2 x. A ) e. ZZ )
42	40, 18, 41	sylancr 661	. . . . . . . . . . . 12 |- ( A e. NN -> ( 2 x. A ) e. ZZ )
43	42	3ad2ant1 1015	. . . . . . . . . . 11 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( 2 x. A ) e. ZZ )
44		simp2 995	. . . . . . . . . . 11 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) )
45		elfzm11 11693	. . . . . . . . . . . 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 482	. . . . . . . . . . 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 1225	. . . . . . . . . 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 1008	. . . . . . . . 9 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b < ( 2 x. A ) )
49	34, 38, 48	ltled 9666	. . . . . . . 8 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> b <_ ( 2 x. A ) )
50	38, 34	subge0d 10081	. . . . . . . 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 1015	. . . . . . . 8 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> A e. RR )
53		nncn 10482	. . . . . . . . . . 11 |- ( A e. NN -> A e. CC )
54		2times 10593	. . . . . . . . . . . . 13 |- ( A e. CC -> ( 2 x. A ) = ( A + A ) )
55	54	oveq1d 6233	. . . . . . . . . . . 12 |- ( A e. CC -> ( ( 2 x. A ) - A ) = ( ( A + A ) - A ) )
56		pncan2 9762	. . . . . . . . . . . . 13 |- ( ( A e. CC /\ A e. CC ) -> ( ( A + A ) - A ) = A )
57	56	anidms 643	. . . . . . . . . . . 12 |- ( A e. CC -> ( ( A + A ) - A ) = A )
58	55, 57	eqtrd 2437	. . . . . . . . . . 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 1015	. . . . . . . . 9 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( ( 2 x. A ) - A ) = A )
61		simp3 996	. . . . . . . . 9 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> A <_ b )
62	60, 61	eqbrtrd 4404	. . . . . . . 8 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( ( 2 x. A ) - A ) <_ b )
63	38, 52, 34, 62	subled 10094	. . . . . . 7 |- ( ( A e. NN /\ b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ A <_ b ) -> ( ( 2 x. A ) - b ) <_ A )
64	51, 63	jca 530	. . . . . 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 1226	. . . . 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 661	. . . . . . . 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 10911	. . . . . . 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 11621	. . . . . . 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 1226	. . . . . 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 463	. . . . 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 753	. . . . . . . . 9 |- ( ( ( A e. NN /\ N e. ZZ ) /\ ( b e. ( 0 ... ( ( 2 x. A ) - 1 ) ) /\ ( 2 x. A ) || ( b - N ) ) ) -> N e. ZZ )
73		simprr 755	. . . . . . . . 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 31111	. . . . . . . . 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 1227	. . . . . . . 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 10911	. . . . . . . . 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 14049	. . . . . . . . 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 659	. . . . . . . 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 10907	. . . . . . . . 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 10808	. . . . . . . . . 10 |- ( N e. ZZ -> N e. CC )
82	81	ad2antlr 724	. . . . . . . . 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 9873	. . . . . . . 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 10907	. . . . . . . . 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 9555	. . . . . . . . 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 9888	. . . . . . . 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 2437	. . . . . . 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 4410	. . . . . 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 463	. . . . 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 391	. . . 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 2397	. . . . . 6 |- ( a = ( ( 2 x. A ) - b ) -> N = N )
93	91, 92	acongeq12d 31122	. . . . 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 3152	. . . 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 659	. . 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 9623	. 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 2892	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 366   /\ wa 367   /\ w3a 971   = wceq 1399   e. wcel 1836   E.wrex 2747   class class class wbr 4384  (class class class)co 6218   CCcc 9423   RRcr 9424   0cc0 9425   1c1 9426   + caddc 9428   x. cmul 9430   < clt 9561   <_ cle 9562   - cmin 9740   -ucneg 9741   NNcn 10474   2c2 10524   ZZcz 10803   ...cfz 11615   || cdvds 14011

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633  ax-4 1646  ax-5 1719  ax-6 1765  ax-7 1808  ax-8 1838  ax-9 1840  ax-10 1855  ax-11 1860  ax-12 1872  ax-13 2020  ax-ext 2374  ax-sep 4505  ax-nul 4513  ax-pow 4560  ax-pr 4618  ax-un 6513  ax-cnex 9481  ax-resscn 9482  ax-1cn 9483  ax-icn 9484  ax-addcl 9485  ax-addrcl 9486  ax-mulcl 9487  ax-mulrcl 9488  ax-mulcom 9489  ax-addass 9490  ax-mulass 9491  ax-distr 9492  ax-i2m1 9493  ax-1ne0 9494  ax-1rid 9495  ax-rnegex 9496  ax-rrecex 9497  ax-cnre 9498  ax-pre-lttri 9499  ax-pre-lttrn 9500  ax-pre-ltadd 9501  ax-pre-mulgt0 9502  ax-pre-sup 9503

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1628  df-nf 1632  df-sb 1758  df-eu 2236  df-mo 2237  df-clab 2382  df-cleq 2388  df-clel 2391  df-nfc 2546  df-ne 2593  df-nel 2594  df-ral 2751  df-rex 2752  df-reu 2753  df-rmo 2754  df-rab 2755  df-v 3053  df-sbc 3270  df-csb 3366  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-pss 3422  df-nul 3729  df-if 3875  df-pw 3946  df-sn 3962  df-pr 3964  df-tp 3966  df-op 3968  df-uni 4181  df-iun 4262  df-br 4385  df-opab 4443  df-mpt 4444  df-tr 4478  df-eprel 4722  df-id 4726  df-po 4731  df-so 4732  df-fr 4769  df-we 4771  df-ord 4812  df-on 4813  df-lim 4814  df-suc 4815  df-xp 4936  df-rel 4937  df-cnv 4938  df-co 4939  df-dm 4940  df-rn 4941  df-res 4942  df-ima 4943  df-iota 5477  df-fun 5515  df-fn 5516  df-f 5517  df-f1 5518  df-fo 5519  df-f1o 5520  df-fv 5521  df-riota 6180  df-ov 6221  df-oprab 6222  df-mpt2 6223  df-om 6622  df-1st 6721  df-2nd 6722  df-recs 6982  df-rdg 7016  df-er 7251  df-en 7458  df-dom 7459  df-sdom 7460  df-sup 7838  df-pnf 9563  df-mnf 9564  df-xr 9565  df-ltxr 9566  df-le 9567  df-sub 9742  df-neg 9743  df-div 10146  df-nn 10475  df-2 10533  df-n0 10735  df-z 10804  df-uz 11024  df-rp 11162  df-fz 11616  df-fl 11851  df-mod 11920  df-dvds 14012

This theorem is referenced by:  jm2.26  31150