Metamath Proof Explorer

Theorem rabdiophlem2

Description: Lemma for arithmetic diophantine sets. Reuse a polynomial expression under a new quantifier. (Contributed by Stefan O'Rear, 10-Oct-2014)

Ref Expression
Hypothesis rabdiophlem2.1 ⊢ 𝑀 = ( 𝑁 + 1 )
Assertion rabdiophlem2 ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ↦ ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 rabdiophlem2.1 ⊢ 𝑀 = ( 𝑁 + 1 )
2 nfcv ⊢ Ⅎ 𝑎 𝐴
3 nfcsb1v ⊢ Ⅎ 𝑢 ⦋ 𝑎 / 𝑢 ⦌ 𝐴
4 csbeq1a ⊢ ( 𝑢 = 𝑎 → 𝐴 = ⦋ 𝑎 / 𝑢 ⦌ 𝐴 )
5 2 3 4 cbvmpt ⊢ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) = ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ⦋ 𝑎 / 𝑢 ⦌ 𝐴 )
6 5 fveq1i ⊢ ( ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ) = ( ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ⦋ 𝑎 / 𝑢 ⦌ 𝐴 ) ‘ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) )
7 eqid ⊢ ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ⦋ 𝑎 / 𝑢 ⦌ 𝐴 ) = ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ⦋ 𝑎 / 𝑢 ⦌ 𝐴 )
8 csbeq1 ⊢ ( 𝑎 = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) → ⦋ 𝑎 / 𝑢 ⦌ 𝐴 = ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 )
9 1 mapfzcons1cl ⊢ ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) → ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) )
10 9 adantl ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ) → ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) )
11 mzpf ⊢ ( ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ )
12 eqid ⊢ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) = ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 )
13 12 fmpt ⊢ ( ∀ 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ ↔ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) : ( ℤ ↑m ( 1 ... 𝑁 ) ) ⟶ ℤ )
14 11 13 sylibr ⊢ ( ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) → ∀ 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ )
15 14 ad2antlr ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ) → ∀ 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ )
16 nfcsb1v ⊢ Ⅎ 𝑢 ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴
17 16 nfel1 ⊢ Ⅎ 𝑢 ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 ∈ ℤ
18 csbeq1a ⊢ ( 𝑢 = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) → 𝐴 = ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 )
19 18 eleq1d ⊢ ( 𝑢 = ( 𝑡 ↾ ( 1 ... 𝑁 ) ) → ( 𝐴 ∈ ℤ ↔ ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 ∈ ℤ ) )
20 17 19 rspc ⊢ ( ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) → ( ∀ 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) 𝐴 ∈ ℤ → ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 ∈ ℤ ) )
21 10 15 20 sylc ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ) → ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 ∈ ℤ )
22 7 8 10 21 fvmptd3 ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ) → ( ( 𝑎 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ ⦋ 𝑎 / 𝑢 ⦌ 𝐴 ) ‘ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ) = ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 )
23 6 22 eqtr2id ⊢ ( ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) ∧ 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ) → ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 = ( ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ) )
24 23 mpteq2dva ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ↦ ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 ) = ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ↦ ( ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ) ) )
25 ovexd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 1 ... 𝑀 ) ∈ V )
26 fzssp1 ⊢ ( 1 ... 𝑁 ) ⊆ ( 1 ... ( 𝑁 + 1 ) )
27 1 oveq2i ⊢ ( 1 ... 𝑀 ) = ( 1 ... ( 𝑁 + 1 ) )
28 26 27 sseqtrri ⊢ ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 )
29 28 a1i ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 ) )
30 simpr ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) )
31 mzpresrename ⊢ ( ( ( 1 ... 𝑀 ) ∈ V ∧ ( 1 ... 𝑁 ) ⊆ ( 1 ... 𝑀 ) ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ↦ ( ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑀 ) ) )
32 25 29 30 31 syl3anc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ↦ ( ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ‘ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) ) ) ∈ ( mzPoly ‘ ( 1 ... 𝑀 ) ) )
33 24 32 eqeltrd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑢 ∈ ( ℤ ↑m ( 1 ... 𝑁 ) ) ↦ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑁 ) ) ) → ( 𝑡 ∈ ( ℤ ↑m ( 1 ... 𝑀 ) ) ↦ ⦋ ( 𝑡 ↾ ( 1 ... 𝑁 ) ) / 𝑢 ⦌ 𝐴 ) ∈ ( mzPoly ‘ ( 1 ... 𝑀 ) ) )