Step | Hyp | Ref
| Expression |
1 | | breq1 3968 |
. . . . 5
#
# |
2 | 1 | elrab 2868 |
. . . 4
# # |
3 | | divrecap 8561 |
. . . . 5
# |
4 | 3 | 3expb 1186 |
. . . 4
# |
5 | 2, 4 | sylan2b 285 |
. . 3
# |
6 | 5 | mpoeq3ia 5886 |
. 2
#
# |
7 | | addcncntop.j |
. . . . . 6
|
8 | 7 | cntoptopon 12932 |
. . . . 5
TopOn |
9 | 8 | a1i 9 |
. . . 4
TopOn |
10 | | divcnap.k |
. . . . 5
↾t #
|
11 | | ssrab2 3213 |
. . . . . 6
#
|
12 | | resttopon 12571 |
. . . . . 6
TopOn
#
↾t #
TopOn
#
|
13 | 9, 11, 12 | sylancl 410 |
. . . . 5
↾t #
TopOn
#
|
14 | 10, 13 | eqeltrid 2244 |
. . . 4
TopOn #
|
15 | 9, 14 | cnmpt1st 12688 |
. . . 4
# |
16 | 9, 14 | cnmpt2nd 12689 |
. . . . 5
# |
17 | | eqid 2157 |
. . . . . . . 8
# # |
18 | | breq1 3968 |
. . . . . . . . . 10
#
# |
19 | 18 | elrab 2868 |
. . . . . . . . 9
# # |
20 | | recclap 8552 |
. . . . . . . . 9
# |
21 | 19, 20 | sylbi 120 |
. . . . . . . 8
#
|
22 | 17, 21 | fmpti 5619 |
. . . . . . 7
# #
|
23 | | breq1 3968 |
. . . . . . . . . . 11
#
# |
24 | 23 | elrab 2868 |
. . . . . . . . . 10
# # |
25 | | eqid 2157 |
. . . . . . . . . . . 12
inf inf |
26 | 25 | reccn2ap 11210 |
. . . . . . . . . . 11
#
#
|
27 | 26 | 3expa 1185 |
. . . . . . . . . 10
#
#
|
28 | 24, 27 | sylanb 282 |
. . . . . . . . 9
#
#
|
29 | | ovres 5960 |
. . . . . . . . . . . . . . 15
# #
# # |
30 | | elrabi 2865 |
. . . . . . . . . . . . . . . 16
#
|
31 | | elrabi 2865 |
. . . . . . . . . . . . . . . 16
#
|
32 | | eqid 2157 |
. . . . . . . . . . . . . . . . . 18
|
33 | 32 | cnmetdval 12929 |
. . . . . . . . . . . . . . . . 17
|
34 | | abssub 11001 |
. . . . . . . . . . . . . . . . 17
|
35 | 33, 34 | eqtrd 2190 |
. . . . . . . . . . . . . . . 16
|
36 | 30, 31, 35 | syl2an 287 |
. . . . . . . . . . . . . . 15
# #
|
37 | 29, 36 | eqtrd 2190 |
. . . . . . . . . . . . . 14
# #
# # |
38 | 37 | breq1d 3975 |
. . . . . . . . . . . . 13
# #
#
#
|
39 | 24 | simprbi 273 |
. . . . . . . . . . . . . . . . . 18
#
# |
40 | 30, 39 | recclapd 8654 |
. . . . . . . . . . . . . . . . 17
#
|
41 | | oveq2 5832 |
. . . . . . . . . . . . . . . . . 18
|
42 | 41, 17 | fvmptg 5544 |
. . . . . . . . . . . . . . . . 17
# # |
43 | 40, 42 | mpdan 418 |
. . . . . . . . . . . . . . . 16
#
# |
44 | | breq1 3968 |
. . . . . . . . . . . . . . . . . . . 20
#
# |
45 | 44 | elrab 2868 |
. . . . . . . . . . . . . . . . . . 19
# # |
46 | 45 | simprbi 273 |
. . . . . . . . . . . . . . . . . 18
#
# |
47 | 31, 46 | recclapd 8654 |
. . . . . . . . . . . . . . . . 17
#
|
48 | | oveq2 5832 |
. . . . . . . . . . . . . . . . . 18
|
49 | 48, 17 | fvmptg 5544 |
. . . . . . . . . . . . . . . . 17
# # |
50 | 47, 49 | mpdan 418 |
. . . . . . . . . . . . . . . 16
#
# |
51 | 43, 50 | oveqan12d 5843 |
. . . . . . . . . . . . . . 15
# #
# #
|
52 | 32 | cnmetdval 12929 |
. . . . . . . . . . . . . . . . 17
|
53 | | abssub 11001 |
. . . . . . . . . . . . . . . . 17
|
54 | 52, 53 | eqtrd 2190 |
. . . . . . . . . . . . . . . 16
|
55 | 40, 47, 54 | syl2an 287 |
. . . . . . . . . . . . . . 15
# #
|
56 | 51, 55 | eqtrd 2190 |
. . . . . . . . . . . . . 14
# #
# #
|
57 | 56 | breq1d 3975 |
. . . . . . . . . . . . 13
# #
#
# |
58 | 38, 57 | imbi12d 233 |
. . . . . . . . . . . 12
# #
# # #
#
|
59 | 58 | ralbidva 2453 |
. . . . . . . . . . 11
#
#
# # #
#
#
|
60 | 59 | rexbidv 2458 |
. . . . . . . . . 10
#
#
# # #
#
#
|
61 | 60 | adantr 274 |
. . . . . . . . 9
#
#
# # #
#
#
|
62 | 28, 61 | mpbird 166 |
. . . . . . . 8
#
#
# # #
# |
63 | 62 | rgen2 2543 |
. . . . . . 7
#
#
# # #
# |
64 | | cnxmet 12931 |
. . . . . . . . 9
|
65 | | xmetres2 12779 |
. . . . . . . . 9
#
#
#
# |
66 | 64, 11, 65 | mp2an 423 |
. . . . . . . 8
# #
#
|
67 | | eqid 2157 |
. . . . . . . . . . . 12
# #
# # |
68 | | eqid 2157 |
. . . . . . . . . . . 12
# #
# # |
69 | 67, 7, 68 | metrest 12906 |
. . . . . . . . . . 11
# ↾t #
#
#
|
70 | 64, 11, 69 | mp2an 423 |
. . . . . . . . . 10
↾t # #
#
|
71 | 10, 70 | eqtri 2178 |
. . . . . . . . 9
#
#
|
72 | 71, 7 | metcn 12914 |
. . . . . . . 8
# # #
#
# #
#
#
# # #
# |
73 | 66, 64, 72 | mp2an 423 |
. . . . . . 7
# # #
#
#
# # #
# |
74 | 22, 63, 73 | mpbir2an 927 |
. . . . . 6
# |
75 | 74 | a1i 9 |
. . . . 5
# |
76 | | oveq2 5832 |
. . . . 5
|
77 | 9, 14, 16, 14, 75, 76 | cnmpt21 12691 |
. . . 4
# |
78 | 7 | mulcncntop 12954 |
. . . . 5
|
79 | 78 | a1i 9 |
. . . 4
|
80 | 9, 14, 15, 77, 79 | cnmpt22f 12695 |
. . 3
# |
81 | 80 | mptru 1344 |
. 2
# |
82 | 6, 81 | eqeltri 2230 |
1
# |