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

Theorem vdwlem9 16380
 Description: Lemma for vdw 16385. (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 5036 . . 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 16375 . . . 4 (𝜑𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
9 ovex 7183 . . . . 5 (𝑅m (1...𝑊)) ∈ V
10 ovex 7183 . . . . 5 (1...𝑉) ∈ V
119, 10elmap 8453 . . . 4 (𝐹 ∈ ((𝑅m (1...𝑊)) ↑m (1...𝑉)) ↔ 𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
128, 11sylibr 237 . . 3 (𝜑𝐹 ∈ ((𝑅m (1...𝑊)) ↑m (1...𝑉)))
131, 2, 12rspcdva 3543 . 2 (𝜑𝐾 MonoAP 𝐹)
14 vdwlem9.k . . . . . 6 (𝜑𝐾 ∈ (ℤ‘2))
15 eluz2nn 12324 . . . . . 6 (𝐾 ∈ (ℤ‘2) → 𝐾 ∈ ℕ)
1614, 15syl 17 . . . . 5 (𝜑𝐾 ∈ ℕ)
1716nnnn0d 11994 . . . 4 (𝜑𝐾 ∈ ℕ0)
1810, 17, 8vdwmc 16369 . . 3 (𝜑 → (𝐾 MonoAP 𝐹 ↔ ∃𝑔𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔})))
19 vdwlem9.g . . . . . . . . 9 (𝜑 → ∀𝑔 ∈ (𝑅m (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
2019adantr 484 . . . . . . . 8 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ∀𝑔 ∈ (𝑅m (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
21 simprr 772 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))
2216adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐾 ∈ ℕ)
23 simprll 778 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ ℕ)
24 simprlr 779 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑑 ∈ ℕ)
25 vdwapid1 16366 . . . . . . . . . . . . 13 ((𝐾 ∈ ℕ ∧ 𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑))
2622, 23, 24, 25syl3anc 1368 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ (𝑎(AP‘𝐾)𝑑))
2721, 26sseldd 3893 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ (𝐹 “ {𝑔}))
288ffnd 6499 . . . . . . . . . . . . 13 (𝜑𝐹 Fn (1...𝑉))
2928adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐹 Fn (1...𝑉))
30 fniniseg 6821 . . . . . . . . . . . 12 (𝐹 Fn (1...𝑉) → (𝑎 ∈ (𝐹 “ {𝑔}) ↔ (𝑎 ∈ (1...𝑉) ∧ (𝐹𝑎) = 𝑔)))
3129, 30syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 ∈ (𝐹 “ {𝑔}) ↔ (𝑎 ∈ (1...𝑉) ∧ (𝐹𝑎) = 𝑔)))
3227, 31mpbid 235 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 ∈ (1...𝑉) ∧ (𝐹𝑎) = 𝑔))
3332simprd 499 . . . . . . . . 9 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝐹𝑎) = 𝑔)
348adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
3532simpld 498 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ (1...𝑉))
3634, 35ffvelrnd 6843 . . . . . . . . 9 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝐹𝑎) ∈ (𝑅m (1...𝑊)))
3733, 36eqeltrrd 2853 . . . . . . . 8 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑔 ∈ (𝑅m (1...𝑊)))
38 rsp 3134 . . . . . . . 8 (∀𝑔 ∈ (𝑅m (1...𝑊))(⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (𝑔 ∈ (𝑅m (1...𝑊)) → (⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔)))
3920, 37, 38sylc 65 . . . . . . 7 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔))
403adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑉 ∈ ℕ)
414adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑊 ∈ ℕ)
425adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑅 ∈ Fin)
436adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
44 vdwlem9.m . . . . . . . . . . 11 (𝜑𝑀 ∈ ℕ)
4544adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑀 ∈ ℕ)
46 ovex 7183 . . . . . . . . . . . 12 (1...𝑊) ∈ V
47 elmapg 8429 . . . . . . . . . . . 12 ((𝑅 ∈ Fin ∧ (1...𝑊) ∈ V) → (𝑔 ∈ (𝑅m (1...𝑊)) ↔ 𝑔:(1...𝑊)⟶𝑅))
4842, 46, 47sylancl 589 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑔 ∈ (𝑅m (1...𝑊)) ↔ 𝑔:(1...𝑊)⟶𝑅))
4937, 48mpbid 235 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑔:(1...𝑊)⟶𝑅)
5014adantr 484 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐾 ∈ (ℤ‘2))
5140, 41, 42, 43, 7, 45, 49, 50, 23, 24, 21vdwlem7 16378 . . . . . . . . 9 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (⟨𝑀, 𝐾⟩ PolyAP 𝑔 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)))
52 olc 865 . . . . . . . . . 10 ((𝐾 + 1) MonoAP 𝑔 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔))
5352a1i 11 . . . . . . . . 9 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP 𝑔 → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)))
5451, 53jaod 856 . . . . . . . 8 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((⟨𝑀, 𝐾⟩ PolyAP 𝑔 ∨ (𝐾 + 1) MonoAP 𝑔) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝑔)))
55 oveq1 7157 . . . . . . . . . . . . . . . . . . 19 (𝑥 = 𝑎 → (𝑥 − 1) = (𝑎 − 1))
5655oveq1d 7165 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → ((𝑥 − 1) + 𝑉) = ((𝑎 − 1) + 𝑉))
5756oveq2d 7166 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (𝑊 · ((𝑥 − 1) + 𝑉)) = (𝑊 · ((𝑎 − 1) + 𝑉)))
5857oveq2d 7166 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))) = (𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))
5958fveq2d 6662 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))) = (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
6059mpteq2dv 5128 . . . . . . . . . . . . . 14 (𝑥 = 𝑎 → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))))
6146mptex 6977 . . . . . . . . . . . . . 14 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) ∈ V
6260, 7, 61fvmpt 6759 . . . . . . . . . . . . 13 (𝑎 ∈ (1...𝑉) → (𝐹𝑎) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))))
6335, 62syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝐹𝑎) = (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))))
6463, 33eqtr3d 2795 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) = 𝑔)
6564breq2d 5044 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) ↔ (𝐾 + 1) MonoAP 𝑔))
6617adantr 484 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝐾 ∈ ℕ0)
67 peano2nn0 11974 . . . . . . . . . . . 12 (𝐾 ∈ ℕ0 → (𝐾 + 1) ∈ ℕ0)
6866, 67syl 17 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝐾 + 1) ∈ ℕ0)
69 nnm1nn0 11975 . . . . . . . . . . . . . 14 (𝑎 ∈ ℕ → (𝑎 − 1) ∈ ℕ0)
7023, 69syl 17 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 − 1) ∈ ℕ0)
71 nn0nnaddcl 11965 . . . . . . . . . . . . 13 (((𝑎 − 1) ∈ ℕ0𝑉 ∈ ℕ) → ((𝑎 − 1) + 𝑉) ∈ ℕ)
7270, 40, 71syl2anc 587 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝑎 − 1) + 𝑉) ∈ ℕ)
7341, 72nnmulcld 11727 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · ((𝑎 − 1) + 𝑉)) ∈ ℕ)
7423, 40nnaddcld 11726 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ∈ ℕ)
7541, 74nnmulcld 11727 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ∈ ℕ)
7675nnzd 12125 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ∈ ℤ)
77 2nn 11747 . . . . . . . . . . . . . . . . 17 2 ∈ ℕ
78 nnmulcl 11698 . . . . . . . . . . . . . . . . 17 ((2 ∈ ℕ ∧ 𝑉 ∈ ℕ) → (2 · 𝑉) ∈ ℕ)
7977, 3, 78sylancr 590 . . . . . . . . . . . . . . . 16 (𝜑 → (2 · 𝑉) ∈ ℕ)
804, 79nnmulcld 11727 . . . . . . . . . . . . . . 15 (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℕ)
8180nnzd 12125 . . . . . . . . . . . . . 14 (𝜑 → (𝑊 · (2 · 𝑉)) ∈ ℤ)
8281adantr 484 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ ℤ)
8323nnred 11689 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ ℝ)
8440nnred 11689 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑉 ∈ ℝ)
85 elfzle2 12960 . . . . . . . . . . . . . . . . 17 (𝑎 ∈ (1...𝑉) → 𝑎𝑉)
8635, 85syl 17 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎𝑉)
8783, 84, 84, 86leadd1dd 11292 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ≤ (𝑉 + 𝑉))
8840nncnd 11690 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑉 ∈ ℂ)
89882timesd 11917 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (2 · 𝑉) = (𝑉 + 𝑉))
9087, 89breqtrrd 5060 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ≤ (2 · 𝑉))
9174nnred 11689 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 + 𝑉) ∈ ℝ)
9279nnred 11689 . . . . . . . . . . . . . . . 16 (𝜑 → (2 · 𝑉) ∈ ℝ)
9392adantr 484 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (2 · 𝑉) ∈ ℝ)
9441nnred 11689 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑊 ∈ ℝ)
9541nngt0d 11723 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 0 < 𝑊)
96 lemul2 11531 . . . . . . . . . . . . . . 15 (((𝑎 + 𝑉) ∈ ℝ ∧ (2 · 𝑉) ∈ ℝ ∧ (𝑊 ∈ ℝ ∧ 0 < 𝑊)) → ((𝑎 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))))
9791, 93, 94, 95, 96syl112anc 1371 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝑎 + 𝑉) ≤ (2 · 𝑉) ↔ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))))
9890, 97mpbid 235 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉)))
99 eluz2 12288 . . . . . . . . . . . . 13 ((𝑊 · (2 · 𝑉)) ∈ (ℤ‘(𝑊 · (𝑎 + 𝑉))) ↔ ((𝑊 · (𝑎 + 𝑉)) ∈ ℤ ∧ (𝑊 · (2 · 𝑉)) ∈ ℤ ∧ (𝑊 · (𝑎 + 𝑉)) ≤ (𝑊 · (2 · 𝑉))))
10076, 82, 98, 99syl3anbrc 1340 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ (ℤ‘(𝑊 · (𝑎 + 𝑉))))
10141nncnd 11690 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑊 ∈ ℂ)
102 1cnd 10674 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 1 ∈ ℂ)
10370nn0cnd 11996 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑎 − 1) ∈ ℂ)
104103, 88addcld 10698 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝑎 − 1) + 𝑉) ∈ ℂ)
105101, 102, 104adddid 10703 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (1 + ((𝑎 − 1) + 𝑉))) = ((𝑊 · 1) + (𝑊 · ((𝑎 − 1) + 𝑉))))
106102, 103, 88addassd 10701 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((1 + (𝑎 − 1)) + 𝑉) = (1 + ((𝑎 − 1) + 𝑉)))
107 ax-1cn 10633 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
10823nncnd 11690 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → 𝑎 ∈ ℂ)
109 pncan3 10932 . . . . . . . . . . . . . . . . . 18 ((1 ∈ ℂ ∧ 𝑎 ∈ ℂ) → (1 + (𝑎 − 1)) = 𝑎)
110107, 108, 109sylancr 590 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (1 + (𝑎 − 1)) = 𝑎)
111110oveq1d 7165 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((1 + (𝑎 − 1)) + 𝑉) = (𝑎 + 𝑉))
112106, 111eqtr3d 2795 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (1 + ((𝑎 − 1) + 𝑉)) = (𝑎 + 𝑉))
113112oveq2d 7166 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (1 + ((𝑎 − 1) + 𝑉))) = (𝑊 · (𝑎 + 𝑉)))
114101mulid1d 10696 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · 1) = 𝑊)
115114oveq1d 7165 . . . . . . . . . . . . . 14 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝑊 · 1) + (𝑊 · ((𝑎 − 1) + 𝑉))) = (𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉))))
116105, 113, 1153eqtr3d 2801 . . . . . . . . . . . . 13 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (𝑎 + 𝑉)) = (𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉))))
117116fveq2d 6662 . . . . . . . . . . . 12 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (ℤ‘(𝑊 · (𝑎 + 𝑉))) = (ℤ‘(𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
118100, 117eleqtrd 2854 . . . . . . . . . . 11 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → (𝑊 · (2 · 𝑉)) ∈ (ℤ‘(𝑊 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
119 fvoveq1 7173 . . . . . . . . . . . 12 (𝑦 = 𝑧 → (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉)))) = (𝐻‘(𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
120119cbvmptv 5135 . . . . . . . . . . 11 (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) = (𝑧 ∈ (1...𝑊) ↦ (𝐻‘(𝑧 + (𝑊 · ((𝑎 − 1) + 𝑉)))))
12142, 68, 41, 73, 43, 118, 120vdwlem2 16373 . . . . . . . . . 10 ((𝜑 ∧ ((𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ) ∧ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}))) → ((𝐾 + 1) MonoAP (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑎 − 1) + 𝑉))))) → (𝐾 + 1) MonoAP 𝐻))
12265, 121sylbird 263 . . . . . . . . 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 460 . . . . 5 ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ ℕ)) → ((𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
127126rexlimdvva 3218 . . . 4 (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
128127exlimdv 1934 . . 3 (𝜑 → (∃𝑔𝑎 ∈ ℕ ∃𝑑 ∈ ℕ (𝑎(AP‘𝐾)𝑑) ⊆ (𝐹 “ {𝑔}) → (⟨(𝑀 + 1), 𝐾⟩ PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐻)))
12918, 128sylbid 243 . 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 209   ∧ wa 399   ∨ wo 844   = wceq 1538  ∃wex 1781   ∈ wcel 2111  ∀wral 3070  ∃wrex 3071  Vcvv 3409   ⊆ wss 3858  {csn 4522  ⟨cop 4528   class class class wbr 5032   ↦ cmpt 5112  ◡ccnv 5523   “ cima 5527   Fn wfn 6330  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150   ↑m cmap 8416  Fincfn 8527  ℂcc 10573  ℝcr 10574  0cc0 10575  1c1 10576   + caddc 10578   · cmul 10580   < clt 10713   ≤ cle 10714   − cmin 10908  ℕcn 11674  2c2 11729  ℕ0cn0 11934  ℤcz 12020  ℤ≥cuz 12282  ...cfz 12939  APcvdwa 16356   MonoAP cvdwm 16357   PolyAP cvdwp 16358 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-oadd 8116  df-er 8299  df-map 8418  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-dju 9363  df-card 9401  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-nn 11675  df-2 11737  df-n0 11935  df-z 12021  df-uz 12283  df-rp 12431  df-fz 12940  df-hash 13741  df-vdwap 16359  df-vdwmc 16360  df-vdwpc 16361 This theorem is referenced by:  vdwlem10  16381
 Copyright terms: Public domain W3C validator