Theorem nnmordi 3188

Description: Ordering property of multiplication. Half of Proposition 8.19 of [TakeutiZaring] p. 63, limited to natural numbers.

Assertion

Ref	Expression
nnmordi	|- ((A e. om /\ B e. om /\ C e. om) -> ((A e. B /\ (/) e. C) -> (C .o A) e. (C .o B)))

Proof of Theorem nnmordi

Step	Hyp	Ref	Expression
1		opreq2 3007	. . . . . . . . . . . . 13 |- (x = suc A -> (C .o x) = (C .o suc A))
2	1	sseq2d 1528	. . . . . . . . . . . 12 |- (x = suc A -> ((C .o suc A) (_ (C .o x) <-> (C .o suc A) (_ (C .o suc A)))
3	2	imbi2d 464	. . . . . . . . . . 11 |- (x = suc A -> ((C e. om -> (C .o suc A) (_ (C .o x)) <-> (C e. om -> (C .o suc A) (_ (C .o suc A))))
4		opreq2 3007	. . . . . . . . . . . . 13 |- (x = y -> (C .o x) = (C .o y))
5	4	sseq2d 1528	. . . . . . . . . . . 12 |- (x = y -> ((C .o suc A) (_ (C .o x) <-> (C .o suc A) (_ (C .o y)))
6	5	imbi2d 464	. . . . . . . . . . 11 |- (x = y -> ((C e. om -> (C .o suc A) (_ (C .o x)) <-> (C e. om -> (C .o suc A) (_ (C .o y))))
7		opreq2 3007	. . . . . . . . . . . . 13 |- (x = suc y -> (C .o x) = (C .o suc y))
8	7	sseq2d 1528	. . . . . . . . . . . 12 |- (x = suc y -> ((C .o suc A) (_ (C .o x) <-> (C .o suc A) (_ (C .o suc y)))
9	8	imbi2d 464	. . . . . . . . . . 11 |- (x = suc y -> ((C e. om -> (C .o suc A) (_ (C .o x)) <-> (C e. om -> (C .o suc A) (_ (C .o suc y))))
10		opreq2 3007	. . . . . . . . . . . . 13 |- (x = B -> (C .o x) = (C .o B))
11	10	sseq2d 1528	. . . . . . . . . . . 12 |- (x = B -> ((C .o suc A) (_ (C .o x) <-> (C .o suc A) (_ (C .o B)))
12	11	imbi2d 464	. . . . . . . . . . 11 |- (x = B -> ((C e. om -> (C .o suc A) (_ (C .o x)) <-> (C e. om -> (C .o suc A) (_ (C .o B))))
13		ssid 1519	. . . . . . . . . . . . 13 |- (C .o suc A) (_ (C .o suc A)
14	13	a1i 7	. . . . . . . . . . . 12 |- (C e. om -> (C .o suc A) (_ (C .o suc A))
15	14	a1i 7	. . . . . . . . . . 11 |- (suc A e. om -> (C e. om -> (C .o suc A) (_ (C .o suc A)))
16		sstr2 1510	. . . . . . . . . . . . . . . . . 18 |- ((C .o suc A) (_ (C .o y) -> ((C .o y) (_ ((C .o y) +o C) -> (C .o suc A) (_ ((C .o y) +o C)))
17		pm3.27 260	. . . . . . . . . . . . . . . . . . . . . 22 |- ((C e. om /\ (C .o y) e. om) -> (C .o y) e. om)
18		nnont 2379	. . . . . . . . . . . . . . . . . . . . . 22 |- ((C .o y) e. om -> (C .o y) e. On)
19		oa0 3124	. . . . . . . . . . . . . . . . . . . . . 22 |- ((C .o y) e. On -> ((C .o y) +o (/)) = (C .o y))
20	17, 18, 19	3syl 21	. . . . . . . . . . . . . . . . . . . . 21 |- ((C e. om /\ (C .o y) e. om) -> ((C .o y) +o (/)) = (C .o y))
21		peano1 2390	. . . . . . . . . . . . . . . . . . . . . 22 |- (/) e. om
22		0ss 1725	. . . . . . . . . . . . . . . . . . . . . . 23 |- (/) (_ C
23		nnaword 3185	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((/) e. om /\ C e. om /\ (C .o y) e. om) -> ((/) (_ C <-> ((C .o y) +o (/)) (_ ((C .o y) +o C)))
24	22, 23	mpbii 168	. . . . . . . . . . . . . . . . . . . . . 22 |- (((/) e. om /\ C e. om /\ (C .o y) e. om) -> ((C .o y) +o (/)) (_ ((C .o y) +o C))
25	21, 24	mp3an1 639	. . . . . . . . . . . . . . . . . . . . 21 |- ((C e. om /\ (C .o y) e. om) -> ((C .o y) +o (/)) (_ ((C .o y) +o C))
26	20, 25	eqsstr3d 1535	. . . . . . . . . . . . . . . . . . . 20 |- ((C e. om /\ (C .o y) e. om) -> (C .o y) (_ ((C .o y) +o C))
27		nnmcl 3173	. . . . . . . . . . . . . . . . . . . 20 |- ((C e. om /\ y e. om) -> (C .o y) e. om)
28	26, 27	sylan2 346	. . . . . . . . . . . . . . . . . . 19 |- ((C e. om /\ (C e. om /\ y e. om)) -> (C .o y) (_ ((C .o y) +o C))
29	28	anabss5 384	. . . . . . . . . . . . . . . . . 18 |- ((C e. om /\ y e. om) -> (C .o y) (_ ((C .o y) +o C))
30	16, 29	syl5 22	. . . . . . . . . . . . . . . . 17 |- ((C .o suc A) (_ (C .o y) -> ((C e. om /\ y e. om) -> (C .o suc A) (_ ((C .o y) +o C)))
31	30	com12 13	. . . . . . . . . . . . . . . 16 |- ((C e. om /\ y e. om) -> ((C .o suc A) (_ (C .o y) -> (C .o suc A) (_ ((C .o y) +o C)))
32		nnmsuc 3169	. . . . . . . . . . . . . . . . 17 |- ((C e. om /\ y e. om) -> (C .o suc y) = ((C .o y) +o C))
33	32	sseq2d 1528	. . . . . . . . . . . . . . . 16 |- ((C e. om /\ y e. om) -> ((C .o suc A) (_ (C .o suc y) <-> (C .o suc A) (_ ((C .o y) +o C)))
34	31, 33	sylibrd 179	. . . . . . . . . . . . . . 15 |- ((C e. om /\ y e. om) -> ((C .o suc A) (_ (C .o y) -> (C .o suc A) (_ (C .o suc y)))
35	34	exp 291	. . . . . . . . . . . . . 14 |- (C e. om -> (y e. om -> ((C .o suc A) (_ (C .o y) -> (C .o suc A) (_ (C .o suc y))))
36	35	com12 13	. . . . . . . . . . . . 13 |- (y e. om -> (C e. om -> ((C .o suc A) (_ (C .o y) -> (C .o suc A) (_ (C .o suc y))))
37	36	ad2antll 320	. . . . . . . . . . . 12 |- (((y e. om /\ suc A e. om) /\ suc A (_ y) -> (C e. om -> ((C .o suc A) (_ (C .o y) -> (C .o suc A) (_ (C .o suc y))))
38	37	a2d 15	. . . . . . . . . . 11 |- (((y e. om /\ suc A e. om) /\ suc A (_ y) -> ((C e. om -> (C .o suc A) (_ (C .o y)) -> (C e. om -> (C .o suc A) (_ (C .o suc y))))
39	3, 6, 9, 12, 15, 38	findsg 2398	. . . . . . . . . 10 |- (((B e. om /\ suc A e. om) /\ suc A (_ B) -> (C e. om -> (C .o suc A) (_ (C .o B)))
40	39	exp 291	. . . . . . . . 9 |- ((B e. om /\ suc A e. om) -> (suc A (_ B -> (C e. om -> (C .o suc A) (_ (C .o B))))
41		peano2b 2388	. . . . . . . . 9 |- (A e. om <-> suc A e. om)
42	40, 41	sylan2b 347	. . . . . . . 8 |- ((B e. om /\ A e. om) -> (suc A (_ B -> (C e. om -> (C .o suc A) (_ (C .o B))))
43		ordsucss 2320	. . . . . . . . . 10 |- (Ord B -> (A e. B -> suc A (_ B))
44	43	imp 277	. . . . . . . . 9 |- ((Ord B /\ A e. B) -> suc A (_ B)
45		nnord 2381	. . . . . . . . 9 |- (B e. om -> Ord B)
46	44, 45	sylan 343	. . . . . . . 8 |- ((B e. om /\ A e. B) -> suc A (_ B)
47	42, 46	syl5 22	. . . . . . 7 |- ((B e. om /\ A e. om) -> ((B e. om /\ A e. B) -> (C e. om -> (C .o suc A) (_ (C .o B))))
48	47	exp4b 296	. . . . . 6 |- (B e. om -> (A e. om -> (B e. om -> (A e. B -> (C e. om -> (C .o suc A) (_ (C .o B))))))
49	48	pm2.43b 61	. . . . 5 |- (A e. om -> (B e. om -> (A e. B -> (C e. om -> (C .o suc A) (_ (C .o B)))))
50	49	com34 36	. . . 4 |- (A e. om -> (B e. om -> (C e. om -> (A e. B -> (C .o suc A) (_ (C .o B)))))
51	50	3imp 608	. . 3 |- ((A e. om /\ B e. om /\ C e. om) -> (A e. B -> (C .o suc A) (_ (C .o B)))
52		nnmsuc 3169	. . . . . . . 8 |- ((C e. om /\ A e. om) -> (C .o suc A) = ((C .o A) +o C))
53	52	sseq1d 1527	. . . . . . 7 |- ((C e. om /\ A e. om) -> ((C .o suc A) (_ (C .o B) <-> ((C .o A) +o C) (_ (C .o B)))
54		ssel 1502	. . . . . . 7 |- (((C .o A) +o C) (_ (C .o B) -> ((C .o A) e. ((C .o A) +o C) -> (C .o A) e. (C .o B)))
55	53, 54	syl6bi 187	. . . . . 6 |- ((C e. om /\ A e. om) -> ((C .o suc A) (_ (C .o B) -> ((C .o A) e. ((C .o A) +o C) -> (C .o A) e. (C .o B))))
56		nnaordi 3176	. . . . . . . . 9 |- ((C e. om /\ (C .o A) e. om) -> ((/) e. C -> ((C .o A) +o (/)) e. ((C .o A) +o C)))
57		pm3.27 260	. . . . . . . . . . 11 |- ((C e. om /\ (C .o A) e. om) -> (C .o A) e. om)
58		nnont 2379	. . . . . . . . . . 11 |- ((C .o A) e. om -> (C .o A) e. On)
59		oa0 3124	. . . . . . . . . . 11 |- ((C .o A) e. On -> ((C .o A) +o (/)) = (C .o A))
60	57, 58, 59	3syl 21	. . . . . . . . . 10 |- ((C e. om /\ (C .o A) e. om) -> ((C .o A) +o (/)) = (C .o A))
61	60	eleq1d 1155	. . . . . . . . 9 |- ((C e. om /\ (C .o A) e. om) -> (((C .o A) +o (/)) e. ((C .o A) +o C) <-> (C .o A) e. ((C .o