vdwlem5 - Metamath Proof Explorer

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

Theorem vdwlem5 16961

Description: Lemma for vdw 16970. (Contributed by Mario Carneiro, 12-Sep-2014.)

**Hypotheses**
Ref	Expression
vdwlem3.v	⊢ (𝜑 → 𝑉 ∈ ℕ)
vdwlem3.w	⊢ (𝜑 → 𝑊 ∈ ℕ)
vdwlem4.r	⊢ (𝜑 → 𝑅 ∈ Fin)
vdwlem4.h	⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
vdwlem4.f	⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))
vdwlem7.m	⊢ (𝜑 → 𝑀 ∈ ℕ)
vdwlem7.g	⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅)
vdwlem7.k	⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘2))
vdwlem7.a	⊢ (𝜑 → 𝐴 ∈ ℕ)
vdwlem7.d	⊢ (𝜑 → 𝐷 ∈ ℕ)
vdwlem7.s	⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (^◡𝐹 “ {𝐺}))
vdwlem6.b	⊢ (𝜑 → 𝐵 ∈ ℕ)
vdwlem6.e	⊢ (𝜑 → 𝐸:(1...𝑀)⟶ℕ)
vdwlem6.s	⊢ (𝜑 → ∀𝑖 ∈ (1...𝑀)((𝐵 + (𝐸‘𝑖))(AP‘𝐾)(𝐸‘𝑖)) ⊆ (^◡𝐺 “ {(𝐺‘(𝐵 + (𝐸‘𝑖)))}))
vdwlem6.j	⊢ 𝐽 = (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝐵 + (𝐸‘𝑖))))
vdwlem6.r	⊢ (𝜑 → (♯‘ran 𝐽) = 𝑀)
vdwlem6.t	⊢ 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)))
vdwlem6.p	⊢ 𝑃 = (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝐸‘𝑗)) + (𝑊 · 𝐷)))

**Assertion**
Ref	Expression
vdwlem5	⊢ (𝜑 → 𝑇 ∈ ℕ)

Distinct variable groups: 𝑥,𝑦,𝐴 𝑖,𝑗,𝑥,𝑦,𝐺 𝑖,𝐾,𝑗,𝑥,𝑦 𝑖,𝐽,𝑗,𝑥 𝑃,𝑖,𝑥 𝜑,𝑖,𝑗,𝑥,𝑦 𝑅,𝑖,𝑥,𝑦 𝐵,𝑖,𝑗,𝑥,𝑦 𝑖,𝐻,𝑥,𝑦 𝑖,𝑀,𝑗,𝑥,𝑦 𝐷,𝑗,𝑥,𝑦 𝑖,𝐸,𝑗,𝑥,𝑦 𝑖,𝑊,𝑗,𝑥,𝑦 𝑇,𝑖,𝑥 𝑥,𝑉,𝑦 Allowed substitution hints: 𝐴(𝑖,𝑗) 𝐷(𝑖) 𝑃(𝑦,𝑗) 𝑅(𝑗) 𝑇(𝑦,𝑗) 𝐹(𝑥,𝑦,𝑖,𝑗) 𝐻(𝑗) 𝐽(𝑦) 𝑉(𝑖,𝑗)

**Proof of Theorem vdwlem5**
Step	Hyp	Ref	Expression
1		vdwlem6.t	. 2 ⊢ 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)))
2		vdwlem6.b	. . 3 ⊢ (𝜑 → 𝐵 ∈ ℕ)
3		vdwlem3.w	. . . . 5 ⊢ (𝜑 → 𝑊 ∈ ℕ)
4	3	nnnn0d 12570	. . . 4 ⊢ (𝜑 → 𝑊 ∈ ℕ₀)
5		vdwlem7.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ ℕ)
6		vdwlem3.v	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ ℕ)
7	6	nncnd 12266	. . . . . . . . 9 ⊢ (𝜑 → 𝑉 ∈ ℂ)
8		vdwlem7.d	. . . . . . . . . 10 ⊢ (𝜑 → 𝐷 ∈ ℕ)
9	8	nncnd 12266	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℂ)
10	7, 9	subcld 11609	. . . . . . . 8 ⊢ (𝜑 → (𝑉 − 𝐷) ∈ ℂ)
11	5	nncnd 12266	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
12	10, 11	npcand 11613	. . . . . . 7 ⊢ (𝜑 → (((𝑉 − 𝐷) − 𝐴) + 𝐴) = (𝑉 − 𝐷))
13	7, 9, 11	subsub4d 11640	. . . . . . . . . 10 ⊢ (𝜑 → ((𝑉 − 𝐷) − 𝐴) = (𝑉 − (𝐷 + 𝐴)))
14	9, 11	addcomd 11454	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 + 𝐴) = (𝐴 + 𝐷))
15	14	oveq2d 7442	. . . . . . . . . 10 ⊢ (𝜑 → (𝑉 − (𝐷 + 𝐴)) = (𝑉 − (𝐴 + 𝐷)))
16	13, 15	eqtrd 2768	. . . . . . . . 9 ⊢ (𝜑 → ((𝑉 − 𝐷) − 𝐴) = (𝑉 − (𝐴 + 𝐷)))
17		cnvimass 6090	. . . . . . . . . . . . 13 ⊢ (^◡𝐹 “ {𝐺}) ⊆ dom 𝐹
18		vdwlem4.r	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑅 ∈ Fin)
19		vdwlem4.h	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
20		vdwlem4.f	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))
21	6, 3, 18, 19, 20	vdwlem4 16960	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐹:(1...𝑉)⟶(𝑅 ↑_m (1...𝑊)))
22	17, 21	fssdm 6747	. . . . . . . . . . . 12 ⊢ (𝜑 → (^◡𝐹 “ {𝐺}) ⊆ (1...𝑉))
23		vdwlem7.s	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (^◡𝐹 “ {𝐺}))
24		ssun2 4175	. . . . . . . . . . . . . . 15 ⊢ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷) ⊆ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))
25		vdwlem7.k	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐾 ∈ (ℤ_≥‘2))
26		uz2m1nn 12945	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (ℤ_≥‘2) → (𝐾 − 1) ∈ ℕ)
27	25, 26	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 − 1) ∈ ℕ)
28	5, 8	nnaddcld 12302	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 + 𝐷) ∈ ℕ)
29		vdwapid1 16951	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 − 1) ∈ ℕ ∧ (𝐴 + 𝐷) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + 𝐷) ∈ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))
30	27, 28, 8, 29	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴 + 𝐷) ∈ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))
31	24, 30	sselid 3980	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 + 𝐷) ∈ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)))
32		eluz2nn 12906	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (ℤ_≥‘2) → 𝐾 ∈ ℕ)
33	25, 32	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐾 ∈ ℕ)
34	33	nncnd 12266	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐾 ∈ ℂ)
35		ax-1cn 11204	. . . . . . . . . . . . . . . . . 18 ⊢ 1 ∈ ℂ
36		npcan 11507	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
37	34, 35, 36	sylancl 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
38	37	fveq2d 6906	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (AP‘((𝐾 − 1) + 1)) = (AP‘𝐾))
39	38	oveqd 7443	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = (𝐴(AP‘𝐾)𝐷))
40		nnm1nn0 12551	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ₀)
41	33, 40	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐾 − 1) ∈ ℕ₀)
42		vdwapun 16950	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 − 1) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)))
43	41, 5, 8, 42	syl3anc 1368	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)))
44	39, 43	eqtr3d 2770	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)))
45	31, 44	eleqtrrd 2832	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐴 + 𝐷) ∈ (𝐴(AP‘𝐾)𝐷))
46	23, 45	sseldd 3983	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 + 𝐷) ∈ (^◡𝐹 “ {𝐺}))
47	22, 46	sseldd 3983	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐴 + 𝐷) ∈ (1...𝑉))
48		elfzuz3 13538	. . . . . . . . . . 11 ⊢ ((𝐴 + 𝐷) ∈ (1...𝑉) → 𝑉 ∈ (ℤ_≥‘(𝐴 + 𝐷)))
49	47, 48	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑉 ∈ (ℤ_≥‘(𝐴 + 𝐷)))
50		uznn0sub 12899	. . . . . . . . . 10 ⊢ (𝑉 ∈ (ℤ_≥‘(𝐴 + 𝐷)) → (𝑉 − (𝐴 + 𝐷)) ∈ ℕ₀)
51	49, 50	syl 17	. . . . . . . . 9 ⊢ (𝜑 → (𝑉 − (𝐴 + 𝐷)) ∈ ℕ₀)
52	16, 51	eqeltrd 2829	. . . . . . . 8 ⊢ (𝜑 → ((𝑉 − 𝐷) − 𝐴) ∈ ℕ₀)
53		nn0nnaddcl 12541	. . . . . . . 8 ⊢ ((((𝑉 − 𝐷) − 𝐴) ∈ ℕ₀ ∧ 𝐴 ∈ ℕ) → (((𝑉 − 𝐷) − 𝐴) + 𝐴) ∈ ℕ)
54	52, 5, 53	syl2anc 582	. . . . . . 7 ⊢ (𝜑 → (((𝑉 − 𝐷) − 𝐴) + 𝐴) ∈ ℕ)
55	12, 54	eqeltrrd 2830	. . . . . 6 ⊢ (𝜑 → (𝑉 − 𝐷) ∈ ℕ)
56	5, 55	nnaddcld 12302	. . . . 5 ⊢ (𝜑 → (𝐴 + (𝑉 − 𝐷)) ∈ ℕ)
57		nnm1nn0 12551	. . . . 5 ⊢ ((𝐴 + (𝑉 − 𝐷)) ∈ ℕ → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈ ℕ₀)
58	56, 57	syl 17	. . . 4 ⊢ (𝜑 → ((𝐴 + (𝑉 − 𝐷)) − 1) ∈ ℕ₀)
59	4, 58	nn0mulcld 12575	. . 3 ⊢ (𝜑 → (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) ∈ ℕ₀)
60		nnnn0addcl 12540	. . 3 ⊢ ((𝐵 ∈ ℕ ∧ (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1)) ∈ ℕ₀) → (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) ∈ ℕ)
61	2, 59, 60	syl2anc 582	. 2 ⊢ (𝜑 → (𝐵 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) ∈ ℕ)
62	1, 61	eqeltrid 2833	1 ⊢ (𝜑 → 𝑇 ∈ ℕ)

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 ∀wral 3058 ∪ cun 3947 ⊆ wss 3949 ifcif 4532 {csn 4632 ↦ cmpt 5235 ^◡ccnv 5681 ran crn 5683 “ cima 5685 ⟶wf 6549 ‘cfv 6553 (class class class)co 7426 ↑_m cmap 8851 Fincfn 8970 ℂcc 11144 0cc0 11146 1c1 11147 + caddc 11149 · cmul 11151 − cmin 11482 ℕcn 12250 2c2 12305 ℕ₀cn0 12510 ℤ_≥cuz 12860 ...cfz 13524 ♯chash 14329 APcvdwa 16941

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-10 2129 ax-11 2146 ax-12 2166 ax-ext 2699 ax-rep 5289 ax-sep 5303 ax-nul 5310 ax-pow 5369 ax-pr 5433 ax-un 7746 ax-cnex 11202 ax-resscn 11203 ax-1cn 11204 ax-icn 11205 ax-addcl 11206 ax-addrcl 11207 ax-mulcl 11208 ax-mulrcl 11209 ax-mulcom 11210 ax-addass 11211 ax-mulass 11212 ax-distr 11213 ax-i2m1 11214 ax-1ne0 11215 ax-1rid 11216 ax-rnegex 11217 ax-rrecex 11218 ax-cnre 11219 ax-pre-lttri 11220 ax-pre-lttrn 11221 ax-pre-ltadd 11222 ax-pre-mulgt0 11223

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2529 df-eu 2558 df-clab 2706 df-cleq 2720 df-clel 2806 df-nfc 2881 df-ne 2938 df-nel 3044 df-ral 3059 df-rex 3068 df-reu 3375 df-rab 3431 df-v 3475 df-sbc 3779 df-csb 3895 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-pss 3968 df-nul 4327 df-if 4533 df-pw 4608 df-sn 4633 df-pr 4635 df-op 4639 df-uni 4913 df-iun 5002 df-br 5153 df-opab 5215 df-mpt 5236 df-tr 5270 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6310 df-ord 6377 df-on 6378 df-lim 6379 df-suc 6380 df-iota 6505 df-fun 6555 df-fn 6556 df-f 6557 df-f1 6558 df-fo 6559 df-f1o 6560 df-fv 6561 df-riota 7382 df-ov 7429 df-oprab 7430 df-mpo 7431 df-om 7877 df-1st 7999 df-2nd 8000 df-frecs 8293 df-wrecs 8324 df-recs 8398 df-rdg 8437 df-er 8731 df-map 8853 df-en 8971 df-dom 8972 df-sdom 8973 df-pnf 11288 df-mnf 11289 df-xr 11290 df-ltxr 11291 df-le 11292 df-sub 11484 df-neg 11485 df-nn 12251 df-2 12313 df-n0 12511 df-z 12597 df-uz 12861 df-fz 13525 df-vdwap 16944

This theorem is referenced by: vdwlem6 16962

W3C validator