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