Step | Hyp | Ref
| Expression |
1 | | fzofi 12773 |
. . . 4
..^ |
2 | 1 | a1i 11 |
. . 3
..^ |
3 | | hgt750leme.n |
. . . . . . 7
|
4 | 3 | nnnn0d 11351 |
. . . . . 6
|
5 | | 3nn0 11310 |
. . . . . . 7
|
6 | 5 | a1i 11 |
. . . . . 6
|
7 | | ssid 3624 |
. . . . . . 7
|
8 | 7 | a1i 11 |
. . . . . 6
|
9 | 4, 6, 8 | reprfi2 30701 |
. . . . 5
repr |
10 | | ssrab2 3687 |
. . . . . 6
repr
repr |
11 | 10 | a1i 11 |
. . . . 5
repr repr |
12 | 9, 11 | ssfid 8183 |
. . . 4
repr
|
13 | 12 | adantr 481 |
. . 3
..^ repr |
14 | | vmaf 24845 |
. . . . . 6
Λ |
15 | 14 | a1i 11 |
. . . . 5
..^ repr Λ |
16 | 7 | a1i 11 |
. . . . . . 7
..^ repr |
17 | 4 | nn0zd 11480 |
. . . . . . . 8
|
18 | 17 | ad2antrr 762 |
. . . . . . 7
..^ repr |
19 | 5 | a1i 11 |
. . . . . . 7
..^ repr |
20 | | simpr 477 |
. . . . . . . 8
..^ repr repr |
21 | 10, 20 | sseldi 3601 |
. . . . . . 7
..^ repr repr |
22 | 16, 18, 19, 21 | reprf 30690 |
. . . . . 6
..^ repr ..^ |
23 | | c0ex 10034 |
. . . . . . . . 9
|
24 | 23 | tpid1 4303 |
. . . . . . . 8
|
25 | | fzo0to3tp 12554 |
. . . . . . . 8
..^ |
26 | 24, 25 | eleqtrri 2700 |
. . . . . . 7
..^ |
27 | 26 | a1i 11 |
. . . . . 6
..^ repr ..^ |
28 | 22, 27 | ffvelrnd 6360 |
. . . . 5
..^ repr |
29 | 15, 28 | ffvelrnd 6360 |
. . . 4
..^ repr Λ |
30 | | 1ex 10035 |
. . . . . . . . . 10
|
31 | 30 | tpid2 4304 |
. . . . . . . . 9
|
32 | 31, 25 | eleqtrri 2700 |
. . . . . . . 8
..^ |
33 | 32 | a1i 11 |
. . . . . . 7
..^ repr ..^ |
34 | 22, 33 | ffvelrnd 6360 |
. . . . . 6
..^ repr |
35 | 15, 34 | ffvelrnd 6360 |
. . . . 5
..^ repr Λ |
36 | | 2ex 11092 |
. . . . . . . . . 10
|
37 | 36 | tpid3 4307 |
. . . . . . . . 9
|
38 | 37, 25 | eleqtrri 2700 |
. . . . . . . 8
..^ |
39 | 38 | a1i 11 |
. . . . . . 7
..^ repr ..^ |
40 | 22, 39 | ffvelrnd 6360 |
. . . . . 6
..^ repr |
41 | 15, 40 | ffvelrnd 6360 |
. . . . 5
..^ repr Λ |
42 | 35, 41 | remulcld 10070 |
. . . 4
..^ repr Λ Λ |
43 | 29, 42 | remulcld 10070 |
. . 3
..^ repr Λ Λ Λ |
44 | | vmage0 24847 |
. . . . 5
Λ |
45 | 28, 44 | syl 17 |
. . . 4
..^ repr Λ |
46 | | vmage0 24847 |
. . . . . 6
Λ |
47 | 34, 46 | syl 17 |
. . . . 5
..^ repr Λ |
48 | | vmage0 24847 |
. . . . . 6
Λ |
49 | 40, 48 | syl 17 |
. . . . 5
..^ repr Λ |
50 | 35, 41, 47, 49 | mulge0d 10604 |
. . . 4
..^ repr Λ Λ |
51 | 29, 42, 45, 50 | mulge0d 10604 |
. . 3
..^ repr Λ Λ Λ |
52 | 2, 13, 43, 51 | fsumiunle 29575 |
. 2
..^ repr Λ Λ Λ ..^ repr Λ Λ Λ |
53 | | eqid 2622 |
. . . 4
repr repr |
54 | | inss2 3834 |
. . . . . 6
|
55 | | prmssnn 15390 |
. . . . . 6
|
56 | 54, 55 | sstri 3612 |
. . . . 5
|
57 | 56 | a1i 11 |
. . . 4
|
58 | 53, 8, 57, 4, 6 | reprdifc 30705 |
. . 3
repr repr ..^ repr |
59 | 58 | sumeq1d 14431 |
. 2
repr reprΛ Λ Λ
..^ repr Λ Λ Λ |
60 | | ssrab2 3687 |
. . . . . . . 8
repr
repr |
61 | 60 | a1i 11 |
. . . . . . 7
repr repr |
62 | 9, 61 | ssfid 8183 |
. . . . . 6
repr
|
63 | 14 | a1i 11 |
. . . . . . . 8
repr Λ |
64 | 7 | a1i 11 |
. . . . . . . . . 10
repr |
65 | 17 | adantr 481 |
. . . . . . . . . 10
repr |
66 | 5 | a1i 11 |
. . . . . . . . . 10
repr |
67 | 61 | sselda 3603 |
. . . . . . . . . 10
repr repr |
68 | 64, 65, 66, 67 | reprf 30690 |
. . . . . . . . 9
repr ..^ |
69 | 26 | a1i 11 |
. . . . . . . . 9
repr ..^ |
70 | 68, 69 | ffvelrnd 6360 |
. . . . . . . 8
repr |
71 | 63, 70 | ffvelrnd 6360 |
. . . . . . 7
repr Λ |
72 | 32 | a1i 11 |
. . . . . . . . . 10
repr ..^ |
73 | 68, 72 | ffvelrnd 6360 |
. . . . . . . . 9
repr |
74 | 63, 73 | ffvelrnd 6360 |
. . . . . . . 8
repr Λ |
75 | 38 | a1i 11 |
. . . . . . . . . 10
repr ..^ |
76 | 68, 75 | ffvelrnd 6360 |
. . . . . . . . 9
repr |
77 | 63, 76 | ffvelrnd 6360 |
. . . . . . . 8
repr Λ |
78 | 74, 77 | remulcld 10070 |
. . . . . . 7
repr Λ Λ |
79 | 71, 78 | remulcld 10070 |
. . . . . 6
repr Λ Λ Λ |
80 | 62, 79 | fsumrecl 14465 |
. . . . 5
repr Λ Λ Λ |
81 | 80 | recnd 10068 |
. . . 4
repr Λ Λ Λ |
82 | | fsumconst 14522 |
. . . 4
..^ repr Λ Λ Λ ..^ repr Λ Λ Λ ..^ repr Λ Λ Λ |
83 | 2, 81, 82 | syl2anc 693 |
. . 3
..^ repr Λ Λ Λ ..^ repr Λ Λ Λ |
84 | | fveq1 6190 |
. . . . . . . 8
|
85 | 84 | fveq2d 6195 |
. . . . . . 7
Λ Λ |
86 | | fveq1 6190 |
. . . . . . . . 9
|
87 | 86 | fveq2d 6195 |
. . . . . . . 8
Λ Λ |
88 | | fveq1 6190 |
. . . . . . . . 9
|
89 | 88 | fveq2d 6195 |
. . . . . . . 8
Λ Λ |
90 | 87, 89 | oveq12d 6668 |
. . . . . . 7
Λ Λ Λ Λ |
91 | 85, 90 | oveq12d 6668 |
. . . . . 6
Λ Λ Λ Λ Λ Λ |
92 | | 3nn 11186 |
. . . . . . . . . 10
|
93 | 92 | a1i 11 |
. . . . . . . . 9
|
94 | 93 | ralrimivw 2967 |
. . . . . . . 8
..^ |
95 | 94 | r19.21bi 2932 |
. . . . . . 7
..^ |
96 | 17 | adantr 481 |
. . . . . . 7
..^ |
97 | 7 | a1i 11 |
. . . . . . 7
..^ |
98 | | simpr 477 |
. . . . . . 7
..^ ..^ |
99 | | fveq1 6190 |
. . . . . . . . . 10
|
100 | 99 | eleq1d 2686 |
. . . . . . . . 9
|
101 | 100 | notbid 308 |
. . . . . . . 8
|
102 | 101 | cbvrabv 3199 |
. . . . . . 7
repr repr |
103 | | fveq1 6190 |
. . . . . . . . . 10
|
104 | 103 | eleq1d 2686 |
. . . . . . . . 9
|
105 | 104 | notbid 308 |
. . . . . . . 8
|
106 | 105 | cbvrabv 3199 |
. . . . . . 7
repr repr |
107 | | eqid 2622 |
. . . . . . 7
..^ pmTrsp..^
..^ pmTrsp..^ |
108 | | hgt750lema.f |
. . . . . . 7
repr ..^ pmTrsp..^ |
109 | 95, 96, 97, 98, 102, 106, 107, 108 | reprpmtf1o 30704 |
. . . . . 6
..^ repr repr |
110 | | eqidd 2623 |
. . . . . 6
..^ repr |
111 | 79 | adantlr 751 |
. . . . . . 7
..^ repr Λ Λ Λ |
112 | 111 | recnd 10068 |
. . . . . 6
..^ repr Λ Λ Λ |
113 | 91, 13, 109, 110, 112 | fsumf1o 14454 |
. . . . 5
..^ repr Λ Λ Λ repr Λ Λ Λ |
114 | | fveq2 6191 |
. . . . . . . . . 10
|
115 | 114 | fveq1d 6193 |
. . . . . . . . 9
|
116 | 115 | fveq2d 6195 |
. . . . . . . 8
Λ Λ |
117 | 114 | fveq1d 6193 |
. . . . . . . . . 10
|
118 | 117 | fveq2d 6195 |
. . . . . . . . 9
Λ Λ |
119 | 114 | fveq1d 6193 |
. . . . . . . . . 10
|
120 | 119 | fveq2d 6195 |
. . . . . . . . 9
Λ Λ |
121 | 118, 120 | oveq12d 6668 |
. . . . . . . 8
Λ Λ Λ Λ |
122 | 116, 121 | oveq12d 6668 |
. . . . . . 7
Λ Λ Λ Λ Λ Λ |
123 | 122 | cbvsumv 14426 |
. . . . . 6
repr Λ Λ Λ repr Λ Λ Λ |
124 | 123 | a1i 11 |
. . . . 5
..^ repr Λ Λ Λ
repr Λ Λ Λ |
125 | | ovexd 6680 |
. . . . . . . 8
..^ repr ..^ |
126 | 98 | adantr 481 |
. . . . . . . 8
..^ repr ..^ |
127 | 125, 126,
27, 107 | pmtridf1o 29856 |
. . . . . . 7
..^ repr ..^ pmTrsp..^ ..^..^ |
128 | 108, 127,
22, 15, 20 | hgt750lemg 30732 |
. . . . . 6
..^ repr Λ Λ Λ Λ Λ Λ |
129 | 128 | sumeq2dv 14433 |
. . . . 5
..^ repr Λ Λ Λ
repr Λ Λ Λ |
130 | 113, 124,
129 | 3eqtrrd 2661 |
. . . 4
..^ repr Λ Λ Λ
repr Λ Λ Λ |
131 | 130 | sumeq2dv 14433 |
. . 3
..^ repr Λ Λ Λ ..^ repr Λ Λ Λ |
132 | | hashfzo0 13217 |
. . . . . . 7
..^ |
133 | 5, 132 | ax-mp 5 |
. . . . . 6
..^ |
134 | 133 | a1i 11 |
. . . . 5
..^ |
135 | 134 | eqcomd 2628 |
. . . 4
..^ |
136 | | hgt750lemb.a |
. . . . . 6
repr |
137 | 136 | a1i 11 |
. . . . 5
repr |
138 | 137 | sumeq1d 14431 |
. . . 4
Λ Λ Λ
repr Λ Λ Λ |
139 | 135, 138 | oveq12d 6668 |
. . 3
Λ Λ Λ ..^ repr Λ Λ Λ |
140 | 83, 131, 139 | 3eqtr4rd 2667 |
. 2
Λ Λ Λ ..^ repr Λ Λ Λ |
141 | 52, 59, 140 | 3brtr4d 4685 |
1
repr reprΛ Λ Λ
Λ Λ Λ |