Metamath Proof Explorer

Theorem dgrlt

Description: Two ways to say that the degree of F is strictly less than N . (Contributed by Mario Carneiro, 25-Jul-2014)

Ref Expression
Hypotheses dgreq0.1 ⊢ 𝑁 = ( deg ‘ 𝐹 )
dgreq0.2 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
Assertion dgrlt ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐹 = 0𝑝 ∨ 𝑁 < 𝑀 ) ↔ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) )

Proof

Step Hyp Ref Expression
1 dgreq0.1 ⊢ 𝑁 = ( deg ‘ 𝐹 )
2 dgreq0.2 ⊢ 𝐴 = ( coeff ‘ 𝐹 )
3 simpr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → 𝐹 = 0𝑝 )
4 3 fveq2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → ( deg ‘ 𝐹 ) = ( deg ‘ 0𝑝 ) )
5 dgr0 ⊢ ( deg ‘ 0𝑝 ) = 0
6 5 eqcomi ⊢ 0 = ( deg ‘ 0𝑝 )
7 4 1 6 3eqtr4g ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → 𝑁 = 0 )
8 nn0ge0 ⊢ ( 𝑀 ∈ ℕ0 → 0 ≤ 𝑀 )
9 8 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → 0 ≤ 𝑀 )
10 7 9 eqbrtrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → 𝑁 ≤ 𝑀 )
11 3 fveq2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → ( coeff ‘ 𝐹 ) = ( coeff ‘ 0𝑝 ) )
12 coe0 ⊢ ( coeff ‘ 0𝑝 ) = ( ℕ0 × { 0 } )
13 12 eqcomi ⊢ ( ℕ0 × { 0 } ) = ( coeff ‘ 0𝑝 )
14 11 2 13 3eqtr4g ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → 𝐴 = ( ℕ0 × { 0 } ) )
15 14 fveq1d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → ( 𝐴 ‘ 𝑀 ) = ( ( ℕ0 × { 0 } ) ‘ 𝑀 ) )
16 c0ex ⊢ 0 ∈ V
17 16 fvconst2 ⊢ ( 𝑀 ∈ ℕ0 → ( ( ℕ0 × { 0 } ) ‘ 𝑀 ) = 0 )
18 17 ad2antlr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → ( ( ℕ0 × { 0 } ) ‘ 𝑀 ) = 0 )
19 15 18 eqtrd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → ( 𝐴 ‘ 𝑀 ) = 0 )
20 10 19 jca ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝐹 = 0𝑝 ) → ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) )
21 dgrcl ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( deg ‘ 𝐹 ) ∈ ℕ0 )
22 1 21 eqeltrid ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℕ0 )
23 22 nn0red ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → 𝑁 ∈ ℝ )
24 nn0re ⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℝ )
25 ltle ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑁 < 𝑀 → 𝑁 ≤ 𝑀 ) )
26 23 24 25 syl2an ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 < 𝑀 → 𝑁 ≤ 𝑀 ) )
27 26 imp ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 < 𝑀 ) → 𝑁 ≤ 𝑀 )
28 2 1 dgrub ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ∧ ( 𝐴 ‘ 𝑀 ) ≠ 0 ) → 𝑀 ≤ 𝑁 )
29 28 3expia ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑀 ) ≠ 0 → 𝑀 ≤ 𝑁 ) )
30 lenlt ⊢ ( ( 𝑀 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
31 24 23 30 syl2anr ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 ≤ 𝑁 ↔ ¬ 𝑁 < 𝑀 ) )
32 29 31 sylibd ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐴 ‘ 𝑀 ) ≠ 0 → ¬ 𝑁 < 𝑀 ) )
33 32 necon4ad ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 < 𝑀 → ( 𝐴 ‘ 𝑀 ) = 0 ) )
34 33 imp ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 < 𝑀 ) → ( 𝐴 ‘ 𝑀 ) = 0 )
35 27 34 jca ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 < 𝑀 ) → ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) )
36 20 35 jaodan ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝐹 = 0𝑝 ∨ 𝑁 < 𝑀 ) ) → ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) )
37 leloe ⊢ ( ( 𝑁 ∈ ℝ ∧ 𝑀 ∈ ℝ ) → ( 𝑁 ≤ 𝑀 ↔ ( 𝑁 < 𝑀 ∨ 𝑁 = 𝑀 ) ) )
38 23 24 37 syl2an ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → ( 𝑁 ≤ 𝑀 ↔ ( 𝑁 < 𝑀 ∨ 𝑁 = 𝑀 ) ) )
39 38 biimpa ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑁 ≤ 𝑀 ) → ( 𝑁 < 𝑀 ∨ 𝑁 = 𝑀 ) )
40 39 adantrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) → ( 𝑁 < 𝑀 ∨ 𝑁 = 𝑀 ) )
41 fveq2 ⊢ ( 𝑁 = 𝑀 → ( 𝐴 ‘ 𝑁 ) = ( 𝐴 ‘ 𝑀 ) )
42 1 2 dgreq0 ⊢ ( 𝐹 ∈ ( Poly ‘ 𝑆 ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )
43 42 ad2antrr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )
44 simprr ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) → ( 𝐴 ‘ 𝑀 ) = 0 )
45 44 eqeq2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) → ( ( 𝐴 ‘ 𝑁 ) = ( 𝐴 ‘ 𝑀 ) ↔ ( 𝐴 ‘ 𝑁 ) = 0 ) )
46 43 45 bitr4d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) → ( 𝐹 = 0𝑝 ↔ ( 𝐴 ‘ 𝑁 ) = ( 𝐴 ‘ 𝑀 ) ) )
47 41 46 imbitrrid ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) → ( 𝑁 = 𝑀 → 𝐹 = 0𝑝 ) )
48 47 orim2d ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) → ( ( 𝑁 < 𝑀 ∨ 𝑁 = 𝑀 ) → ( 𝑁 < 𝑀 ∨ 𝐹 = 0𝑝 ) ) )
49 40 48 mpd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) → ( 𝑁 < 𝑀 ∨ 𝐹 = 0𝑝 ) )
50 49 orcomd ⊢ ( ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) ∧ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) → ( 𝐹 = 0𝑝 ∨ 𝑁 < 𝑀 ) )
51 36 50 impbida ⊢ ( ( 𝐹 ∈ ( Poly ‘ 𝑆 ) ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐹 = 0𝑝 ∨ 𝑁 < 𝑀 ) ↔ ( 𝑁 ≤ 𝑀 ∧ ( 𝐴 ‘ 𝑀 ) = 0 ) ) )