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 e. _om /\ C e. _om ) /\ (/) e. C ) -> ( A e. B -> ( C .o A ) e. ( C .o B ) ) )

Proof

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