Step | Hyp | Ref
| Expression |
1 | | opklefing 4448 |
. . . 4
Nn Nn fin Nn |
2 | 1 | 3adant3 975 |
. . 3
Nn Nn Nn fin Nn |
3 | | addcnnul 4453 |
. . . . . . . . . 10
|
4 | 3 | simpld 445 |
. . . . . . . . 9
|
5 | 4 | a1i 10 |
. . . . . . . 8
Nn Nn Nn
|
6 | | nncaddccl 4419 |
. . . . . . . . . . . . . 14
Nn Nn Nn |
7 | 6 | 3adant1 973 |
. . . . . . . . . . . . 13
Nn Nn Nn Nn |
8 | | addcass 4415 |
. . . . . . . . . . . . . . 15
|
9 | | addceq1 4383 |
. . . . . . . . . . . . . . 15
1c 1c |
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . . . . . 14
1c
1c |
11 | 10 | a1i 10 |
. . . . . . . . . . . . 13
Nn Nn Nn 1c
1c |
12 | | addceq2 4384 |
. . . . . . . . . . . . . . . 16
|
13 | | addceq1 4383 |
. . . . . . . . . . . . . . . 16
1c 1c |
14 | 12, 13 | syl 15 |
. . . . . . . . . . . . . . 15
1c 1c |
15 | 14 | eqeq2d 2364 |
. . . . . . . . . . . . . 14
1c 1c 1c 1c |
16 | 15 | rspcev 2955 |
. . . . . . . . . . . . 13
Nn 1c 1c Nn 1c
1c |
17 | 7, 11, 16 | syl2anc 642 |
. . . . . . . . . . . 12
Nn Nn Nn Nn
1c 1c |
18 | | eqeq1 2359 |
. . . . . . . . . . . . 13
1c
1c
1c 1c |
19 | 18 | rexbidv 2635 |
. . . . . . . . . . . 12
1c
Nn 1c Nn 1c 1c |
20 | 17, 19 | syl5ibrcom 213 |
. . . . . . . . . . 11
Nn Nn Nn
1c
Nn
1c |
21 | 20 | 3expa 1151 |
. . . . . . . . . 10
Nn Nn Nn
1c Nn 1c |
22 | 21 | adantllr 699 |
. . . . . . . . 9
Nn Nn
Nn Nn
1c Nn 1c |
23 | 22 | rexlimdva 2738 |
. . . . . . . 8
Nn Nn Nn Nn 1c Nn 1c |
24 | 5, 23 | anim12d 546 |
. . . . . . 7
Nn Nn Nn
Nn 1c Nn 1c |
25 | | addcexg 4393 |
. . . . . . . . 9
Nn Nn |
26 | 25 | adantlr 695 |
. . . . . . . 8
Nn Nn Nn
|
27 | | simplr 731 |
. . . . . . . 8
Nn Nn Nn
Nn |
28 | | opkltfing 4449 |
. . . . . . . 8
Nn fin
Nn 1c |
29 | 26, 27, 28 | syl2anc 642 |
. . . . . . 7
Nn Nn Nn fin
Nn 1c |
30 | | opkltfing 4449 |
. . . . . . . 8
Nn Nn fin
Nn
1c |
31 | 30 | adantr 451 |
. . . . . . 7
Nn Nn Nn fin
Nn 1c |
32 | 24, 29, 31 | 3imtr4d 259 |
. . . . . 6
Nn Nn Nn fin fin |
33 | | opkeq1 4059 |
. . . . . . . 8
|
34 | 33 | eleq1d 2419 |
. . . . . . 7
fin
fin |
35 | 34 | imbi1d 308 |
. . . . . 6
fin fin fin fin |
36 | 32, 35 | syl5ibrcom 213 |
. . . . 5
Nn Nn Nn
fin fin |
37 | 36 | rexlimdva 2738 |
. . . 4
Nn Nn
Nn fin fin |
38 | 37 | 3adant2 974 |
. . 3
Nn Nn Nn
Nn fin fin |
39 | 2, 38 | sylbid 206 |
. 2
Nn Nn Nn fin fin fin |
40 | 39 | imp3a 420 |
1
Nn Nn Nn fin fin fin |