Metamath Proof Explorer

Theorem nnmordi

Description: Ordering property of multiplication. Half of Proposition 8.19 of TakeutiZaring p. 63, limited to natural numbers. (Contributed by NM, 18-Sep-1995) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nnmordi ( ( ( 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 elnn ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ∈ ω ) → 𝐴 ∈ ω )
2 1 expcom ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ 𝐵 → 𝐴 ∈ ω ) )
3 eleq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝐵 ) )
4 oveq2 ⊢ ( 𝑥 = 𝐵 → ( 𝐶 ·o 𝑥 ) = ( 𝐶 ·o 𝐵 ) )
5 4 eleq2d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )
6 3 5 imbi12d ⊢ ( 𝑥 = 𝐵 → ( ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ↔ ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) )
7 6 imbi2d ⊢ ( 𝑥 = 𝐵 → ( ( ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ) ↔ ( ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) )
8 eleq2 ⊢ ( 𝑥 = ∅ → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ∅ ) )
9 oveq2 ⊢ ( 𝑥 = ∅ → ( 𝐶 ·o 𝑥 ) = ( 𝐶 ·o ∅ ) )
10 9 eleq2d ⊢ ( 𝑥 = ∅ → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o ∅ ) ) )
11 8 10 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ↔ ( 𝐴 ∈ ∅ → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o ∅ ) ) ) )
12 eleq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ 𝑦 ) )
13 oveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐶 ·o 𝑥 ) = ( 𝐶 ·o 𝑦 ) )
14 13 eleq2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) )
15 12 14 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ↔ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) )
16 eleq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ suc 𝑦 ) )
17 oveq2 ⊢ ( 𝑥 = suc 𝑦 → ( 𝐶 ·o 𝑥 ) = ( 𝐶 ·o suc 𝑦 ) )
18 17 eleq2d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) )
19 16 18 imbi12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ↔ ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) ) )
20 noel ⊢ ¬ 𝐴 ∈ ∅
21 20 pm2.21i ⊢ ( 𝐴 ∈ ∅ → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o ∅ ) )
22 21 a1i ⊢ ( ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ ∅ → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o ∅ ) ) )
23 elsuci ⊢ ( 𝐴 ∈ suc 𝑦 → ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) )
24 nnmcl ⊢ ( ( 𝐶 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐶 ·o 𝑦 ) ∈ ω )
25 simpl ⊢ ( ( 𝐶 ∈ ω ∧ 𝑦 ∈ ω ) → 𝐶 ∈ ω )
26 24 25 jca ⊢ ( ( 𝐶 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) )
27 nnaword1 ⊢ ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) → ( 𝐶 ·o 𝑦 ) ⊆ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) )
28 27 sseld ⊢ ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
29 28 imim2d ⊢ ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) ) )
30 29 imp ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) → ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
31 30 adantrl ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
32 nna0 ⊢ ( ( 𝐶 ·o 𝑦 ) ∈ ω → ( ( 𝐶 ·o 𝑦 ) +o ∅ ) = ( 𝐶 ·o 𝑦 ) )
33 32 ad2antrr ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝑦 ) +o ∅ ) = ( 𝐶 ·o 𝑦 ) )
34 nnaordi ⊢ ( ( 𝐶 ∈ ω ∧ ( 𝐶 ·o 𝑦 ) ∈ ω ) → ( ∅ ∈ 𝐶 → ( ( 𝐶 ·o 𝑦 ) +o ∅ ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
35 34 ancoms ⊢ ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) → ( ∅ ∈ 𝐶 → ( ( 𝐶 ·o 𝑦 ) +o ∅ ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
36 35 imp ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐶 ·o 𝑦 ) +o ∅ ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) )
37 33 36 eqeltrrd ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝑦 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) )
38 oveq2 ⊢ ( 𝐴 = 𝑦 → ( 𝐶 ·o 𝐴 ) = ( 𝐶 ·o 𝑦 ) )
39 38 eleq1d ⊢ ( 𝐴 = 𝑦 → ( ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ↔ ( 𝐶 ·o 𝑦 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
40 37 39 syl5ibrcom ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 = 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
41 40 adantrr ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( 𝐴 = 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
42 31 41 jaod ⊢ ( ( ( ( 𝐶 ·o 𝑦 ) ∈ ω ∧ 𝐶 ∈ ω ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
43 26 42 sylan ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝑦 ∈ ω ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
44 23 43 syl5 ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝑦 ∈ ω ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
45 nnmsuc ⊢ ( ( 𝐶 ∈ ω ∧ 𝑦 ∈ ω ) → ( 𝐶 ·o suc 𝑦 ) = ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) )
46 45 eleq2d ⊢ ( ( 𝐶 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
47 46 adantr ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝑦 ∈ ω ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ↔ ( 𝐶 ·o 𝐴 ) ∈ ( ( 𝐶 ·o 𝑦 ) +o 𝐶 ) ) )
48 44 47 sylibrd ⊢ ( ( ( 𝐶 ∈ ω ∧ 𝑦 ∈ ω ) ∧ ( ∅ ∈ 𝐶 ∧ ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) )
49 48 exp43 ⊢ ( 𝐶 ∈ ω → ( 𝑦 ∈ ω → ( ∅ ∈ 𝐶 → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) ) ) ) )
50 49 com12 ⊢ ( 𝑦 ∈ ω → ( 𝐶 ∈ ω → ( ∅ ∈ 𝐶 → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) ) ) ) )
51 50 adantld ⊢ ( 𝑦 ∈ ω → ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) → ( ∅ ∈ 𝐶 → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) ) ) ) )
52 51 impd ⊢ ( 𝑦 ∈ ω → ( ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( ( 𝐴 ∈ 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o suc 𝑦 ) ) ) ) )
53 11 15 19 22 52 finds2 ⊢ ( 𝑥 ∈ ω → ( ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝑥 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝑥 ) ) ) )
54 7 53 vtoclga ⊢ ( 𝐵 ∈ ω → ( ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) )
55 54 com23 ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ 𝐵 → ( ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) )
56 55 exp4a ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ 𝐵 → ( ( 𝐴 ∈ ω ∧ 𝐶 ∈ ω ) → ( ∅ ∈ 𝐶 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) )
57 56 exp4a ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ 𝐵 → ( 𝐴 ∈ ω → ( 𝐶 ∈ ω → ( ∅ ∈ 𝐶 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) ) )
58 2 57 mpdd ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ 𝐵 → ( 𝐶 ∈ ω → ( ∅ ∈ 𝐶 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) )
59 58 com34 ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ 𝐵 → ( ∅ ∈ 𝐶 → ( 𝐶 ∈ ω → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) )
60 59 com24 ⊢ ( 𝐵 ∈ ω → ( 𝐶 ∈ ω → ( ∅ ∈ 𝐶 → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) ) ) )
61 60 imp31 ⊢ ( ( ( 𝐵 ∈ ω ∧ 𝐶 ∈ ω ) ∧ ∅ ∈ 𝐶 ) → ( 𝐴 ∈ 𝐵 → ( 𝐶 ·o 𝐴 ) ∈ ( 𝐶 ·o 𝐵 ) ) )