Step | Hyp | Ref
| Expression |
1 | | breq1 3992 |
. . . . 5
#
# |
2 | 1 | elrab 2886 |
. . . 4
# # |
3 | | divrecap 8605 |
. . . . 5
# |
4 | 3 | 3expb 1199 |
. . . 4
# |
5 | 2, 4 | sylan2b 285 |
. . 3
# |
6 | 5 | mpoeq3ia 5918 |
. 2
#
# |
7 | | addcncntop.j |
. . . . . 6
|
8 | 7 | cntoptopon 13326 |
. . . . 5
TopOn |
9 | 8 | a1i 9 |
. . . 4
TopOn |
10 | | divcnap.k |
. . . . 5
↾t #
|
11 | | ssrab2 3232 |
. . . . . 6
#
|
12 | | resttopon 12965 |
. . . . . 6
TopOn
#
↾t #
TopOn
#
|
13 | 9, 11, 12 | sylancl 411 |
. . . . 5
↾t #
TopOn
#
|
14 | 10, 13 | eqeltrid 2257 |
. . . 4
TopOn #
|
15 | 9, 14 | cnmpt1st 13082 |
. . . 4
# |
16 | 9, 14 | cnmpt2nd 13083 |
. . . . 5
# |
17 | | eqid 2170 |
. . . . . . . 8
# # |
18 | | breq1 3992 |
. . . . . . . . . 10
#
# |
19 | 18 | elrab 2886 |
. . . . . . . . 9
# # |
20 | | recclap 8596 |
. . . . . . . . 9
# |
21 | 19, 20 | sylbi 120 |
. . . . . . . 8
#
|
22 | 17, 21 | fmpti 5648 |
. . . . . . 7
# #
|
23 | | breq1 3992 |
. . . . . . . . . . 11
#
# |
24 | 23 | elrab 2886 |
. . . . . . . . . 10
# # |
25 | | eqid 2170 |
. . . . . . . . . . . 12
inf inf |
26 | 25 | reccn2ap 11276 |
. . . . . . . . . . 11
#
#
|
27 | 26 | 3expa 1198 |
. . . . . . . . . 10
#
#
|
28 | 24, 27 | sylanb 282 |
. . . . . . . . 9
#
#
|
29 | | ovres 5992 |
. . . . . . . . . . . . . . 15
# #
# # |
30 | | elrabi 2883 |
. . . . . . . . . . . . . . . 16
#
|
31 | | elrabi 2883 |
. . . . . . . . . . . . . . . 16
#
|
32 | | eqid 2170 |
. . . . . . . . . . . . . . . . . 18
|
33 | 32 | cnmetdval 13323 |
. . . . . . . . . . . . . . . . 17
|
34 | | abssub 11065 |
. . . . . . . . . . . . . . . . 17
|
35 | 33, 34 | eqtrd 2203 |
. . . . . . . . . . . . . . . 16
|
36 | 30, 31, 35 | syl2an 287 |
. . . . . . . . . . . . . . 15
# #
|
37 | 29, 36 | eqtrd 2203 |
. . . . . . . . . . . . . 14
# #
# # |
38 | 37 | breq1d 3999 |
. . . . . . . . . . . . 13
# #
#
#
|
39 | 24 | simprbi 273 |
. . . . . . . . . . . . . . . . . 18
#
# |
40 | 30, 39 | recclapd 8698 |
. . . . . . . . . . . . . . . . 17
#
|
41 | | oveq2 5861 |
. . . . . . . . . . . . . . . . . 18
|
42 | 41, 17 | fvmptg 5572 |
. . . . . . . . . . . . . . . . 17
# # |
43 | 40, 42 | mpdan 419 |
. . . . . . . . . . . . . . . 16
#
# |
44 | | breq1 3992 |
. . . . . . . . . . . . . . . . . . . 20
#
# |
45 | 44 | elrab 2886 |
. . . . . . . . . . . . . . . . . . 19
# # |
46 | 45 | simprbi 273 |
. . . . . . . . . . . . . . . . . 18
#
# |
47 | 31, 46 | recclapd 8698 |
. . . . . . . . . . . . . . . . 17
#
|
48 | | oveq2 5861 |
. . . . . . . . . . . . . . . . . 18
|
49 | 48, 17 | fvmptg 5572 |
. . . . . . . . . . . . . . . . 17
# # |
50 | 47, 49 | mpdan 419 |
. . . . . . . . . . . . . . . 16
#
# |
51 | 43, 50 | oveqan12d 5872 |
. . . . . . . . . . . . . . 15
# #
# #
|
52 | 32 | cnmetdval 13323 |
. . . . . . . . . . . . . . . . 17
|
53 | | abssub 11065 |
. . . . . . . . . . . . . . . . 17
|
54 | 52, 53 | eqtrd 2203 |
. . . . . . . . . . . . . . . 16
|
55 | 40, 47, 54 | syl2an 287 |
. . . . . . . . . . . . . . 15
# #
|
56 | 51, 55 | eqtrd 2203 |
. . . . . . . . . . . . . 14
# #
# #
|
57 | 56 | breq1d 3999 |
. . . . . . . . . . . . 13
# #
#
# |
58 | 38, 57 | imbi12d 233 |
. . . . . . . . . . . 12
# #
# # #
#
|
59 | 58 | ralbidva 2466 |
. . . . . . . . . . 11
#
#
# # #
#
#
|
60 | 59 | rexbidv 2471 |
. . . . . . . . . 10
#
#
# # #
#
#
|
61 | 60 | adantr 274 |
. . . . . . . . 9
#
#
# # #
#
#
|
62 | 28, 61 | mpbird 166 |
. . . . . . . 8
#
#
# # #
# |
63 | 62 | rgen2 2556 |
. . . . . . 7
#
#
# # #
# |
64 | | cnxmet 13325 |
. . . . . . . . 9
|
65 | | xmetres2 13173 |
. . . . . . . . 9
#
#
#
# |
66 | 64, 11, 65 | mp2an 424 |
. . . . . . . 8
# #
#
|
67 | | eqid 2170 |
. . . . . . . . . . . 12
# #
# # |
68 | | eqid 2170 |
. . . . . . . . . . . 12
# #
# # |
69 | 67, 7, 68 | metrest 13300 |
. . . . . . . . . . 11
# ↾t #
#
#
|
70 | 64, 11, 69 | mp2an 424 |
. . . . . . . . . 10
↾t # #
#
|
71 | 10, 70 | eqtri 2191 |
. . . . . . . . 9
#
#
|
72 | 71, 7 | metcn 13308 |
. . . . . . . 8
# # #
#
# #
#
#
# # #
# |
73 | 66, 64, 72 | mp2an 424 |
. . . . . . 7
# # #
#
#
# # #
# |
74 | 22, 63, 73 | mpbir2an 937 |
. . . . . 6
# |
75 | 74 | a1i 9 |
. . . . 5
# |
76 | | oveq2 5861 |
. . . . 5
|
77 | 9, 14, 16, 14, 75, 76 | cnmpt21 13085 |
. . . 4
# |
78 | 7 | mulcncntop 13348 |
. . . . 5
|
79 | 78 | a1i 9 |
. . . 4
|
80 | 9, 14, 15, 77, 79 | cnmpt22f 13089 |
. . 3
# |
81 | 80 | mptru 1357 |
. 2
# |
82 | 6, 81 | eqeltri 2243 |
1
# |