| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | breq2 5147 | . . 3
⊢ (𝑓 = 𝐹 → (𝐾 MonoAP 𝑓 ↔ 𝐾 MonoAP 𝐹)) | 
| 2 |  | vdwlem9.a | . . 3
⊢ (𝜑 → ∀𝑓 ∈ ((𝑅 ↑m (1...𝑊)) ↑m (1...𝑉))𝐾 MonoAP 𝑓) | 
| 3 |  | vdwlem9.v | . . . . 5
⊢ (𝜑 → 𝑉 ∈ ℕ) | 
| 4 |  | vdwlem9.w | . . . . 5
⊢ (𝜑 → 𝑊 ∈ ℕ) | 
| 5 |  | vdw.r | . . . . 5
⊢ (𝜑 → 𝑅 ∈ Fin) | 
| 6 |  | vdwlem9.h | . . . . 5
⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) | 
| 7 |  | vdwlem9.f | . . . . 5
⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))))) | 
| 8 | 3, 4, 5, 6, 7 | vdwlem4 17022 | . . . 4
⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑m (1...𝑊))) | 
| 9 |  | ovex 7464 | . . . . 5
⊢ (𝑅 ↑m (1...𝑊)) ∈ V | 
| 10 |  | ovex 7464 | . . . . 5
⊢
(1...𝑉) ∈
V | 
| 11 | 9, 10 | elmap 8911 | . . . 4
⊢ (𝐹 ∈ ((𝑅 ↑m (1...𝑊)) ↑m (1...𝑉)) ↔ 𝐹:(1...𝑉)⟶(𝑅 ↑m (1...𝑊))) | 
| 12 | 8, 11 | sylibr 234 | . . 3
⊢ (𝜑 → 𝐹 ∈ ((𝑅 ↑m (1...𝑊)) ↑m (1...𝑉))) | 
| 13 | 1, 2, 12 | rspcdva 3623 | . 2
⊢ (𝜑 → 𝐾 MonoAP 𝐹) | 
| 14 |  | vdwlem9.k | . . . . . 6
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘2)) | 
| 15 |  | eluz2nn 12924 | . . . . . 6
⊢ (𝐾 ∈
(ℤ≥‘2) → 𝐾 ∈ ℕ) | 
| 16 | 14, 15 | syl 17 | . . . . 5
⊢ (𝜑 → 𝐾 ∈ ℕ) | 
| 17 | 16 | nnnn0d 12587 | . . . 4
⊢ (𝜑 → 𝐾 ∈
ℕ0) | 
| 18 | 10, 17, 8 | vdwmc 17016 | . . 3
⊢ (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑔∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) | 
| 19 |  | vdwlem9.g | . . . . . . . . 9
⊢ (𝜑 → ∀𝑔 ∈ (𝑅 ↑m (1...𝑊))(〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) | 
| 20 | 19 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ∀𝑔 ∈ (𝑅 ↑m (1...𝑊))(〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) | 
| 21 |  | simprr 773 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔})) | 
| 22 | 16 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐾 ∈ ℕ) | 
| 23 |  | simprll 779 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ ℕ) | 
| 24 |  | simprlr 780 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑑 ∈ ℕ) | 
| 25 |  | vdwapid1 17013 | . . . . . . . . . . . . 13
⊢ ((𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑)) | 
| 26 | 22, 23, 24, 25 | syl3anc 1373 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑)) | 
| 27 | 21, 26 | sseldd 3984 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ (◡𝐹 “ {𝑔})) | 
| 28 | 8 | ffnd 6737 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐹 Fn (1...𝑉)) | 
| 29 | 28 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐹 Fn (1...𝑉)) | 
| 30 |  | fniniseg 7080 | . . . . . . . . . . . 12
⊢ (𝐹 Fn (1...𝑉) → (𝑎 ∈ (◡𝐹 “ {𝑔}) ↔ (𝑎 ∈ (1...𝑉) ∧ (𝐹‘𝑎) = 𝑔))) | 
| 31 | 29, 30 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 ∈ (◡𝐹 “ {𝑔}) ↔ (𝑎 ∈ (1...𝑉) ∧ (𝐹‘𝑎) = 𝑔))) | 
| 32 | 27, 31 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 ∈ (1...𝑉) ∧ (𝐹‘𝑎) = 𝑔)) | 
| 33 | 32 | simprd 495 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝐹‘𝑎) = 𝑔) | 
| 34 | 8 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐹:(1...𝑉)⟶(𝑅 ↑m (1...𝑊))) | 
| 35 | 32 | simpld 494 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ (1...𝑉)) | 
| 36 | 34, 35 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝐹‘𝑎) ∈ (𝑅 ↑m (1...𝑊))) | 
| 37 | 33, 36 | eqeltrrd 2842 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑔 ∈ (𝑅 ↑m (1...𝑊))) | 
| 38 |  | rsp 3247 | . . . . . . . 8
⊢
(∀𝑔 ∈
(𝑅 ↑m
(1...𝑊))(〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (𝑔 ∈ (𝑅 ↑m (1...𝑊)) → (〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))) | 
| 39 | 20, 37, 38 | sylc 65 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)) | 
| 40 | 3 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑉 ∈ ℕ) | 
| 41 | 4 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑊 ∈ ℕ) | 
| 42 | 5 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑅 ∈ Fin) | 
| 43 | 6 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) | 
| 44 |  | vdwlem9.m | . . . . . . . . . . 11
⊢ (𝜑 → 𝑀 ∈ ℕ) | 
| 45 | 44 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑀 ∈ ℕ) | 
| 46 |  | ovex 7464 | . . . . . . . . . . . 12
⊢
(1...𝑊) ∈
V | 
| 47 |  | elmapg 8879 | . . . . . . . . . . . 12
⊢ ((𝑅 ∈ Fin ∧ (1...𝑊) ∈ V) → (𝑔 ∈ (𝑅 ↑m (1...𝑊)) ↔ 𝑔:(1...𝑊)⟶𝑅)) | 
| 48 | 42, 46, 47 | sylancl 586 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑔 ∈ (𝑅 ↑m (1...𝑊)) ↔ 𝑔:(1...𝑊)⟶𝑅)) | 
| 49 | 37, 48 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑔:(1...𝑊)⟶𝑅) | 
| 50 | 14 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐾 ∈
(ℤ≥‘2)) | 
| 51 | 40, 41, 42, 43, 7, 45, 49, 50, 23, 24, 21 | vdwlem7 17025 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (〈𝑀, 𝐾〉 PolyAP 𝑔 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔))) | 
| 52 |  | olc 869 | . . . . . . . . . 10
⊢ ((𝐾 + 1) MonoAP 𝑔 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)) | 
| 53 | 52 | a1i 11 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP 𝑔 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔))) | 
| 54 | 51, 53 | jaod 860 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔))) | 
| 55 |  | oveq1 7438 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑎 → (𝑥 − 1) = (𝑎 − 1)) | 
| 56 | 55 | oveq1d 7446 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑎 → ((𝑥 − 1) + 𝑉) = ((𝑎 − 1) + 𝑉)) | 
| 57 | 56 | oveq2d 7447 | . . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑎 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝑎 − 1) + 𝑉))) | 
| 58 | 57 | oveq2d 7447 | . . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑎 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))) | 
| 59 | 58 | fveq2d 6910 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑎 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) | 
| 60 | 59 | mpteq2dv 5244 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑎 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))))) | 
| 61 | 46 | mptex 7243 | . . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) ∈ V | 
| 62 | 60, 7, 61 | fvmpt 7016 | . . . . . . . . . . . . 13
⊢ (𝑎 ∈ (1...𝑉) → (𝐹‘𝑎) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))))) | 
| 63 | 35, 62 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝐹‘𝑎) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))))) | 
| 64 | 63, 33 | eqtr3d 2779 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) = 𝑔) | 
| 65 | 64 | breq2d 5155 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) ↔ (𝐾 + 1) MonoAP 𝑔)) | 
| 66 | 17 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝐾 ∈
ℕ0) | 
| 67 |  | peano2nn0 12566 | . . . . . . . . . . . 12
⊢ (𝐾 ∈ ℕ0
→ (𝐾 + 1) ∈
ℕ0) | 
| 68 | 66, 67 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝐾 + 1) ∈
ℕ0) | 
| 69 |  | nnm1nn0 12567 | . . . . . . . . . . . . . 14
⊢ (𝑎 ∈ ℕ → (𝑎 − 1) ∈
ℕ0) | 
| 70 | 23, 69 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 − 1) ∈
ℕ0) | 
| 71 |  | nn0nnaddcl 12557 | . . . . . . . . . . . . 13
⊢ (((𝑎 − 1) ∈
ℕ0 ∧ 𝑉
∈ ℕ) → ((𝑎
− 1) + 𝑉) ∈
ℕ) | 
| 72 | 70, 40, 71 | syl2anc 584 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝑎 − 1) + 𝑉) ∈ ℕ) | 
| 73 | 41, 72 | nnmulcld 12319 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · ((𝑎 − 1) + 𝑉)) ∈ ℕ) | 
| 74 | 23, 40 | nnaddcld 12318 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ∈ ℕ) | 
| 75 | 41, 74 | nnmulcld 12319 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ∈ ℕ) | 
| 76 | 75 | nnzd 12640 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ∈ ℤ) | 
| 77 |  | 2nn 12339 | . . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℕ | 
| 78 |  | nnmulcl 12290 | . . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℕ ∧ 𝑉
∈ ℕ) → (2 · 𝑉) ∈ ℕ) | 
| 79 | 77, 3, 78 | sylancr 587 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · 𝑉) ∈
ℕ) | 
| 80 | 4, 79 | nnmulcld 12319 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℕ) | 
| 81 | 80 | nnzd 12640 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℤ) | 
| 82 | 81 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ ℤ) | 
| 83 | 23 | nnred 12281 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ ℝ) | 
| 84 | 40 | nnred 12281 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑉 ∈ ℝ) | 
| 85 |  | elfzle2 13568 | . . . . . . . . . . . . . . . . 17
⊢ (𝑎 ∈ (1...𝑉) → 𝑎 ≤ 𝑉) | 
| 86 | 35, 85 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ≤ 𝑉) | 
| 87 | 83, 84, 84, 86 | leadd1dd 11877 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ≤ (𝑉 + 𝑉)) | 
| 88 | 40 | nncnd 12282 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑉 ∈ ℂ) | 
| 89 | 88 | 2timesd 12509 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (2 · 𝑉) = (𝑉 + 𝑉)) | 
| 90 | 87, 89 | breqtrrd 5171 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ≤ (2 · 𝑉)) | 
| 91 | 74 | nnred 12281 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ∈ ℝ) | 
| 92 | 79 | nnred 12281 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (2 · 𝑉) ∈
ℝ) | 
| 93 | 92 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (2 · 𝑉) ∈ ℝ) | 
| 94 | 41 | nnred 12281 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑊 ∈ ℝ) | 
| 95 | 41 | nngt0d 12315 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 0 < 𝑊) | 
| 96 |  | lemul2 12120 | . . . . . . . . . . . . . . 15
⊢ (((𝑎 + 𝑉) ∈ ℝ ∧ (2 · 𝑉) ∈ ℝ ∧ (𝑊 ∈ ℝ ∧ 0 <
𝑊)) → ((𝑎 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))) | 
| 97 | 91, 93, 94, 95, 96 | syl112anc 1376 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝑎 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))) | 
| 98 | 90, 97 | mpbid 232 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))) | 
| 99 |  | eluz2 12884 | . . . . . . . . . . . . 13
⊢ ((𝑊 · (2 · 𝑉)) ∈
(ℤ≥‘(𝑊 · (𝑎 + 𝑉))) ↔ ((𝑊 · (𝑎 + 𝑉)) ∈ ℤ ∧ (𝑊 · (2 · 𝑉)) ∈ ℤ ∧ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))) | 
| 100 | 76, 82, 98, 99 | syl3anbrc 1344 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈
(ℤ≥‘(𝑊 · (𝑎 + 𝑉)))) | 
| 101 | 41 | nncnd 12282 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑊 ∈ ℂ) | 
| 102 |  | 1cnd 11256 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 1 ∈
ℂ) | 
| 103 | 70 | nn0cnd 12589 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑎 − 1) ∈ ℂ) | 
| 104 | 103, 88 | addcld 11280 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝑎 − 1) + 𝑉) ∈ ℂ) | 
| 105 | 101, 102,
104 | adddid 11285 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (1 + ((𝑎 − 1) + 𝑉))) = ((𝑊 · 1) + (𝑊 · ((𝑎 − 1) + 𝑉)))) | 
| 106 | 102, 103,
88 | addassd 11283 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((1 + (𝑎 − 1)) + 𝑉) = (1 + ((𝑎 − 1) + 𝑉))) | 
| 107 |  | ax-1cn 11213 | . . . . . . . . . . . . . . . . . 18
⊢ 1 ∈
ℂ | 
| 108 | 23 | nncnd 12282 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → 𝑎 ∈ ℂ) | 
| 109 |  | pncan3 11516 | . . . . . . . . . . . . . . . . . 18
⊢ ((1
∈ ℂ ∧ 𝑎
∈ ℂ) → (1 + (𝑎 − 1)) = 𝑎) | 
| 110 | 107, 108,
109 | sylancr 587 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (1 + (𝑎 − 1)) = 𝑎) | 
| 111 | 110 | oveq1d 7446 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((1 + (𝑎 − 1)) + 𝑉) = (𝑎 + 𝑉)) | 
| 112 | 106, 111 | eqtr3d 2779 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (1 + ((𝑎 − 1) + 𝑉)) = (𝑎 + 𝑉)) | 
| 113 | 112 | oveq2d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (1 + ((𝑎 − 1) + 𝑉))) = (𝑊 · (𝑎 + 𝑉))) | 
| 114 | 101 | mulridd 11278 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · 1) = 𝑊) | 
| 115 | 114 | oveq1d 7446 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝑊 · 1) + (𝑊 · ((𝑎 − 1) + 𝑉))) = (𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉)))) | 
| 116 | 105, 113,
115 | 3eqtr3d 2785 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) = (𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉)))) | 
| 117 | 116 | fveq2d 6910 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) →
(ℤ≥‘(𝑊 · (𝑎 + 𝑉))) = (ℤ≥‘(𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉))))) | 
| 118 | 100, 117 | eleqtrd 2843 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈
(ℤ≥‘(𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉))))) | 
| 119 |  | fvoveq1 7454 | . . . . . . . . . . . 12
⊢ (𝑦 = 𝑧 → (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))) = (𝐻‘(𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉))))) | 
| 120 | 119 | cbvmptv 5255 | . . . . . . . . . . 11
⊢ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) = (𝑧 ∈ (1...𝑊) ↦ (𝐻‘(𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉))))) | 
| 121 | 42, 68, 41, 73, 43, 118, 120 | vdwlem2 17020 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) → (𝐾 + 1) MonoAP 𝐻)) | 
| 122 | 65, 121 | sylbird 260 | . . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP 𝑔 → (𝐾 + 1) MonoAP 𝐻)) | 
| 123 | 122 | orim2d 969 | . . . . . . . 8
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) | 
| 124 | 54, 123 | syld 47 | . . . . . . 7
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → ((〈𝑀, 𝐾〉 PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) | 
| 125 | 39, 124 | mpd 15 | . . . . . 6
⊢ ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}))) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)) | 
| 126 | 125 | expr 456 | . . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) | 
| 127 | 126 | rexlimdvva 3213 | . . . 4
⊢ (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) | 
| 128 | 127 | exlimdv 1933 | . . 3
⊢ (𝜑 → (∃𝑔∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (◡𝐹 “ {𝑔}) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) | 
| 129 | 18, 128 | sylbid 240 | . 2
⊢ (𝜑 → (𝐾 MonoAP 𝐹 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))) | 
| 130 | 13, 129 | mpd 15 | 1
⊢ (𝜑 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)) |