Step | Hyp | Ref
| Expression |
1 | | simpl3 1194 |
. . . . . 6
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β (degβπ) < (degAAβπ΄)) |
2 | | simpl2 1193 |
. . . . . . . . 9
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β π β
(Polyββ)) |
3 | | dgrcl 25610 |
. . . . . . . . 9
β’ (π β (Polyββ)
β (degβπ) β
β0) |
4 | 2, 3 | syl 17 |
. . . . . . . 8
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β (degβπ) β
β0) |
5 | 4 | nn0red 12479 |
. . . . . . 7
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β (degβπ) β β) |
6 | | simpl1 1192 |
. . . . . . . . 9
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β π΄ β πΈ) |
7 | | dgraacl 41516 |
. . . . . . . . 9
β’ (π΄ β πΈ β
(degAAβπ΄)
β β) |
8 | 6, 7 | syl 17 |
. . . . . . . 8
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β (degAAβπ΄) β β) |
9 | 8 | nnred 12173 |
. . . . . . 7
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β (degAAβπ΄) β β) |
10 | 5, 9 | ltnled 11307 |
. . . . . 6
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β ((degβπ) < (degAAβπ΄) β Β¬
(degAAβπ΄)
β€ (degβπ))) |
11 | 1, 10 | mpbid 231 |
. . . . 5
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β Β¬ (degAAβπ΄) β€ (degβπ)) |
12 | | simpl2 1193 |
. . . . . . 7
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ (π β
0π β§ (πβπ΄) = 0)) β π β
(Polyββ)) |
13 | | simprl 770 |
. . . . . . 7
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ (π β
0π β§ (πβπ΄) = 0)) β π β
0π) |
14 | | simpl1 1192 |
. . . . . . . 8
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ (π β
0π β§ (πβπ΄) = 0)) β π΄ β πΈ) |
15 | | aacn 25693 |
. . . . . . . 8
β’ (π΄ β πΈ β π΄ β
β) |
16 | 14, 15 | syl 17 |
. . . . . . 7
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ (π β
0π β§ (πβπ΄) = 0)) β π΄ β β) |
17 | | simprr 772 |
. . . . . . 7
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ (π β
0π β§ (πβπ΄) = 0)) β (πβπ΄) = 0) |
18 | | dgraaub 41518 |
. . . . . . 7
β’ (((π β (Polyββ)
β§ π β
0π) β§ (π΄ β β β§ (πβπ΄) = 0)) β (degAAβπ΄) β€ (degβπ)) |
19 | 12, 13, 16, 17, 18 | syl22anc 838 |
. . . . . 6
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ (π β
0π β§ (πβπ΄) = 0)) β (degAAβπ΄) β€ (degβπ)) |
20 | 19 | expr 458 |
. . . . 5
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β ((πβπ΄) = 0 β (degAAβπ΄) β€ (degβπ))) |
21 | 11, 20 | mtod 197 |
. . . 4
β’ (((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β§ π β
0π) β Β¬ (πβπ΄) = 0) |
22 | 21 | ex 414 |
. . 3
β’ ((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β (π β
0π β Β¬ (πβπ΄) = 0)) |
23 | 22 | necon4ad 2959 |
. 2
β’ ((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β ((πβπ΄) = 0 β π = 0π)) |
24 | | 0pval 25051 |
. . . . 5
β’ (π΄ β β β
(0πβπ΄) = 0) |
25 | 15, 24 | syl 17 |
. . . 4
β’ (π΄ β πΈ β
(0πβπ΄) = 0) |
26 | | fveq1 6842 |
. . . . 5
β’ (π = 0π β
(πβπ΄) = (0πβπ΄)) |
27 | 26 | eqeq1d 2735 |
. . . 4
β’ (π = 0π β
((πβπ΄) = 0 β
(0πβπ΄) = 0)) |
28 | 25, 27 | syl5ibrcom 247 |
. . 3
β’ (π΄ β πΈ β (π = 0π β
(πβπ΄) = 0)) |
29 | 28 | 3ad2ant1 1134 |
. 2
β’ ((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β (π =
0π β (πβπ΄) = 0)) |
30 | 23, 29 | impbid 211 |
1
β’ ((π΄ β πΈ β§ π β (Polyββ)
β§ (degβπ) <
(degAAβπ΄))
β ((πβπ΄) = 0 β π = 0π)) |