Theorem vdwlem3

Description: Lemma for vdw . (Contributed by Mario Carneiro, 13-Sep-2014)

	Ref	Expression
Hypotheses	vdwlem3.v	|- ( ph -> V e. NN )
	vdwlem3.w	|- ( ph -> W e. NN )
	vdwlem3.a	|- ( ph -> A e. ( 1 ... V ) )
	vdwlem3.b	|- ( ph -> B e. ( 1 ... W ) )
Assertion	vdwlem3	|- ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		vdwlem3.v	|- ( ph -> V e. NN )
2		vdwlem3.w	|- ( ph -> W e. NN )
3		vdwlem3.a	|- ( ph -> A e. ( 1 ... V ) )
4		vdwlem3.b	|- ( ph -> B e. ( 1 ... W ) )
5		elfznn	|- ( B e. ( 1 ... W ) -> B e. NN )
6	4 5	syl	|- ( ph -> B e. NN )
7		elfznn	|- ( A e. ( 1 ... V ) -> A e. NN )
8	3 7	syl	|- ( ph -> A e. NN )
9		nnm1nn0	|- ( A e. NN -> ( A - 1 ) e. NN0 )
10	8 9	syl	|- ( ph -> ( A - 1 ) e. NN0 )
11		nn0nnaddcl	|- ( ( ( A - 1 ) e. NN0 /\ V e. NN ) -> ( ( A - 1 ) + V ) e. NN )
12	10 1 11	syl2anc	|- ( ph -> ( ( A - 1 ) + V ) e. NN )
13	2 12	nnmulcld	|- ( ph -> ( W x. ( ( A - 1 ) + V ) ) e. NN )
14	6 13	nnaddcld	|- ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. NN )
15	14	nnred	|- ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. RR )
16	8 1	nnaddcld	|- ( ph -> ( A + V ) e. NN )
17	2 16	nnmulcld	|- ( ph -> ( W x. ( A + V ) ) e. NN )
18	17	nnred	|- ( ph -> ( W x. ( A + V ) ) e. RR )
19		2nn	|- 2 e. NN
20		nnmulcl	|- ( ( 2 e. NN /\ V e. NN ) -> ( 2 x. V ) e. NN )
21	19 1 20	sylancr	|- ( ph -> ( 2 x. V ) e. NN )
22	2 21	nnmulcld	|- ( ph -> ( W x. ( 2 x. V ) ) e. NN )
23	22	nnred	|- ( ph -> ( W x. ( 2 x. V ) ) e. RR )
24		elfzle2	|- ( B e. ( 1 ... W ) -> B <_ W )
25	4 24	syl	|- ( ph -> B <_ W )
26		nnre	|- ( B e. NN -> B e. RR )
27		nnre	|- ( W e. NN -> W e. RR )
28		nnre	|- ( ( W x. ( ( A - 1 ) + V ) ) e. NN -> ( W x. ( ( A - 1 ) + V ) ) e. RR )
29		leadd1	|- ( ( B e. RR /\ W e. RR /\ ( W x. ( ( A - 1 ) + V ) ) e. RR ) -> ( B <_ W <-> ( B + ( W x. ( ( A - 1 ) + V ) ) ) <_ ( W + ( W x. ( ( A - 1 ) + V ) ) ) ) )
30	26 27 28 29	syl3an	|- ( ( B e. NN /\ W e. NN /\ ( W x. ( ( A - 1 ) + V ) ) e. NN ) -> ( B <_ W <-> ( B + ( W x. ( ( A - 1 ) + V ) ) ) <_ ( W + ( W x. ( ( A - 1 ) + V ) ) ) ) )
31	6 2 13 30	syl3anc	|- ( ph -> ( B <_ W <-> ( B + ( W x. ( ( A - 1 ) + V ) ) ) <_ ( W + ( W x. ( ( A - 1 ) + V ) ) ) ) )
32	25 31	mpbid	|- ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) <_ ( W + ( W x. ( ( A - 1 ) + V ) ) ) )
33	2	nncnd	|- ( ph -> W e. CC )
34		1cnd	|- ( ph -> 1 e. CC )
35	12	nncnd	|- ( ph -> ( ( A - 1 ) + V ) e. CC )
36	33 34 35	adddid	|- ( ph -> ( W x. ( 1 + ( ( A - 1 ) + V ) ) ) = ( ( W x. 1 ) + ( W x. ( ( A - 1 ) + V ) ) ) )
37	10	nn0cnd	|- ( ph -> ( A - 1 ) e. CC )
38	1	nncnd	|- ( ph -> V e. CC )
39	34 37 38	addassd	|- ( ph -> ( ( 1 + ( A - 1 ) ) + V ) = ( 1 + ( ( A - 1 ) + V ) ) )
40		ax-1cn	|- 1 e. CC
41	8	nncnd	|- ( ph -> A e. CC )
42		pncan3	|- ( ( 1 e. CC /\ A e. CC ) -> ( 1 + ( A - 1 ) ) = A )
43	40 41 42	sylancr	|- ( ph -> ( 1 + ( A - 1 ) ) = A )
44	43	oveq1d	|- ( ph -> ( ( 1 + ( A - 1 ) ) + V ) = ( A + V ) )
45	39 44	eqtr3d	|- ( ph -> ( 1 + ( ( A - 1 ) + V ) ) = ( A + V ) )
46	45	oveq2d	|- ( ph -> ( W x. ( 1 + ( ( A - 1 ) + V ) ) ) = ( W x. ( A + V ) ) )
47	33	mulid1d	|- ( ph -> ( W x. 1 ) = W )
48	47	oveq1d	|- ( ph -> ( ( W x. 1 ) + ( W x. ( ( A - 1 ) + V ) ) ) = ( W + ( W x. ( ( A - 1 ) + V ) ) ) )
49	36 46 48	3eqtr3d	|- ( ph -> ( W x. ( A + V ) ) = ( W + ( W x. ( ( A - 1 ) + V ) ) ) )
50	32 49	breqtrrd	|- ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) <_ ( W x. ( A + V ) ) )
51	8	nnred	|- ( ph -> A e. RR )
52	1	nnred	|- ( ph -> V e. RR )
53		elfzle2	|- ( A e. ( 1 ... V ) -> A <_ V )
54	3 53	syl	|- ( ph -> A <_ V )
55	51 52 52 54	leadd1dd	|- ( ph -> ( A + V ) <_ ( V + V ) )
56	38	2timesd	|- ( ph -> ( 2 x. V ) = ( V + V ) )
57	55 56	breqtrrd	|- ( ph -> ( A + V ) <_ ( 2 x. V ) )
58	16	nnred	|- ( ph -> ( A + V ) e. RR )
59	21	nnred	|- ( ph -> ( 2 x. V ) e. RR )
60	2	nnred	|- ( ph -> W e. RR )
61	2	nngt0d	|- ( ph -> 0 < W )
62		lemul2	|- ( ( ( A + V ) e. RR /\ ( 2 x. V ) e. RR /\ ( W e. RR /\ 0 < W ) ) -> ( ( A + V ) <_ ( 2 x. V ) <-> ( W x. ( A + V ) ) <_ ( W x. ( 2 x. V ) ) ) )
63	58 59 60 61 62	syl112anc	|- ( ph -> ( ( A + V ) <_ ( 2 x. V ) <-> ( W x. ( A + V ) ) <_ ( W x. ( 2 x. V ) ) ) )
64	57 63	mpbid	|- ( ph -> ( W x. ( A + V ) ) <_ ( W x. ( 2 x. V ) ) )
65	15 18 23 50 64	letrd	|- ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) <_ ( W x. ( 2 x. V ) ) )
66		nnuz	|- NN = ( ZZ>= ` 1 )
67	14 66	eleqtrdi	|- ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. ( ZZ>= ` 1 ) )
68	22	nnzd	|- ( ph -> ( W x. ( 2 x. V ) ) e. ZZ )
69		elfz5	|- ( ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. ( ZZ>= ` 1 ) /\ ( W x. ( 2 x. V ) ) e. ZZ ) -> ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) <-> ( B + ( W x. ( ( A - 1 ) + V ) ) ) <_ ( W x. ( 2 x. V ) ) ) )
70	67 68 69	syl2anc	|- ( ph -> ( ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) <-> ( B + ( W x. ( ( A - 1 ) + V ) ) ) <_ ( W x. ( 2 x. V ) ) ) )
71	65 70	mpbird	|- ( ph -> ( B + ( W x. ( ( A - 1 ) + V ) ) ) e. ( 1 ... ( W x. ( 2 x. V ) ) ) )