Metamath Proof Explorer

Theorem vdwlem3

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

Ref Expression
Hypotheses vdwlem3.v ⊢ ( 𝜑 → 𝑉 ∈ ℕ )
vdwlem3.w ⊢ ( 𝜑 → 𝑊 ∈ ℕ )
vdwlem3.a ⊢ ( 𝜑 → 𝐴 ∈ ( 1 ... 𝑉 ) )
vdwlem3.b ⊢ ( 𝜑 → 𝐵 ∈ ( 1 ... 𝑊 ) )
Assertion vdwlem3 ( 𝜑 → ( 𝐵 + ( 𝑊 · ( ( 𝐴 − 1 ) + 𝑉 ) ) ) ∈ ( 1 ... ( 𝑊 · ( 2 · 𝑉 ) ) ) )

Proof

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