This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem plyeq0

Description: If a polynomial is zero at every point (or even just zero at the positive integers), then all the coefficients must be zero. This is the basis for the method of equating coefficients of equal polynomials, and ensures that df-coe is well-defined. (Contributed by Mario Carneiro, 22-Jul-2014)

Ref Expression
Hypotheses plyeq0.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
plyeq0.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
plyeq0.3 ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
plyeq0.4 ⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
plyeq0.5 ⊢ ( 𝜑 → 0𝑝 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
Assertion plyeq0 ( 𝜑 → 𝐴 = ( ℕ0 × { 0 } ) )

Proof

Step Hyp Ref Expression
1 plyeq0.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2 plyeq0.2 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
3 plyeq0.3 ⊢ ( 𝜑 → 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
4 plyeq0.4 ⊢ ( 𝜑 → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
5 plyeq0.5 ⊢ ( 𝜑 → 0𝑝 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
6 0cnd ⊢ ( 𝜑 → 0 ∈ ℂ )
7 6 snssd ⊢ ( 𝜑 → { 0 } ⊆ ℂ )
8 1 7 unssd ⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ⊆ ℂ )
9 cnex ⊢ ℂ ∈ V
10 ssexg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ⊆ ℂ ∧ ℂ ∈ V ) → ( 𝑆 ∪ { 0 } ) ∈ V )
11 8 9 10 sylancl ⊢ ( 𝜑 → ( 𝑆 ∪ { 0 } ) ∈ V )
12 nn0ex ⊢ ℕ0 ∈ V
13 elmapg ⊢ ( ( ( 𝑆 ∪ { 0 } ) ∈ V ∧ ℕ0 ∈ V ) → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
14 11 12 13 sylancl ⊢ ( 𝜑 → ( 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) ↔ 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) ) )
15 3 14 mpbid ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) )
16 15 ffnd ⊢ ( 𝜑 → 𝐴 Fn ℕ0 )
17 imadmrn ⊢ ( 𝐴 “ dom 𝐴 ) = ran 𝐴
18 fdm ⊢ ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) → dom 𝐴 = ℕ0 )
19 fimacnv ⊢ ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) → ( ◡ 𝐴 “ ( 𝑆 ∪ { 0 } ) ) = ℕ0 )
20 18 19 eqtr4d ⊢ ( 𝐴 : ℕ0 ⟶ ( 𝑆 ∪ { 0 } ) → dom 𝐴 = ( ◡ 𝐴 “ ( 𝑆 ∪ { 0 } ) ) )
21 15 20 syl ⊢ ( 𝜑 → dom 𝐴 = ( ◡ 𝐴 “ ( 𝑆 ∪ { 0 } ) ) )
22 simpr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) = ∅ ) → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) = ∅ )
23 1 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → 𝑆 ⊆ ℂ )
24 2 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → 𝑁 ∈ ℕ0 )
25 3 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → 𝐴 ∈ ( ( 𝑆 ∪ { 0 } ) ↑m ℕ0 ) )
26 4 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → ( 𝐴 “ ( ℤ≥ ‘ ( 𝑁 + 1 ) ) ) = { 0 } )
27 5 adantr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → 0𝑝 = ( 𝑧 ∈ ℂ ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝐴 ‘ 𝑘 ) · ( 𝑧 ↑ 𝑘 ) ) ) )
28 eqid ⊢ sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < ) = sup ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) , ℝ , < )
29 simpr ⊢ ( ( 𝜑 ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ )
30 23 24 25 26 27 28 29 plyeq0lem ⊢ ¬ ( 𝜑 ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ )
31 30 pm2.21i ⊢ ( ( 𝜑 ∧ ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ≠ ∅ ) → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) = ∅ )
32 22 31 pm2.61dane ⊢ ( 𝜑 → ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) = ∅ )
33 32 uneq1d ⊢ ( 𝜑 → ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ∪ ( ◡ 𝐴 “ { 0 } ) ) = ( ∅ ∪ ( ◡ 𝐴 “ { 0 } ) ) )
34 undif1 ⊢ ( ( 𝑆 ∖ { 0 } ) ∪ { 0 } ) = ( 𝑆 ∪ { 0 } )
35 34 imaeq2i ⊢ ( ◡ 𝐴 “ ( ( 𝑆 ∖ { 0 } ) ∪ { 0 } ) ) = ( ◡ 𝐴 “ ( 𝑆 ∪ { 0 } ) )
36 imaundi ⊢ ( ◡ 𝐴 “ ( ( 𝑆 ∖ { 0 } ) ∪ { 0 } ) ) = ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ∪ ( ◡ 𝐴 “ { 0 } ) )
37 35 36 eqtr3i ⊢ ( ◡ 𝐴 “ ( 𝑆 ∪ { 0 } ) ) = ( ( ◡ 𝐴 “ ( 𝑆 ∖ { 0 } ) ) ∪ ( ◡ 𝐴 “ { 0 } ) )
38 un0 ⊢ ( ( ◡ 𝐴 “ { 0 } ) ∪ ∅ ) = ( ◡ 𝐴 “ { 0 } )
39 uncom ⊢ ( ( ◡ 𝐴 “ { 0 } ) ∪ ∅ ) = ( ∅ ∪ ( ◡ 𝐴 “ { 0 } ) )
40 38 39 eqtr3i ⊢ ( ◡ 𝐴 “ { 0 } ) = ( ∅ ∪ ( ◡ 𝐴 “ { 0 } ) )
41 33 37 40 3eqtr4g ⊢ ( 𝜑 → ( ◡ 𝐴 “ ( 𝑆 ∪ { 0 } ) ) = ( ◡ 𝐴 “ { 0 } ) )
42 21 41 eqtrd ⊢ ( 𝜑 → dom 𝐴 = ( ◡ 𝐴 “ { 0 } ) )
43 eqimss ⊢ ( dom 𝐴 = ( ◡ 𝐴 “ { 0 } ) → dom 𝐴 ⊆ ( ◡ 𝐴 “ { 0 } ) )
44 42 43 syl ⊢ ( 𝜑 → dom 𝐴 ⊆ ( ◡ 𝐴 “ { 0 } ) )
45 15 ffund ⊢ ( 𝜑 → Fun 𝐴 )
46 ssid ⊢ dom 𝐴 ⊆ dom 𝐴
47 funimass3 ⊢ ( ( Fun 𝐴 ∧ dom 𝐴 ⊆ dom 𝐴 ) → ( ( 𝐴 “ dom 𝐴 ) ⊆ { 0 } ↔ dom 𝐴 ⊆ ( ◡ 𝐴 “ { 0 } ) ) )
48 45 46 47 sylancl ⊢ ( 𝜑 → ( ( 𝐴 “ dom 𝐴 ) ⊆ { 0 } ↔ dom 𝐴 ⊆ ( ◡ 𝐴 “ { 0 } ) ) )
49 44 48 mpbird ⊢ ( 𝜑 → ( 𝐴 “ dom 𝐴 ) ⊆ { 0 } )
50 17 49 eqsstrrid ⊢ ( 𝜑 → ran 𝐴 ⊆ { 0 } )
51 df-f ⊢ ( 𝐴 : ℕ0 ⟶ { 0 } ↔ ( 𝐴 Fn ℕ0 ∧ ran 𝐴 ⊆ { 0 } ) )
52 16 50 51 sylanbrc ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ { 0 } )
53 c0ex ⊢ 0 ∈ V
54 53 fconst2 ⊢ ( 𝐴 : ℕ0 ⟶ { 0 } ↔ 𝐴 = ( ℕ0 × { 0 } ) )
55 52 54 sylib ⊢ ( 𝜑 → 𝐴 = ( ℕ0 × { 0 } ) )