Step | Hyp | Ref
| Expression |
1 | | an4 797 |
. . 3
Nn 1c
Nn
1c
Nn 1c Nn 1c |
2 | | simpl 443 |
. . . . 5
|
3 | 2 | a1i 10 |
. . . 4
Nn Nn Nn |
4 | | reeanv 2778 |
. . . . 5
Nn
Nn 1c 1c
Nn 1c Nn 1c |
5 | | addccom 4406 |
. . . . . . . . . 10
1c
1c |
6 | | peano2 4403 |
. . . . . . . . . 10
Nn
1c
Nn |
7 | 5, 6 | syl5eqel 2437 |
. . . . . . . . 9
Nn 1c Nn |
8 | | nncaddccl 4419 |
. . . . . . . . 9
Nn 1c Nn 1c Nn |
9 | 7, 8 | sylan2 460 |
. . . . . . . 8
Nn Nn 1c Nn |
10 | 9 | adantl 452 |
. . . . . . 7
Nn Nn Nn Nn Nn 1c Nn |
11 | | addceq1 4383 |
. . . . . . . . . 10
1c
1c
|
12 | | addceq1 4383 |
. . . . . . . . . 10
1c 1c
1c
1c |
13 | 11, 12 | syl 15 |
. . . . . . . . 9
1c
1c
1c
1c |
14 | 13 | eqeq2d 2364 |
. . . . . . . 8
1c
1c
1c 1c |
15 | 14 | biimpa 470 |
. . . . . . 7
1c 1c 1c 1c |
16 | | addceq2 4384 |
. . . . . . . . . . . 12
1c
1c |
17 | | addcass 4415 |
. . . . . . . . . . . . 13
1c 1c |
18 | | addcass 4415 |
. . . . . . . . . . . . 13
1c 1c |
19 | 17, 18 | eqtri 2373 |
. . . . . . . . . . . 12
1c
1c |
20 | 16, 19 | syl6eqr 2403 |
. . . . . . . . . . 11
1c
1c |
21 | | addceq1 4383 |
. . . . . . . . . . 11
1c 1c
1c
1c |
22 | 20, 21 | syl 15 |
. . . . . . . . . 10
1c 1c
1c
1c |
23 | 22 | eqeq2d 2364 |
. . . . . . . . 9
1c
1c
1c
1c |
24 | 23 | rspcev 2955 |
. . . . . . . 8
1c Nn
1c
1c
Nn 1c |
25 | 24 | ex 423 |
. . . . . . 7
1c
Nn
1c
1c Nn
1c |
26 | 10, 15, 25 | syl2im 34 |
. . . . . 6
Nn Nn Nn Nn Nn
1c 1c
Nn 1c |
27 | 26 | rexlimdvva 2745 |
. . . . 5
Nn Nn Nn
Nn
Nn 1c 1c
Nn 1c |
28 | 4, 27 | syl5bir 209 |
. . . 4
Nn Nn Nn
Nn 1c Nn 1c
Nn 1c |
29 | 3, 28 | anim12d 546 |
. . 3
Nn Nn Nn
Nn 1c Nn 1c
Nn 1c |
30 | 1, 29 | syl5bi 208 |
. 2
Nn Nn Nn
Nn 1c
Nn
1c
Nn 1c |
31 | | opkltfing 4449 |
. . . 4
Nn Nn fin
Nn
1c |
32 | 31 | 3adant3 975 |
. . 3
Nn Nn Nn fin
Nn
1c |
33 | | opkltfing 4449 |
. . . 4
Nn Nn fin
Nn
1c |
34 | 33 | 3adant1 973 |
. . 3
Nn Nn Nn fin
Nn
1c |
35 | 32, 34 | anbi12d 691 |
. 2
Nn Nn Nn fin fin
Nn
1c
Nn
1c |
36 | | opkltfing 4449 |
. . 3
Nn Nn fin
Nn
1c |
37 | 36 | 3adant2 974 |
. 2
Nn Nn Nn fin
Nn
1c |
38 | 30, 35, 37 | 3imtr4d 259 |
1
Nn Nn Nn fin fin fin |