Step | Hyp | Ref
| Expression |
1 | | vdwlem8.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℕ) |
2 | 1 | nncnd 10913 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | | vdwlem8.d |
. . . . . . . . . 10
⊢ (𝜑 → 𝐷 ∈ ℕ) |
4 | 3 | nncnd 10913 |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℂ) |
5 | 2, 4 | addcomd 10117 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 + 𝐷) = (𝐷 + 𝐴)) |
6 | 5 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (𝑊 − (𝐴 + 𝐷)) = (𝑊 − (𝐷 + 𝐴))) |
7 | | vdwlem8.w |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ∈ ℕ) |
8 | 7 | nncnd 10913 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ ℂ) |
9 | 8, 4, 2 | subsub4d 10302 |
. . . . . . 7
⊢ (𝜑 → ((𝑊 − 𝐷) − 𝐴) = (𝑊 − (𝐷 + 𝐴))) |
10 | 6, 9 | eqtr4d 2647 |
. . . . . 6
⊢ (𝜑 → (𝑊 − (𝐴 + 𝐷)) = ((𝑊 − 𝐷) − 𝐴)) |
11 | 10 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐴) + (𝑊 − (𝐴 + 𝐷))) = ((𝐴 + 𝐴) + ((𝑊 − 𝐷) − 𝐴))) |
12 | 8, 4 | subcld 10271 |
. . . . . 6
⊢ (𝜑 → (𝑊 − 𝐷) ∈ ℂ) |
13 | 2, 2, 12 | ppncand 10311 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝐴) + ((𝑊 − 𝐷) − 𝐴)) = (𝐴 + (𝑊 − 𝐷))) |
14 | 11, 13 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝐴) + (𝑊 − (𝐴 + 𝐷))) = (𝐴 + (𝑊 − 𝐷))) |
15 | 1, 1 | nnaddcld 10944 |
. . . . 5
⊢ (𝜑 → (𝐴 + 𝐴) ∈ ℕ) |
16 | | vdwlem8.s |
. . . . . . . 8
⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐺 “ {𝐶})) |
17 | | cnvimass 5404 |
. . . . . . . . 9
⊢ (◡𝐺 “ {𝐶}) ⊆ dom 𝐺 |
18 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐹‘(𝑥 + 𝑊)) ∈ V |
19 | | vdwlem8.g |
. . . . . . . . . 10
⊢ 𝐺 = (𝑥 ∈ (1...𝑊) ↦ (𝐹‘(𝑥 + 𝑊))) |
20 | 18, 19 | dmmpti 5936 |
. . . . . . . . 9
⊢ dom 𝐺 = (1...𝑊) |
21 | 17, 20 | sseqtri 3600 |
. . . . . . . 8
⊢ (◡𝐺 “ {𝐶}) ⊆ (1...𝑊) |
22 | 16, 21 | syl6ss 3580 |
. . . . . . 7
⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (1...𝑊)) |
23 | | ssun2 3739 |
. . . . . . . . 9
⊢ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷) ⊆ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)) |
24 | | vdwlem8.k |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘2)) |
25 | | uz2m1nn 11639 |
. . . . . . . . . . 11
⊢ (𝐾 ∈
(ℤ≥‘2) → (𝐾 − 1) ∈ ℕ) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 − 1) ∈ ℕ) |
27 | 1, 3 | nnaddcld 10944 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 + 𝐷) ∈ ℕ) |
28 | | vdwapid1 15517 |
. . . . . . . . . 10
⊢ (((𝐾 − 1) ∈ ℕ ∧
(𝐴 + 𝐷) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + 𝐷) ∈ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)) |
29 | 26, 27, 3, 28 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 + 𝐷) ∈ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)) |
30 | 23, 29 | sseldi 3566 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 + 𝐷) ∈ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))) |
31 | | eluz2nn 11602 |
. . . . . . . . . . . . . 14
⊢ (𝐾 ∈
(ℤ≥‘2) → 𝐾 ∈ ℕ) |
32 | 24, 31 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ ℕ) |
33 | 32 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐾 ∈ ℂ) |
34 | | ax-1cn 9873 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℂ |
35 | | npcan 10169 |
. . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℂ ∧ 1 ∈
ℂ) → ((𝐾 −
1) + 1) = 𝐾) |
36 | 33, 34, 35 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾) |
37 | 36 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝜑 → (AP‘((𝐾 − 1) + 1)) =
(AP‘𝐾)) |
38 | 37 | oveqd 6566 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = (𝐴(AP‘𝐾)𝐷)) |
39 | 26 | nnnn0d 11228 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐾 − 1) ∈
ℕ0) |
40 | | vdwapun 15516 |
. . . . . . . . . 10
⊢ (((𝐾 − 1) ∈
ℕ0 ∧ 𝐴
∈ ℕ ∧ 𝐷
∈ ℕ) → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))) |
41 | 39, 1, 3, 40 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))) |
42 | 38, 41 | eqtr3d 2646 |
. . . . . . . 8
⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))) |
43 | 30, 42 | eleqtrrd 2691 |
. . . . . . 7
⊢ (𝜑 → (𝐴 + 𝐷) ∈ (𝐴(AP‘𝐾)𝐷)) |
44 | 22, 43 | sseldd 3569 |
. . . . . 6
⊢ (𝜑 → (𝐴 + 𝐷) ∈ (1...𝑊)) |
45 | | elfzuz3 12210 |
. . . . . 6
⊢ ((𝐴 + 𝐷) ∈ (1...𝑊) → 𝑊 ∈ (ℤ≥‘(𝐴 + 𝐷))) |
46 | | uznn0sub 11595 |
. . . . . 6
⊢ (𝑊 ∈
(ℤ≥‘(𝐴 + 𝐷)) → (𝑊 − (𝐴 + 𝐷)) ∈
ℕ0) |
47 | 44, 45, 46 | 3syl 18 |
. . . . 5
⊢ (𝜑 → (𝑊 − (𝐴 + 𝐷)) ∈
ℕ0) |
48 | | nnnn0addcl 11200 |
. . . . 5
⊢ (((𝐴 + 𝐴) ∈ ℕ ∧ (𝑊 − (𝐴 + 𝐷)) ∈ ℕ0) →
((𝐴 + 𝐴) + (𝑊 − (𝐴 + 𝐷))) ∈ ℕ) |
49 | 15, 47, 48 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((𝐴 + 𝐴) + (𝑊 − (𝐴 + 𝐷))) ∈ ℕ) |
50 | 14, 49 | eqeltrrd 2689 |
. . 3
⊢ (𝜑 → (𝐴 + (𝑊 − 𝐷)) ∈ ℕ) |
51 | | 1nn 10908 |
. . . . . . . 8
⊢ 1 ∈
ℕ |
52 | | f1osng 6089 |
. . . . . . . 8
⊢ ((1
∈ ℕ ∧ 𝐷
∈ ℕ) → {〈1, 𝐷〉}:{1}–1-1-onto→{𝐷}) |
53 | 51, 3, 52 | sylancr 694 |
. . . . . . 7
⊢ (𝜑 → {〈1, 𝐷〉}:{1}–1-1-onto→{𝐷}) |
54 | | f1of 6050 |
. . . . . . 7
⊢
({〈1, 𝐷〉}:{1}–1-1-onto→{𝐷} → {〈1, 𝐷〉}:{1}⟶{𝐷}) |
55 | 53, 54 | syl 17 |
. . . . . 6
⊢ (𝜑 → {〈1, 𝐷〉}:{1}⟶{𝐷}) |
56 | 3 | snssd 4281 |
. . . . . 6
⊢ (𝜑 → {𝐷} ⊆ ℕ) |
57 | 55, 56 | fssd 5970 |
. . . . 5
⊢ (𝜑 → {〈1, 𝐷〉}:{1}⟶ℕ) |
58 | | 1z 11284 |
. . . . . . 7
⊢ 1 ∈
ℤ |
59 | | fzsn 12254 |
. . . . . . 7
⊢ (1 ∈
ℤ → (1...1) = {1}) |
60 | 58, 59 | ax-mp 5 |
. . . . . 6
⊢ (1...1) =
{1} |
61 | 60 | feq2i 5950 |
. . . . 5
⊢
({〈1, 𝐷〉}:(1...1)⟶ℕ ↔
{〈1, 𝐷〉}:{1}⟶ℕ) |
62 | 57, 61 | sylibr 223 |
. . . 4
⊢ (𝜑 → {〈1, 𝐷〉}:(1...1)⟶ℕ) |
63 | | nnex 10903 |
. . . . 5
⊢ ℕ
∈ V |
64 | | ovex 6577 |
. . . . 5
⊢ (1...1)
∈ V |
65 | 63, 64 | elmap 7772 |
. . . 4
⊢
({〈1, 𝐷〉}
∈ (ℕ ↑𝑚 (1...1)) ↔ {〈1, 𝐷〉}:(1...1)⟶ℕ) |
66 | 62, 65 | sylibr 223 |
. . 3
⊢ (𝜑 → {〈1, 𝐷〉} ∈ (ℕ
↑𝑚 (1...1))) |
67 | 1, 7 | nnaddcld 10944 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 + 𝑊) ∈ ℕ) |
68 | 67 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + 𝑊) ∈ ℕ) |
69 | | elfznn0 12302 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (0...(𝐾 − 1)) → 𝑚 ∈ ℕ0) |
70 | 3 | nnnn0d 11228 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
71 | | nn0mulcl 11206 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℕ0
∧ 𝐷 ∈
ℕ0) → (𝑚 · 𝐷) ∈
ℕ0) |
72 | 69, 70, 71 | syl2anr 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈
ℕ0) |
73 | | nnnn0addcl 11200 |
. . . . . . . . . . . . 13
⊢ (((𝐴 + 𝑊) ∈ ℕ ∧ (𝑚 · 𝐷) ∈ ℕ0) → ((𝐴 + 𝑊) + (𝑚 · 𝐷)) ∈ ℕ) |
74 | 68, 72, 73 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + 𝑊) + (𝑚 · 𝐷)) ∈ ℕ) |
75 | | nnuz 11599 |
. . . . . . . . . . . 12
⊢ ℕ =
(ℤ≥‘1) |
76 | 74, 75 | syl6eleq 2698 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + 𝑊) + (𝑚 · 𝐷)) ∈
(ℤ≥‘1)) |
77 | 16 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐺 “ {𝐶})) |
78 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)) |
79 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑚 → (𝑛 · 𝐷) = (𝑚 · 𝐷)) |
80 | 79 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑚 → (𝐴 + (𝑛 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) |
81 | 80 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → ((𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)) ↔ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷)))) |
82 | 81 | rspcev 3282 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑚 ∈ (0...(𝐾 − 1)) ∧ (𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑚 · 𝐷))) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) |
83 | 78, 82 | mpan2 703 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ (0...(𝐾 − 1)) → ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) |
84 | 32 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
85 | | vdwapval 15515 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐾 ∈ ℕ0
∧ 𝐴 ∈ ℕ
∧ 𝐷 ∈ ℕ)
→ ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))) |
86 | 84, 1, 3, 85 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷) ↔ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷)))) |
87 | 86 | biimpar 501 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ∃𝑛 ∈ (0...(𝐾 − 1))(𝐴 + (𝑚 · 𝐷)) = (𝐴 + (𝑛 · 𝐷))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷)) |
88 | 83, 87 | sylan2 490 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (𝐴(AP‘𝐾)𝐷)) |
89 | 77, 88 | sseldd 3569 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (◡𝐺 “ {𝐶})) |
90 | 18, 19 | fnmpti 5935 |
. . . . . . . . . . . . . . . 16
⊢ 𝐺 Fn (1...𝑊) |
91 | | fniniseg 6246 |
. . . . . . . . . . . . . . . 16
⊢ (𝐺 Fn (1...𝑊) → ((𝐴 + (𝑚 · 𝐷)) ∈ (◡𝐺 “ {𝐶}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑊) ∧ (𝐺‘(𝐴 + (𝑚 · 𝐷))) = 𝐶))) |
92 | 90, 91 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 + (𝑚 · 𝐷)) ∈ (◡𝐺 “ {𝐶}) ↔ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑊) ∧ (𝐺‘(𝐴 + (𝑚 · 𝐷))) = 𝐶)) |
93 | 89, 92 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑊) ∧ (𝐺‘(𝐴 + (𝑚 · 𝐷))) = 𝐶)) |
94 | 93 | simpld 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑊)) |
95 | | elfzuz3 12210 |
. . . . . . . . . . . . 13
⊢ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑊) → 𝑊 ∈ (ℤ≥‘(𝐴 + (𝑚 · 𝐷)))) |
96 | | eluzelz 11573 |
. . . . . . . . . . . . . 14
⊢ (𝑊 ∈
(ℤ≥‘(𝐴 + (𝑚 · 𝐷))) → 𝑊 ∈ ℤ) |
97 | | eluzadd 11592 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈
(ℤ≥‘(𝐴 + (𝑚 · 𝐷))) ∧ 𝑊 ∈ ℤ) → (𝑊 + 𝑊) ∈
(ℤ≥‘((𝐴 + (𝑚 · 𝐷)) + 𝑊))) |
98 | 96, 97 | mpdan 699 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈
(ℤ≥‘(𝐴 + (𝑚 · 𝐷))) → (𝑊 + 𝑊) ∈
(ℤ≥‘((𝐴 + (𝑚 · 𝐷)) + 𝑊))) |
99 | 94, 95, 98 | 3syl 18 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑊 + 𝑊) ∈
(ℤ≥‘((𝐴 + (𝑚 · 𝐷)) + 𝑊))) |
100 | 8 | 2timesd 11152 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (2 · 𝑊) = (𝑊 + 𝑊)) |
101 | 100 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (2 · 𝑊) = (𝑊 + 𝑊)) |
102 | 2 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝐴 ∈ ℂ) |
103 | 8 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → 𝑊 ∈ ℂ) |
104 | 72 | nn0cnd 11230 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑚 · 𝐷) ∈ ℂ) |
105 | 102, 103,
104 | add32d 10142 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + 𝑊) + (𝑚 · 𝐷)) = ((𝐴 + (𝑚 · 𝐷)) + 𝑊)) |
106 | 105 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) →
(ℤ≥‘((𝐴 + 𝑊) + (𝑚 · 𝐷))) = (ℤ≥‘((𝐴 + (𝑚 · 𝐷)) + 𝑊))) |
107 | 99, 101, 106 | 3eltr4d 2703 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (2 · 𝑊) ∈
(ℤ≥‘((𝐴 + 𝑊) + (𝑚 · 𝐷)))) |
108 | | elfzuzb 12207 |
. . . . . . . . . . 11
⊢ (((𝐴 + 𝑊) + (𝑚 · 𝐷)) ∈ (1...(2 · 𝑊)) ↔ (((𝐴 + 𝑊) + (𝑚 · 𝐷)) ∈ (ℤ≥‘1)
∧ (2 · 𝑊) ∈
(ℤ≥‘((𝐴 + 𝑊) + (𝑚 · 𝐷))))) |
109 | 76, 107, 108 | sylanbrc 695 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → ((𝐴 + 𝑊) + (𝑚 · 𝐷)) ∈ (1...(2 · 𝑊))) |
110 | 105 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘((𝐴 + 𝑊) + (𝑚 · 𝐷))) = (𝐹‘((𝐴 + (𝑚 · 𝐷)) + 𝑊))) |
111 | | oveq1 6556 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝑥 + 𝑊) = ((𝐴 + (𝑚 · 𝐷)) + 𝑊)) |
112 | 111 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (𝐴 + (𝑚 · 𝐷)) → (𝐹‘(𝑥 + 𝑊)) = (𝐹‘((𝐴 + (𝑚 · 𝐷)) + 𝑊))) |
113 | | fvex 6113 |
. . . . . . . . . . . . 13
⊢ (𝐹‘((𝐴 + (𝑚 · 𝐷)) + 𝑊)) ∈ V |
114 | 112, 19, 113 | fvmpt 6191 |
. . . . . . . . . . . 12
⊢ ((𝐴 + (𝑚 · 𝐷)) ∈ (1...𝑊) → (𝐺‘(𝐴 + (𝑚 · 𝐷))) = (𝐹‘((𝐴 + (𝑚 · 𝐷)) + 𝑊))) |
115 | 94, 114 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐴 + (𝑚 · 𝐷))) = (𝐹‘((𝐴 + (𝑚 · 𝐷)) + 𝑊))) |
116 | 93 | simprd 478 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐺‘(𝐴 + (𝑚 · 𝐷))) = 𝐶) |
117 | 110, 115,
116 | 3eqtr2d 2650 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝐹‘((𝐴 + 𝑊) + (𝑚 · 𝐷))) = 𝐶) |
118 | 109, 117 | jca 553 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (((𝐴 + 𝑊) + (𝑚 · 𝐷)) ∈ (1...(2 · 𝑊)) ∧ (𝐹‘((𝐴 + 𝑊) + (𝑚 · 𝐷))) = 𝐶)) |
119 | | eleq1 2676 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝐴 + 𝑊) + (𝑚 · 𝐷)) → (𝑥 ∈ (1...(2 · 𝑊)) ↔ ((𝐴 + 𝑊) + (𝑚 · 𝐷)) ∈ (1...(2 · 𝑊)))) |
120 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑥 = ((𝐴 + 𝑊) + (𝑚 · 𝐷)) → (𝐹‘𝑥) = (𝐹‘((𝐴 + 𝑊) + (𝑚 · 𝐷)))) |
121 | 120 | eqeq1d 2612 |
. . . . . . . . . 10
⊢ (𝑥 = ((𝐴 + 𝑊) + (𝑚 · 𝐷)) → ((𝐹‘𝑥) = 𝐶 ↔ (𝐹‘((𝐴 + 𝑊) + (𝑚 · 𝐷))) = 𝐶)) |
122 | 119, 121 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑥 = ((𝐴 + 𝑊) + (𝑚 · 𝐷)) → ((𝑥 ∈ (1...(2 · 𝑊)) ∧ (𝐹‘𝑥) = 𝐶) ↔ (((𝐴 + 𝑊) + (𝑚 · 𝐷)) ∈ (1...(2 · 𝑊)) ∧ (𝐹‘((𝐴 + 𝑊) + (𝑚 · 𝐷))) = 𝐶))) |
123 | 118, 122 | syl5ibrcom 236 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (0...(𝐾 − 1))) → (𝑥 = ((𝐴 + 𝑊) + (𝑚 · 𝐷)) → (𝑥 ∈ (1...(2 · 𝑊)) ∧ (𝐹‘𝑥) = 𝐶))) |
124 | 123 | rexlimdva 3013 |
. . . . . . 7
⊢ (𝜑 → (∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝑊) + (𝑚 · 𝐷)) → (𝑥 ∈ (1...(2 · 𝑊)) ∧ (𝐹‘𝑥) = 𝐶))) |
125 | | vdwapval 15515 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℕ0
∧ (𝐴 + 𝑊) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝑥 ∈ ((𝐴 + 𝑊)(AP‘𝐾)𝐷) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝑊) + (𝑚 · 𝐷)))) |
126 | 84, 67, 3, 125 | syl3anc 1318 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑊)(AP‘𝐾)𝐷) ↔ ∃𝑚 ∈ (0...(𝐾 − 1))𝑥 = ((𝐴 + 𝑊) + (𝑚 · 𝐷)))) |
127 | | vdwlem8.f |
. . . . . . . 8
⊢ (𝜑 → 𝐹:(1...(2 · 𝑊))⟶𝑅) |
128 | | ffn 5958 |
. . . . . . . 8
⊢ (𝐹:(1...(2 · 𝑊))⟶𝑅 → 𝐹 Fn (1...(2 · 𝑊))) |
129 | | fniniseg 6246 |
. . . . . . . 8
⊢ (𝐹 Fn (1...(2 · 𝑊)) → (𝑥 ∈ (◡𝐹 “ {𝐶}) ↔ (𝑥 ∈ (1...(2 · 𝑊)) ∧ (𝐹‘𝑥) = 𝐶))) |
130 | 127, 128,
129 | 3syl 18 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (◡𝐹 “ {𝐶}) ↔ (𝑥 ∈ (1...(2 · 𝑊)) ∧ (𝐹‘𝑥) = 𝐶))) |
131 | 124, 126,
130 | 3imtr4d 282 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ((𝐴 + 𝑊)(AP‘𝐾)𝐷) → 𝑥 ∈ (◡𝐹 “ {𝐶}))) |
132 | 131 | ssrdv 3574 |
. . . . 5
⊢ (𝜑 → ((𝐴 + 𝑊)(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐶})) |
133 | | fvsng 6352 |
. . . . . . . . 9
⊢ ((1
∈ ℕ ∧ 𝐷
∈ ℕ) → ({〈1, 𝐷〉}‘1) = 𝐷) |
134 | 51, 3, 133 | sylancr 694 |
. . . . . . . 8
⊢ (𝜑 → ({〈1, 𝐷〉}‘1) = 𝐷) |
135 | 134 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)) = ((𝐴 + (𝑊 − 𝐷)) + 𝐷)) |
136 | 2, 12, 4 | addassd 9941 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 + (𝑊 − 𝐷)) + 𝐷) = (𝐴 + ((𝑊 − 𝐷) + 𝐷))) |
137 | 8, 4 | npcand 10275 |
. . . . . . . 8
⊢ (𝜑 → ((𝑊 − 𝐷) + 𝐷) = 𝑊) |
138 | 137 | oveq2d 6565 |
. . . . . . 7
⊢ (𝜑 → (𝐴 + ((𝑊 − 𝐷) + 𝐷)) = (𝐴 + 𝑊)) |
139 | 135, 136,
138 | 3eqtrd 2648 |
. . . . . 6
⊢ (𝜑 → ((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)) = (𝐴 + 𝑊)) |
140 | 139, 134 | oveq12d 6567 |
. . . . 5
⊢ (𝜑 → (((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))(AP‘𝐾)({〈1, 𝐷〉}‘1)) = ((𝐴 + 𝑊)(AP‘𝐾)𝐷)) |
141 | 139 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))) = (𝐹‘(𝐴 + 𝑊))) |
142 | | vdwapid1 15517 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷)) |
143 | 32, 1, 3, 142 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ (𝐴(AP‘𝐾)𝐷)) |
144 | 16, 143 | sseldd 3569 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ (◡𝐺 “ {𝐶})) |
145 | | fniniseg 6246 |
. . . . . . . . . . . 12
⊢ (𝐺 Fn (1...𝑊) → (𝐴 ∈ (◡𝐺 “ {𝐶}) ↔ (𝐴 ∈ (1...𝑊) ∧ (𝐺‘𝐴) = 𝐶))) |
146 | 90, 145 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ (◡𝐺 “ {𝐶}) ↔ (𝐴 ∈ (1...𝑊) ∧ (𝐺‘𝐴) = 𝐶)) |
147 | 144, 146 | sylib 207 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 ∈ (1...𝑊) ∧ (𝐺‘𝐴) = 𝐶)) |
148 | 147 | simpld 474 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ (1...𝑊)) |
149 | | oveq1 6556 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝐴 → (𝑥 + 𝑊) = (𝐴 + 𝑊)) |
150 | 149 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑥 = 𝐴 → (𝐹‘(𝑥 + 𝑊)) = (𝐹‘(𝐴 + 𝑊))) |
151 | | fvex 6113 |
. . . . . . . . . 10
⊢ (𝐹‘(𝐴 + 𝑊)) ∈ V |
152 | 150, 19, 151 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝐴 ∈ (1...𝑊) → (𝐺‘𝐴) = (𝐹‘(𝐴 + 𝑊))) |
153 | 148, 152 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝐴) = (𝐹‘(𝐴 + 𝑊))) |
154 | 147 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → (𝐺‘𝐴) = 𝐶) |
155 | 141, 153,
154 | 3eqtr2d 2650 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))) = 𝐶) |
156 | 155 | sneqd 4137 |
. . . . . 6
⊢ (𝜑 → {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))} = {𝐶}) |
157 | 156 | imaeq2d 5385 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))}) = (◡𝐹 “ {𝐶})) |
158 | 132, 140,
157 | 3sstr4d 3611 |
. . . 4
⊢ (𝜑 → (((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))(AP‘𝐾)({〈1, 𝐷〉}‘1)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))})) |
159 | 158 | ralrimivw 2950 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ (1...1)(((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))(AP‘𝐾)({〈1, 𝐷〉}‘1)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))})) |
160 | 155 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝜑 → (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))) = (𝑖 ∈ (1...1) ↦ 𝐶)) |
161 | | fconstmpt 5085 |
. . . . . . . 8
⊢ ((1...1)
× {𝐶}) = (𝑖 ∈ (1...1) ↦ 𝐶) |
162 | 160, 161 | syl6eqr 2662 |
. . . . . . 7
⊢ (𝜑 → (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))) = ((1...1) ×
{𝐶})) |
163 | 162 | rneqd 5274 |
. . . . . 6
⊢ (𝜑 → ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))) = ran ((1...1) ×
{𝐶})) |
164 | | elfz3 12222 |
. . . . . . . 8
⊢ (1 ∈
ℤ → 1 ∈ (1...1)) |
165 | | ne0i 3880 |
. . . . . . . 8
⊢ (1 ∈
(1...1) → (1...1) ≠ ∅) |
166 | 58, 164, 165 | mp2b 10 |
. . . . . . 7
⊢ (1...1)
≠ ∅ |
167 | | rnxp 5483 |
. . . . . . 7
⊢ ((1...1)
≠ ∅ → ran ((1...1) × {𝐶}) = {𝐶}) |
168 | 166, 167 | ax-mp 5 |
. . . . . 6
⊢ ran
((1...1) × {𝐶}) =
{𝐶} |
169 | 163, 168 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 → ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))) = {𝐶}) |
170 | 169 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))))) = (#‘{𝐶})) |
171 | | vdwlem8.c |
. . . . 5
⊢ 𝐶 ∈ V |
172 | | hashsng 13020 |
. . . . 5
⊢ (𝐶 ∈ V → (#‘{𝐶}) = 1) |
173 | 171, 172 | ax-mp 5 |
. . . 4
⊢
(#‘{𝐶}) =
1 |
174 | 170, 173 | syl6eq 2660 |
. . 3
⊢ (𝜑 → (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))))) = 1) |
175 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → (𝑎 + (𝑑‘𝑖)) = ((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))) |
176 | 175 | oveq1d 6564 |
. . . . . . 7
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → ((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = (((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖))) |
177 | 175 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → (𝐹‘(𝑎 + (𝑑‘𝑖))) = (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))) |
178 | 177 | sneqd 4137 |
. . . . . . . 8
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → {(𝐹‘(𝑎 + (𝑑‘𝑖)))} = {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))}) |
179 | 178 | imaeq2d 5385 |
. . . . . . 7
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → (◡𝐹 “ {(𝐹‘(𝑎 + (𝑑‘𝑖)))}) = (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))})) |
180 | 176, 179 | sseq12d 3597 |
. . . . . 6
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → (((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝑎 + (𝑑‘𝑖)))}) ↔ (((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))}))) |
181 | 180 | ralbidv 2969 |
. . . . 5
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → (∀𝑖 ∈ (1...1)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝑎 + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...1)(((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))}))) |
182 | 177 | mpteq2dv 4673 |
. . . . . . . 8
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → (𝑖 ∈ (1...1) ↦ (𝐹‘(𝑎 + (𝑑‘𝑖)))) = (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))))) |
183 | 182 | rneqd 5274 |
. . . . . . 7
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → ran (𝑖 ∈ (1...1) ↦ (𝐹‘(𝑎 + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))))) |
184 | 183 | fveq2d 6107 |
. . . . . 6
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘(𝑎 + (𝑑‘𝑖))))) = (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))))) |
185 | 184 | eqeq1d 2612 |
. . . . 5
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → ((#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘(𝑎 + (𝑑‘𝑖))))) = 1 ↔ (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))))) = 1)) |
186 | 181, 185 | anbi12d 743 |
. . . 4
⊢ (𝑎 = (𝐴 + (𝑊 − 𝐷)) → ((∀𝑖 ∈ (1...1)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝑎 + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘(𝑎 + (𝑑‘𝑖))))) = 1) ↔ (∀𝑖 ∈ (1...1)(((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))))) = 1))) |
187 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑑 = {〈1, 𝐷〉} → (𝑑‘𝑖) = ({〈1, 𝐷〉}‘𝑖)) |
188 | | elfz1eq 12223 |
. . . . . . . . . . 11
⊢ (𝑖 ∈ (1...1) → 𝑖 = 1) |
189 | 188 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑖 ∈ (1...1) →
({〈1, 𝐷〉}‘𝑖) = ({〈1, 𝐷〉}‘1)) |
190 | 187, 189 | sylan9eq 2664 |
. . . . . . . . 9
⊢ ((𝑑 = {〈1, 𝐷〉} ∧ 𝑖 ∈ (1...1)) → (𝑑‘𝑖) = ({〈1, 𝐷〉}‘1)) |
191 | 190 | oveq2d 6565 |
. . . . . . . 8
⊢ ((𝑑 = {〈1, 𝐷〉} ∧ 𝑖 ∈ (1...1)) → ((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)) = ((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))) |
192 | 191, 190 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝑑 = {〈1, 𝐷〉} ∧ 𝑖 ∈ (1...1)) → (((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = (((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))(AP‘𝐾)({〈1, 𝐷〉}‘1))) |
193 | 191 | fveq2d 6107 |
. . . . . . . . 9
⊢ ((𝑑 = {〈1, 𝐷〉} ∧ 𝑖 ∈ (1...1)) → (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))) = (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))) |
194 | 193 | sneqd 4137 |
. . . . . . . 8
⊢ ((𝑑 = {〈1, 𝐷〉} ∧ 𝑖 ∈ (1...1)) → {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))} = {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))}) |
195 | 194 | imaeq2d 5385 |
. . . . . . 7
⊢ ((𝑑 = {〈1, 𝐷〉} ∧ 𝑖 ∈ (1...1)) → (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))}) = (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))})) |
196 | 192, 195 | sseq12d 3597 |
. . . . . 6
⊢ ((𝑑 = {〈1, 𝐷〉} ∧ 𝑖 ∈ (1...1)) → ((((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))}) ↔ (((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))(AP‘𝐾)({〈1, 𝐷〉}‘1)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))}))) |
197 | 196 | ralbidva 2968 |
. . . . 5
⊢ (𝑑 = {〈1, 𝐷〉} → (∀𝑖 ∈ (1...1)(((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))}) ↔ ∀𝑖 ∈ (1...1)(((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))(AP‘𝐾)({〈1, 𝐷〉}‘1)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))}))) |
198 | 193 | mpteq2dva 4672 |
. . . . . . . 8
⊢ (𝑑 = {〈1, 𝐷〉} → (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))) = (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))))) |
199 | 198 | rneqd 5274 |
. . . . . . 7
⊢ (𝑑 = {〈1, 𝐷〉} → ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))) = ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))))) |
200 | 199 | fveq2d 6107 |
. . . . . 6
⊢ (𝑑 = {〈1, 𝐷〉} → (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))))) = (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))))) |
201 | 200 | eqeq1d 2612 |
. . . . 5
⊢ (𝑑 = {〈1, 𝐷〉} → ((#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))))) = 1 ↔ (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))))) = 1)) |
202 | 197, 201 | anbi12d 743 |
. . . 4
⊢ (𝑑 = {〈1, 𝐷〉} → ((∀𝑖 ∈ (1...1)(((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘((𝐴 + (𝑊 − 𝐷)) + (𝑑‘𝑖))))) = 1) ↔ (∀𝑖 ∈ (1...1)(((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))(AP‘𝐾)({〈1, 𝐷〉}‘1)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))}) ∧ (#‘ran
(𝑖 ∈ (1...1) ↦
(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))))) = 1))) |
203 | 186, 202 | rspc2ev 3295 |
. . 3
⊢ (((𝐴 + (𝑊 − 𝐷)) ∈ ℕ ∧ {〈1, 𝐷〉} ∈ (ℕ
↑𝑚 (1...1)) ∧ (∀𝑖 ∈ (1...1)(((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))(AP‘𝐾)({〈1, 𝐷〉}‘1)) ⊆ (◡𝐹 “ {(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1)))}) ∧ (#‘ran
(𝑖 ∈ (1...1) ↦
(𝐹‘((𝐴 + (𝑊 − 𝐷)) + ({〈1, 𝐷〉}‘1))))) = 1)) →
∃𝑎 ∈ ℕ
∃𝑑 ∈ (ℕ
↑𝑚 (1...1))(∀𝑖 ∈ (1...1)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝑎 + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘(𝑎 + (𝑑‘𝑖))))) = 1)) |
204 | 50, 66, 159, 174, 203 | syl112anc 1322 |
. 2
⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚
(1...1))(∀𝑖 ∈
(1...1)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝑎 + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘(𝑎 + (𝑑‘𝑖))))) = 1)) |
205 | | ovex 6577 |
. . 3
⊢ (1...(2
· 𝑊)) ∈
V |
206 | 51 | a1i 11 |
. . 3
⊢ (𝜑 → 1 ∈
ℕ) |
207 | | eqid 2610 |
. . 3
⊢ (1...1) =
(1...1) |
208 | 205, 84, 127, 206, 207 | vdwpc 15522 |
. 2
⊢ (𝜑 → (〈1, 𝐾〉 PolyAP 𝐹 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑𝑚
(1...1))(∀𝑖 ∈
(1...1)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐹 “ {(𝐹‘(𝑎 + (𝑑‘𝑖)))}) ∧ (#‘ran (𝑖 ∈ (1...1) ↦ (𝐹‘(𝑎 + (𝑑‘𝑖))))) = 1))) |
209 | 204, 208 | mpbird 246 |
1
⊢ (𝜑 → 〈1, 𝐾〉 PolyAP 𝐹) |