Step | Hyp | Ref
| Expression |
1 | | fveq2 6846 |
. . . . 5
โข (๐น = 0 โ (๐ทโ๐น) = (๐ทโ 0 )) |
2 | 1 | breq1d 5119 |
. . . 4
โข (๐น = 0 โ ((๐ทโ๐น) < ((๐ทโ๐บ) + ๐) โ (๐ทโ 0 ) < ((๐ทโ๐บ) + ๐))) |
3 | 2 | rexbidv 3172 |
. . 3
โข (๐น = 0 โ (โ๐ โ โ0
(๐ทโ๐น) < ((๐ทโ๐บ) + ๐) โ โ๐ โ โ0 (๐ทโ 0 ) < ((๐ทโ๐บ) + ๐))) |
4 | | nnssnn0 12424 |
. . . . 5
โข โ
โ โ0 |
5 | | ply1divalg.r1 |
. . . . . . . . . 10
โข (๐ โ ๐
โ Ring) |
6 | 5 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐น โ 0 ) โ ๐
โ Ring) |
7 | | ply1divalg.f |
. . . . . . . . . 10
โข (๐ โ ๐น โ ๐ต) |
8 | 7 | adantr 482 |
. . . . . . . . 9
โข ((๐ โง ๐น โ 0 ) โ ๐น โ ๐ต) |
9 | | simpr 486 |
. . . . . . . . 9
โข ((๐ โง ๐น โ 0 ) โ ๐น โ 0 ) |
10 | | ply1divalg.d |
. . . . . . . . . 10
โข ๐ท = ( deg1
โ๐
) |
11 | | ply1divalg.p |
. . . . . . . . . 10
โข ๐ = (Poly1โ๐
) |
12 | | ply1divalg.z |
. . . . . . . . . 10
โข 0 =
(0gโ๐) |
13 | | ply1divalg.b |
. . . . . . . . . 10
โข ๐ต = (Baseโ๐) |
14 | 10, 11, 12, 13 | deg1nn0cl 25476 |
. . . . . . . . 9
โข ((๐
โ Ring โง ๐น โ ๐ต โง ๐น โ 0 ) โ (๐ทโ๐น) โ
โ0) |
15 | 6, 8, 9, 14 | syl3anc 1372 |
. . . . . . . 8
โข ((๐ โง ๐น โ 0 ) โ (๐ทโ๐น) โ
โ0) |
16 | 15 | nn0red 12482 |
. . . . . . 7
โข ((๐ โง ๐น โ 0 ) โ (๐ทโ๐น) โ โ) |
17 | | ply1divalg.g1 |
. . . . . . . . . 10
โข (๐ โ ๐บ โ ๐ต) |
18 | | ply1divalg.g2 |
. . . . . . . . . 10
โข (๐ โ ๐บ โ 0 ) |
19 | 10, 11, 12, 13 | deg1nn0cl 25476 |
. . . . . . . . . 10
โข ((๐
โ Ring โง ๐บ โ ๐ต โง ๐บ โ 0 ) โ (๐ทโ๐บ) โ
โ0) |
20 | 5, 17, 18, 19 | syl3anc 1372 |
. . . . . . . . 9
โข (๐ โ (๐ทโ๐บ) โ
โ0) |
21 | 20 | nn0red 12482 |
. . . . . . . 8
โข (๐ โ (๐ทโ๐บ) โ โ) |
22 | 21 | adantr 482 |
. . . . . . 7
โข ((๐ โง ๐น โ 0 ) โ (๐ทโ๐บ) โ โ) |
23 | 16, 22 | resubcld 11591 |
. . . . . 6
โข ((๐ โง ๐น โ 0 ) โ ((๐ทโ๐น) โ (๐ทโ๐บ)) โ โ) |
24 | | arch 12418 |
. . . . . 6
โข (((๐ทโ๐น) โ (๐ทโ๐บ)) โ โ โ โ๐ โ โ ((๐ทโ๐น) โ (๐ทโ๐บ)) < ๐) |
25 | 23, 24 | syl 17 |
. . . . 5
โข ((๐ โง ๐น โ 0 ) โ โ๐ โ โ ((๐ทโ๐น) โ (๐ทโ๐บ)) < ๐) |
26 | | ssrexv 4015 |
. . . . 5
โข (โ
โ โ0 โ (โ๐ โ โ ((๐ทโ๐น) โ (๐ทโ๐บ)) < ๐ โ โ๐ โ โ0 ((๐ทโ๐น) โ (๐ทโ๐บ)) < ๐)) |
27 | 4, 25, 26 | mpsyl 68 |
. . . 4
โข ((๐ โง ๐น โ 0 ) โ โ๐ โ โ0
((๐ทโ๐น) โ (๐ทโ๐บ)) < ๐) |
28 | 16 | adantr 482 |
. . . . . . 7
โข (((๐ โง ๐น โ 0 ) โง ๐ โ โ0) โ (๐ทโ๐น) โ โ) |
29 | 21 | ad2antrr 725 |
. . . . . . 7
โข (((๐ โง ๐น โ 0 ) โง ๐ โ โ0) โ (๐ทโ๐บ) โ โ) |
30 | | nn0re 12430 |
. . . . . . . 8
โข (๐ โ โ0
โ ๐ โ
โ) |
31 | 30 | adantl 483 |
. . . . . . 7
โข (((๐ โง ๐น โ 0 ) โง ๐ โ โ0) โ ๐ โ
โ) |
32 | 28, 29, 31 | ltsubadd2d 11761 |
. . . . . 6
โข (((๐ โง ๐น โ 0 ) โง ๐ โ โ0) โ (((๐ทโ๐น) โ (๐ทโ๐บ)) < ๐ โ (๐ทโ๐น) < ((๐ทโ๐บ) + ๐))) |
33 | 32 | biimpd 228 |
. . . . 5
โข (((๐ โง ๐น โ 0 ) โง ๐ โ โ0) โ (((๐ทโ๐น) โ (๐ทโ๐บ)) < ๐ โ (๐ทโ๐น) < ((๐ทโ๐บ) + ๐))) |
34 | 33 | reximdva 3162 |
. . . 4
โข ((๐ โง ๐น โ 0 ) โ (โ๐ โ โ0
((๐ทโ๐น) โ (๐ทโ๐บ)) < ๐ โ โ๐ โ โ0 (๐ทโ๐น) < ((๐ทโ๐บ) + ๐))) |
35 | 27, 34 | mpd 15 |
. . 3
โข ((๐ โง ๐น โ 0 ) โ โ๐ โ โ0
(๐ทโ๐น) < ((๐ทโ๐บ) + ๐)) |
36 | | 0nn0 12436 |
. . . 4
โข 0 โ
โ0 |
37 | 10, 11, 12 | deg1z 25475 |
. . . . . 6
โข (๐
โ Ring โ (๐ทโ 0 ) =
-โ) |
38 | 5, 37 | syl 17 |
. . . . 5
โข (๐ โ (๐ทโ 0 ) =
-โ) |
39 | | 0re 11165 |
. . . . . . 7
โข 0 โ
โ |
40 | | readdcl 11142 |
. . . . . . 7
โข (((๐ทโ๐บ) โ โ โง 0 โ โ)
โ ((๐ทโ๐บ) + 0) โ
โ) |
41 | 21, 39, 40 | sylancl 587 |
. . . . . 6
โข (๐ โ ((๐ทโ๐บ) + 0) โ โ) |
42 | 41 | mnfltd 13053 |
. . . . 5
โข (๐ โ -โ < ((๐ทโ๐บ) + 0)) |
43 | 38, 42 | eqbrtrd 5131 |
. . . 4
โข (๐ โ (๐ทโ 0 ) < ((๐ทโ๐บ) + 0)) |
44 | | oveq2 7369 |
. . . . . 6
โข (๐ = 0 โ ((๐ทโ๐บ) + ๐) = ((๐ทโ๐บ) + 0)) |
45 | 44 | breq2d 5121 |
. . . . 5
โข (๐ = 0 โ ((๐ทโ 0 ) < ((๐ทโ๐บ) + ๐) โ (๐ทโ 0 ) < ((๐ทโ๐บ) + 0))) |
46 | 45 | rspcev 3583 |
. . . 4
โข ((0
โ โ0 โง (๐ทโ 0 ) < ((๐ทโ๐บ) + 0)) โ โ๐ โ โ0 (๐ทโ 0 ) < ((๐ทโ๐บ) + ๐)) |
47 | 36, 43, 46 | sylancr 588 |
. . 3
โข (๐ โ โ๐ โ โ0 (๐ทโ 0 ) < ((๐ทโ๐บ) + ๐)) |
48 | 3, 35, 47 | pm2.61ne 3027 |
. 2
โข (๐ โ โ๐ โ โ0 (๐ทโ๐น) < ((๐ทโ๐บ) + ๐)) |
49 | | fveq2 6846 |
. . . . . 6
โข (๐ = ๐น โ (๐ทโ๐) = (๐ทโ๐น)) |
50 | 49 | breq1d 5119 |
. . . . 5
โข (๐ = ๐น โ ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ (๐ทโ๐น) < ((๐ทโ๐บ) + ๐))) |
51 | | fvoveq1 7384 |
. . . . . . 7
โข (๐ = ๐น โ (๐ทโ(๐ โ (๐บ โ ๐))) = (๐ทโ(๐น โ (๐บ โ ๐)))) |
52 | 51 | breq1d 5119 |
. . . . . 6
โข (๐ = ๐น โ ((๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ (๐ทโ(๐น โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
53 | 52 | rexbidv 3172 |
. . . . 5
โข (๐ = ๐น โ (โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ โ๐ โ ๐ต (๐ทโ(๐น โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
54 | 50, 53 | imbi12d 345 |
. . . 4
โข (๐ = ๐น โ (((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ ((๐ทโ๐น) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐น โ (๐บ โ ๐))) < (๐ทโ๐บ)))) |
55 | | oveq2 7369 |
. . . . . . . . . 10
โข (๐ = 0 โ ((๐ทโ๐บ) + ๐) = ((๐ทโ๐บ) + 0)) |
56 | 55 | breq2d 5121 |
. . . . . . . . 9
โข (๐ = 0 โ ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ (๐ทโ๐) < ((๐ทโ๐บ) + 0))) |
57 | 56 | imbi1d 342 |
. . . . . . . 8
โข (๐ = 0 โ (((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ ((๐ทโ๐) < ((๐ทโ๐บ) + 0) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) |
58 | 57 | ralbidv 3171 |
. . . . . . 7
โข (๐ = 0 โ (โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + 0) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) |
59 | 58 | imbi2d 341 |
. . . . . 6
โข (๐ = 0 โ ((๐ โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) โ (๐ โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + 0) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))))) |
60 | | oveq2 7369 |
. . . . . . . . . 10
โข (๐ = ๐ โ ((๐ทโ๐บ) + ๐) = ((๐ทโ๐บ) + ๐)) |
61 | 60 | breq2d 5121 |
. . . . . . . . 9
โข (๐ = ๐ โ ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ (๐ทโ๐) < ((๐ทโ๐บ) + ๐))) |
62 | 61 | imbi1d 342 |
. . . . . . . 8
โข (๐ = ๐ โ (((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) |
63 | 62 | ralbidv 3171 |
. . . . . . 7
โข (๐ = ๐ โ (โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) |
64 | 63 | imbi2d 341 |
. . . . . 6
โข (๐ = ๐ โ ((๐ โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) โ (๐ โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))))) |
65 | | oveq2 7369 |
. . . . . . . . . 10
โข (๐ = (๐ + 1) โ ((๐ทโ๐บ) + ๐) = ((๐ทโ๐บ) + (๐ + 1))) |
66 | 65 | breq2d 5121 |
. . . . . . . . 9
โข (๐ = (๐ + 1) โ ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) |
67 | 66 | imbi1d 342 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) |
68 | 67 | ralbidv 3171 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) |
69 | 68 | imbi2d 341 |
. . . . . 6
โข (๐ = (๐ + 1) โ ((๐ โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) โ (๐ โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))))) |
70 | 11 | ply1ring 21642 |
. . . . . . . . . . . 12
โข (๐
โ Ring โ ๐ โ Ring) |
71 | 5, 70 | syl 17 |
. . . . . . . . . . 11
โข (๐ โ ๐ โ Ring) |
72 | 13, 12 | ring0cl 19998 |
. . . . . . . . . . 11
โข (๐ โ Ring โ 0 โ ๐ต) |
73 | 71, 72 | syl 17 |
. . . . . . . . . 10
โข (๐ โ 0 โ ๐ต) |
74 | 73 | ad2antrr 725 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ต) โง (๐ทโ๐) < ((๐ทโ๐บ) + 0)) โ 0 โ ๐ต) |
75 | | ply1divalg.t |
. . . . . . . . . . . . . . . . 17
โข โ =
(.rโ๐) |
76 | 13, 75, 12 | ringrz 20020 |
. . . . . . . . . . . . . . . 16
โข ((๐ โ Ring โง ๐บ โ ๐ต) โ (๐บ โ 0 ) = 0 ) |
77 | 71, 17, 76 | syl2anc 585 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐บ โ 0 ) = 0 ) |
78 | 77 | oveq2d 7377 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ โ (๐บ โ 0 )) = (๐ โ 0 )) |
79 | 78 | adantr 482 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ต) โ (๐ โ (๐บ โ 0 )) = (๐ โ 0 )) |
80 | | ringgrp 19977 |
. . . . . . . . . . . . . . 15
โข (๐ โ Ring โ ๐ โ Grp) |
81 | 71, 80 | syl 17 |
. . . . . . . . . . . . . 14
โข (๐ โ ๐ โ Grp) |
82 | | ply1divalg.m |
. . . . . . . . . . . . . . 15
โข โ =
(-gโ๐) |
83 | 13, 12, 82 | grpsubid1 18840 |
. . . . . . . . . . . . . 14
โข ((๐ โ Grp โง ๐ โ ๐ต) โ (๐ โ 0 ) = ๐) |
84 | 81, 83 | sylan 581 |
. . . . . . . . . . . . 13
โข ((๐ โง ๐ โ ๐ต) โ (๐ โ 0 ) = ๐) |
85 | 79, 84 | eqtr2d 2774 |
. . . . . . . . . . . 12
โข ((๐ โง ๐ โ ๐ต) โ ๐ = (๐ โ (๐บ โ 0 ))) |
86 | 85 | fveq2d 6850 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ต) โ (๐ทโ๐) = (๐ทโ(๐ โ (๐บ โ 0 )))) |
87 | 20 | nn0cnd 12483 |
. . . . . . . . . . . . 13
โข (๐ โ (๐ทโ๐บ) โ โ) |
88 | 87 | addid1d 11363 |
. . . . . . . . . . . 12
โข (๐ โ ((๐ทโ๐บ) + 0) = (๐ทโ๐บ)) |
89 | 88 | adantr 482 |
. . . . . . . . . . 11
โข ((๐ โง ๐ โ ๐ต) โ ((๐ทโ๐บ) + 0) = (๐ทโ๐บ)) |
90 | 86, 89 | breq12d 5122 |
. . . . . . . . . 10
โข ((๐ โง ๐ โ ๐ต) โ ((๐ทโ๐) < ((๐ทโ๐บ) + 0) โ (๐ทโ(๐ โ (๐บ โ 0 ))) < (๐ทโ๐บ))) |
91 | 90 | biimpa 478 |
. . . . . . . . 9
โข (((๐ โง ๐ โ ๐ต) โง (๐ทโ๐) < ((๐ทโ๐บ) + 0)) โ (๐ทโ(๐ โ (๐บ โ 0 ))) < (๐ทโ๐บ)) |
92 | | oveq2 7369 |
. . . . . . . . . . . . 13
โข (๐ = 0 โ (๐บ โ ๐) = (๐บ โ 0 )) |
93 | 92 | oveq2d 7377 |
. . . . . . . . . . . 12
โข (๐ = 0 โ (๐ โ (๐บ โ ๐)) = (๐ โ (๐บ โ 0 ))) |
94 | 93 | fveq2d 6850 |
. . . . . . . . . . 11
โข (๐ = 0 โ (๐ทโ(๐ โ (๐บ โ ๐))) = (๐ทโ(๐ โ (๐บ โ 0 )))) |
95 | 94 | breq1d 5119 |
. . . . . . . . . 10
โข (๐ = 0 โ ((๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ (๐ทโ(๐ โ (๐บ โ 0 ))) < (๐ทโ๐บ))) |
96 | 95 | rspcev 3583 |
. . . . . . . . 9
โข (( 0 โ ๐ต โง (๐ทโ(๐ โ (๐บ โ 0 ))) < (๐ทโ๐บ)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) |
97 | 74, 91, 96 | syl2anc 585 |
. . . . . . . 8
โข (((๐ โง ๐ โ ๐ต) โง (๐ทโ๐) < ((๐ทโ๐บ) + 0)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) |
98 | 97 | ex 414 |
. . . . . . 7
โข ((๐ โง ๐ โ ๐ต) โ ((๐ทโ๐) < ((๐ทโ๐บ) + 0) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
99 | 98 | ralrimiva 3140 |
. . . . . 6
โข (๐ โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + 0) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
100 | | nn0addcl 12456 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ทโ๐บ) โ โ0 โง ๐ โ โ0)
โ ((๐ทโ๐บ) + ๐) โ
โ0) |
101 | 20, 100 | sylan 581 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ๐ โ โ0) โ ((๐ทโ๐บ) + ๐) โ
โ0) |
102 | 101 | adantr 482 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ ((๐ทโ๐บ) + ๐) โ
โ0) |
103 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ ๐
โ Ring) |
104 | | simprl 770 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ ๐ โ ๐ต) |
105 | 10, 11, 13 | deg1cl 25471 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ต โ (๐ทโ๐) โ (โ0 โช
{-โ})) |
106 | 20 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐ทโ๐บ) โ
โ0) |
107 | | peano2nn0 12461 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐ โ โ0
โ (๐ + 1) โ
โ0) |
108 | 107 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐ + 1) โ
โ0) |
109 | 106, 108 | nn0addcld 12485 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((๐ทโ๐บ) + (๐ + 1)) โ
โ0) |
110 | 109 | nn0zd 12533 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((๐ทโ๐บ) + (๐ + 1)) โ โค) |
111 | | degltlem1 25460 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ทโ๐) โ (โ0 โช
{-โ}) โง ((๐ทโ๐บ) + (๐ + 1)) โ โค) โ ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ (๐ทโ๐) โค (((๐ทโ๐บ) + (๐ + 1)) โ 1))) |
112 | 105, 110,
111 | syl2an2 685 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ (๐ทโ๐) โค (((๐ทโ๐บ) + (๐ + 1)) โ 1))) |
113 | 112 | biimpd 228 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ (๐ทโ๐) โค (((๐ทโ๐บ) + (๐ + 1)) โ 1))) |
114 | 113 | impr 456 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (๐ทโ๐) โค (((๐ทโ๐บ) + (๐ + 1)) โ 1)) |
115 | 20 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ โ0) โ (๐ทโ๐บ) โ
โ0) |
116 | 115 | nn0cnd 12483 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โ0) โ (๐ทโ๐บ) โ โ) |
117 | | nn0cn 12431 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ โ0
โ ๐ โ
โ) |
118 | 117 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โง ๐ โ โ0) โ ๐ โ
โ) |
119 | | peano2cn 11335 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ โ โ (๐ + 1) โ
โ) |
120 | 118, 119 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โ0) โ (๐ + 1) โ
โ) |
121 | | 1cnd 11158 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โ0) โ 1 โ
โ) |
122 | 116, 120,
121 | addsubassd 11540 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โ0) โ (((๐ทโ๐บ) + (๐ + 1)) โ 1) = ((๐ทโ๐บ) + ((๐ + 1) โ 1))) |
123 | | ax-1cn 11117 |
. . . . . . . . . . . . . . . . . . . . 21
โข 1 โ
โ |
124 | | pncan 11415 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((๐ โ โ โง 1 โ
โ) โ ((๐ + 1)
โ 1) = ๐) |
125 | 118, 123,
124 | sylancl 587 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐ โง ๐ โ โ0) โ ((๐ + 1) โ 1) = ๐) |
126 | 125 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ๐ โ โ0) โ ((๐ทโ๐บ) + ((๐ + 1) โ 1)) = ((๐ทโ๐บ) + ๐)) |
127 | 122, 126 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ๐ โ โ0) โ (((๐ทโ๐บ) + (๐ + 1)) โ 1) = ((๐ทโ๐บ) + ๐)) |
128 | 127 | adantr 482 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (((๐ทโ๐บ) + (๐ + 1)) โ 1) = ((๐ทโ๐บ) + ๐)) |
129 | 114, 128 | breqtrd 5135 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (๐ทโ๐) โค ((๐ทโ๐บ) + ๐)) |
130 | 71 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐ โ Ring) |
131 | 17 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐บ โ ๐ต) |
132 | 5 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐
โ Ring) |
133 | | ply1divex.i |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ ๐ผ โ ๐พ) |
134 | 133 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐ผ โ ๐พ) |
135 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข
(coe1โ๐) = (coe1โ๐) |
136 | | ply1divex.k |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ๐พ = (Baseโ๐
) |
137 | 135, 13, 11, 136 | coe1f 21605 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ ๐ต โ (coe1โ๐):โ0โถ๐พ) |
138 | 137 | adantl 483 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (coe1โ๐):โ0โถ๐พ) |
139 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐ โ โ0) |
140 | 106, 139 | nn0addcld 12485 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((๐ทโ๐บ) + ๐) โ
โ0) |
141 | 138, 140 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((coe1โ๐)โ((๐ทโ๐บ) + ๐)) โ ๐พ) |
142 | | ply1divex.u |
. . . . . . . . . . . . . . . . . . . . 21
โข ยท =
(.rโ๐
) |
143 | 136, 142 | ringcl 19989 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐
โ Ring โง ๐ผ โ ๐พ โง ((coe1โ๐)โ((๐ทโ๐บ) + ๐)) โ ๐พ) โ (๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))) โ ๐พ) |
144 | 132, 134,
141, 143 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))) โ ๐พ) |
145 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
โข
(var1โ๐
) = (var1โ๐
) |
146 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
โข (
ยท๐ โ๐) = ( ยท๐
โ๐) |
147 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
โข
(mulGrpโ๐) =
(mulGrpโ๐) |
148 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . 20
โข
(.gโ(mulGrpโ๐)) =
(.gโ(mulGrpโ๐)) |
149 | 136, 11, 145, 146, 147, 148, 13 | ply1tmcl 21666 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐
โ Ring โง (๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))) โ ๐พ โง ๐ โ โ0) โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))) โ ๐ต) |
150 | 132, 144,
139, 149 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))) โ ๐ต) |
151 | 13, 75 | ringcl 19989 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ Ring โง ๐บ โ ๐ต โง ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))) โ ๐ต) โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ ๐ต) |
152 | 130, 131,
150, 151 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ ๐ต) |
153 | 152 | adantrr 716 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ ๐ต) |
154 | 106 | nn0red 12482 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐ทโ๐บ) โ โ) |
155 | 154 | leidd 11729 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐ทโ๐บ) โค (๐ทโ๐บ)) |
156 | 10, 136, 11, 145, 146, 147, 148 | deg1tmle 25505 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐
โ Ring โง (๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))) โ ๐พ โง ๐ โ โ0) โ (๐ทโ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โค ๐) |
157 | 132, 144,
139, 156 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐ทโ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โค ๐) |
158 | 11, 10, 132, 13, 75, 131, 150, 106, 139, 155, 157 | deg1mulle2 25497 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐ทโ(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โค ((๐ทโ๐บ) + ๐)) |
159 | 158 | adantrr 716 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (๐ทโ(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โค ((๐ทโ๐บ) + ๐)) |
160 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
โข
(coe1โ(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) =
(coe1โ(๐บ
โ
((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) |
161 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
โข
(0gโ๐
) = (0gโ๐
) |
162 | 161, 136,
11, 145, 146, 147, 148, 13, 75, 142, 131, 132, 144, 139, 106 | coe1tmmul2fv 21672 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((coe1โ(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))โ(๐ + (๐ทโ๐บ))) = (((coe1โ๐บ)โ(๐ทโ๐บ)) ยท (๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))))) |
163 | 106 | nn0cnd 12483 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐ทโ๐บ) โ โ) |
164 | 117 | ad2antlr 726 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐ โ โ) |
165 | 163, 164 | addcomd 11365 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((๐ทโ๐บ) + ๐) = (๐ + (๐ทโ๐บ))) |
166 | 165 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((coe1โ(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))โ((๐ทโ๐บ) + ๐)) = ((coe1โ(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))โ(๐ + (๐ทโ๐บ)))) |
167 | | ply1divex.g3 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ โ
(((coe1โ๐บ)โ(๐ทโ๐บ)) ยท ๐ผ) = 1 ) |
168 | 167 | oveq1d 7376 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ
((((coe1โ๐บ)โ(๐ทโ๐บ)) ยท ๐ผ) ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))) = ( 1 ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))) |
169 | 168 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((((coe1โ๐บ)โ(๐ทโ๐บ)) ยท ๐ผ) ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))) = ( 1 ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))) |
170 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . . . . . . 24
โข
(coe1โ๐บ) = (coe1โ๐บ) |
171 | 170, 13, 11, 136 | coe1f 21605 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข (๐บ โ ๐ต โ (coe1โ๐บ):โ0โถ๐พ) |
172 | 17, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
โข (๐ โ
(coe1โ๐บ):โ0โถ๐พ) |
173 | 172 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . . . . 21
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (coe1โ๐บ):โ0โถ๐พ) |
174 | 173, 106 | ffvelcdmd 7040 |
. . . . . . . . . . . . . . . . . . . 20
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((coe1โ๐บ)โ(๐ทโ๐บ)) โ ๐พ) |
175 | 136, 142 | ringass 19992 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐
โ Ring โง
(((coe1โ๐บ)โ(๐ทโ๐บ)) โ ๐พ โง ๐ผ โ ๐พ โง ((coe1โ๐)โ((๐ทโ๐บ) + ๐)) โ ๐พ)) โ ((((coe1โ๐บ)โ(๐ทโ๐บ)) ยท ๐ผ) ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))) = (((coe1โ๐บ)โ(๐ทโ๐บ)) ยท (๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))))) |
176 | 132, 174,
134, 141, 175 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((((coe1โ๐บ)โ(๐ทโ๐บ)) ยท ๐ผ) ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))) = (((coe1โ๐บ)โ(๐ทโ๐บ)) ยท (๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))))) |
177 | | ply1divex.o |
. . . . . . . . . . . . . . . . . . . . 21
โข 1 =
(1rโ๐
) |
178 | 136, 142,
177 | ringlidm 20000 |
. . . . . . . . . . . . . . . . . . . 20
โข ((๐
โ Ring โง
((coe1โ๐)โ((๐ทโ๐บ) + ๐)) โ ๐พ) โ ( 1 ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))) = ((coe1โ๐)โ((๐ทโ๐บ) + ๐))) |
179 | 132, 141,
178 | syl2anc 585 |
. . . . . . . . . . . . . . . . . . 19
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ( 1 ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))) = ((coe1โ๐)โ((๐ทโ๐บ) + ๐))) |
180 | 169, 176,
179 | 3eqtr3rd 2782 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((coe1โ๐)โ((๐ทโ๐บ) + ๐)) = (((coe1โ๐บ)โ(๐ทโ๐บ)) ยท (๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐))))) |
181 | 162, 166,
180 | 3eqtr4rd 2784 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ((coe1โ๐)โ((๐ทโ๐บ) + ๐)) = ((coe1โ(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))โ((๐ทโ๐บ) + ๐))) |
182 | 181 | adantrr 716 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ ((coe1โ๐)โ((๐ทโ๐บ) + ๐)) = ((coe1โ(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))โ((๐ทโ๐บ) + ๐))) |
183 | 10, 11, 13, 82, 102, 103, 104, 129, 153, 159, 135, 160, 182 | deg1sublt 25498 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (๐ทโ(๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) < ((๐ทโ๐บ) + ๐)) |
184 | 183 | adantlrr 720 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ0 โง
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (๐ทโ(๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) < ((๐ทโ๐บ) + ๐)) |
185 | | fveq2 6846 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐ทโ๐) = (๐ทโ(๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) |
186 | 185 | breq1d 5119 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ (๐ทโ(๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) < ((๐ทโ๐บ) + ๐))) |
187 | | fvoveq1 7384 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐ทโ(๐ โ (๐บ โ ๐))) = (๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐)))) |
188 | 187 | breq1d 5119 |
. . . . . . . . . . . . . . . . 17
โข (๐ = (๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ ((๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ (๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
189 | 188 | rexbidv 3172 |
. . . . . . . . . . . . . . . 16
โข (๐ = (๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ โ๐ โ ๐ต (๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
190 | 186, 189 | imbi12d 345 |
. . . . . . . . . . . . . . 15
โข (๐ = (๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ ((๐ทโ(๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ)))) |
191 | | simplrr 777 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ โ0 โง
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
192 | 81 | ad2antrr 725 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐ โ Grp) |
193 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
194 | 13, 82 | grpsubcl 18835 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ Grp โง ๐ โ ๐ต โง (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ ๐ต) โ (๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ ๐ต) |
195 | 192, 193,
152, 194 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ ๐ต) |
196 | 195 | adantrr 716 |
. . . . . . . . . . . . . . . 16
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ ๐ต) |
197 | 196 | adantlrr 720 |
. . . . . . . . . . . . . . 15
โข (((๐ โง (๐ โ โ0 โง
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ ๐ต) |
198 | 190, 191,
197 | rspcdva 3584 |
. . . . . . . . . . . . . 14
โข (((๐ โง (๐ โ โ0 โง
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ ((๐ทโ(๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
199 | 184, 198 | mpd 15 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ0 โง
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ โ๐ โ ๐ต (๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ)) |
200 | 71 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ๐ โ Ring) |
201 | | simpr 486 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
202 | 150 | adantr 482 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))) โ ๐ต) |
203 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
โข
(+gโ๐) = (+gโ๐) |
204 | 13, 203 | ringacl 20007 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โ Ring โง ๐ โ ๐ต โง ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))) โ ๐ต) โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ ๐ต) |
205 | 200, 201,
202, 204 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ ๐ต) |
206 | 81 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ๐ โ Grp) |
207 | | simplr 768 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
208 | 152 | adantr 482 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ ๐ต) |
209 | 17 | ad3antrrr 729 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ๐บ โ ๐ต) |
210 | 13, 75 | ringcl 19989 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ Ring โง ๐บ โ ๐ต โง ๐ โ ๐ต) โ (๐บ โ ๐) โ ๐ต) |
211 | 200, 209,
201, 210 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ (๐บ โ ๐) โ ๐ต) |
212 | 13, 203, 82 | grpsubsub4 18848 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((๐ โ Grp โง (๐ โ ๐ต โง (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ ๐ต โง (๐บ โ ๐) โ ๐ต)) โ ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐)) = (๐ โ ((๐บ โ ๐)(+gโ๐)(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) |
213 | 206, 207,
208, 211, 212 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐)) = (๐ โ ((๐บ โ ๐)(+gโ๐)(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) |
214 | 13, 203, 75 | ringdi 19995 |
. . . . . . . . . . . . . . . . . . . . . . 23
โข ((๐ โ Ring โง (๐บ โ ๐ต โง ๐ โ ๐ต โง ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))) โ ๐ต)) โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) = ((๐บ โ ๐)(+gโ๐)(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) |
215 | 200, 209,
201, 202, 214 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) = ((๐บ โ ๐)(+gโ๐)(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) |
216 | 215 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . . . 21
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ (๐ โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) = (๐ โ ((๐บ โ ๐)(+gโ๐)(๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) |
217 | 213, 216 | eqtr4d 2776 |
. . . . . . . . . . . . . . . . . . . 20
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐)) = (๐ โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) |
218 | 217 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . 19
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ (๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) = (๐ทโ(๐ โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))) |
219 | 218 | breq1d 5119 |
. . . . . . . . . . . . . . . . . 18
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ((๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ) โ (๐ทโ(๐ โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) < (๐ทโ๐บ))) |
220 | 219 | biimpd 228 |
. . . . . . . . . . . . . . . . 17
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ((๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ) โ (๐ทโ(๐ โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) < (๐ทโ๐บ))) |
221 | | oveq2 7369 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ = (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ (๐บ โ ๐) = (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))) |
222 | 221 | oveq2d 7377 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ = (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ (๐ โ (๐บ โ ๐)) = (๐ โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) |
223 | 222 | fveq2d 6850 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ = (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ (๐ทโ(๐ โ (๐บ โ ๐))) = (๐ทโ(๐ โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))))))) |
224 | 223 | breq1d 5119 |
. . . . . . . . . . . . . . . . . 18
โข (๐ = (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ ((๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ (๐ทโ(๐ โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) < (๐ทโ๐บ))) |
225 | 224 | rspcev 3583 |
. . . . . . . . . . . . . . . . 17
โข (((๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
)))) โ ๐ต โง (๐ทโ(๐ โ (๐บ โ (๐(+gโ๐)((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))))) < (๐ทโ๐บ)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) |
226 | 205, 220,
225 | syl6an 683 |
. . . . . . . . . . . . . . . 16
โข ((((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โง ๐ โ ๐ต) โ ((๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
227 | 226 | rexlimdva 3149 |
. . . . . . . . . . . . . . 15
โข (((๐ โง ๐ โ โ0) โง ๐ โ ๐ต) โ (โ๐ โ ๐ต (๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
228 | 227 | adantrr 716 |
. . . . . . . . . . . . . 14
โข (((๐ โง ๐ โ โ0) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (โ๐ โ ๐ต (๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
229 | 228 | adantlrr 720 |
. . . . . . . . . . . . 13
โข (((๐ โง (๐ โ โ0 โง
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ (โ๐ โ ๐ต (๐ทโ((๐ โ (๐บ โ ((๐ผ ยท
((coe1โ๐)โ((๐ทโ๐บ) + ๐)))( ยท๐
โ๐)(๐(.gโ(mulGrpโ๐))(var1โ๐
))))) โ (๐บ โ ๐))) < (๐ทโ๐บ) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
230 | 199, 229 | mpd 15 |
. . . . . . . . . . . 12
โข (((๐ โง (๐ โ โ0 โง
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) โง (๐ โ ๐ต โง (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) |
231 | 230 | expr 458 |
. . . . . . . . . . 11
โข (((๐ โง (๐ โ โ0 โง
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) โง ๐ โ ๐ต) โ ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
232 | 231 | ralrimiva 3140 |
. . . . . . . . . 10
โข ((๐ โง (๐ โ โ0 โง
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
233 | | fveq2 6846 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (๐ทโ๐) = (๐ทโ๐)) |
234 | 233 | breq1d 5119 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ (๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)))) |
235 | | fvoveq1 7384 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐ทโ(๐ โ (๐บ โ ๐))) = (๐ทโ(๐ โ (๐บ โ ๐)))) |
236 | 235 | breq1d 5119 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
237 | 236 | rexbidv 3172 |
. . . . . . . . . . . . 13
โข (๐ = ๐ โ (โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
238 | | oveq2 7369 |
. . . . . . . . . . . . . . . . 17
โข (๐ = ๐ โ (๐บ โ ๐) = (๐บ โ ๐)) |
239 | 238 | oveq2d 7377 |
. . . . . . . . . . . . . . . 16
โข (๐ = ๐ โ (๐ โ (๐บ โ ๐)) = (๐ โ (๐บ โ ๐))) |
240 | 239 | fveq2d 6850 |
. . . . . . . . . . . . . . 15
โข (๐ = ๐ โ (๐ทโ(๐ โ (๐บ โ ๐))) = (๐ทโ(๐ โ (๐บ โ ๐)))) |
241 | 240 | breq1d 5119 |
. . . . . . . . . . . . . 14
โข (๐ = ๐ โ ((๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
242 | 241 | cbvrexvw 3225 |
. . . . . . . . . . . . 13
โข
(โ๐ โ
๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) |
243 | 237, 242 | bitrdi 287 |
. . . . . . . . . . . 12
โข (๐ = ๐ โ (โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
244 | 234, 243 | imbi12d 345 |
. . . . . . . . . . 11
โข (๐ = ๐ โ (((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) |
245 | 244 | cbvralvw 3224 |
. . . . . . . . . 10
โข
(โ๐ โ
๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
246 | 232, 245 | sylib 217 |
. . . . . . . . 9
โข ((๐ โง (๐ โ โ0 โง
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
247 | 246 | exp32 422 |
. . . . . . . 8
โข (๐ โ (๐ โ โ0 โ
(โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))))) |
248 | 247 | com12 32 |
. . . . . . 7
โข (๐ โ โ0
โ (๐ โ
(โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)) โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))))) |
249 | 248 | a2d 29 |
. . . . . 6
โข (๐ โ โ0
โ ((๐ โ
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) โ (๐ โ โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + (๐ + 1)) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))))) |
250 | 59, 64, 69, 64, 99, 249 | nn0ind 12606 |
. . . . 5
โข (๐ โ โ0
โ (๐ โ
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ)))) |
251 | 250 | impcom 409 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ
โ๐ โ ๐ต ((๐ทโ๐) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐ โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
252 | 7 | adantr 482 |
. . . 4
โข ((๐ โง ๐ โ โ0) โ ๐น โ ๐ต) |
253 | 54, 251, 252 | rspcdva 3584 |
. . 3
โข ((๐ โง ๐ โ โ0) โ ((๐ทโ๐น) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐น โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
254 | 253 | rexlimdva 3149 |
. 2
โข (๐ โ (โ๐ โ โ0 (๐ทโ๐น) < ((๐ทโ๐บ) + ๐) โ โ๐ โ ๐ต (๐ทโ(๐น โ (๐บ โ ๐))) < (๐ทโ๐บ))) |
255 | 48, 254 | mpd 15 |
1
โข (๐ โ โ๐ โ ๐ต (๐ทโ(๐น โ (๐บ โ ๐))) < (๐ทโ๐บ)) |