Step | Hyp | Ref
| Expression |
1 | | iscmet3.2 |
. . . . 5
|
2 | 1 | cmetcau 23087 |
. . . 4
|
3 | 2 | a1d 25 |
. . 3
|
4 | 3 | ralrimiva 2966 |
. 2
|
5 | | iscmet3.4 |
. . . . 5
|
6 | 5 | adantr 481 |
. . . 4
|
7 | | simpr 477 |
. . . . . . . . 9
CauFil
CauFil |
8 | | 1rp 11836 |
. . . . . . . . . . 11
|
9 | | rphalfcl 11858 |
. . . . . . . . . . 11
|
10 | 8, 9 | ax-mp 5 |
. . . . . . . . . 10
|
11 | | rpexpcl 12879 |
. . . . . . . . . 10
|
12 | 10, 11 | mpan 706 |
. . . . . . . . 9
|
13 | | cfili 23066 |
. . . . . . . . 9
CauFil
|
14 | 7, 12, 13 | syl2an 494 |
. . . . . . . 8
CauFil
|
15 | 14 | ralrimiva 2966 |
. . . . . . 7
CauFil
|
16 | | vex 3203 |
. . . . . . . 8
|
17 | | znnen 14941 |
. . . . . . . . 9
|
18 | | nnenom 12779 |
. . . . . . . . 9
|
19 | 17, 18 | entri 8010 |
. . . . . . . 8
|
20 | | raleq 3138 |
. . . . . . . . 9
|
21 | 20 | raleqbi1dv 3146 |
. . . . . . . 8
|
22 | 16, 19, 21 | axcc4 9261 |
. . . . . . 7
|
23 | 15, 22 | syl 17 |
. . . . . 6
CauFil
|
24 | | iscmet3.3 |
. . . . . . . . . . . 12
|
25 | 24 | ad2antrr 762 |
. . . . . . . . . . 11
CauFil
|
26 | | iscmet3.1 |
. . . . . . . . . . . 12
|
27 | 26 | uzenom 12763 |
. . . . . . . . . . 11
|
28 | | endom 7982 |
. . . . . . . . . . 11
|
29 | 25, 27, 28 | 3syl 18 |
. . . . . . . . . 10
CauFil
|
30 | | dfin5 3582 |
. . . . . . . . . . . . . . 15
|
31 | | fzn0 12355 |
. . . . . . . . . . . . . . . . . . . . 21
|
32 | 31 | biimpri 218 |
. . . . . . . . . . . . . . . . . . . 20
|
33 | 32, 26 | eleq2s 2719 |
. . . . . . . . . . . . . . . . . . 19
|
34 | | simprr 796 |
. . . . . . . . . . . . . . . . . . . . . 22
CauFil |
35 | | elfzelz 12342 |
. . . . . . . . . . . . . . . . . . . . . 22
|
36 | | ffvelrn 6357 |
. . . . . . . . . . . . . . . . . . . . . 22
|
37 | 34, 35, 36 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . 21
CauFil
|
38 | | metxmet 22139 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
|
39 | 5, 38 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
|
40 | 39 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
|
41 | | simpl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
CauFil CauFil |
42 | | cfilfil 23065 |
. . . . . . . . . . . . . . . . . . . . . . 23
CauFil |
43 | 40, 41, 42 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . 22
CauFil |
44 | | filelss 21656 |
. . . . . . . . . . . . . . . . . . . . . 22
|
45 | 43, 44 | sylan 488 |
. . . . . . . . . . . . . . . . . . . . 21
CauFil
|
46 | 37, 45 | syldan 487 |
. . . . . . . . . . . . . . . . . . . 20
CauFil
|
47 | 46 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . 19
CauFil
|
48 | | r19.2z 4060 |
. . . . . . . . . . . . . . . . . . 19
|
49 | 33, 47, 48 | syl2anr 495 |
. . . . . . . . . . . . . . . . . 18
CauFil
|
50 | | iinss 4571 |
. . . . . . . . . . . . . . . . . 18
|
51 | 49, 50 | syl 17 |
. . . . . . . . . . . . . . . . 17
CauFil
|
52 | 6 | ad2antrr 762 |
. . . . . . . . . . . . . . . . . 18
CauFil
|
53 | | elfvdm 6220 |
. . . . . . . . . . . . . . . . . 18
|
54 | | fvi 6255 |
. . . . . . . . . . . . . . . . . 18
|
55 | 52, 53, 54 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
CauFil
|
56 | 51, 55 | sseqtr4d 3642 |
. . . . . . . . . . . . . . . 16
CauFil
|
57 | | sseqin2 3817 |
. . . . . . . . . . . . . . . 16
|
58 | 56, 57 | sylib 208 |
. . . . . . . . . . . . . . 15
CauFil
|
59 | 30, 58 | syl5eqr 2670 |
. . . . . . . . . . . . . 14
CauFil
|
60 | 43 | adantr 481 |
. . . . . . . . . . . . . . 15
CauFil
|
61 | 37 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . 18
CauFil |
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . 17
CauFil
|
63 | 33 | adantl 482 |
. . . . . . . . . . . . . . . . 17
CauFil
|
64 | | fzfid 12772 |
. . . . . . . . . . . . . . . . 17
CauFil
|
65 | | iinfi 8323 |
. . . . . . . . . . . . . . . . 17
|
66 | 60, 62, 63, 64, 65 | syl13anc 1328 |
. . . . . . . . . . . . . . . 16
CauFil
|
67 | | filfi 21663 |
. . . . . . . . . . . . . . . . 17
|
68 | 60, 67 | syl 17 |
. . . . . . . . . . . . . . . 16
CauFil
|
69 | 66, 68 | eleqtrd 2703 |
. . . . . . . . . . . . . . 15
CauFil
|
70 | | fileln0 21654 |
. . . . . . . . . . . . . . 15
|
71 | 60, 69, 70 | syl2anc 693 |
. . . . . . . . . . . . . 14
CauFil
|
72 | 59, 71 | eqnetrd 2861 |
. . . . . . . . . . . . 13
CauFil
|
73 | | rabn0 3958 |
. . . . . . . . . . . . 13
|
74 | 72, 73 | sylib 208 |
. . . . . . . . . . . 12
CauFil
|
75 | 74 | ralrimiva 2966 |
. . . . . . . . . . 11
CauFil
|
76 | 75 | adantrrr 761 |
. . . . . . . . . 10
CauFil
|
77 | | fvex 6201 |
. . . . . . . . . . 11
|
78 | | eleq1 2689 |
. . . . . . . . . . . 12
|
79 | | fvex 6201 |
. . . . . . . . . . . . 13
|
80 | | eliin 4525 |
. . . . . . . . . . . . 13
|
81 | 79, 80 | ax-mp 5 |
. . . . . . . . . . . 12
|
82 | 78, 81 | syl6bb 276 |
. . . . . . . . . . 11
|
83 | 77, 82 | axcc4dom 9263 |
. . . . . . . . . 10
|
84 | 29, 76, 83 | syl2anc 693 |
. . . . . . . . 9
CauFil
|
85 | | df-ral 2917 |
. . . . . . . . . . . . 13
|
86 | | 19.29 1801 |
. . . . . . . . . . . . 13
|
87 | 85, 86 | sylanb 489 |
. . . . . . . . . . . 12
|
88 | 24 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
CauFil
|
89 | 5 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
CauFil
|
90 | | simprrl 804 |
. . . . . . . . . . . . . . . 16
CauFil
|
91 | | feq3 6028 |
. . . . . . . . . . . . . . . . 17
|
92 | 89, 53, 54, 91 | 4syl 19 |
. . . . . . . . . . . . . . . 16
CauFil
|
93 | 90, 92 | mpbid 222 |
. . . . . . . . . . . . . . 15
CauFil
|
94 | | simplrr 801 |
. . . . . . . . . . . . . . . . 17
CauFil
|
95 | 94 | simprd 479 |
. . . . . . . . . . . . . . . 16
CauFil
|
96 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
|
97 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
|
98 | 97 | breq2d 4665 |
. . . . . . . . . . . . . . . . . . 19
|
99 | 96, 98 | raleqbidv 3152 |
. . . . . . . . . . . . . . . . . 18
|
100 | 96, 99 | raleqbidv 3152 |
. . . . . . . . . . . . . . . . 17
|
101 | 100 | cbvralv 3171 |
. . . . . . . . . . . . . . . 16
|
102 | 95, 101 | sylib 208 |
. . . . . . . . . . . . . . 15
CauFil
|
103 | | simprrr 805 |
. . . . . . . . . . . . . . . 16
CauFil
|
104 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
105 | 104 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . 19
|
106 | 105 | cbvralv 3171 |
. . . . . . . . . . . . . . . . . 18
|
107 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
|
108 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
|
109 | 108 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . 19
|
110 | 107, 109 | raleqbidv 3152 |
. . . . . . . . . . . . . . . . . 18
|
111 | 106, 110 | syl5bb 272 |
. . . . . . . . . . . . . . . . 17
|
112 | 111 | cbvralv 3171 |
. . . . . . . . . . . . . . . 16
|
113 | 103, 112 | sylib 208 |
. . . . . . . . . . . . . . 15
CauFil
|
114 | 89, 38 | syl 17 |
. . . . . . . . . . . . . . . 16
CauFil
|
115 | | simplrl 800 |
. . . . . . . . . . . . . . . 16
CauFil
CauFil |
116 | 114, 115,
42 | syl2anc 693 |
. . . . . . . . . . . . . . 15
CauFil
|
117 | 94 | simpld 475 |
. . . . . . . . . . . . . . 15
CauFil
|
118 | 26, 1, 88, 89, 93, 102, 113 | iscmet3lem1 23089 |
. . . . . . . . . . . . . . . 16
CauFil
|
119 | | simprl 794 |
. . . . . . . . . . . . . . . 16
CauFil
|
120 | 118, 93, 119 | mp2d 49 |
. . . . . . . . . . . . . . 15
CauFil
|
121 | 26, 1, 88, 89, 93, 102, 113, 116, 117, 120 | iscmet3lem2 23090 |
. . . . . . . . . . . . . 14
CauFil
|
122 | 121 | ex 450 |
. . . . . . . . . . . . 13
CauFil
|
123 | 122 | exlimdv 1861 |
. . . . . . . . . . . 12
CauFil
|
124 | 87, 123 | syl5 34 |
. . . . . . . . . . 11
CauFil
|
125 | 124 | expdimp 453 |
. . . . . . . . . 10
CauFil
|
126 | 125 | an32s 846 |
. . . . . . . . 9
CauFil
|
127 | 84, 126 | mpd 15 |
. . . . . . . 8
CauFil
|
128 | 127 | expr 643 |
. . . . . . 7
CauFil
|
129 | 128 | exlimdv 1861 |
. . . . . 6
CauFil
|
130 | 23, 129 | mpd 15 |
. . . . 5
CauFil
|
131 | 130 | ralrimiva 2966 |
. . . 4
CauFil |
132 | 1 | iscmet 23082 |
. . . 4
CauFil |
133 | 6, 131, 132 | sylanbrc 698 |
. . 3
|
134 | 133 | ex 450 |
. 2
|
135 | 4, 134 | impbid2 216 |
1
|