Step | Hyp | Ref
| Expression |
1 | | omndmul.n |
. 2
β’ (π β π β
β0) |
2 | | oveq1 7365 |
. . . 4
β’ (π = 0 β (π Β· π) = (0 Β· π)) |
3 | | oveq1 7365 |
. . . 4
β’ (π = 0 β (π Β· π) = (0 Β· π)) |
4 | 2, 3 | breq12d 5119 |
. . 3
β’ (π = 0 β ((π Β· π) β€ (π Β· π) β (0 Β· π) β€ (0 Β· π))) |
5 | | oveq1 7365 |
. . . 4
β’ (π = π β (π Β· π) = (π Β· π)) |
6 | | oveq1 7365 |
. . . 4
β’ (π = π β (π Β· π) = (π Β· π)) |
7 | 5, 6 | breq12d 5119 |
. . 3
β’ (π = π β ((π Β· π) β€ (π Β· π) β (π Β· π) β€ (π Β· π))) |
8 | | oveq1 7365 |
. . . 4
β’ (π = (π + 1) β (π Β· π) = ((π + 1) Β· π)) |
9 | | oveq1 7365 |
. . . 4
β’ (π = (π + 1) β (π Β· π) = ((π + 1) Β· π)) |
10 | 8, 9 | breq12d 5119 |
. . 3
β’ (π = (π + 1) β ((π Β· π) β€ (π Β· π) β ((π + 1) Β· π) β€ ((π + 1) Β· π))) |
11 | | oveq1 7365 |
. . . 4
β’ (π = π β (π Β· π) = (π Β· π)) |
12 | | oveq1 7365 |
. . . 4
β’ (π = π β (π Β· π) = (π Β· π)) |
13 | 11, 12 | breq12d 5119 |
. . 3
β’ (π = π β ((π Β· π) β€ (π Β· π) β (π Β· π) β€ (π Β· π))) |
14 | | omndmul.o |
. . . . . 6
β’ (π β π β oMnd) |
15 | | omndtos 31962 |
. . . . . 6
β’ (π β oMnd β π β Toset) |
16 | | tospos 18314 |
. . . . . 6
β’ (π β Toset β π β Poset) |
17 | 14, 15, 16 | 3syl 18 |
. . . . 5
β’ (π β π β Poset) |
18 | | omndmul.y |
. . . . . . 7
β’ (π β π β π΅) |
19 | | omndmul.0 |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
20 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ) = (0gβπ) |
21 | | omndmul.2 |
. . . . . . . 8
β’ Β· =
(.gβπ) |
22 | 19, 20, 21 | mulg0 18884 |
. . . . . . 7
β’ (π β π΅ β (0 Β· π) = (0gβπ)) |
23 | 18, 22 | syl 17 |
. . . . . 6
β’ (π β (0 Β· π) = (0gβπ)) |
24 | | omndmnd 31961 |
. . . . . . 7
β’ (π β oMnd β π β Mnd) |
25 | 19, 20 | mndidcl 18576 |
. . . . . . 7
β’ (π β Mnd β
(0gβπ)
β π΅) |
26 | 14, 24, 25 | 3syl 18 |
. . . . . 6
β’ (π β (0gβπ) β π΅) |
27 | 23, 26 | eqeltrd 2834 |
. . . . 5
β’ (π β (0 Β· π) β π΅) |
28 | | omndmul.1 |
. . . . . 6
β’ β€ =
(leβπ) |
29 | 19, 28 | posref 18212 |
. . . . 5
β’ ((π β Poset β§ (0 Β· π) β π΅) β (0 Β· π) β€ (0 Β· π)) |
30 | 17, 27, 29 | syl2anc 585 |
. . . 4
β’ (π β (0 Β· π) β€ (0 Β· π)) |
31 | | omndmul.x |
. . . . 5
β’ (π β π β π΅) |
32 | 19, 20, 21 | mulg0 18884 |
. . . . . . . 8
β’ (π β π΅ β (0 Β· π) = (0gβπ)) |
33 | 32 | adantr 482 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β (0 Β· π) = (0gβπ)) |
34 | 22 | adantl 483 |
. . . . . . 7
β’ ((π β π΅ β§ π β π΅) β (0 Β· π) = (0gβπ)) |
35 | 33, 34 | eqtr4d 2776 |
. . . . . 6
β’ ((π β π΅ β§ π β π΅) β (0 Β· π) = (0 Β· π)) |
36 | 35 | breq1d 5116 |
. . . . 5
β’ ((π β π΅ β§ π β π΅) β ((0 Β· π) β€ (0 Β· π) β (0 Β· π) β€ (0 Β· π))) |
37 | 31, 18, 36 | syl2anc 585 |
. . . 4
β’ (π β ((0 Β· π) β€ (0 Β· π) β (0 Β· π) β€ (0 Β· π))) |
38 | 30, 37 | mpbird 257 |
. . 3
β’ (π β (0 Β· π) β€ (0 Β· π)) |
39 | | eqid 2733 |
. . . . 5
β’
(+gβπ) = (+gβπ) |
40 | 14 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β π β oMnd) |
41 | 18 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β π β π΅) |
42 | 40, 24 | syl 17 |
. . . . . 6
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β π β Mnd) |
43 | | simplr 768 |
. . . . . 6
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β π β β0) |
44 | 31 | ad2antrr 725 |
. . . . . 6
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β π β π΅) |
45 | 19, 21, 42, 43, 44 | mulgnn0cld 18902 |
. . . . 5
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β (π Β· π) β π΅) |
46 | 19, 21, 42, 43, 41 | mulgnn0cld 18902 |
. . . . 5
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β (π Β· π) β π΅) |
47 | | simpr 486 |
. . . . 5
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β (π Β· π) β€ (π Β· π)) |
48 | | omndmul.l |
. . . . . 6
β’ (π β π β€ π) |
49 | 48 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β π β€ π) |
50 | | omndmul.c |
. . . . . 6
β’ (π β π β CMnd) |
51 | 50 | ad2antrr 725 |
. . . . 5
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β π β CMnd) |
52 | 19, 28, 39, 40, 41, 45, 44, 46, 47, 49, 51 | omndadd2d 31965 |
. . . 4
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β ((π Β· π)(+gβπ)π) β€ ((π Β· π)(+gβπ)π)) |
53 | 19, 21, 39 | mulgnn0p1 18892 |
. . . . 5
β’ ((π β Mnd β§ π β β0
β§ π β π΅) β ((π + 1) Β· π) = ((π Β· π)(+gβπ)π)) |
54 | 42, 43, 44, 53 | syl3anc 1372 |
. . . 4
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β ((π + 1) Β· π) = ((π Β· π)(+gβπ)π)) |
55 | 19, 21, 39 | mulgnn0p1 18892 |
. . . . 5
β’ ((π β Mnd β§ π β β0
β§ π β π΅) β ((π + 1) Β· π) = ((π Β· π)(+gβπ)π)) |
56 | 42, 43, 41, 55 | syl3anc 1372 |
. . . 4
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β ((π + 1) Β· π) = ((π Β· π)(+gβπ)π)) |
57 | 52, 54, 56 | 3brtr4d 5138 |
. . 3
β’ (((π β§ π β β0) β§ (π Β· π) β€ (π Β· π)) β ((π + 1) Β· π) β€ ((π + 1) Β· π)) |
58 | 4, 7, 10, 13, 38, 57 | nn0indd 12605 |
. 2
β’ ((π β§ π β β0) β (π Β· π) β€ (π Β· π)) |
59 | 1, 58 | mpdan 686 |
1
β’ (π β (π Β· π) β€ (π Β· π)) |