Proof of Theorem vdwlem3
| Step | Hyp | Ref
| Expression |
| 1 | | vdwlem3.b |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ (1...𝑊)) |
| 2 | | elfznn 13593 |
. . . . . 6
⊢ (𝐵 ∈ (1...𝑊) → 𝐵 ∈ ℕ) |
| 3 | 1, 2 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℕ) |
| 4 | | vdwlem3.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ ℕ) |
| 5 | | vdwlem3.a |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (1...𝑉)) |
| 6 | | elfznn 13593 |
. . . . . . . . 9
⊢ (𝐴 ∈ (1...𝑉) → 𝐴 ∈ ℕ) |
| 7 | 5, 6 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℕ) |
| 8 | | nnm1nn0 12567 |
. . . . . . . 8
⊢ (𝐴 ∈ ℕ → (𝐴 − 1) ∈
ℕ0) |
| 9 | 7, 8 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝐴 − 1) ∈
ℕ0) |
| 10 | | vdwlem3.v |
. . . . . . 7
⊢ (𝜑 → 𝑉 ∈ ℕ) |
| 11 | | nn0nnaddcl 12557 |
. . . . . . 7
⊢ (((𝐴 − 1) ∈
ℕ0 ∧ 𝑉
∈ ℕ) → ((𝐴
− 1) + 𝑉) ∈
ℕ) |
| 12 | 9, 10, 11 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℕ) |
| 13 | 4, 12 | nnmulcld 12319 |
. . . . 5
⊢ (𝜑 → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ) |
| 14 | 3, 13 | nnaddcld 12318 |
. . . 4
⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℕ) |
| 15 | 14 | nnred 12281 |
. . 3
⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ ℝ) |
| 16 | 7, 10 | nnaddcld 12318 |
. . . . 5
⊢ (𝜑 → (𝐴 + 𝑉) ∈ ℕ) |
| 17 | 4, 16 | nnmulcld 12319 |
. . . 4
⊢ (𝜑 → (𝑊 · (𝐴 + 𝑉)) ∈ ℕ) |
| 18 | 17 | nnred 12281 |
. . 3
⊢ (𝜑 → (𝑊 · (𝐴 + 𝑉)) ∈ ℝ) |
| 19 | | 2nn 12339 |
. . . . . 6
⊢ 2 ∈
ℕ |
| 20 | | nnmulcl 12290 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ 𝑉
∈ ℕ) → (2 · 𝑉) ∈ ℕ) |
| 21 | 19, 10, 20 | sylancr 587 |
. . . . 5
⊢ (𝜑 → (2 · 𝑉) ∈
ℕ) |
| 22 | 4, 21 | nnmulcld 12319 |
. . . 4
⊢ (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℕ) |
| 23 | 22 | nnred 12281 |
. . 3
⊢ (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℝ) |
| 24 | | elfzle2 13568 |
. . . . . 6
⊢ (𝐵 ∈ (1...𝑊) → 𝐵 ≤ 𝑊) |
| 25 | 1, 24 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 ≤ 𝑊) |
| 26 | | nnre 12273 |
. . . . . . 7
⊢ (𝐵 ∈ ℕ → 𝐵 ∈
ℝ) |
| 27 | | nnre 12273 |
. . . . . . 7
⊢ (𝑊 ∈ ℕ → 𝑊 ∈
ℝ) |
| 28 | | nnre 12273 |
. . . . . . 7
⊢ ((𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ → (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℝ) |
| 29 | | leadd1 11731 |
. . . . . . 7
⊢ ((𝐵 ∈ ℝ ∧ 𝑊 ∈ ℝ ∧ (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℝ) → (𝐵 ≤ 𝑊 ↔ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ≤ (𝑊 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
| 30 | 26, 27, 28, 29 | syl3an 1161 |
. . . . . 6
⊢ ((𝐵 ∈ ℕ ∧ 𝑊 ∈ ℕ ∧ (𝑊 · ((𝐴 − 1) + 𝑉)) ∈ ℕ) → (𝐵 ≤ 𝑊 ↔ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ≤ (𝑊 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
| 31 | 3, 4, 13, 30 | syl3anc 1373 |
. . . . 5
⊢ (𝜑 → (𝐵 ≤ 𝑊 ↔ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ≤ (𝑊 + (𝑊 · ((𝐴 − 1) + 𝑉))))) |
| 32 | 25, 31 | mpbid 232 |
. . . 4
⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ≤ (𝑊 + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
| 33 | 4 | nncnd 12282 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ ℂ) |
| 34 | | 1cnd 11256 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℂ) |
| 35 | 12 | nncnd 12282 |
. . . . . 6
⊢ (𝜑 → ((𝐴 − 1) + 𝑉) ∈ ℂ) |
| 36 | 33, 34, 35 | adddid 11285 |
. . . . 5
⊢ (𝜑 → (𝑊 · (1 + ((𝐴 − 1) + 𝑉))) = ((𝑊 · 1) + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
| 37 | 9 | nn0cnd 12589 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 − 1) ∈ ℂ) |
| 38 | 10 | nncnd 12282 |
. . . . . . . 8
⊢ (𝜑 → 𝑉 ∈ ℂ) |
| 39 | 34, 37, 38 | addassd 11283 |
. . . . . . 7
⊢ (𝜑 → ((1 + (𝐴 − 1)) + 𝑉) = (1 + ((𝐴 − 1) + 𝑉))) |
| 40 | | ax-1cn 11213 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
| 41 | 7 | nncnd 12282 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 42 | | pncan3 11516 |
. . . . . . . . 9
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 + (𝐴 − 1)) = 𝐴) |
| 43 | 40, 41, 42 | sylancr 587 |
. . . . . . . 8
⊢ (𝜑 → (1 + (𝐴 − 1)) = 𝐴) |
| 44 | 43 | oveq1d 7446 |
. . . . . . 7
⊢ (𝜑 → ((1 + (𝐴 − 1)) + 𝑉) = (𝐴 + 𝑉)) |
| 45 | 39, 44 | eqtr3d 2779 |
. . . . . 6
⊢ (𝜑 → (1 + ((𝐴 − 1) + 𝑉)) = (𝐴 + 𝑉)) |
| 46 | 45 | oveq2d 7447 |
. . . . 5
⊢ (𝜑 → (𝑊 · (1 + ((𝐴 − 1) + 𝑉))) = (𝑊 · (𝐴 + 𝑉))) |
| 47 | 33 | mulridd 11278 |
. . . . . 6
⊢ (𝜑 → (𝑊 · 1) = 𝑊) |
| 48 | 47 | oveq1d 7446 |
. . . . 5
⊢ (𝜑 → ((𝑊 · 1) + (𝑊 · ((𝐴 − 1) + 𝑉))) = (𝑊 + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
| 49 | 36, 46, 48 | 3eqtr3d 2785 |
. . . 4
⊢ (𝜑 → (𝑊 · (𝐴 + 𝑉)) = (𝑊 + (𝑊 · ((𝐴 − 1) + 𝑉)))) |
| 50 | 32, 49 | breqtrrd 5171 |
. . 3
⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ≤ (𝑊 · (𝐴 + 𝑉))) |
| 51 | 7 | nnred 12281 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 52 | 10 | nnred 12281 |
. . . . . 6
⊢ (𝜑 → 𝑉 ∈ ℝ) |
| 53 | | elfzle2 13568 |
. . . . . . 7
⊢ (𝐴 ∈ (1...𝑉) → 𝐴 ≤ 𝑉) |
| 54 | 5, 53 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝑉) |
| 55 | 51, 52, 52, 54 | leadd1dd 11877 |
. . . . 5
⊢ (𝜑 → (𝐴 + 𝑉) ≤ (𝑉 + 𝑉)) |
| 56 | 38 | 2timesd 12509 |
. . . . 5
⊢ (𝜑 → (2 · 𝑉) = (𝑉 + 𝑉)) |
| 57 | 55, 56 | breqtrrd 5171 |
. . . 4
⊢ (𝜑 → (𝐴 + 𝑉) ≤ (2 · 𝑉)) |
| 58 | 16 | nnred 12281 |
. . . . 5
⊢ (𝜑 → (𝐴 + 𝑉) ∈ ℝ) |
| 59 | 21 | nnred 12281 |
. . . . 5
⊢ (𝜑 → (2 · 𝑉) ∈
ℝ) |
| 60 | 4 | nnred 12281 |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ ℝ) |
| 61 | 4 | nngt0d 12315 |
. . . . 5
⊢ (𝜑 → 0 < 𝑊) |
| 62 | | lemul2 12120 |
. . . . 5
⊢ (((𝐴 + 𝑉) ∈ ℝ ∧ (2 · 𝑉) ∈ ℝ ∧ (𝑊 ∈ ℝ ∧ 0 <
𝑊)) → ((𝐴 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝐴 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))) |
| 63 | 58, 59, 60, 61, 62 | syl112anc 1376 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝐴 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))) |
| 64 | 57, 63 | mpbid 232 |
. . 3
⊢ (𝜑 → (𝑊 · (𝐴 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))) |
| 65 | 15, 18, 23, 50, 64 | letrd 11418 |
. 2
⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ≤ (𝑊 · (2 · 𝑉))) |
| 66 | | nnuz 12921 |
. . . 4
⊢ ℕ =
(ℤ≥‘1) |
| 67 | 14, 66 | eleqtrdi 2851 |
. . 3
⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈
(ℤ≥‘1)) |
| 68 | 22 | nnzd 12640 |
. . 3
⊢ (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℤ) |
| 69 | | elfz5 13556 |
. . 3
⊢ (((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ (ℤ≥‘1)
∧ (𝑊 · (2
· 𝑉)) ∈
ℤ) → ((𝐵 +
(𝑊 · ((𝐴 − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ≤ (𝑊 · (2 · 𝑉)))) |
| 70 | 67, 68, 69 | syl2anc 584 |
. 2
⊢ (𝜑 → ((𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉))) ↔ (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ≤ (𝑊 · (2 · 𝑉)))) |
| 71 | 65, 70 | mpbird 257 |
1
⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 − 1) + 𝑉))) ∈ (1...(𝑊 · (2 · 𝑉)))) |