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 𝐵 ) ) )