Step | Hyp | Ref
| Expression |
1 | | df-3an 1090 |
. . 3
β’ ((π β oMnd β§ (π β π΅ β§ π β β0) β§ 0 β€ π) β ((π β oMnd β§ (π β π΅ β§ π β β0)) β§ 0 β€ π)) |
2 | | anass 470 |
. . . 4
β’ (((π β oMnd β§ π β π΅) β§ π β β0) β (π β oMnd β§ (π β π΅ β§ π β
β0))) |
3 | 2 | anbi1i 625 |
. . 3
β’ ((((π β oMnd β§ π β π΅) β§ π β β0) β§ 0 β€ π) β ((π β oMnd β§ (π β π΅ β§ π β β0)) β§ 0 β€ π)) |
4 | 1, 3 | bitr4i 278 |
. 2
β’ ((π β oMnd β§ (π β π΅ β§ π β β0) β§ 0 β€ π) β (((π β oMnd β§ π β π΅) β§ π β β0) β§ 0 β€ π)) |
5 | | simplr 768 |
. . 3
β’ ((((π β oMnd β§ π β π΅) β§ π β β0) β§ 0 β€ π) β π β
β0) |
6 | | oveq1 7365 |
. . . . 5
β’ (π = 0 β (π Β· π) = (0 Β· π)) |
7 | 6 | breq2d 5118 |
. . . 4
β’ (π = 0 β ( 0 β€ (π Β· π) β 0 β€ (0 Β· π))) |
8 | | oveq1 7365 |
. . . . 5
β’ (π = π β (π Β· π) = (π Β· π)) |
9 | 8 | breq2d 5118 |
. . . 4
β’ (π = π β ( 0 β€ (π Β· π) β 0 β€ (π Β· π))) |
10 | | oveq1 7365 |
. . . . 5
β’ (π = (π + 1) β (π Β· π) = ((π + 1) Β· π)) |
11 | 10 | breq2d 5118 |
. . . 4
β’ (π = (π + 1) β ( 0 β€ (π Β· π) β 0 β€ ((π + 1) Β· π))) |
12 | | oveq1 7365 |
. . . . 5
β’ (π = π β (π Β· π) = (π Β· π)) |
13 | 12 | breq2d 5118 |
. . . 4
β’ (π = π β ( 0 β€ (π Β· π) β 0 β€ (π Β· π))) |
14 | | omndtos 31962 |
. . . . . . . 8
β’ (π β oMnd β π β Toset) |
15 | | tospos 18314 |
. . . . . . . 8
β’ (π β Toset β π β Poset) |
16 | 14, 15 | syl 17 |
. . . . . . 7
β’ (π β oMnd β π β Poset) |
17 | | omndmnd 31961 |
. . . . . . . 8
β’ (π β oMnd β π β Mnd) |
18 | | omndmul.0 |
. . . . . . . . 9
β’ π΅ = (Baseβπ) |
19 | | omndmul2.3 |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
20 | 18, 19 | mndidcl 18576 |
. . . . . . . 8
β’ (π β Mnd β 0 β π΅) |
21 | 17, 20 | syl 17 |
. . . . . . 7
β’ (π β oMnd β 0 β π΅) |
22 | | omndmul.1 |
. . . . . . . 8
β’ β€ =
(leβπ) |
23 | 18, 22 | posref 18212 |
. . . . . . 7
β’ ((π β Poset β§ 0 β π΅) β 0 β€ 0 ) |
24 | 16, 21, 23 | syl2anc 585 |
. . . . . 6
β’ (π β oMnd β 0 β€ 0
) |
25 | 24 | ad3antrrr 729 |
. . . . 5
β’ ((((π β oMnd β§ π β π΅) β§ π β β0) β§ 0 β€ π) β 0 β€ 0 ) |
26 | | omndmul2.2 |
. . . . . . 7
β’ Β· =
(.gβπ) |
27 | 18, 19, 26 | mulg0 18884 |
. . . . . 6
β’ (π β π΅ β (0 Β· π) = 0 ) |
28 | 27 | ad3antlr 730 |
. . . . 5
β’ ((((π β oMnd β§ π β π΅) β§ π β β0) β§ 0 β€ π) β (0 Β· π) = 0 ) |
29 | 25, 28 | breqtrrd 5134 |
. . . 4
β’ ((((π β oMnd β§ π β π΅) β§ π β β0) β§ 0 β€ π) β 0 β€ (0 Β· π)) |
30 | 16 | ad5antr 733 |
. . . . 5
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β π β Poset) |
31 | 17 | ad5antr 733 |
. . . . . . 7
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β π β Mnd) |
32 | 31, 20 | syl 17 |
. . . . . 6
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β 0 β π΅) |
33 | | simplr 768 |
. . . . . . 7
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β π β β0) |
34 | | simp-5r 785 |
. . . . . . 7
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β π β π΅) |
35 | 18, 26, 31, 33, 34 | mulgnn0cld 18902 |
. . . . . 6
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β (π Β· π) β π΅) |
36 | | simpr32 1265 |
. . . . . . . . . 10
β’ ((π β oMnd β§ (π β π΅ β§ π β β0 β§ ( 0 β€ π β§ π β β0 β§ 0 β€ (π Β· π)))) β π β β0) |
37 | | 1nn0 12434 |
. . . . . . . . . . 11
β’ 1 β
β0 |
38 | 37 | a1i 11 |
. . . . . . . . . 10
β’ ((π β oMnd β§ (π β π΅ β§ π β β0 β§ ( 0 β€ π β§ π β β0 β§ 0 β€ (π Β· π)))) β 1 β
β0) |
39 | 36, 38 | nn0addcld 12482 |
. . . . . . . . 9
β’ ((π β oMnd β§ (π β π΅ β§ π β β0 β§ ( 0 β€ π β§ π β β0 β§ 0 β€ (π Β· π)))) β (π + 1) β
β0) |
40 | 39 | 3anassrs 1361 |
. . . . . . . 8
β’ ((((π β oMnd β§ π β π΅) β§ π β β0) β§ ( 0 β€ π β§ π β β0 β§ 0 β€ (π Β· π))) β (π + 1) β
β0) |
41 | 40 | 3anassrs 1361 |
. . . . . . 7
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β (π + 1) β
β0) |
42 | 18, 26, 31, 41, 34 | mulgnn0cld 18902 |
. . . . . 6
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β ((π + 1) Β· π) β π΅) |
43 | 32, 35, 42 | 3jca 1129 |
. . . . 5
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β ( 0 β π΅ β§ (π Β· π) β π΅ β§ ((π + 1) Β· π) β π΅)) |
44 | | simpr 486 |
. . . . 5
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β 0 β€ (π Β· π)) |
45 | | simp-4l 782 |
. . . . . . . 8
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β π β oMnd) |
46 | 17 | ad4antr 731 |
. . . . . . . . 9
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β π β Mnd) |
47 | 46, 20 | syl 17 |
. . . . . . . 8
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β 0 β π΅) |
48 | | simp-4r 783 |
. . . . . . . 8
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β π β π΅) |
49 | | simpr 486 |
. . . . . . . . 9
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β π β
β0) |
50 | 18, 26, 46, 49, 48 | mulgnn0cld 18902 |
. . . . . . . 8
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β (π Β· π) β π΅) |
51 | | simplr 768 |
. . . . . . . 8
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β 0 β€ π) |
52 | | eqid 2733 |
. . . . . . . . 9
β’
(+gβπ) = (+gβπ) |
53 | 18, 22, 52 | omndadd 31963 |
. . . . . . . 8
β’ ((π β oMnd β§ ( 0 β π΅ β§ π β π΅ β§ (π Β· π) β π΅) β§ 0 β€ π) β ( 0 (+gβπ)(π Β· π)) β€ (π(+gβπ)(π Β· π))) |
54 | 45, 47, 48, 50, 51, 53 | syl131anc 1384 |
. . . . . . 7
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β ( 0
(+gβπ)(π Β· π)) β€ (π(+gβπ)(π Β· π))) |
55 | 18, 52, 19 | mndlid 18581 |
. . . . . . . 8
β’ ((π β Mnd β§ (π Β· π) β π΅) β ( 0 (+gβπ)(π Β· π)) = (π Β· π)) |
56 | 46, 50, 55 | syl2anc 585 |
. . . . . . 7
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β ( 0
(+gβπ)(π Β· π)) = (π Β· π)) |
57 | 37 | a1i 11 |
. . . . . . . . 9
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β 1 β
β0) |
58 | 18, 26, 52 | mulgnn0dir 18911 |
. . . . . . . . 9
β’ ((π β Mnd β§ (1 β
β0 β§ π
β β0 β§ π β π΅)) β ((1 + π) Β· π) = ((1 Β· π)(+gβπ)(π Β· π))) |
59 | 46, 57, 49, 48, 58 | syl13anc 1373 |
. . . . . . . 8
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β ((1 +
π) Β· π) = ((1 Β· π)(+gβπ)(π Β· π))) |
60 | | 1cnd 11155 |
. . . . . . . . . . 11
β’ (((π β oMnd β§ π β π΅) β§ (π β β0 β§ 0 β€ π β§ π β β0)) β 1 β
β) |
61 | | simpr3 1197 |
. . . . . . . . . . . 12
β’ (((π β oMnd β§ π β π΅) β§ (π β β0 β§ 0 β€ π β§ π β β0)) β π β
β0) |
62 | 61 | nn0cnd 12480 |
. . . . . . . . . . 11
β’ (((π β oMnd β§ π β π΅) β§ (π β β0 β§ 0 β€ π β§ π β β0)) β π β
β) |
63 | 60, 62 | addcomd 11362 |
. . . . . . . . . 10
β’ (((π β oMnd β§ π β π΅) β§ (π β β0 β§ 0 β€ π β§ π β β0)) β (1 +
π) = (π + 1)) |
64 | 63 | 3anassrs 1361 |
. . . . . . . . 9
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β (1 +
π) = (π + 1)) |
65 | 64 | oveq1d 7373 |
. . . . . . . 8
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β ((1 +
π) Β· π) = ((π + 1) Β· π)) |
66 | 18, 26 | mulg1 18888 |
. . . . . . . . . 10
β’ (π β π΅ β (1 Β· π) = π) |
67 | 48, 66 | syl 17 |
. . . . . . . . 9
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β (1 Β· π) = π) |
68 | 67 | oveq1d 7373 |
. . . . . . . 8
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β ((1 Β· π)(+gβπ)(π Β· π)) = (π(+gβπ)(π Β· π))) |
69 | 59, 65, 68 | 3eqtr3rd 2782 |
. . . . . . 7
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β (π(+gβπ)(π Β· π)) = ((π + 1) Β· π)) |
70 | 54, 56, 69 | 3brtr3d 5137 |
. . . . . 6
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β (π Β· π) β€ ((π + 1) Β· π)) |
71 | 70 | adantr 482 |
. . . . 5
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β (π Β· π) β€ ((π + 1) Β· π)) |
72 | 18, 22 | postr 18214 |
. . . . . 6
β’ ((π β Poset β§ ( 0 β π΅ β§ (π Β· π) β π΅ β§ ((π + 1) Β· π) β π΅)) β (( 0 β€ (π Β· π) β§ (π Β· π) β€ ((π + 1) Β· π)) β 0 β€ ((π + 1) Β· π))) |
73 | 72 | imp 408 |
. . . . 5
β’ (((π β Poset β§ ( 0 β π΅ β§ (π Β· π) β π΅ β§ ((π + 1) Β· π) β π΅)) β§ ( 0 β€ (π Β· π) β§ (π Β· π) β€ ((π + 1) Β· π))) β 0 β€ ((π + 1) Β· π)) |
74 | 30, 43, 44, 71, 73 | syl22anc 838 |
. . . 4
β’
((((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β§ 0 β€ (π Β· π)) β 0 β€ ((π + 1) Β· π)) |
75 | 7, 9, 11, 13, 29, 74 | nn0indd 12605 |
. . 3
β’
(((((π β oMnd
β§ π β π΅) β§ π β β0) β§ 0 β€ π) β§ π β β0) β 0 β€ (π Β· π)) |
76 | 5, 75 | mpdan 686 |
. 2
β’ ((((π β oMnd β§ π β π΅) β§ π β β0) β§ 0 β€ π) β 0 β€ (π Β· π)) |
77 | 4, 76 | sylbi 216 |
1
β’ ((π β oMnd β§ (π β π΅ β§ π β β0) β§ 0 β€ π) β 0 β€ (π Β· π)) |