Step | Hyp | Ref
| Expression |
1 | | vdwlem9.v |
. . . . 5
⊢ (𝜑 → 𝑉 ∈ ℕ) |
2 | | vdwlem9.w |
. . . . 5
⊢ (𝜑 → 𝑊 ∈ ℕ) |
3 | | vdw.r |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ Fin) |
4 | | vdwlem9.h |
. . . . 5
⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) |
5 | | vdwlem9.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))))) |
6 | 1, 2, 3, 4, 5 | vdwlem4 15526 |
. . . 4
⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑𝑚 (1...𝑊))) |
7 | | ovex 6577 |
. . . . 5
⊢ (𝑅 ↑𝑚
(1...𝑊)) ∈
V |
8 | | ovex 6577 |
. . . . 5
⊢
(1...𝑉) ∈
V |
9 | 7, 8 | elmap 7772 |
. . . 4
⊢ (𝐹 ∈ ((𝑅 ↑𝑚 (1...𝑊)) ↑𝑚
(1...𝑉)) ↔ 𝐹:(1...𝑉)⟶(𝑅 ↑𝑚 (1...𝑊))) |
10 | 6, 9 | sylibr 223 |
. . 3
⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↑𝑚 (1...𝑊)) ↑𝑚
(1...𝑉))) |
11 | | vdwlem9.a |
. . 3
⊢ (𝜑 → ∀𝑓 ∈ ((𝑅 ↑𝑚 (1...𝑊)) ↑𝑚
(1...𝑉))𝐾 MonoAP 𝑓) |
12 | | breq2 4587 |
. . . 4
⊢ (𝑓 = 𝐹 → (𝐾 MonoAP 𝑓 ↔ 𝐾 MonoAP 𝐹)) |
13 | 12 | rspcv 3278 |
. . 3
⊢ (𝐹 ∈ ((𝑅 ↑𝑚 (1...𝑊)) ↑𝑚
(1...𝑉)) →
(∀𝑓 ∈ ((𝑅 ↑𝑚
(1...𝑊))
↑𝑚 (1...𝑉))𝐾 MonoAP 𝑓 → 𝐾 MonoAP 𝐹)) |
14 | 10, 11, 13 | sylc 63 |
. 2
⊢ (𝜑 → 𝐾 MonoAP 𝐹) |
15 | | vdwlem9.k |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘2)) |
16 | | eluz2nn 11602 |
. . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘2) → 𝐾 ∈ ℕ) |
17 | 15, 16 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈ ℕ) |
18 | 17 | nnnn0d 11228 |
. . . 4
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
19 | 8, 18, 6 | vdwmc 15520 |
. . 3
⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑔∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) |
20 | | vdwlem9.g |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑊))(〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) |
21 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ∀𝑔 ∈ (𝑅 ↑𝑚 (1...𝑊))(〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) |
22 | | simprr 792 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔})) |
23 | 17 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐾 ∈ ℕ) |
24 | | simprll 798 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ ℕ) |
25 | | simprlr 799 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑑 ∈ ℕ) |
26 | | vdwapid1 15517 |
. . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑)) |
27 | 23, 24, 25, 26 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑)) |
28 | 22, 27 | sseldd 3569 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ (◡𝐹 “ {𝑔})) |
29 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝐹:(1...𝑉)⟶(𝑅 ↑𝑚 (1...𝑊)) → 𝐹 Fn (1...𝑉)) |
30 | 6, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn (1...𝑉)) |
31 | 30 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐹 Fn (1...𝑉)) |
32 | | fniniseg 6246 |
. . . . . . . . . . . 12
⊢ (𝐹 Fn (1...𝑉) → (𝑎 ∈ (◡𝐹 “ {𝑔}) ↔ (𝑎 ∈ (1...𝑉) ∧ (𝐹‘𝑎) = 𝑔))) |
33 | 31, 32 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 ∈ (◡𝐹 “ {𝑔}) ↔ (𝑎 ∈ (1...𝑉) ∧ (𝐹‘𝑎) = 𝑔))) |
34 | 28, 33 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 ∈ (1...𝑉) ∧ (𝐹‘𝑎) = 𝑔)) |
35 | 34 | simprd 478 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝐹‘𝑎) = 𝑔) |
36 | 6 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐹:(1...𝑉)⟶(𝑅 ↑𝑚 (1...𝑊))) |
37 | 34 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ (1...𝑉)) |
38 | 36, 37 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝐹‘𝑎) ∈ (𝑅 ↑𝑚 (1...𝑊))) |
39 | 35, 38 | eqeltrrd 2689 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑔 ∈ (𝑅 ↑𝑚 (1...𝑊))) |
40 | | rsp 2913 |
. . . . . . . 8
⊢
(∀𝑔 ∈
(𝑅
↑𝑚 (1...𝑊))(〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (𝑔 ∈ (𝑅 ↑𝑚 (1...𝑊)) → (〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) |
41 | 21, 39, 40 | sylc 63 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) |
42 | 1 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑉 ∈ ℕ) |
43 | 2 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑊 ∈ ℕ) |
44 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑅 ∈ Fin) |
45 | 4 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) |
46 | | vdwlem9.m |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) |
47 | 46 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑀 ∈ ℕ) |
48 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
(1...𝑊) ∈
V |
49 | | elmapg 7757 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ Fin ∧ (1...𝑊) ∈ V) → (𝑔 ∈ (𝑅 ↑𝑚 (1...𝑊)) ↔ 𝑔:(1...𝑊)⟶𝑅)) |
50 | 44, 48, 49 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑔 ∈ (𝑅 ↑𝑚 (1...𝑊)) ↔ 𝑔:(1...𝑊)⟶𝑅)) |
51 | 39, 50 | mpbid 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑔:(1...𝑊)⟶𝑅) |
52 | 15 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐾 ∈
(ℤ≥‘2)) |
53 | 42, 43, 44, 45, 5, 47, 51, 52, 24, 25, 22 | vdwlem7 15529 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (〈𝑀, 𝐾〉 PolyAP 𝑔 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔))) |
54 | | olc 398 |
. . . . . . . . . 10
⊢ ((𝐾 + 1) MonoAP 𝑔 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)) |
55 | 54 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP 𝑔 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔))) |
56 | 53, 55 | jaod 394 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔))) |
57 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (𝑥 − 1) = (𝑎 − 1)) |
58 | 57 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → ((𝑥 − 1) + 𝑉) = ((𝑎 − 1) + 𝑉)) |
59 | 58 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝑎 − 1) + 𝑉))) |
60 | 59 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))) |
61 | 60 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) |
62 | 61 | mpteq2dv 4673 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))))) |
63 | 48 | mptex 6390 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) ∈ V |
64 | 62, 5, 63 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ (1...𝑉) → (𝐹‘𝑎) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))))) |
65 | 37, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝐹‘𝑎) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))))) |
66 | 65, 35 | eqtr3d 2646 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) = 𝑔) |
67 | 66 | breq2d 4595 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) ↔ (𝐾 + 1) MonoAP 𝑔)) |
68 | 18 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐾 ∈
ℕ0) |
69 | | peano2nn0 11210 |
. . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ0) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝐾 + 1) ∈
ℕ0) |
71 | | nnm1nn0 11211 |
. . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ → (𝑎 − 1) ∈
ℕ0) |
72 | 24, 71 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 − 1) ∈
ℕ0) |
73 | | nn0nnaddcl 11201 |
. . . . . . . . . . . . 13
⊢ (((𝑎 − 1) ∈
ℕ0 ∧ 𝑉
∈ ℕ) → ((𝑎
− 1) + 𝑉) ∈
ℕ) |
74 | 72, 42, 73 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝑎 − 1) + 𝑉) ∈ ℕ) |
75 | 43, 74 | nnmulcld 10945 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · ((𝑎 − 1) + 𝑉)) ∈ ℕ) |
76 | 24, 42 | nnaddcld 10944 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ∈ ℕ) |
77 | 43, 76 | nnmulcld 10945 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ∈ ℕ) |
78 | 77 | nnzd 11357 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ∈ ℤ) |
79 | | 2nn 11062 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ |
80 | | nnmulcl 10920 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℕ ∧ 𝑉
∈ ℕ) → (2 · 𝑉) ∈ ℕ) |
81 | 79, 1, 80 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · 𝑉) ∈
ℕ) |
82 | 2, 81 | nnmulcld 10945 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℕ) |
83 | 82 | nnzd 11357 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℤ) |
84 | 83 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ ℤ) |
85 | 24 | nnred 10912 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ ℝ) |
86 | 42 | nnred 10912 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑉 ∈ ℝ) |
87 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (1...𝑉) → 𝑎 ≤ 𝑉) |
88 | 37, 87 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ≤ 𝑉) |
89 | 85, 86, 86, 88 | leadd1dd 10520 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ≤ (𝑉 + 𝑉)) |
90 | 42 | nncnd 10913 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑉 ∈ ℂ) |
91 | 90 | 2timesd 11152 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (2 · 𝑉) = (𝑉 + 𝑉)) |
92 | 89, 91 | breqtrrd 4611 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ≤ (2 · 𝑉)) |
93 | 76 | nnred 10912 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ∈ ℝ) |
94 | 81 | nnred 10912 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · 𝑉) ∈
ℝ) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (2 · 𝑉) ∈ ℝ) |
96 | 43 | nnred 10912 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑊 ∈ ℝ) |
97 | 43 | nngt0d 10941 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 0 < 𝑊) |
98 | | lemul2 10755 |
. . . . . . . . . . . . . . 15
⊢ (((𝑎 + 𝑉) ∈ ℝ ∧ (2 · 𝑉) ∈ ℝ ∧ (𝑊 ∈ ℝ ∧ 0 <
𝑊)) → ((𝑎 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))) |
99 | 93, 95, 96, 97, 98 | syl112anc 1322 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝑎 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))) |
100 | 92, 99 | mpbid 221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))) |
101 | | eluz2 11569 |
. . . . . . . . . . . . 13
⊢ ((𝑊 · (2 · 𝑉)) ∈
(ℤ≥‘(𝑊 · (𝑎 + 𝑉))) ↔ ((𝑊 · (𝑎 + 𝑉)) ∈ ℤ ∧ (𝑊 · (2 · 𝑉)) ∈ ℤ ∧ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))) |
102 | 78, 84, 100, 101 | syl3anbrc 1239 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈
(ℤ≥‘(𝑊 · (𝑎 + 𝑉)))) |
103 | 43 | nncnd 10913 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑊 ∈ ℂ) |
104 | | 1cnd 9935 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 1 ∈
ℂ) |
105 | 72 | nn0cnd 11230 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 − 1) ∈ ℂ) |
106 | 105, 90 | addcld 9938 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝑎 − 1) + 𝑉) ∈ ℂ) |
107 | 103, 104,
106 | adddid 9943 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (1 + ((𝑎 − 1) + 𝑉))) = ((𝑊 · 1) + (𝑊 · ((𝑎 − 1) + 𝑉)))) |
108 | 104, 105,
90 | addassd 9941 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((1 + (𝑎 − 1)) + 𝑉) = (1 + ((𝑎 − 1) + 𝑉))) |
109 | | ax-1cn 9873 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ |
110 | 24 | nncnd 10913 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ ℂ) |
111 | | pncan3 10168 |
. . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ 𝑎
∈ ℂ) → (1 + (𝑎 − 1)) = 𝑎) |
112 | 109, 110,
111 | sylancr 694 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (1 + (𝑎 − 1)) = 𝑎) |
113 | 112 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((1 + (𝑎 − 1)) + 𝑉) = (𝑎 + 𝑉)) |
114 | 108, 113 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (1 + ((𝑎 − 1) + 𝑉)) = (𝑎 + 𝑉)) |
115 | 114 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (1 + ((𝑎 − 1) + 𝑉))) = (𝑊 · (𝑎 + 𝑉))) |
116 | 103 | mulid1d 9936 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · 1) = 𝑊) |
117 | 116 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝑊 · 1) + (𝑊 · ((𝑎 − 1) + 𝑉))) = (𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉)))) |
118 | 107, 115,
117 | 3eqtr3d 2652 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) = (𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉)))) |
119 | 118 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) →
(ℤ≥‘(𝑊 · (𝑎 + 𝑉))) = (ℤ≥‘(𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉))))) |
120 | 102, 119 | eleqtrd 2690 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈
(ℤ≥‘(𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉))))) |
121 | | oveq1 6556 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑧 → (𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))) = (𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉)))) |
122 | 121 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))) = (𝐻‘(𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉))))) |
123 | 122 | cbvmptv 4678 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) = (𝑧 ∈ (1...𝑊) ↦ (𝐻‘(𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉))))) |
124 | 44, 70, 43, 75, 45, 120, 123 | vdwlem2 15524 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) → (𝐾 + 1) MonoAP 𝐻)) |
125 | 67, 124 | sylbird 249 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP 𝑔 → (𝐾 + 1) MonoAP 𝐻)) |
126 | 125 | orim2d 881 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) |
127 | 56, 126 | syld 46 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) |
128 | 41, 127 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)) |
129 | 128 | expr 641 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) |
130 | 129 | rexlimdvva 3020 |
. . . 4
⊢ (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) |
131 | 130 | exlimdv 1848 |
. . 3
⊢ (𝜑 → (∃𝑔∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) |
132 | 19, 131 | sylbid 229 |
. 2
⊢ (𝜑 → (𝐾 MonoAP 𝐹 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) |
133 | 14, 132 | mpd 15 |
1
⊢ (𝜑 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)) |