Proof of Theorem vdwlem5
Step | Hyp | Ref
| Expression |
1 | | vdwlem6.t |
. 2
⊢ 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) |
2 | | vdwlem6.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℕ) |
3 | | vdwlem3.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ ℕ) |
4 | 3 | nnnn0d 11228 |
. . . 4
⊢ (𝜑 → 𝑊 ∈
ℕ0) |
5 | | vdwlem7.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℕ) |
6 | | vdwlem3.v |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ ℕ) |
7 | 6 | nncnd 10913 |
. . . . . . . . 9
⊢ (𝜑 → 𝑉 ∈ ℂ) |
8 | | vdwlem7.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℕ) |
9 | 8 | nncnd 10913 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℂ) |
10 | 7, 9 | subcld 10271 |
. . . . . . . 8
⊢ (𝜑 → (𝑉 − 𝐷) ∈ ℂ) |
11 | 5 | nncnd 10913 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
12 | 10, 11 | npcand 10275 |
. . . . . . 7
⊢ (𝜑 → (((𝑉 − 𝐷) − 𝐴) + 𝐴) = (𝑉 − 𝐷)) |
13 | 7, 9, 11 | subsub4d 10302 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝑉 − 𝐷) − 𝐴) = (𝑉 − (𝐷 + 𝐴))) |
14 | 9, 11 | addcomd 10117 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷 + 𝐴) = (𝐴 + 𝐷)) |
15 | 14 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑉 − (𝐷 + 𝐴)) = (𝑉 − (𝐴 + 𝐷))) |
16 | 13, 15 | eqtrd 2644 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑉 − 𝐷) − 𝐴) = (𝑉 − (𝐴 + 𝐷))) |
17 | | cnvimass 5404 |
. . . . . . . . . . . . 13
⊢ (◡𝐹 “ {𝐺}) ⊆ dom 𝐹 |
18 | | vdwlem4.r |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑅 ∈ Fin) |
19 | | vdwlem4.h |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) |
20 | | vdwlem4.f |
. . . . . . . . . . . . . . 15
⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))))) |
21 | 6, 3, 18, 19, 20 | vdwlem4 15526 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑𝑚 (1...𝑊))) |
22 | | fdm 5964 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(1...𝑉)⟶(𝑅 ↑𝑚 (1...𝑊)) → dom 𝐹 = (1...𝑉)) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → dom 𝐹 = (1...𝑉)) |
24 | 17, 23 | syl5sseq 3616 |
. . . . . . . . . . . 12
⊢ (𝜑 → (◡𝐹 “ {𝐺}) ⊆ (1...𝑉)) |
25 | | vdwlem7.s |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐺})) |
26 | | ssun2 3739 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷) ⊆ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)) |
27 | | vdwlem7.k |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘2)) |
28 | | uz2m1nn 11639 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈
(ℤ≥‘2) → (𝐾 − 1) ∈ ℕ) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾 − 1) ∈ ℕ) |
30 | 5, 8 | nnaddcld 10944 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 + 𝐷) ∈ ℕ) |
31 | | vdwapid1 15517 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 − 1) ∈ ℕ ∧
(𝐴 + 𝐷) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + 𝐷) ∈ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)) |
32 | 29, 30, 8, 31 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 + 𝐷) ∈ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)) |
33 | 26, 32 | sseldi 3566 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 + 𝐷) ∈ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))) |
34 | | eluz2nn 11602 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐾 ∈
(ℤ≥‘2) → 𝐾 ∈ ℕ) |
35 | 27, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ∈ ℕ) |
36 | 35 | nncnd 10913 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐾 ∈ ℂ) |
37 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
38 | | npcan 10169 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 −
1) + 1) = 𝐾) |
39 | 36, 37, 38 | sylancl 693 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾) |
40 | 39 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (AP‘((𝐾 − 1) + 1)) =
(AP‘𝐾)) |
41 | 40 | oveqd 6566 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = (𝐴(AP‘𝐾)𝐷)) |
42 | | nnm1nn0 11211 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈
ℕ0) |
43 | 35, 42 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐾 − 1) ∈
ℕ0) |
44 | | vdwapun 15516 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐾 − 1) ∈
ℕ0 ∧ 𝐴
∈ ℕ ∧ 𝐷
∈ ℕ) → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))) |
45 | 43, 5, 8, 44 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))) |
46 | 41, 45 | eqtr3d 2646 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))) |
47 | 33, 46 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 + 𝐷) ∈ (𝐴(AP‘𝐾)𝐷)) |
48 | 25, 47 | sseldd 3569 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 + 𝐷) ∈ (◡𝐹 “ {𝐺})) |
49 | 24, 48 | sseldd 3569 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 + 𝐷) ∈ (1...𝑉)) |
50 | | elfzuz3 12210 |
. . . . . . . . . . 11
⊢ ((𝐴 + 𝐷) ∈ (1...𝑉) → 𝑉 ∈ (ℤ≥‘(𝐴 + 𝐷))) |
51 | 49, 50 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑉 ∈ (ℤ≥‘(𝐴 + 𝐷))) |
52 | | uznn0sub 11595 |
. . . . . . . . . 10
⊢ (𝑉 ∈
(ℤ≥‘(𝐴 + 𝐷)) → (𝑉 − (𝐴 + 𝐷)) ∈
ℕ0) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (𝑉 − (𝐴 + 𝐷)) ∈
ℕ0) |
54 | 16, 53 | eqeltrd 2688 |
. . . . . . . 8
⊢ (𝜑 → ((𝑉 − 𝐷) − 𝐴) ∈
ℕ0) |
55 | | nn0nnaddcl 11201 |
. . . . . . . 8
⊢ ((((𝑉 − 𝐷) − 𝐴) ∈ ℕ0 ∧ 𝐴 ∈ ℕ) → (((𝑉 − 𝐷) − 𝐴) + 𝐴) ∈ ℕ) |
56 | 54, 5, 55 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (((𝑉 − 𝐷) − 𝐴) + 𝐴) ∈ ℕ) |
57 | 12, 56 | eqeltrrd 2689 |
. . . . . 6
⊢ (𝜑 → (𝑉 − 𝐷) ∈ ℕ) |
58 | 5, 57 | nnaddcld 10944 |
. . . . 5
⊢ (𝜑 → (𝐴 + (𝑉 − 𝐷)) ∈ ℕ) |
59 | | nnm1nn0 11211 |
. . . . 5
⊢ ((𝐴 + (𝑉 − 𝐷)) ∈ ℕ → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈
ℕ0) |
60 | 58, 59 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈
ℕ0) |
61 | 4, 60 | nn0mulcld 11233 |
. . 3
⊢ (𝜑 → (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) ∈
ℕ0) |
62 | | nnnn0addcl 11200 |
. . 3
⊢ ((𝐵 ∈ ℕ ∧ (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) ∈ ℕ0)
→ (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) ∈
ℕ) |
63 | 2, 61, 62 | syl2anc 691 |
. 2
⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) ∈
ℕ) |
64 | 1, 63 | syl5eqel 2692 |
1
⊢ (𝜑 → 𝑇 ∈ ℕ) |