Metamath Proof Explorer


Theorem nnmord

Description: Ordering property of multiplication. Proposition 8.19 of TakeutiZaring p. 63, limited to natural numbers. (Contributed by NM, 22-Jan-1996) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnmord A ω B ω C ω A B C C 𝑜 A C 𝑜 B

Proof

Step Hyp Ref Expression
1 nnmordi B ω C ω C A B C 𝑜 A C 𝑜 B
2 1 ex B ω C ω C A B C 𝑜 A C 𝑜 B
3 2 impcomd B ω C ω A B C C 𝑜 A C 𝑜 B
4 3 3adant1 A ω B ω C ω A B C C 𝑜 A C 𝑜 B
5 ne0i C 𝑜 A C 𝑜 B C 𝑜 B
6 nnm0r B ω 𝑜 B =
7 oveq1 C = C 𝑜 B = 𝑜 B
8 7 eqeq1d C = C 𝑜 B = 𝑜 B =
9 6 8 syl5ibrcom B ω C = C 𝑜 B =
10 9 necon3d B ω C 𝑜 B C
11 5 10 syl5 B ω C 𝑜 A C 𝑜 B C
12 11 adantr B ω C ω C 𝑜 A C 𝑜 B C
13 nnord C ω Ord C
14 ord0eln0 Ord C C C
15 13 14 syl C ω C C
16 15 adantl B ω C ω C C
17 12 16 sylibrd B ω C ω C 𝑜 A C 𝑜 B C
18 17 3adant1 A ω B ω C ω C 𝑜 A C 𝑜 B C
19 oveq2 A = B C 𝑜 A = C 𝑜 B
20 19 a1i A ω B ω C ω C A = B C 𝑜 A = C 𝑜 B
21 nnmordi A ω C ω C B A C 𝑜 B C 𝑜 A
22 21 3adantl2 A ω B ω C ω C B A C 𝑜 B C 𝑜 A
23 20 22 orim12d A ω B ω C ω C A = B B A C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
24 23 con3d A ω B ω C ω C ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A ¬ A = B B A
25 simpl3 A ω B ω C ω C C ω
26 simpl1 A ω B ω C ω C A ω
27 nnmcl C ω A ω C 𝑜 A ω
28 25 26 27 syl2anc A ω B ω C ω C C 𝑜 A ω
29 simpl2 A ω B ω C ω C B ω
30 nnmcl C ω B ω C 𝑜 B ω
31 25 29 30 syl2anc A ω B ω C ω C C 𝑜 B ω
32 nnord C 𝑜 A ω Ord C 𝑜 A
33 nnord C 𝑜 B ω Ord C 𝑜 B
34 ordtri2 Ord C 𝑜 A Ord C 𝑜 B C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
35 32 33 34 syl2an C 𝑜 A ω C 𝑜 B ω C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
36 28 31 35 syl2anc A ω B ω C ω C C 𝑜 A C 𝑜 B ¬ C 𝑜 A = C 𝑜 B C 𝑜 B C 𝑜 A
37 nnord A ω Ord A
38 nnord B ω Ord B
39 ordtri2 Ord A Ord B A B ¬ A = B B A
40 37 38 39 syl2an A ω B ω A B ¬ A = B B A
41 26 29 40 syl2anc A ω B ω C ω C A B ¬ A = B B A
42 24 36 41 3imtr4d A ω B ω C ω C C 𝑜 A C 𝑜 B A B
43 42 ex A ω B ω C ω C C 𝑜 A C 𝑜 B A B
44 43 com23 A ω B ω C ω C 𝑜 A C 𝑜 B C A B
45 18 44 mpdd A ω B ω C ω C 𝑜 A C 𝑜 B A B
46 45 18 jcad A ω B ω C ω C 𝑜 A C 𝑜 B A B C
47 4 46 impbid A ω B ω C ω A B C C 𝑜 A C 𝑜 B