MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  vdwlem9 Structured version   Visualization version   GIF version

Theorem vdwlem9 16986
Description: Lemma for vdw 16991. (Contributed by Mario Carneiro, 12-Sep-2014.)
Hypotheses
Ref Expression
vdw.r (𝜑𝑅 ∈ Fin)
vdwlem9.k (𝜑𝐾 ∈ (ℤ‘2))
vdwlem9.s (𝜑 → ∀𝑠 ∈ Fin ∃𝑛 ∈ ℕ ∀𝑓 ∈ (𝑠m (1...𝑛))𝐾 MonoAP 𝑓)
vdwlem9.m (𝜑𝑀 ∈ ℕ)
vdwlem9.w (𝜑𝑊 ∈ ℕ)
vdwlem9.g (𝜑 → ∀𝑔 ∈ (𝑅m (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
vdwlem9.v (𝜑𝑉 ∈ ℕ)
vdwlem9.a (𝜑 → ∀𝑓 ∈ ((𝑅m (1...𝑊)) ↑m (1...𝑉))𝐾 MonoAP 𝑓)
vdwlem9.h (𝜑𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
vdwlem9.f 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))
Assertion
Ref Expression
vdwlem9 (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))
Distinct variable groups:   𝑔,𝑛,𝑥,𝑦,𝜑   𝑥,𝑓,𝑦,𝑉   𝑓,𝑊,𝑥,𝑦   𝑓,𝑔,𝐹,𝑥,𝑦   𝑓,𝑛,𝑠,𝐾,𝑔,𝑥,𝑦   𝑓,𝑀,𝑔,𝑛,𝑥,𝑦   𝑅,𝑓,𝑔,𝑛,𝑠,𝑥,𝑦   𝑔,𝐻,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑓,𝑠)   𝐹(𝑛,𝑠)   𝐻(𝑓,𝑛,𝑠)   𝑀(𝑠)   𝑉(𝑔,𝑛,𝑠)   𝑊(𝑔,𝑛,𝑠)

Proof of Theorem vdwlem9
Dummy variables 𝑎 𝑑 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 breq2 5149 . . 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) + 𝑉))))))
83, 4, 5, 6, 7vdwlem4 16981 . . . 4 (𝜑𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
9 ovex 7449 . . . . 5 (𝑅m (1...𝑊)) ∈ V
10 ovex 7449 . . . . 5 (1...𝑉) ∈ V
119, 10elmap 8892 . . . 4 (𝐹 ∈ ((𝑅m (1...𝑊)) ↑m (1...𝑉)) ↔ 𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
128, 11sylibr 233 . . 3 (𝜑𝐹 ∈ ((𝑅m (1...𝑊)) ↑m (1...𝑉)))
131, 2, 12rspcdva 3608 . 2 (𝜑𝐾 MonoAP 𝐹)
14 vdwlem9.k . . . . . 6 (𝜑𝐾 ∈ (ℤ‘2))
15 eluz2nn 12914 . . . . . 6 (𝐾 ∈ (ℤ‘2) → 𝐾 ∈ ℕ)
1614, 15syl 17 . . . . 5 (𝜑𝐾 ∈ ℕ)
1716nnnn0d 12578 . . . 4 (𝜑𝐾 ∈ ℕ0)
1810, 17, 8vdwmc 16975 . . 3 (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑔𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔})))
19 vdwlem9.g . . . . . . . . 9 (𝜑 → ∀𝑔 ∈ (𝑅m (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
2019adantr 479 . . . . . . . 8 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ∀𝑔 ∈ (𝑅m (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
21 simprr 771 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))
2216adantr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐾 ∈ ℕ)
23 simprll 777 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ ℕ)
24 simprlr 778 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑑 ∈ ℕ)
25 vdwapid1 16972 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑))
2622, 23, 24, 25syl3anc 1368 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑))
2721, 26sseldd 3979 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ (𝐹 “ {𝑔}))
288ffnd 6721 . . . . . . . . . . . . 13 (𝜑𝐹 Fn (1...𝑉))
2928adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐹 Fn (1...𝑉))
30 fniniseg 7065 . . . . . . . . . . . 12 (𝐹 Fn (1...𝑉) → (𝑎 ∈ (𝐹 “ {𝑔}) ↔ (𝑎 ∈ (1...𝑉) ∧ (𝐹𝑎) = 𝑔)))
3129, 30syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 ∈ (𝐹 “ {𝑔}) ↔ (𝑎 ∈ (1...𝑉) ∧ (𝐹𝑎) = 𝑔)))
3227, 31mpbid 231 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 ∈ (1...𝑉) ∧ (𝐹𝑎) = 𝑔))
3332simprd 494 . . . . . . . . 9 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝐹𝑎) = 𝑔)
348adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
3532simpld 493 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ (1...𝑉))
3634, 35ffvelcdmd 7091 . . . . . . . . 9 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝐹𝑎) ∈ (𝑅m (1...𝑊)))
3733, 36eqeltrrd 2827 . . . . . . . 8 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑔 ∈ (𝑅m (1...𝑊)))
38 rsp 3235 . . . . . . . 8 (∀𝑔 ∈ (𝑅m (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (𝑔 ∈ (𝑅m (1...𝑊)) → (⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)))
3920, 37, 38sylc 65 . . . . . . 7 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
403adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑉 ∈ ℕ)
414adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑊 ∈ ℕ)
425adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑅 ∈ Fin)
436adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
44 vdwlem9.m . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ)
4544adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑀 ∈ ℕ)
46 ovex 7449 . . . . . . . . . . . 12 (1...𝑊) ∈ V
47 elmapg 8860 . . . . . . . . . . . 12 ((𝑅 ∈ Fin ∧ (1...𝑊) ∈ V) → (𝑔 ∈ (𝑅m (1...𝑊)) ↔ 𝑔:(1...𝑊)⟶𝑅))
4842, 46, 47sylancl 584 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑔 ∈ (𝑅m (1...𝑊)) ↔ 𝑔:(1...𝑊)⟶𝑅))
4937, 48mpbid 231 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑔:(1...𝑊)⟶𝑅)
5014adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐾 ∈ (ℤ‘2))
5140, 41, 42, 43, 7, 45, 49, 50, 23, 24, 21vdwlem7 16984 . . . . . . . . 9 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (⟨𝑀, 𝐾⟩ PolyAP 𝑔 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)))
52 olc 866 . . . . . . . . . 10 ((𝐾 + 1) MonoAP 𝑔 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔))
5352a1i 11 . . . . . . . . 9 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP 𝑔 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)))
5451, 53jaod 857 . . . . . . . 8 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)))
55 oveq1 7423 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → (𝑥 − 1) = (𝑎 − 1))
5655oveq1d 7431 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → ((𝑥 − 1) + 𝑉) = ((𝑎 − 1) + 𝑉))
5756oveq2d 7432 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝑎 − 1) + 𝑉)))
5857oveq2d 7432 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))
5958fveq2d 6897 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
6059mpteq2dv 5247 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))))
6146mptex 7232 . . . . . . . . . . . . . 14 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) ∈ V
6260, 7, 61fvmpt 7001 . . . . . . . . . . . . 13 (𝑎 ∈ (1...𝑉) → (𝐹𝑎) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))))
6335, 62syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝐹𝑎) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))))
6463, 33eqtr3d 2768 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) = 𝑔)
6564breq2d 5157 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) ↔ (𝐾 + 1) MonoAP 𝑔))
6617adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐾 ∈ ℕ0)
67 peano2nn0 12558 . . . . . . . . . . . 12 (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
6866, 67syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝐾 + 1) ∈ ℕ0)
69 nnm1nn0 12559 . . . . . . . . . . . . . 14 (𝑎 ∈ ℕ → (𝑎 − 1) ∈ ℕ0)
7023, 69syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 − 1) ∈ ℕ0)
71 nn0nnaddcl 12549 . . . . . . . . . . . . 13 (((𝑎 − 1) ∈ ℕ0𝑉 ∈ ℕ) → ((𝑎 − 1) + 𝑉) ∈ ℕ)
7270, 40, 71syl2anc 582 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝑎 − 1) + 𝑉) ∈ ℕ)
7341, 72nnmulcld 12311 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · ((𝑎 − 1) + 𝑉)) ∈ ℕ)
7423, 40nnaddcld 12310 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ∈ ℕ)
7541, 74nnmulcld 12311 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ∈ ℕ)
7675nnzd 12631 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ∈ ℤ)
77 2nn 12331 . . . . . . . . . . . . . . . . 17 2 ∈ ℕ
78 nnmulcl 12282 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ ∧ 𝑉 ∈ ℕ) → (2 · 𝑉) ∈ ℕ)
7977, 3, 78sylancr 585 . . . . . . . . . . . . . . . 16 (𝜑 → (2 · 𝑉) ∈ ℕ)
804, 79nnmulcld 12311 . . . . . . . . . . . . . . 15 (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℕ)
8180nnzd 12631 . . . . . . . . . . . . . 14 (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℤ)
8281adantr 479 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ ℤ)
8323nnred 12273 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ ℝ)
8440nnred 12273 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑉 ∈ ℝ)
85 elfzle2 13553 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (1...𝑉) → 𝑎𝑉)
8635, 85syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎𝑉)
8783, 84, 84, 86leadd1dd 11869 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ≤ (𝑉 + 𝑉))
8840nncnd 12274 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑉 ∈ ℂ)
89882timesd 12501 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (2 · 𝑉) = (𝑉 + 𝑉))
9087, 89breqtrrd 5173 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ≤ (2 · 𝑉))
9174nnred 12273 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ∈ ℝ)
9279nnred 12273 . . . . . . . . . . . . . . . 16 (𝜑 → (2 · 𝑉) ∈ ℝ)
9392adantr 479 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (2 · 𝑉) ∈ ℝ)
9441nnred 12273 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑊 ∈ ℝ)
9541nngt0d 12307 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 0 < 𝑊)
96 lemul2 12112 . . . . . . . . . . . . . . 15 (((𝑎 + 𝑉) ∈ ℝ ∧ (2 · 𝑉) ∈ ℝ ∧ (𝑊 ∈ ℝ ∧ 0 < 𝑊)) → ((𝑎 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))))
9791, 93, 94, 95, 96syl112anc 1371 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝑎 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))))
9890, 97mpbid 231 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))
99 eluz2 12874 . . . . . . . . . . . . 13 ((𝑊 · (2 · 𝑉)) ∈ (ℤ‘(𝑊 · (𝑎 + 𝑉))) ↔ ((𝑊 · (𝑎 + 𝑉)) ∈ ℤ ∧ (𝑊 · (2 · 𝑉)) ∈ ℤ ∧ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))))
10076, 82, 98, 99syl3anbrc 1340 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ (ℤ‘(𝑊 · (𝑎 + 𝑉))))
10141nncnd 12274 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑊 ∈ ℂ)
102 1cnd 11250 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 1 ∈ ℂ)
10370nn0cnd 12580 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 − 1) ∈ ℂ)
104103, 88addcld 11274 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝑎 − 1) + 𝑉) ∈ ℂ)
105101, 102, 104adddid 11279 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (1 + ((𝑎 − 1) + 𝑉))) = ((𝑊 · 1) + (𝑊 · ((𝑎 − 1) + 𝑉))))
106102, 103, 88addassd 11277 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((1 + (𝑎 − 1)) + 𝑉) = (1 + ((𝑎 − 1) + 𝑉)))
107 ax-1cn 11207 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
10823nncnd 12274 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ ℂ)
109 pncan3 11509 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (1 + (𝑎 − 1)) = 𝑎)
110107, 108, 109sylancr 585 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (1 + (𝑎 − 1)) = 𝑎)
111110oveq1d 7431 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((1 + (𝑎 − 1)) + 𝑉) = (𝑎 + 𝑉))
112106, 111eqtr3d 2768 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (1 + ((𝑎 − 1) + 𝑉)) = (𝑎 + 𝑉))
113112oveq2d 7432 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (1 + ((𝑎 − 1) + 𝑉))) = (𝑊 · (𝑎 + 𝑉)))
114101mulridd 11272 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · 1) = 𝑊)
115114oveq1d 7431 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝑊 · 1) + (𝑊 · ((𝑎 − 1) + 𝑉))) = (𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉))))
116105, 113, 1153eqtr3d 2774 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) = (𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉))))
117116fveq2d 6897 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (ℤ‘(𝑊 · (𝑎 + 𝑉))) = (ℤ‘(𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
118100, 117eleqtrd 2828 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ (ℤ‘(𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
119 fvoveq1 7439 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))) = (𝐻‘(𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
120119cbvmptv 5258 . . . . . . . . . . 11 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) = (𝑧 ∈ (1...𝑊) ↦ (𝐻‘(𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
12142, 68, 41, 73, 43, 118, 120vdwlem2 16979 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) → (𝐾 + 1) MonoAP 𝐻))
12265, 121sylbird 259 . . . . . . . . 9 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP 𝑔 → (𝐾 + 1) MonoAP 𝐻))
123122orim2d 964 . . . . . . . 8 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
12454, 123syld 47 . . . . . . 7 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
12539, 124mpd 15 . . . . . 6 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))
126125expr 455 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
127126rexlimdvva 3202 . . . 4 (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
128127exlimdv 1929 . . 3 (𝜑 → (∃𝑔𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
12918, 128sylbid 239 . 2 (𝜑 → (𝐾 MonoAP 𝐹 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
13013, 129mpd 15 1 (𝜑 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wo 845   = wceq 1534  wex 1774  wcel 2099  wral 3051  wrex 3060  Vcvv 3462  wss 3946  {csn 4623  cop 4629   class class class wbr 5145  cmpt 5228  ccnv 5673  cima 5677   Fn wfn 6541  wf 6542  cfv 6546  (class class class)co 7416  m cmap 8847  Fincfn 8966  cc 11147  cr 11148  0cc0 11149  1c1 11150   + caddc 11152   · cmul 11154   < clt 11289  cle 11290  cmin 11485  cn 12258  2c2 12313  0cn0 12518  cz 12604  cuz 12868  ...cfz 13532  APcvdwa 16962   MonoAP cvdwm 16963   PolyAP cvdwp 16964
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5282  ax-sep 5296  ax-nul 5303  ax-pow 5361  ax-pr 5425  ax-un 7738  ax-cnex 11205  ax-resscn 11206  ax-1cn 11207  ax-icn 11208  ax-addcl 11209  ax-addrcl 11210  ax-mulcl 11211  ax-mulrcl 11212  ax-mulcom 11213  ax-addass 11214  ax-mulass 11215  ax-distr 11216  ax-i2m1 11217  ax-1ne0 11218  ax-1rid 11219  ax-rnegex 11220  ax-rrecex 11221  ax-cnre 11222  ax-pre-lttri 11223  ax-pre-lttrn 11224  ax-pre-ltadd 11225  ax-pre-mulgt0 11226
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-br 5146  df-opab 5208  df-mpt 5229  df-tr 5263  df-id 5572  df-eprel 5578  df-po 5586  df-so 5587  df-fr 5629  df-we 5631  df-xp 5680  df-rel 5681  df-cnv 5682  df-co 5683  df-dm 5684  df-rn 5685  df-res 5686  df-ima 5687  df-pred 6304  df-ord 6371  df-on 6372  df-lim 6373  df-suc 6374  df-iota 6498  df-fun 6548  df-fn 6549  df-f 6550  df-f1 6551  df-fo 6552  df-f1o 6553  df-fv 6554  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-om 7869  df-1st 7995  df-2nd 7996  df-frecs 8288  df-wrecs 8319  df-recs 8393  df-rdg 8432  df-1o 8488  df-oadd 8492  df-er 8726  df-map 8849  df-en 8967  df-dom 8968  df-sdom 8969  df-fin 8970  df-dju 9937  df-card 9975  df-pnf 11291  df-mnf 11292  df-xr 11293  df-ltxr 11294  df-le 11295  df-sub 11487  df-neg 11488  df-nn 12259  df-2 12321  df-n0 12519  df-z 12605  df-uz 12869  df-rp 13023  df-fz 13533  df-hash 14343  df-vdwap 16965  df-vdwmc 16966  df-vdwpc 16967
This theorem is referenced by:  vdwlem10  16987
  Copyright terms: Public domain W3C validator