Proof of Theorem metnrmlem3
Step | Hyp | Ref
| Expression |
1 | | metnrmlem.g |
. . . 4
inf |
2 | | metdscn.j |
. . . 4
|
3 | | metnrmlem.1 |
. . . 4
|
4 | | metnrmlem.3 |
. . . 4
|
5 | | metnrmlem.2 |
. . . 4
|
6 | | incom 3805 |
. . . . 5
|
7 | | metnrmlem.4 |
. . . . 5
|
8 | 6, 7 | syl5eq 2668 |
. . . 4
|
9 | | metnrmlem.v |
. . . 4
|
10 | 1, 2, 3, 4, 5, 8, 9 | metnrmlem2 22663 |
. . 3
|
11 | 10 | simpld 475 |
. 2
|
12 | | metdscn.f |
. . . 4
inf |
13 | | metnrmlem.u |
. . . 4
|
14 | 12, 2, 3, 5, 4, 7, 13 | metnrmlem2 22663 |
. . 3
|
15 | 14 | simpld 475 |
. 2
|
16 | 10 | simprd 479 |
. 2
|
17 | 14 | simprd 479 |
. 2
|
18 | 9 | ineq1i 3810 |
. . . 4
|
19 | | iunin1 4585 |
. . . 4
|
20 | 18, 19 | eqtr4i 2647 |
. . 3
|
21 | 13 | ineq2i 3811 |
. . . . . . . 8
|
22 | | iunin2 4584 |
. . . . . . . 8
|
23 | 21, 22 | eqtr4i 2647 |
. . . . . . 7
|
24 | 3 | adantr 481 |
. . . . . . . . . . . 12
|
25 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
|
26 | 25 | cldss 20833 |
. . . . . . . . . . . . . . . 16
|
27 | 5, 26 | syl 17 |
. . . . . . . . . . . . . . 15
|
28 | 2 | mopnuni 22246 |
. . . . . . . . . . . . . . . 16
|
29 | 3, 28 | syl 17 |
. . . . . . . . . . . . . . 15
|
30 | 27, 29 | sseqtr4d 3642 |
. . . . . . . . . . . . . 14
|
31 | 30 | sselda 3603 |
. . . . . . . . . . . . 13
|
32 | 31 | adantrr 753 |
. . . . . . . . . . . 12
|
33 | 25 | cldss 20833 |
. . . . . . . . . . . . . . . 16
|
34 | 4, 33 | syl 17 |
. . . . . . . . . . . . . . 15
|
35 | 34, 29 | sseqtr4d 3642 |
. . . . . . . . . . . . . 14
|
36 | 35 | sselda 3603 |
. . . . . . . . . . . . 13
|
37 | 36 | adantrl 752 |
. . . . . . . . . . . 12
|
38 | 1, 2, 3, 4, 5, 8 | metnrmlem1a 22661 |
. . . . . . . . . . . . . . . 16
|
39 | 38 | simprd 479 |
. . . . . . . . . . . . . . 15
|
40 | 39 | adantrr 753 |
. . . . . . . . . . . . . 14
|
41 | 40 | rphalfcld 11884 |
. . . . . . . . . . . . 13
|
42 | 41 | rpxrd 11873 |
. . . . . . . . . . . 12
|
43 | 12, 2, 3, 5, 4, 7 | metnrmlem1a 22661 |
. . . . . . . . . . . . . . . 16
|
44 | 43 | adantrl 752 |
. . . . . . . . . . . . . . 15
|
45 | 44 | simprd 479 |
. . . . . . . . . . . . . 14
|
46 | 45 | rphalfcld 11884 |
. . . . . . . . . . . . 13
|
47 | 46 | rpxrd 11873 |
. . . . . . . . . . . 12
|
48 | 40 | rpred 11872 |
. . . . . . . . . . . . . . . 16
|
49 | 48 | rehalfcld 11279 |
. . . . . . . . . . . . . . 15
|
50 | 45 | rpred 11872 |
. . . . . . . . . . . . . . . 16
|
51 | 50 | rehalfcld 11279 |
. . . . . . . . . . . . . . 15
|
52 | | rexadd 12063 |
. . . . . . . . . . . . . . 15
|
53 | 49, 51, 52 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
54 | 48 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
55 | 50 | recnd 10068 |
. . . . . . . . . . . . . . 15
|
56 | | 2cnd 11093 |
. . . . . . . . . . . . . . 15
|
57 | | 2ne0 11113 |
. . . . . . . . . . . . . . . 16
|
58 | 57 | a1i 11 |
. . . . . . . . . . . . . . 15
|
59 | 54, 55, 56, 58 | divdird 10839 |
. . . . . . . . . . . . . 14
|
60 | 53, 59 | eqtr4d 2659 |
. . . . . . . . . . . . 13
|
61 | 1, 2, 3, 4, 5, 8 | metnrmlem1 22662 |
. . . . . . . . . . . . . . . . . 18
|
62 | 61 | ancom2s 844 |
. . . . . . . . . . . . . . . . 17
|
63 | | xmetsym 22152 |
. . . . . . . . . . . . . . . . . 18
|
64 | 24, 37, 32, 63 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
65 | 62, 64 | breqtrd 4679 |
. . . . . . . . . . . . . . . 16
|
66 | 12, 2, 3, 5, 4, 7 | metnrmlem1 22662 |
. . . . . . . . . . . . . . . 16
|
67 | 40 | rpxrd 11873 |
. . . . . . . . . . . . . . . . 17
|
68 | 45 | rpxrd 11873 |
. . . . . . . . . . . . . . . . 17
|
69 | | xmetcl 22136 |
. . . . . . . . . . . . . . . . . 18
|
70 | 24, 32, 37, 69 | syl3anc 1326 |
. . . . . . . . . . . . . . . . 17
|
71 | | xle2add 12089 |
. . . . . . . . . . . . . . . . 17
|
72 | 67, 68, 70, 70, 71 | syl22anc 1327 |
. . . . . . . . . . . . . . . 16
|
73 | 65, 66, 72 | mp2and 715 |
. . . . . . . . . . . . . . 15
|
74 | 48, 50 | readdcld 10069 |
. . . . . . . . . . . . . . . . . 18
|
75 | 74 | recnd 10068 |
. . . . . . . . . . . . . . . . 17
|
76 | 75, 56, 58 | divcan2d 10803 |
. . . . . . . . . . . . . . . 16
|
77 | | 2re 11090 |
. . . . . . . . . . . . . . . . 17
|
78 | 74 | rehalfcld 11279 |
. . . . . . . . . . . . . . . . 17
|
79 | | rexmul 12101 |
. . . . . . . . . . . . . . . . 17
|
80 | 77, 78, 79 | sylancr 695 |
. . . . . . . . . . . . . . . 16
|
81 | | rexadd 12063 |
. . . . . . . . . . . . . . . . 17
|
82 | 48, 50, 81 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
83 | 76, 80, 82 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . 15
|
84 | | x2times 12129 |
. . . . . . . . . . . . . . . 16
|
85 | 70, 84 | syl 17 |
. . . . . . . . . . . . . . 15
|
86 | 73, 83, 85 | 3brtr4d 4685 |
. . . . . . . . . . . . . 14
|
87 | 78 | rexrd 10089 |
. . . . . . . . . . . . . . 15
|
88 | | 2rp 11837 |
. . . . . . . . . . . . . . . 16
|
89 | 88 | a1i 11 |
. . . . . . . . . . . . . . 15
|
90 | | xlemul2 12121 |
. . . . . . . . . . . . . . 15
|
91 | 87, 70, 89, 90 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
92 | 86, 91 | mpbird 247 |
. . . . . . . . . . . . 13
|
93 | 60, 92 | eqbrtrd 4675 |
. . . . . . . . . . . 12
|
94 | | bldisj 22203 |
. . . . . . . . . . . 12
|
95 | 24, 32, 37, 42, 47, 93, 94 | syl33anc 1341 |
. . . . . . . . . . 11
|
96 | | eqimss 3657 |
. . . . . . . . . . 11
|
97 | 95, 96 | syl 17 |
. . . . . . . . . 10
|
98 | 97 | anassrs 680 |
. . . . . . . . 9
|
99 | 98 | ralrimiva 2966 |
. . . . . . . 8
|
100 | | iunss 4561 |
. . . . . . . 8
|
101 | 99, 100 | sylibr 224 |
. . . . . . 7
|
102 | 23, 101 | syl5eqss 3649 |
. . . . . 6
|
103 | 102 | ralrimiva 2966 |
. . . . 5
|
104 | | iunss 4561 |
. . . . 5
|
105 | 103, 104 | sylibr 224 |
. . . 4
|
106 | | ss0 3974 |
. . . 4
|
107 | 105, 106 | syl 17 |
. . 3
|
108 | 20, 107 | syl5eq 2668 |
. 2
|
109 | | sseq2 3627 |
. . . 4
|
110 | | ineq1 3807 |
. . . . 5
|
111 | 110 | eqeq1d 2624 |
. . . 4
|
112 | 109, 111 | 3anbi13d 1401 |
. . 3
|
113 | | sseq2 3627 |
. . . 4
|
114 | | ineq2 3808 |
. . . . 5
|
115 | 114 | eqeq1d 2624 |
. . . 4
|
116 | 113, 115 | 3anbi23d 1402 |
. . 3
|
117 | 112, 116 | rspc2ev 3324 |
. 2
|
118 | 11, 15, 16, 17, 108, 117 | syl113anc 1338 |
1
|