Mathbox for Stefan O'Rear < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  rabdiophlem2 Structured version   Visualization version   GIF version

Theorem rabdiophlem2 37837
 Description: Lemma for arithmetic diophantine sets. Reuse a polynomial expression under a new quantifier. (Contributed by Stefan O'Rear, 10-Oct-2014.)
Hypothesis
Ref Expression
rabdiophlem2.1 𝑀 = (𝑁 + 1)
Assertion
Ref Expression
rabdiophlem2 ((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚 (1...𝑀)) ↦ (𝑡 ↾ (1...𝑁)) / 𝑢𝐴) ∈ (mzPoly‘(1...𝑀)))
Distinct variable groups:   𝑢,𝑁,𝑡   𝑢,𝑀,𝑡   𝑡,𝐴
Allowed substitution hint:   𝐴(𝑢)

Proof of Theorem rabdiophlem2
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 nfcv 2890 . . . . . 6 𝑎𝐴
2 nfcsb1v 3678 . . . . . 6 𝑢𝑎 / 𝑢𝐴
3 csbeq1a 3671 . . . . . 6 (𝑢 = 𝑎𝐴 = 𝑎 / 𝑢𝐴)
41, 2, 3cbvmpt 4889 . . . . 5 (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) = (𝑎 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝑎 / 𝑢𝐴)
54fveq1i 6341 . . . 4 ((𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴)‘(𝑡 ↾ (1...𝑁))) = ((𝑎 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝑎 / 𝑢𝐴)‘(𝑡 ↾ (1...𝑁)))
6 rabdiophlem2.1 . . . . . . 7 𝑀 = (𝑁 + 1)
76mapfzcons1cl 37752 . . . . . 6 (𝑡 ∈ (ℤ ↑𝑚 (1...𝑀)) → (𝑡 ↾ (1...𝑁)) ∈ (ℤ ↑𝑚 (1...𝑁)))
87adantl 473 . . . . 5 (((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℤ ↑𝑚 (1...𝑀))) → (𝑡 ↾ (1...𝑁)) ∈ (ℤ ↑𝑚 (1...𝑁)))
9 mzpf 37770 . . . . . . . 8 ((𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴):(ℤ ↑𝑚 (1...𝑁))⟶ℤ)
10 eqid 2748 . . . . . . . . 9 (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) = (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴)
1110fmpt 6532 . . . . . . . 8 (∀𝑢 ∈ (ℤ ↑𝑚 (1...𝑁))𝐴 ∈ ℤ ↔ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴):(ℤ ↑𝑚 (1...𝑁))⟶ℤ)
129, 11sylibr 224 . . . . . . 7 ((𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)) → ∀𝑢 ∈ (ℤ ↑𝑚 (1...𝑁))𝐴 ∈ ℤ)
1312ad2antlr 765 . . . . . 6 (((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℤ ↑𝑚 (1...𝑀))) → ∀𝑢 ∈ (ℤ ↑𝑚 (1...𝑁))𝐴 ∈ ℤ)
14 nfcsb1v 3678 . . . . . . . 8 𝑢(𝑡 ↾ (1...𝑁)) / 𝑢𝐴
1514nfel1 2905 . . . . . . 7 𝑢(𝑡 ↾ (1...𝑁)) / 𝑢𝐴 ∈ ℤ
16 csbeq1a 3671 . . . . . . . 8 (𝑢 = (𝑡 ↾ (1...𝑁)) → 𝐴 = (𝑡 ↾ (1...𝑁)) / 𝑢𝐴)
1716eleq1d 2812 . . . . . . 7 (𝑢 = (𝑡 ↾ (1...𝑁)) → (𝐴 ∈ ℤ ↔ (𝑡 ↾ (1...𝑁)) / 𝑢𝐴 ∈ ℤ))
1815, 17rspc 3431 . . . . . 6 ((𝑡 ↾ (1...𝑁)) ∈ (ℤ ↑𝑚 (1...𝑁)) → (∀𝑢 ∈ (ℤ ↑𝑚 (1...𝑁))𝐴 ∈ ℤ → (𝑡 ↾ (1...𝑁)) / 𝑢𝐴 ∈ ℤ))
198, 13, 18sylc 65 . . . . 5 (((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℤ ↑𝑚 (1...𝑀))) → (𝑡 ↾ (1...𝑁)) / 𝑢𝐴 ∈ ℤ)
20 csbeq1 3665 . . . . . 6 (𝑎 = (𝑡 ↾ (1...𝑁)) → 𝑎 / 𝑢𝐴 = (𝑡 ↾ (1...𝑁)) / 𝑢𝐴)
21 eqid 2748 . . . . . 6 (𝑎 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝑎 / 𝑢𝐴) = (𝑎 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝑎 / 𝑢𝐴)
2220, 21fvmptg 6430 . . . . 5 (((𝑡 ↾ (1...𝑁)) ∈ (ℤ ↑𝑚 (1...𝑁)) ∧ (𝑡 ↾ (1...𝑁)) / 𝑢𝐴 ∈ ℤ) → ((𝑎 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝑎 / 𝑢𝐴)‘(𝑡 ↾ (1...𝑁))) = (𝑡 ↾ (1...𝑁)) / 𝑢𝐴)
238, 19, 22syl2anc 696 . . . 4 (((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℤ ↑𝑚 (1...𝑀))) → ((𝑎 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝑎 / 𝑢𝐴)‘(𝑡 ↾ (1...𝑁))) = (𝑡 ↾ (1...𝑁)) / 𝑢𝐴)
245, 23syl5req 2795 . . 3 (((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) ∧ 𝑡 ∈ (ℤ ↑𝑚 (1...𝑀))) → (𝑡 ↾ (1...𝑁)) / 𝑢𝐴 = ((𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴)‘(𝑡 ↾ (1...𝑁))))
2524mpteq2dva 4884 . 2 ((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚 (1...𝑀)) ↦ (𝑡 ↾ (1...𝑁)) / 𝑢𝐴) = (𝑡 ∈ (ℤ ↑𝑚 (1...𝑀)) ↦ ((𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴)‘(𝑡 ↾ (1...𝑁)))))
26 ovexd 6831 . . 3 ((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (1...𝑀) ∈ V)
27 fzssp1 12548 . . . . 5 (1...𝑁) ⊆ (1...(𝑁 + 1))
286oveq2i 6812 . . . . 5 (1...𝑀) = (1...(𝑁 + 1))
2927, 28sseqtr4i 3767 . . . 4 (1...𝑁) ⊆ (1...𝑀)
3029a1i 11 . . 3 ((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (1...𝑁) ⊆ (1...𝑀))
31 simpr 479 . . 3 ((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁)))
32 mzpresrename 37784 . . 3 (((1...𝑀) ∈ V ∧ (1...𝑁) ⊆ (1...𝑀) ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚 (1...𝑀)) ↦ ((𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴)‘(𝑡 ↾ (1...𝑁)))) ∈ (mzPoly‘(1...𝑀)))
3326, 30, 31, 32syl3anc 1463 . 2 ((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚 (1...𝑀)) ↦ ((𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴)‘(𝑡 ↾ (1...𝑁)))) ∈ (mzPoly‘(1...𝑀)))
3425, 33eqeltrd 2827 1 ((𝑁 ∈ ℕ0 ∧ (𝑢 ∈ (ℤ ↑𝑚 (1...𝑁)) ↦ 𝐴) ∈ (mzPoly‘(1...𝑁))) → (𝑡 ∈ (ℤ ↑𝑚 (1...𝑀)) ↦ (𝑡 ↾ (1...𝑁)) / 𝑢𝐴) ∈ (mzPoly‘(1...𝑀)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   = wceq 1620   ∈ wcel 2127  ∀wral 3038  Vcvv 3328  ⦋csb 3662   ⊆ wss 3703   ↦ cmpt 4869   ↾ cres 5256  ⟶wf 6033  ‘cfv 6037  (class class class)co 6801   ↑𝑚 cmap 8011  1c1 10100   + caddc 10102  ℕ0cn0 11455  ℤcz 11540  ...cfz 12490  mzPolycmzp 37756 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-rep 4911  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043  ax-un 7102  ax-cnex 10155  ax-resscn 10156  ax-1cn 10157  ax-icn 10158  ax-addcl 10159  ax-addrcl 10160  ax-mulcl 10161  ax-mulrcl 10162  ax-mulcom 10163  ax-addass 10164  ax-mulass 10165  ax-distr 10166  ax-i2m1 10167  ax-1ne0 10168  ax-1rid 10169  ax-rnegex 10170  ax-rrecex 10171  ax-cnre 10172  ax-pre-lttri 10173  ax-pre-lttrn 10174  ax-pre-ltadd 10175  ax-pre-mulgt0 10176 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ne 2921  df-nel 3024  df-ral 3043  df-rex 3044  df-reu 3045  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-pss 3719  df-nul 4047  df-if 4219  df-pw 4292  df-sn 4310  df-pr 4312  df-tp 4314  df-op 4316  df-uni 4577  df-int 4616  df-iun 4662  df-br 4793  df-opab 4853  df-mpt 4870  df-tr 4893  df-id 5162  df-eprel 5167  df-po 5175  df-so 5176  df-fr 5213  df-we 5215  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-pred 5829  df-ord 5875  df-on 5876  df-lim 5877  df-suc 5878  df-iota 6000  df-fun 6039  df-fn 6040  df-f 6041  df-f1 6042  df-fo 6043  df-f1o 6044  df-fv 6045  df-riota 6762  df-ov 6804  df-oprab 6805  df-mpt2 6806  df-of 7050  df-om 7219  df-1st 7321  df-2nd 7322  df-wrecs 7564  df-recs 7625  df-rdg 7663  df-er 7899  df-map 8013  df-en 8110  df-dom 8111  df-sdom 8112  df-pnf 10239  df-mnf 10240  df-xr 10241  df-ltxr 10242  df-le 10243  df-sub 10431  df-neg 10432  df-nn 11184  df-n0 11456  df-z 11541  df-uz 11851  df-fz 12491  df-mzpcl 37757  df-mzp 37758 This theorem is referenced by:  elnn0rabdioph  37838  dvdsrabdioph  37845
 Copyright terms: Public domain W3C validator