Step | Hyp | Ref
| Expression |
1 | | rrxmval.1 |
. . . . . . . . 9
finSupp
|
2 | | simprl 794 |
. . . . . . . . 9
|
3 | 1, 2 | rrxfsupp 23185 |
. . . . . . . 8
supp |
4 | | simprr 796 |
. . . . . . . . 9
|
5 | 1, 4 | rrxfsupp 23185 |
. . . . . . . 8
supp |
6 | | unfi 8227 |
. . . . . . . 8
supp supp supp supp |
7 | 3, 5, 6 | syl2anc 693 |
. . . . . . 7
supp supp |
8 | 1, 2 | rrxsuppss 23186 |
. . . . . . . . . 10
supp |
9 | 1, 4 | rrxsuppss 23186 |
. . . . . . . . . 10
supp |
10 | 8, 9 | unssd 3789 |
. . . . . . . . 9
supp supp |
11 | 10 | sselda 3603 |
. . . . . . . 8
supp supp |
12 | 1, 2 | rrxf 23184 |
. . . . . . . . . . 11
|
13 | 12 | ffvelrnda 6359 |
. . . . . . . . . 10
|
14 | 1, 4 | rrxf 23184 |
. . . . . . . . . . 11
|
15 | 14 | ffvelrnda 6359 |
. . . . . . . . . 10
|
16 | 13, 15 | resubcld 10458 |
. . . . . . . . 9
|
17 | 16 | resqcld 13035 |
. . . . . . . 8
|
18 | 11, 17 | syldan 487 |
. . . . . . 7
supp supp |
19 | 7, 18 | fsumrecl 14465 |
. . . . . 6
supp supp |
20 | 16 | sqge0d 13036 |
. . . . . . . 8
|
21 | 11, 20 | syldan 487 |
. . . . . . 7
supp supp |
22 | 7, 18, 21 | fsumge0 14527 |
. . . . . 6
supp supp |
23 | 19, 22 | resqrtcld 14156 |
. . . . 5
supp supp |
24 | 23 | ralrimivva 2971 |
. . . 4
supp supp |
25 | | eqid 2622 |
. . . . 5
supp supp supp supp |
26 | 25 | fmpt2 7237 |
. . . 4
supp supp
supp supp |
27 | 24, 26 | sylib 208 |
. . 3
supp supp |
28 | | rrxmval.d |
. . . . 5
ℝ^ |
29 | 1, 28 | rrxmfval 23189 |
. . . 4
supp supp |
30 | 29 | feq1d 6030 |
. . 3
supp supp |
31 | 27, 30 | mpbird 247 |
. 2
|
32 | | sqrt00 14004 |
. . . . . . 7
supp supp supp supp
supp supp supp supp |
33 | 19, 22, 32 | syl2anc 693 |
. . . . . 6
supp supp supp supp |
34 | 7, 18, 21 | fsum00 14530 |
. . . . . 6
supp supp
supp supp |
35 | 16 | recnd 10068 |
. . . . . . . . . 10
|
36 | | sqeq0 12927 |
. . . . . . . . . 10
|
37 | 35, 36 | syl 17 |
. . . . . . . . 9
|
38 | 13 | recnd 10068 |
. . . . . . . . . 10
|
39 | 15 | recnd 10068 |
. . . . . . . . . 10
|
40 | 38, 39 | subeq0ad 10402 |
. . . . . . . . 9
|
41 | 37, 40 | bitrd 268 |
. . . . . . . 8
|
42 | 11, 41 | syldan 487 |
. . . . . . 7
supp supp |
43 | 42 | ralbidva 2985 |
. . . . . 6
supp supp supp supp |
44 | 33, 34, 43 | 3bitrd 294 |
. . . . 5
supp supp supp supp |
45 | 1, 28 | rrxmval 23188 |
. . . . . . 7
supp supp |
46 | 45 | 3expb 1266 |
. . . . . 6
supp supp |
47 | 46 | eqeq1d 2624 |
. . . . 5
supp supp |
48 | 12 | ffnd 6046 |
. . . . . . 7
|
49 | 14 | ffnd 6046 |
. . . . . . 7
|
50 | | eqfnfv 6311 |
. . . . . . 7
|
51 | 48, 49, 50 | syl2anc 693 |
. . . . . 6
|
52 | | ssun1 3776 |
. . . . . . . . . . 11
supp supp supp |
53 | 52 | a1i 11 |
. . . . . . . . . 10
supp supp supp |
54 | | simpl 473 |
. . . . . . . . . 10
|
55 | | 0red 10041 |
. . . . . . . . . 10
|
56 | 12, 53, 54, 55 | suppssr 7326 |
. . . . . . . . 9
supp supp |
57 | | ssun2 3777 |
. . . . . . . . . . 11
supp supp supp |
58 | 57 | a1i 11 |
. . . . . . . . . 10
supp supp supp |
59 | 14, 58, 54, 55 | suppssr 7326 |
. . . . . . . . 9
supp supp |
60 | 56, 59 | eqtr4d 2659 |
. . . . . . . 8
supp supp |
61 | 60 | ralrimiva 2966 |
. . . . . . 7
supp supp |
62 | 10, 61 | raldifeq 4059 |
. . . . . 6
supp supp |
63 | 51, 62 | bitr4d 271 |
. . . . 5
supp supp |
64 | 44, 47, 63 | 3bitr4d 300 |
. . . 4
|
65 | 7 | 3adant2 1080 |
. . . . . . . . . . 11
supp supp |
66 | | simp2 1062 |
. . . . . . . . . . . 12
|
67 | 1, 66 | rrxfsupp 23185 |
. . . . . . . . . . 11
supp |
68 | | unfi 8227 |
. . . . . . . . . . 11
supp supp
supp supp supp supp |
69 | 65, 67, 68 | syl2anc 693 |
. . . . . . . . . 10
supp supp supp |
70 | 69 | 3expa 1265 |
. . . . . . . . 9
supp supp supp |
71 | 70 | an32s 846 |
. . . . . . . 8
supp supp supp |
72 | 10 | adantr 481 |
. . . . . . . . . . 11
supp supp |
73 | | simpr 477 |
. . . . . . . . . . . 12
|
74 | 1, 73 | rrxsuppss 23186 |
. . . . . . . . . . 11
supp |
75 | 72, 74 | unssd 3789 |
. . . . . . . . . 10
supp supp supp
|
76 | 75 | sselda 3603 |
. . . . . . . . 9
supp supp supp |
77 | 13 | adantlr 751 |
. . . . . . . . . 10
|
78 | 1, 73 | rrxf 23184 |
. . . . . . . . . . 11
|
79 | 78 | ffvelrnda 6359 |
. . . . . . . . . 10
|
80 | 77, 79 | resubcld 10458 |
. . . . . . . . 9
|
81 | 76, 80 | syldan 487 |
. . . . . . . 8
supp supp supp |
82 | 15 | adantlr 751 |
. . . . . . . . . 10
|
83 | 79, 82 | resubcld 10458 |
. . . . . . . . 9
|
84 | 76, 83 | syldan 487 |
. . . . . . . 8
supp supp supp |
85 | 71, 81, 84 | trirn 23183 |
. . . . . . 7
supp supp supp
supp supp supp supp supp supp |
86 | 38 | adantlr 751 |
. . . . . . . . . . . 12
|
87 | 79 | recnd 10068 |
. . . . . . . . . . . 12
|
88 | 39 | adantlr 751 |
. . . . . . . . . . . 12
|
89 | 86, 87, 88 | npncand 10416 |
. . . . . . . . . . 11
|
90 | 89 | oveq1d 6665 |
. . . . . . . . . 10
|
91 | 76, 90 | syldan 487 |
. . . . . . . . 9
supp supp supp |
92 | 91 | sumeq2dv 14433 |
. . . . . . . 8
supp supp supp supp supp supp |
93 | 92 | fveq2d 6195 |
. . . . . . 7
supp supp supp
supp supp supp |
94 | | sqsubswap 12924 |
. . . . . . . . . . . 12
|
95 | 86, 87, 94 | syl2anc 693 |
. . . . . . . . . . 11
|
96 | 76, 95 | syldan 487 |
. . . . . . . . . 10
supp supp supp |
97 | 96 | sumeq2dv 14433 |
. . . . . . . . 9
supp supp supp supp supp supp |
98 | 97 | fveq2d 6195 |
. . . . . . . 8
supp supp supp
supp supp supp |
99 | 98 | oveq1d 6665 |
. . . . . . 7
supp supp supp supp supp supp supp supp supp
supp supp supp |
100 | 85, 93, 99 | 3brtr3d 4684 |
. . . . . 6
supp supp supp
supp supp supp supp supp supp |
101 | 46 | adantr 481 |
. . . . . . 7
supp supp |
102 | | simp1 1061 |
. . . . . . . . . . 11
|
103 | 2 | 3adant2 1080 |
. . . . . . . . . . 11
|
104 | 4 | 3adant2 1080 |
. . . . . . . . . . 11
|
105 | 1, 103 | rrxsuppss 23186 |
. . . . . . . . . . . . 13
supp |
106 | 1, 104 | rrxsuppss 23186 |
. . . . . . . . . . . . 13
supp |
107 | 105, 106 | unssd 3789 |
. . . . . . . . . . . 12
supp supp |
108 | 1, 66 | rrxsuppss 23186 |
. . . . . . . . . . . 12
supp |
109 | 107, 108 | unssd 3789 |
. . . . . . . . . . 11
supp supp supp
|
110 | | ssun1 3776 |
. . . . . . . . . . . 12
supp supp
supp supp supp |
111 | 110 | a1i 11 |
. . . . . . . . . . 11
supp supp supp supp supp |
112 | 1, 28, 102, 103, 104, 109, 69, 111 | rrxmetlem 23190 |
. . . . . . . . . 10
supp supp supp supp supp |
113 | 112 | fveq2d 6195 |
. . . . . . . . 9
supp supp
supp supp supp |
114 | 113 | 3expa 1265 |
. . . . . . . 8
supp supp
supp supp supp |
115 | 114 | an32s 846 |
. . . . . . 7
supp supp
supp supp supp |
116 | 101, 115 | eqtrd 2656 |
. . . . . 6
supp supp supp |
117 | 1, 28 | rrxmval 23188 |
. . . . . . . . . . 11
supp supp |
118 | 117 | 3adant3r 1323 |
. . . . . . . . . 10
supp supp |
119 | 1, 28 | rrxmval 23188 |
. . . . . . . . . . 11
supp supp |
120 | 119 | 3adant3l 1322 |
. . . . . . . . . 10
supp supp |
121 | 118, 120 | oveq12d 6668 |
. . . . . . . . 9
supp supp
supp supp |
122 | | ssun2 3777 |
. . . . . . . . . . . . . 14
supp supp supp supp |
123 | 122 | a1i 11 |
. . . . . . . . . . . . 13
supp supp supp supp |
124 | 52, 110 | sstri 3612 |
. . . . . . . . . . . . . 14
supp supp supp supp |
125 | 124 | a1i 11 |
. . . . . . . . . . . . 13
supp supp supp supp |
126 | 123, 125 | unssd 3789 |
. . . . . . . . . . . 12
supp supp supp supp supp |
127 | 1, 28, 102, 66, 103, 109, 69, 126 | rrxmetlem 23190 |
. . . . . . . . . . 11
supp supp supp supp supp |
128 | 127 | fveq2d 6195 |
. . . . . . . . . 10
supp supp
supp supp supp |
129 | 57, 110 | sstri 3612 |
. . . . . . . . . . . . . 14
supp supp supp supp |
130 | 129 | a1i 11 |
. . . . . . . . . . . . 13
supp supp supp supp |
131 | 123, 130 | unssd 3789 |
. . . . . . . . . . . 12
supp supp supp supp supp |
132 | 1, 28, 102, 66, 104, 109, 69, 131 | rrxmetlem 23190 |
. . . . . . . . . . 11
supp supp supp supp supp |
133 | 132 | fveq2d 6195 |
. . . . . . . . . 10
supp supp
supp supp supp |
134 | 128, 133 | oveq12d 6668 |
. . . . . . . . 9
supp supp
supp supp supp supp supp
supp supp supp |
135 | 121, 134 | eqtrd 2656 |
. . . . . . . 8
supp supp supp
supp supp supp |
136 | 135 | 3expa 1265 |
. . . . . . 7
supp supp supp
supp supp supp |
137 | 136 | an32s 846 |
. . . . . 6
supp supp supp
supp supp supp |
138 | 100, 116,
137 | 3brtr4d 4685 |
. . . . 5
|
139 | 138 | ralrimiva 2966 |
. . . 4
|
140 | 64, 139 | jca 554 |
. . 3
|
141 | 140 | ralrimivva 2971 |
. 2
|
142 | | ovex 6678 |
. . . 4
|
143 | 1, 142 | rabex2 4815 |
. . 3
|
144 | | ismet 22128 |
. . 3
|
145 | 143, 144 | ax-mp 5 |
. 2
|
146 | 31, 141, 145 | sylanbrc 698 |
1
|