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