Metamath Proof Explorer


Theorem nnmwordi

Description: Weak ordering property of multiplication. (Contributed by Mario Carneiro, 17-Nov-2014)

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

Proof

Step Hyp Ref Expression
1 nnmword A ω B ω C ω C A B C 𝑜 A C 𝑜 B
2 1 biimpd A ω B ω C ω C A B C 𝑜 A C 𝑜 B
3 2 ex A ω B ω C ω C A B C 𝑜 A C 𝑜 B
4 nnord C ω Ord C
5 ord0eln0 Ord C C C
6 5 necon2bbid Ord C C = ¬ C
7 4 6 syl C ω C = ¬ C
8 7 3ad2ant3 A ω B ω C ω C = ¬ C
9 ssid
10 nnm0r A ω 𝑜 A =
11 10 adantr A ω B ω 𝑜 A =
12 nnm0r B ω 𝑜 B =
13 12 adantl A ω B ω 𝑜 B =
14 11 13 sseq12d A ω B ω 𝑜 A 𝑜 B
15 9 14 mpbiri A ω B ω 𝑜 A 𝑜 B
16 oveq1 C = C 𝑜 A = 𝑜 A
17 oveq1 C = C 𝑜 B = 𝑜 B
18 16 17 sseq12d C = C 𝑜 A C 𝑜 B 𝑜 A 𝑜 B
19 15 18 syl5ibrcom A ω B ω C = C 𝑜 A C 𝑜 B
20 19 3adant3 A ω B ω C ω C = C 𝑜 A C 𝑜 B
21 8 20 sylbird A ω B ω C ω ¬ C C 𝑜 A C 𝑜 B
22 21 a1dd A ω B ω C ω ¬ C A B C 𝑜 A C 𝑜 B
23 3 22 pm2.61d A ω B ω C ω A B C 𝑜 A C 𝑜 B