vdwlem3

	Ref	Expression
Hypotheses	vdwlem3.v	$⊢ φ \to V \in ℕ$
	vdwlem3.w	$⊢ φ \to W \in ℕ$
	vdwlem3.a	$⊢ φ \to A \in (1 \dots V)$
	vdwlem3.b	$⊢ φ \to B \in (1 \dots W)$
Assertion	vdwlem3	$⊢ φ \to B + W (A - 1 + V) \in (1 \dots W 2 V)$

Proof

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

Metamath Proof Explorer

Theorem vdwlem3

Proof