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 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐴 ∈ 𝐵 ∧ ∅ ∈ 𝐶 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )

Proof

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