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

Theorem vdwlem5 17023
Description: Lemma for vdw 17032. (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
StepHypRef Expression
1 vdwlem6.t . 2 𝑇 = (𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)))
2 vdwlem6.b . . 3 (𝜑𝐵 ∈ ℕ)
3 vdwlem3.w . . . . 5 (𝜑𝑊 ∈ ℕ)
43nnnn0d 12587 . . . 4 (𝜑𝑊 ∈ ℕ0)
5 vdwlem7.a . . . . . 6 (𝜑𝐴 ∈ ℕ)
6 vdwlem3.v . . . . . . . . . 10 (𝜑𝑉 ∈ ℕ)
76nncnd 12282 . . . . . . . . 9 (𝜑𝑉 ∈ ℂ)
8 vdwlem7.d . . . . . . . . . 10 (𝜑𝐷 ∈ ℕ)
98nncnd 12282 . . . . . . . . 9 (𝜑𝐷 ∈ ℂ)
107, 9subcld 11620 . . . . . . . 8 (𝜑 → (𝑉𝐷) ∈ ℂ)
115nncnd 12282 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
1210, 11npcand 11624 . . . . . . 7 (𝜑 → (((𝑉𝐷) − 𝐴) + 𝐴) = (𝑉𝐷))
137, 9, 11subsub4d 11651 . . . . . . . . . 10 (𝜑 → ((𝑉𝐷) − 𝐴) = (𝑉 − (𝐷 + 𝐴)))
149, 11addcomd 11463 . . . . . . . . . . 11 (𝜑 → (𝐷 + 𝐴) = (𝐴 + 𝐷))
1514oveq2d 7447 . . . . . . . . . 10 (𝜑 → (𝑉 − (𝐷 + 𝐴)) = (𝑉 − (𝐴 + 𝐷)))
1613, 15eqtrd 2777 . . . . . . . . 9 (𝜑 → ((𝑉𝐷) − 𝐴) = (𝑉 − (𝐴 + 𝐷)))
17 cnvimass 6100 . . . . . . . . . . . . 13 (𝐹 “ {𝐺}) ⊆ dom 𝐹
18 vdwlem4.r . . . . . . . . . . . . . 14 (𝜑𝑅 ∈ Fin)
19 vdwlem4.h . . . . . . . . . . . . . 14 (𝜑𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅)
20 vdwlem4.f . . . . . . . . . . . . . 14 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉))))))
216, 3, 18, 19, 20vdwlem4 17022 . . . . . . . . . . . . 13 (𝜑𝐹:(1...𝑉)⟶(𝑅m (1...𝑊)))
2217, 21fssdm 6755 . . . . . . . . . . . 12 (𝜑 → (𝐹 “ {𝐺}) ⊆ (1...𝑉))
23 vdwlem7.s . . . . . . . . . . . . 13 (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (𝐹 “ {𝐺}))
24 ssun2 4179 . . . . . . . . . . . . . . 15 ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷) ⊆ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))
25 vdwlem7.k . . . . . . . . . . . . . . . . 17 (𝜑𝐾 ∈ (ℤ‘2))
26 uz2m1nn 12965 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ (ℤ‘2) → (𝐾 − 1) ∈ ℕ)
2725, 26syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 − 1) ∈ ℕ)
285, 8nnaddcld 12318 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 + 𝐷) ∈ ℕ)
29 vdwapid1 17013 . . . . . . . . . . . . . . . 16 (((𝐾 − 1) ∈ ℕ ∧ (𝐴 + 𝐷) ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴 + 𝐷) ∈ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))
3027, 28, 8, 29syl3anc 1373 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴 + 𝐷) ∈ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷))
3124, 30sselid 3981 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 + 𝐷) ∈ ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)))
32 eluz2nn 12924 . . . . . . . . . . . . . . . . . . . 20 (𝐾 ∈ (ℤ‘2) → 𝐾 ∈ ℕ)
3325, 32syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑𝐾 ∈ ℕ)
3433nncnd 12282 . . . . . . . . . . . . . . . . . 18 (𝜑𝐾 ∈ ℂ)
35 ax-1cn 11213 . . . . . . . . . . . . . . . . . 18 1 ∈ ℂ
36 npcan 11517 . . . . . . . . . . . . . . . . . 18 ((𝐾 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝐾 − 1) + 1) = 𝐾)
3734, 35, 36sylancl 586 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐾 − 1) + 1) = 𝐾)
3837fveq2d 6910 . . . . . . . . . . . . . . . 16 (𝜑 → (AP‘((𝐾 − 1) + 1)) = (AP‘𝐾))
3938oveqd 7448 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = (𝐴(AP‘𝐾)𝐷))
40 nnm1nn0 12567 . . . . . . . . . . . . . . . . 17 (𝐾 ∈ ℕ → (𝐾 − 1) ∈ ℕ0)
4133, 40syl 17 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐾 − 1) ∈ ℕ0)
42 vdwapun 17012 . . . . . . . . . . . . . . . 16 (((𝐾 − 1) ∈ ℕ0𝐴 ∈ ℕ ∧ 𝐷 ∈ ℕ) → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)))
4341, 5, 8, 42syl3anc 1373 . . . . . . . . . . . . . . 15 (𝜑 → (𝐴(AP‘((𝐾 − 1) + 1))𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)))
4439, 43eqtr3d 2779 . . . . . . . . . . . . . 14 (𝜑 → (𝐴(AP‘𝐾)𝐷) = ({𝐴} ∪ ((𝐴 + 𝐷)(AP‘(𝐾 − 1))𝐷)))
4531, 44eleqtrrd 2844 . . . . . . . . . . . . 13 (𝜑 → (𝐴 + 𝐷) ∈ (𝐴(AP‘𝐾)𝐷))
4623, 45sseldd 3984 . . . . . . . . . . . 12 (𝜑 → (𝐴 + 𝐷) ∈ (𝐹 “ {𝐺}))
4722, 46sseldd 3984 . . . . . . . . . . 11 (𝜑 → (𝐴 + 𝐷) ∈ (1...𝑉))
48 elfzuz3 13561 . . . . . . . . . . 11 ((𝐴 + 𝐷) ∈ (1...𝑉) → 𝑉 ∈ (ℤ‘(𝐴 + 𝐷)))
4947, 48syl 17 . . . . . . . . . 10 (𝜑𝑉 ∈ (ℤ‘(𝐴 + 𝐷)))
50 uznn0sub 12917 . . . . . . . . . 10 (𝑉 ∈ (ℤ‘(𝐴 + 𝐷)) → (𝑉 − (𝐴 + 𝐷)) ∈ ℕ0)
5149, 50syl 17 . . . . . . . . 9 (𝜑 → (𝑉 − (𝐴 + 𝐷)) ∈ ℕ0)
5216, 51eqeltrd 2841 . . . . . . . 8 (𝜑 → ((𝑉𝐷) − 𝐴) ∈ ℕ0)
53 nn0nnaddcl 12557 . . . . . . . 8 ((((𝑉𝐷) − 𝐴) ∈ ℕ0𝐴 ∈ ℕ) → (((𝑉𝐷) − 𝐴) + 𝐴) ∈ ℕ)
5452, 5, 53syl2anc 584 . . . . . . 7 (𝜑 → (((𝑉𝐷) − 𝐴) + 𝐴) ∈ ℕ)
5512, 54eqeltrrd 2842 . . . . . 6 (𝜑 → (𝑉𝐷) ∈ ℕ)
565, 55nnaddcld 12318 . . . . 5 (𝜑 → (𝐴 + (𝑉𝐷)) ∈ ℕ)
57 nnm1nn0 12567 . . . . 5 ((𝐴 + (𝑉𝐷)) ∈ ℕ → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℕ0)
5856, 57syl 17 . . . 4 (𝜑 → ((𝐴 + (𝑉𝐷)) − 1) ∈ ℕ0)
594, 58nn0mulcld 12592 . . 3 (𝜑 → (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) ∈ ℕ0)
60 nnnn0addcl 12556 . . 3 ((𝐵 ∈ ℕ ∧ (𝑊 · ((𝐴 + (𝑉𝐷)) − 1)) ∈ ℕ0) → (𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) ∈ ℕ)
612, 59, 60syl2anc 584 . 2 (𝜑 → (𝐵 + (𝑊 · ((𝐴 + (𝑉𝐷)) − 1))) ∈ ℕ)
621, 61eqeltrid 2845 1 (𝜑𝑇 ∈ ℕ)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wcel 2108  wral 3061  cun 3949  wss 3951  ifcif 4525  {csn 4626  cmpt 5225  ccnv 5684  ran crn 5686  cima 5688  wf 6557  cfv 6561  (class class class)co 7431  m cmap 8866  Fincfn 8985  cc 11153  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  cmin 11492  cn 12266  2c2 12321  0cn0 12526  cuz 12878  ...cfz 13547  chash 14369  APcvdwa 17003
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-er 8745  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-nn 12267  df-2 12329  df-n0 12527  df-z 12614  df-uz 12879  df-fz 13548  df-vdwap 17006
This theorem is referenced by:  vdwlem6  17024
  Copyright terms: Public domain W3C validator