Metamath Proof Explorer


Theorem nnawordi

Description: Adding to both sides of an inequality in _om . (Contributed by Scott Fenton, 16-Apr-2012) (Revised by Mario Carneiro, 12-May-2012)

Ref Expression
Assertion nnawordi A ω B ω C ω A B A + 𝑜 C B + 𝑜 C

Proof

Step Hyp Ref Expression
1 oveq2 x = A + 𝑜 x = A + 𝑜
2 oveq2 x = B + 𝑜 x = B + 𝑜
3 1 2 sseq12d x = A + 𝑜 x B + 𝑜 x A + 𝑜 B + 𝑜
4 3 imbi2d x = A B A + 𝑜 x B + 𝑜 x A B A + 𝑜 B + 𝑜
5 4 imbi2d x = A ω B ω A B A + 𝑜 x B + 𝑜 x A ω B ω A B A + 𝑜 B + 𝑜
6 oveq2 x = y A + 𝑜 x = A + 𝑜 y
7 oveq2 x = y B + 𝑜 x = B + 𝑜 y
8 6 7 sseq12d x = y A + 𝑜 x B + 𝑜 x A + 𝑜 y B + 𝑜 y
9 8 imbi2d x = y A B A + 𝑜 x B + 𝑜 x A B A + 𝑜 y B + 𝑜 y
10 9 imbi2d x = y A ω B ω A B A + 𝑜 x B + 𝑜 x A ω B ω A B A + 𝑜 y B + 𝑜 y
11 oveq2 x = suc y A + 𝑜 x = A + 𝑜 suc y
12 oveq2 x = suc y B + 𝑜 x = B + 𝑜 suc y
13 11 12 sseq12d x = suc y A + 𝑜 x B + 𝑜 x A + 𝑜 suc y B + 𝑜 suc y
14 13 imbi2d x = suc y A B A + 𝑜 x B + 𝑜 x A B A + 𝑜 suc y B + 𝑜 suc y
15 14 imbi2d x = suc y A ω B ω A B A + 𝑜 x B + 𝑜 x A ω B ω A B A + 𝑜 suc y B + 𝑜 suc y
16 oveq2 x = C A + 𝑜 x = A + 𝑜 C
17 oveq2 x = C B + 𝑜 x = B + 𝑜 C
18 16 17 sseq12d x = C A + 𝑜 x B + 𝑜 x A + 𝑜 C B + 𝑜 C
19 18 imbi2d x = C A B A + 𝑜 x B + 𝑜 x A B A + 𝑜 C B + 𝑜 C
20 19 imbi2d x = C A ω B ω A B A + 𝑜 x B + 𝑜 x A ω B ω A B A + 𝑜 C B + 𝑜 C
21 nnon A ω A On
22 nnon B ω B On
23 oa0 A On A + 𝑜 = A
24 23 adantr A On B On A + 𝑜 = A
25 oa0 B On B + 𝑜 = B
26 25 adantl A On B On B + 𝑜 = B
27 24 26 sseq12d A On B On A + 𝑜 B + 𝑜 A B
28 27 biimprd A On B On A B A + 𝑜 B + 𝑜
29 21 22 28 syl2an A ω B ω A B A + 𝑜 B + 𝑜
30 nnacl A ω y ω A + 𝑜 y ω
31 30 ancoms y ω A ω A + 𝑜 y ω
32 31 adantrr y ω A ω B ω A + 𝑜 y ω
33 nnon A + 𝑜 y ω A + 𝑜 y On
34 eloni A + 𝑜 y On Ord A + 𝑜 y
35 32 33 34 3syl y ω A ω B ω Ord A + 𝑜 y
36 nnacl B ω y ω B + 𝑜 y ω
37 36 ancoms y ω B ω B + 𝑜 y ω
38 37 adantrl y ω A ω B ω B + 𝑜 y ω
39 nnon B + 𝑜 y ω B + 𝑜 y On
40 eloni B + 𝑜 y On Ord B + 𝑜 y
41 38 39 40 3syl y ω A ω B ω Ord B + 𝑜 y
42 ordsucsssuc Ord A + 𝑜 y Ord B + 𝑜 y A + 𝑜 y B + 𝑜 y suc A + 𝑜 y suc B + 𝑜 y
43 35 41 42 syl2anc y ω A ω B ω A + 𝑜 y B + 𝑜 y suc A + 𝑜 y suc B + 𝑜 y
44 43 biimpa y ω A ω B ω A + 𝑜 y B + 𝑜 y suc A + 𝑜 y suc B + 𝑜 y
45 nnasuc A ω y ω A + 𝑜 suc y = suc A + 𝑜 y
46 45 ancoms y ω A ω A + 𝑜 suc y = suc A + 𝑜 y
47 46 adantrr y ω A ω B ω A + 𝑜 suc y = suc A + 𝑜 y
48 nnasuc B ω y ω B + 𝑜 suc y = suc B + 𝑜 y
49 48 ancoms y ω B ω B + 𝑜 suc y = suc B + 𝑜 y
50 49 adantrl y ω A ω B ω B + 𝑜 suc y = suc B + 𝑜 y
51 47 50 sseq12d y ω A ω B ω A + 𝑜 suc y B + 𝑜 suc y suc A + 𝑜 y suc B + 𝑜 y
52 51 adantr y ω A ω B ω A + 𝑜 y B + 𝑜 y A + 𝑜 suc y B + 𝑜 suc y suc A + 𝑜 y suc B + 𝑜 y
53 44 52 mpbird y ω A ω B ω A + 𝑜 y B + 𝑜 y A + 𝑜 suc y B + 𝑜 suc y
54 53 ex y ω A ω B ω A + 𝑜 y B + 𝑜 y A + 𝑜 suc y B + 𝑜 suc y
55 54 imim2d y ω A ω B ω A B A + 𝑜 y B + 𝑜 y A B A + 𝑜 suc y B + 𝑜 suc y
56 55 ex y ω A ω B ω A B A + 𝑜 y B + 𝑜 y A B A + 𝑜 suc y B + 𝑜 suc y
57 56 a2d y ω A ω B ω A B A + 𝑜 y B + 𝑜 y A ω B ω A B A + 𝑜 suc y B + 𝑜 suc y
58 5 10 15 20 29 57 finds C ω A ω B ω A B A + 𝑜 C B + 𝑜 C
59 58 com12 A ω B ω C ω A B A + 𝑜 C B + 𝑜 C
60 59 3impia A ω B ω C ω A B A + 𝑜 C B + 𝑜 C