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 syl5ibr ( ( ( 𝐹 ∈ ( 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 ) ) )