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 ⊢ B ∈ ω ∧ C ∈ ω ∧ ∅ ∈ C → A ∈ B → C ⋅ 𝑜 A ∈ C ⋅ 𝑜 B

Proof

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