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