Metamath Proof Explorer

Theorem omopthlem1

Description: Lemma for omopthi . (Contributed by Scott Fenton, 18-Apr-2012) (Revised by Mario Carneiro, 17-Nov-2014)

Ref Expression
Hypotheses omopthlem1.1 ⊢ A ∈ ω
omopthlem1.2 ⊢ C ∈ ω
Assertion omopthlem1 ⊢ A ∈ C → A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 ∈ C ⋅ 𝑜 C

Proof

Step Hyp Ref Expression
1 omopthlem1.1 ⊢ A ∈ ω
2 omopthlem1.2 ⊢ C ∈ ω
3 peano2 ⊢ A ∈ ω → suc ⁡ A ∈ ω
4 1 3 ax-mp ⊢ suc ⁡ A ∈ ω
5 nnmwordi ⊢ suc ⁡ A ∈ ω ∧ C ∈ ω ∧ suc ⁡ A ∈ ω → suc ⁡ A ⊆ C → suc ⁡ A ⋅ 𝑜 suc ⁡ A ⊆ suc ⁡ A ⋅ 𝑜 C
6 4 2 4 5 mp3an ⊢ suc ⁡ A ⊆ C → suc ⁡ A ⋅ 𝑜 suc ⁡ A ⊆ suc ⁡ A ⋅ 𝑜 C
7 nnmwordri ⊢ suc ⁡ A ∈ ω ∧ C ∈ ω ∧ C ∈ ω → suc ⁡ A ⊆ C → suc ⁡ A ⋅ 𝑜 C ⊆ C ⋅ 𝑜 C
8 4 2 2 7 mp3an ⊢ suc ⁡ A ⊆ C → suc ⁡ A ⋅ 𝑜 C ⊆ C ⋅ 𝑜 C
9 6 8 sstrd ⊢ suc ⁡ A ⊆ C → suc ⁡ A ⋅ 𝑜 suc ⁡ A ⊆ C ⋅ 𝑜 C
10 1 nnoni ⊢ A ∈ On
11 2 nnoni ⊢ C ∈ On
12 10 11 onsucssi ⊢ A ∈ C ↔ suc ⁡ A ⊆ C
13 1 1 nnmcli ⊢ A ⋅ 𝑜 A ∈ ω
14 2onn ⊢ 2 𝑜 ∈ ω
15 1 14 nnmcli ⊢ A ⋅ 𝑜 2 𝑜 ∈ ω
16 13 15 nnacli ⊢ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 ∈ ω
17 16 nnoni ⊢ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 ∈ On
18 2 2 nnmcli ⊢ C ⋅ 𝑜 C ∈ ω
19 18 nnoni ⊢ C ⋅ 𝑜 C ∈ On
20 17 19 onsucssi ⊢ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 ∈ C ⋅ 𝑜 C ↔ suc ⁡ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 ⊆ C ⋅ 𝑜 C
21 4 1 nnmcli ⊢ suc ⁡ A ⋅ 𝑜 A ∈ ω
22 nnasuc ⊢ suc ⁡ A ⋅ 𝑜 A ∈ ω ∧ A ∈ ω → suc ⁡ A ⋅ 𝑜 A + 𝑜 suc ⁡ A = suc ⁡ suc ⁡ A ⋅ 𝑜 A + 𝑜 A
23 21 1 22 mp2an ⊢ suc ⁡ A ⋅ 𝑜 A + 𝑜 suc ⁡ A = suc ⁡ suc ⁡ A ⋅ 𝑜 A + 𝑜 A
24 nnmsuc ⊢ suc ⁡ A ∈ ω ∧ A ∈ ω → suc ⁡ A ⋅ 𝑜 suc ⁡ A = suc ⁡ A ⋅ 𝑜 A + 𝑜 suc ⁡ A
25 4 1 24 mp2an ⊢ suc ⁡ A ⋅ 𝑜 suc ⁡ A = suc ⁡ A ⋅ 𝑜 A + 𝑜 suc ⁡ A
26 nnaass ⊢ A ⋅ 𝑜 A ∈ ω ∧ A ∈ ω ∧ A ∈ ω → A ⋅ 𝑜 A + 𝑜 A + 𝑜 A = A ⋅ 𝑜 A + 𝑜 A + 𝑜 A
27 13 1 1 26 mp3an ⊢ A ⋅ 𝑜 A + 𝑜 A + 𝑜 A = A ⋅ 𝑜 A + 𝑜 A + 𝑜 A
28 nnmcom ⊢ suc ⁡ A ∈ ω ∧ A ∈ ω → suc ⁡ A ⋅ 𝑜 A = A ⋅ 𝑜 suc ⁡ A
29 4 1 28 mp2an ⊢ suc ⁡ A ⋅ 𝑜 A = A ⋅ 𝑜 suc ⁡ A
30 nnmsuc ⊢ A ∈ ω ∧ A ∈ ω → A ⋅ 𝑜 suc ⁡ A = A ⋅ 𝑜 A + 𝑜 A
31 1 1 30 mp2an ⊢ A ⋅ 𝑜 suc ⁡ A = A ⋅ 𝑜 A + 𝑜 A
32 29 31 eqtri ⊢ suc ⁡ A ⋅ 𝑜 A = A ⋅ 𝑜 A + 𝑜 A
33 32 oveq1i ⊢ suc ⁡ A ⋅ 𝑜 A + 𝑜 A = A ⋅ 𝑜 A + 𝑜 A + 𝑜 A
34 nnm2 ⊢ A ∈ ω → A ⋅ 𝑜 2 𝑜 = A + 𝑜 A
35 1 34 ax-mp ⊢ A ⋅ 𝑜 2 𝑜 = A + 𝑜 A
36 35 oveq2i ⊢ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 = A ⋅ 𝑜 A + 𝑜 A + 𝑜 A
37 27 33 36 3eqtr4ri ⊢ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 = suc ⁡ A ⋅ 𝑜 A + 𝑜 A
38 suceq ⊢ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 = suc ⁡ A ⋅ 𝑜 A + 𝑜 A → suc ⁡ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 = suc ⁡ suc ⁡ A ⋅ 𝑜 A + 𝑜 A
39 37 38 ax-mp ⊢ suc ⁡ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 = suc ⁡ suc ⁡ A ⋅ 𝑜 A + 𝑜 A
40 23 25 39 3eqtr4ri ⊢ suc ⁡ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 = suc ⁡ A ⋅ 𝑜 suc ⁡ A
41 40 sseq1i ⊢ suc ⁡ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 ⊆ C ⋅ 𝑜 C ↔ suc ⁡ A ⋅ 𝑜 suc ⁡ A ⊆ C ⋅ 𝑜 C
42 20 41 bitri ⊢ A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 ∈ C ⋅ 𝑜 C ↔ suc ⁡ A ⋅ 𝑜 suc ⁡ A ⊆ C ⋅ 𝑜 C
43 9 12 42 3imtr4i ⊢ A ∈ C → A ⋅ 𝑜 A + 𝑜 A ⋅ 𝑜 2 𝑜 ∈ C ⋅ 𝑜 C