Step | Hyp | Ref
| Expression |
1 | | breq2 5151 |
. . 3
โข (๐ = ๐น โ (๐พ MonoAP ๐ โ ๐พ MonoAP ๐น)) |
2 | | vdwlem9.a |
. . 3
โข (๐ โ โ๐ โ ((๐
โm (1...๐)) โm (1...๐))๐พ MonoAP ๐) |
3 | | vdwlem9.v |
. . . . 5
โข (๐ โ ๐ โ โ) |
4 | | vdwlem9.w |
. . . . 5
โข (๐ โ ๐ โ โ) |
5 | | vdw.r |
. . . . 5
โข (๐ โ ๐
โ Fin) |
6 | | vdwlem9.h |
. . . . 5
โข (๐ โ ๐ป:(1...(๐ ยท (2 ยท ๐)))โถ๐
) |
7 | | vdwlem9.f |
. . . . 5
โข ๐น = (๐ฅ โ (1...๐) โฆ (๐ฆ โ (1...๐) โฆ (๐ปโ(๐ฆ + (๐ ยท ((๐ฅ โ 1) + ๐)))))) |
8 | 3, 4, 5, 6, 7 | vdwlem4 16913 |
. . . 4
โข (๐ โ ๐น:(1...๐)โถ(๐
โm (1...๐))) |
9 | | ovex 7438 |
. . . . 5
โข (๐
โm (1...๐)) โ V |
10 | | ovex 7438 |
. . . . 5
โข
(1...๐) โ
V |
11 | 9, 10 | elmap 8861 |
. . . 4
โข (๐น โ ((๐
โm (1...๐)) โm (1...๐)) โ ๐น:(1...๐)โถ(๐
โm (1...๐))) |
12 | 8, 11 | sylibr 233 |
. . 3
โข (๐ โ ๐น โ ((๐
โm (1...๐)) โm (1...๐))) |
13 | 1, 2, 12 | rspcdva 3613 |
. 2
โข (๐ โ ๐พ MonoAP ๐น) |
14 | | vdwlem9.k |
. . . . . 6
โข (๐ โ ๐พ โ
(โคโฅโ2)) |
15 | | eluz2nn 12864 |
. . . . . 6
โข (๐พ โ
(โคโฅโ2) โ ๐พ โ โ) |
16 | 14, 15 | syl 17 |
. . . . 5
โข (๐ โ ๐พ โ โ) |
17 | 16 | nnnn0d 12528 |
. . . 4
โข (๐ โ ๐พ โ
โ0) |
18 | 10, 17, 8 | vdwmc 16907 |
. . 3
โข (๐ โ (๐พ MonoAP ๐น โ โ๐โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) |
19 | | vdwlem9.g |
. . . . . . . . 9
โข (๐ โ โ๐ โ (๐
โm (1...๐))(โจ๐, ๐พโฉ PolyAP ๐ โจ (๐พ + 1) MonoAP ๐)) |
20 | 19 | adantr 481 |
. . . . . . . 8
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ โ๐ โ (๐
โm (1...๐))(โจ๐, ๐พโฉ PolyAP ๐ โจ (๐พ + 1) MonoAP ๐)) |
21 | | simprr 771 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐})) |
22 | 16 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐พ โ โ) |
23 | | simprll 777 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
24 | | simprlr 778 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
25 | | vdwapid1 16904 |
. . . . . . . . . . . . 13
โข ((๐พ โ โ โง ๐ โ โ โง ๐ โ โ) โ ๐ โ (๐(APโ๐พ)๐)) |
26 | 22, 23, 24, 25 | syl3anc 1371 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ (๐(APโ๐พ)๐)) |
27 | 21, 26 | sseldd 3982 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ (โก๐น โ {๐})) |
28 | 8 | ffnd 6715 |
. . . . . . . . . . . . 13
โข (๐ โ ๐น Fn (1...๐)) |
29 | 28 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐น Fn (1...๐)) |
30 | | fniniseg 7058 |
. . . . . . . . . . . 12
โข (๐น Fn (1...๐) โ (๐ โ (โก๐น โ {๐}) โ (๐ โ (1...๐) โง (๐นโ๐) = ๐))) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ โ (โก๐น โ {๐}) โ (๐ โ (1...๐) โง (๐นโ๐) = ๐))) |
32 | 27, 31 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ โ (1...๐) โง (๐นโ๐) = ๐)) |
33 | 32 | simprd 496 |
. . . . . . . . 9
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐นโ๐) = ๐) |
34 | 8 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐น:(1...๐)โถ(๐
โm (1...๐))) |
35 | 32 | simpld 495 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ (1...๐)) |
36 | 34, 35 | ffvelcdmd 7084 |
. . . . . . . . 9
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐นโ๐) โ (๐
โm (1...๐))) |
37 | 33, 36 | eqeltrrd 2834 |
. . . . . . . 8
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ (๐
โm (1...๐))) |
38 | | rsp 3244 |
. . . . . . . 8
โข
(โ๐ โ
(๐
โm
(1...๐))(โจ๐, ๐พโฉ PolyAP ๐ โจ (๐พ + 1) MonoAP ๐) โ (๐ โ (๐
โm (1...๐)) โ (โจ๐, ๐พโฉ PolyAP ๐ โจ (๐พ + 1) MonoAP ๐))) |
39 | 20, 37, 38 | sylc 65 |
. . . . . . 7
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (โจ๐, ๐พโฉ PolyAP ๐ โจ (๐พ + 1) MonoAP ๐)) |
40 | 3 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
41 | 4 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
42 | 5 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐
โ Fin) |
43 | 6 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ป:(1...(๐ ยท (2 ยท ๐)))โถ๐
) |
44 | | vdwlem9.m |
. . . . . . . . . . 11
โข (๐ โ ๐ โ โ) |
45 | 44 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
46 | | ovex 7438 |
. . . . . . . . . . . 12
โข
(1...๐) โ
V |
47 | | elmapg 8829 |
. . . . . . . . . . . 12
โข ((๐
โ Fin โง (1...๐) โ V) โ (๐ โ (๐
โm (1...๐)) โ ๐:(1...๐)โถ๐
)) |
48 | 42, 46, 47 | sylancl 586 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ โ (๐
โm (1...๐)) โ ๐:(1...๐)โถ๐
)) |
49 | 37, 48 | mpbid 231 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐:(1...๐)โถ๐
) |
50 | 14 | adantr 481 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐พ โ
(โคโฅโ2)) |
51 | 40, 41, 42, 43, 7, 45, 49, 50, 23, 24, 21 | vdwlem7 16916 |
. . . . . . . . 9
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (โจ๐, ๐พโฉ PolyAP ๐ โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐))) |
52 | | olc 866 |
. . . . . . . . . 10
โข ((๐พ + 1) MonoAP ๐ โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐)) |
53 | 52 | a1i 11 |
. . . . . . . . 9
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((๐พ + 1) MonoAP ๐ โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐))) |
54 | 51, 53 | jaod 857 |
. . . . . . . 8
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((โจ๐, ๐พโฉ PolyAP ๐ โจ (๐พ + 1) MonoAP ๐) โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐))) |
55 | | oveq1 7412 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ = ๐ โ (๐ฅ โ 1) = (๐ โ 1)) |
56 | 55 | oveq1d 7420 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ = ๐ โ ((๐ฅ โ 1) + ๐) = ((๐ โ 1) + ๐)) |
57 | 56 | oveq2d 7421 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ = ๐ โ (๐ ยท ((๐ฅ โ 1) + ๐)) = (๐ ยท ((๐ โ 1) + ๐))) |
58 | 57 | oveq2d 7421 |
. . . . . . . . . . . . . . . 16
โข (๐ฅ = ๐ โ (๐ฆ + (๐ ยท ((๐ฅ โ 1) + ๐))) = (๐ฆ + (๐ ยท ((๐ โ 1) + ๐)))) |
59 | 58 | fveq2d 6892 |
. . . . . . . . . . . . . . 15
โข (๐ฅ = ๐ โ (๐ปโ(๐ฆ + (๐ ยท ((๐ฅ โ 1) + ๐)))) = (๐ปโ(๐ฆ + (๐ ยท ((๐ โ 1) + ๐))))) |
60 | 59 | mpteq2dv 5249 |
. . . . . . . . . . . . . 14
โข (๐ฅ = ๐ โ (๐ฆ โ (1...๐) โฆ (๐ปโ(๐ฆ + (๐ ยท ((๐ฅ โ 1) + ๐))))) = (๐ฆ โ (1...๐) โฆ (๐ปโ(๐ฆ + (๐ ยท ((๐ โ 1) + ๐)))))) |
61 | 46 | mptex 7221 |
. . . . . . . . . . . . . 14
โข (๐ฆ โ (1...๐) โฆ (๐ปโ(๐ฆ + (๐ ยท ((๐ โ 1) + ๐))))) โ V |
62 | 60, 7, 61 | fvmpt 6995 |
. . . . . . . . . . . . 13
โข (๐ โ (1...๐) โ (๐นโ๐) = (๐ฆ โ (1...๐) โฆ (๐ปโ(๐ฆ + (๐ ยท ((๐ โ 1) + ๐)))))) |
63 | 35, 62 | syl 17 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐นโ๐) = (๐ฆ โ (1...๐) โฆ (๐ปโ(๐ฆ + (๐ ยท ((๐ โ 1) + ๐)))))) |
64 | 63, 33 | eqtr3d 2774 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ฆ โ (1...๐) โฆ (๐ปโ(๐ฆ + (๐ ยท ((๐ โ 1) + ๐))))) = ๐) |
65 | 64 | breq2d 5159 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((๐พ + 1) MonoAP (๐ฆ โ (1...๐) โฆ (๐ปโ(๐ฆ + (๐ ยท ((๐ โ 1) + ๐))))) โ (๐พ + 1) MonoAP ๐)) |
66 | 17 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐พ โ
โ0) |
67 | | peano2nn0 12508 |
. . . . . . . . . . . 12
โข (๐พ โ โ0
โ (๐พ + 1) โ
โ0) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐พ + 1) โ
โ0) |
69 | | nnm1nn0 12509 |
. . . . . . . . . . . . . 14
โข (๐ โ โ โ (๐ โ 1) โ
โ0) |
70 | 23, 69 | syl 17 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ โ 1) โ
โ0) |
71 | | nn0nnaddcl 12499 |
. . . . . . . . . . . . 13
โข (((๐ โ 1) โ
โ0 โง ๐
โ โ) โ ((๐
โ 1) + ๐) โ
โ) |
72 | 70, 40, 71 | syl2anc 584 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((๐ โ 1) + ๐) โ โ) |
73 | 41, 72 | nnmulcld 12261 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท ((๐ โ 1) + ๐)) โ โ) |
74 | 23, 40 | nnaddcld 12260 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ + ๐) โ โ) |
75 | 41, 74 | nnmulcld 12261 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท (๐ + ๐)) โ โ) |
76 | 75 | nnzd 12581 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท (๐ + ๐)) โ โค) |
77 | | 2nn 12281 |
. . . . . . . . . . . . . . . . 17
โข 2 โ
โ |
78 | | nnmulcl 12232 |
. . . . . . . . . . . . . . . . 17
โข ((2
โ โ โง ๐
โ โ) โ (2 ยท ๐) โ โ) |
79 | 77, 3, 78 | sylancr 587 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 ยท ๐) โ
โ) |
80 | 4, 79 | nnmulcld 12261 |
. . . . . . . . . . . . . . 15
โข (๐ โ (๐ ยท (2 ยท ๐)) โ โ) |
81 | 80 | nnzd 12581 |
. . . . . . . . . . . . . 14
โข (๐ โ (๐ ยท (2 ยท ๐)) โ โค) |
82 | 81 | adantr 481 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท (2 ยท ๐)) โ โค) |
83 | 23 | nnred 12223 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
84 | 40 | nnred 12223 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
85 | | elfzle2 13501 |
. . . . . . . . . . . . . . . . 17
โข (๐ โ (1...๐) โ ๐ โค ๐) |
86 | 35, 85 | syl 17 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โค ๐) |
87 | 83, 84, 84, 86 | leadd1dd 11824 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ + ๐) โค (๐ + ๐)) |
88 | 40 | nncnd 12224 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
89 | 88 | 2timesd 12451 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (2 ยท ๐) = (๐ + ๐)) |
90 | 87, 89 | breqtrrd 5175 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ + ๐) โค (2 ยท ๐)) |
91 | 74 | nnred 12223 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ + ๐) โ โ) |
92 | 79 | nnred 12223 |
. . . . . . . . . . . . . . . 16
โข (๐ โ (2 ยท ๐) โ
โ) |
93 | 92 | adantr 481 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (2 ยท ๐) โ โ) |
94 | 41 | nnred 12223 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
95 | 41 | nngt0d 12257 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ 0 < ๐) |
96 | | lemul2 12063 |
. . . . . . . . . . . . . . 15
โข (((๐ + ๐) โ โ โง (2 ยท ๐) โ โ โง (๐ โ โ โง 0 <
๐)) โ ((๐ + ๐) โค (2 ยท ๐) โ (๐ ยท (๐ + ๐)) โค (๐ ยท (2 ยท ๐)))) |
97 | 91, 93, 94, 95, 96 | syl112anc 1374 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((๐ + ๐) โค (2 ยท ๐) โ (๐ ยท (๐ + ๐)) โค (๐ ยท (2 ยท ๐)))) |
98 | 90, 97 | mpbid 231 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท (๐ + ๐)) โค (๐ ยท (2 ยท ๐))) |
99 | | eluz2 12824 |
. . . . . . . . . . . . 13
โข ((๐ ยท (2 ยท ๐)) โ
(โคโฅโ(๐ ยท (๐ + ๐))) โ ((๐ ยท (๐ + ๐)) โ โค โง (๐ ยท (2 ยท ๐)) โ โค โง (๐ ยท (๐ + ๐)) โค (๐ ยท (2 ยท ๐)))) |
100 | 76, 82, 98, 99 | syl3anbrc 1343 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท (2 ยท ๐)) โ
(โคโฅโ(๐ ยท (๐ + ๐)))) |
101 | 41 | nncnd 12224 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
102 | | 1cnd 11205 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ 1 โ
โ) |
103 | 70 | nn0cnd 12530 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ โ 1) โ โ) |
104 | 103, 88 | addcld 11229 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((๐ โ 1) + ๐) โ โ) |
105 | 101, 102,
104 | adddid 11234 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท (1 + ((๐ โ 1) + ๐))) = ((๐ ยท 1) + (๐ ยท ((๐ โ 1) + ๐)))) |
106 | 102, 103,
88 | addassd 11232 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((1 + (๐ โ 1)) + ๐) = (1 + ((๐ โ 1) + ๐))) |
107 | | ax-1cn 11164 |
. . . . . . . . . . . . . . . . . 18
โข 1 โ
โ |
108 | 23 | nncnd 12224 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ๐ โ โ) |
109 | | pncan3 11464 |
. . . . . . . . . . . . . . . . . 18
โข ((1
โ โ โง ๐
โ โ) โ (1 + (๐ โ 1)) = ๐) |
110 | 107, 108,
109 | sylancr 587 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (1 + (๐ โ 1)) = ๐) |
111 | 110 | oveq1d 7420 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((1 + (๐ โ 1)) + ๐) = (๐ + ๐)) |
112 | 106, 111 | eqtr3d 2774 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (1 + ((๐ โ 1) + ๐)) = (๐ + ๐)) |
113 | 112 | oveq2d 7421 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท (1 + ((๐ โ 1) + ๐))) = (๐ ยท (๐ + ๐))) |
114 | 101 | mulridd 11227 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท 1) = ๐) |
115 | 114 | oveq1d 7420 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((๐ ยท 1) + (๐ ยท ((๐ โ 1) + ๐))) = (๐ + (๐ ยท ((๐ โ 1) + ๐)))) |
116 | 105, 113,
115 | 3eqtr3d 2780 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท (๐ + ๐)) = (๐ + (๐ ยท ((๐ โ 1) + ๐)))) |
117 | 116 | fveq2d 6892 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ
(โคโฅโ(๐ ยท (๐ + ๐))) = (โคโฅโ(๐ + (๐ ยท ((๐ โ 1) + ๐))))) |
118 | 100, 117 | eleqtrd 2835 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (๐ ยท (2 ยท ๐)) โ
(โคโฅโ(๐ + (๐ ยท ((๐ โ 1) + ๐))))) |
119 | | fvoveq1 7428 |
. . . . . . . . . . . 12
โข (๐ฆ = ๐ง โ (๐ปโ(๐ฆ + (๐ ยท ((๐ โ 1) + ๐)))) = (๐ปโ(๐ง + (๐ ยท ((๐ โ 1) + ๐))))) |
120 | 119 | cbvmptv 5260 |
. . . . . . . . . . 11
โข (๐ฆ โ (1...๐) โฆ (๐ปโ(๐ฆ + (๐ ยท ((๐ โ 1) + ๐))))) = (๐ง โ (1...๐) โฆ (๐ปโ(๐ง + (๐ ยท ((๐ โ 1) + ๐))))) |
121 | 42, 68, 41, 73, 43, 118, 120 | vdwlem2 16911 |
. . . . . . . . . 10
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((๐พ + 1) MonoAP (๐ฆ โ (1...๐) โฆ (๐ปโ(๐ฆ + (๐ ยท ((๐ โ 1) + ๐))))) โ (๐พ + 1) MonoAP ๐ป)) |
122 | 65, 121 | sylbird 259 |
. . . . . . . . 9
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((๐พ + 1) MonoAP ๐ โ (๐พ + 1) MonoAP ๐ป)) |
123 | 122 | orim2d 965 |
. . . . . . . 8
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐) โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐ป))) |
124 | 54, 123 | syld 47 |
. . . . . . 7
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ ((โจ๐, ๐พโฉ PolyAP ๐ โจ (๐พ + 1) MonoAP ๐) โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐ป))) |
125 | 39, 124 | mpd 15 |
. . . . . 6
โข ((๐ โง ((๐ โ โ โง ๐ โ โ) โง (๐(APโ๐พ)๐) โ (โก๐น โ {๐}))) โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐ป)) |
126 | 125 | expr 457 |
. . . . 5
โข ((๐ โง (๐ โ โ โง ๐ โ โ)) โ ((๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐ป))) |
127 | 126 | rexlimdvva 3211 |
. . . 4
โข (๐ โ (โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐ป))) |
128 | 127 | exlimdv 1936 |
. . 3
โข (๐ โ (โ๐โ๐ โ โ โ๐ โ โ (๐(APโ๐พ)๐) โ (โก๐น โ {๐}) โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐ป))) |
129 | 18, 128 | sylbid 239 |
. 2
โข (๐ โ (๐พ MonoAP ๐น โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐ป))) |
130 | 13, 129 | mpd 15 |
1
โข (๐ โ (โจ(๐ + 1), ๐พโฉ PolyAP ๐ป โจ (๐พ + 1) MonoAP ๐ป)) |