Step |
Hyp |
Ref |
Expression |
1 |
|
hgt750leme.o |
|- O = { z e. ZZ | -. 2 || z } |
2 |
|
hgt750leme.n |
|- ( ph -> N e. NN ) |
3 |
|
hgt750lemb.2 |
|- ( ph -> 2 <_ N ) |
4 |
|
hgt750lemb.a |
|- A = { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } |
5 |
2
|
nnnn0d |
|- ( ph -> N e. NN0 ) |
6 |
|
3nn0 |
|- 3 e. NN0 |
7 |
6
|
a1i |
|- ( ph -> 3 e. NN0 ) |
8 |
|
ssidd |
|- ( ph -> NN C_ NN ) |
9 |
5 7 8
|
reprfi2 |
|- ( ph -> ( NN ( repr ` 3 ) N ) e. Fin ) |
10 |
4
|
ssrab3 |
|- A C_ ( NN ( repr ` 3 ) N ) |
11 |
|
ssfi |
|- ( ( ( NN ( repr ` 3 ) N ) e. Fin /\ A C_ ( NN ( repr ` 3 ) N ) ) -> A e. Fin ) |
12 |
9 10 11
|
sylancl |
|- ( ph -> A e. Fin ) |
13 |
|
vmaf |
|- Lam : NN --> RR |
14 |
13
|
a1i |
|- ( ( ph /\ n e. A ) -> Lam : NN --> RR ) |
15 |
|
ssidd |
|- ( ( ph /\ n e. A ) -> NN C_ NN ) |
16 |
2
|
nnzd |
|- ( ph -> N e. ZZ ) |
17 |
16
|
adantr |
|- ( ( ph /\ n e. A ) -> N e. ZZ ) |
18 |
6
|
a1i |
|- ( ( ph /\ n e. A ) -> 3 e. NN0 ) |
19 |
|
simpr |
|- ( ( ph /\ n e. A ) -> n e. A ) |
20 |
10 19
|
sselid |
|- ( ( ph /\ n e. A ) -> n e. ( NN ( repr ` 3 ) N ) ) |
21 |
15 17 18 20
|
reprf |
|- ( ( ph /\ n e. A ) -> n : ( 0 ..^ 3 ) --> NN ) |
22 |
|
c0ex |
|- 0 e. _V |
23 |
22
|
tpid1 |
|- 0 e. { 0 , 1 , 2 } |
24 |
|
fzo0to3tp |
|- ( 0 ..^ 3 ) = { 0 , 1 , 2 } |
25 |
23 24
|
eleqtrri |
|- 0 e. ( 0 ..^ 3 ) |
26 |
25
|
a1i |
|- ( ( ph /\ n e. A ) -> 0 e. ( 0 ..^ 3 ) ) |
27 |
21 26
|
ffvelrnd |
|- ( ( ph /\ n e. A ) -> ( n ` 0 ) e. NN ) |
28 |
14 27
|
ffvelrnd |
|- ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 0 ) ) e. RR ) |
29 |
|
1ex |
|- 1 e. _V |
30 |
29
|
tpid2 |
|- 1 e. { 0 , 1 , 2 } |
31 |
30 24
|
eleqtrri |
|- 1 e. ( 0 ..^ 3 ) |
32 |
31
|
a1i |
|- ( ( ph /\ n e. A ) -> 1 e. ( 0 ..^ 3 ) ) |
33 |
21 32
|
ffvelrnd |
|- ( ( ph /\ n e. A ) -> ( n ` 1 ) e. NN ) |
34 |
14 33
|
ffvelrnd |
|- ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 1 ) ) e. RR ) |
35 |
|
2ex |
|- 2 e. _V |
36 |
35
|
tpid3 |
|- 2 e. { 0 , 1 , 2 } |
37 |
36 24
|
eleqtrri |
|- 2 e. ( 0 ..^ 3 ) |
38 |
37
|
a1i |
|- ( ( ph /\ n e. A ) -> 2 e. ( 0 ..^ 3 ) ) |
39 |
21 38
|
ffvelrnd |
|- ( ( ph /\ n e. A ) -> ( n ` 2 ) e. NN ) |
40 |
14 39
|
ffvelrnd |
|- ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 2 ) ) e. RR ) |
41 |
34 40
|
remulcld |
|- ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) e. RR ) |
42 |
28 41
|
remulcld |
|- ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR ) |
43 |
12 42
|
fsumrecl |
|- ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR ) |
44 |
2
|
nnrpd |
|- ( ph -> N e. RR+ ) |
45 |
44
|
relogcld |
|- ( ph -> ( log ` N ) e. RR ) |
46 |
28 34
|
remulcld |
|- ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) e. RR ) |
47 |
12 46
|
fsumrecl |
|- ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) e. RR ) |
48 |
45 47
|
remulcld |
|- ( ph -> ( ( log ` N ) x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) e. RR ) |
49 |
|
fzfi |
|- ( 1 ... N ) e. Fin |
50 |
|
diffi |
|- ( ( 1 ... N ) e. Fin -> ( ( 1 ... N ) \ Prime ) e. Fin ) |
51 |
49 50
|
ax-mp |
|- ( ( 1 ... N ) \ Prime ) e. Fin |
52 |
|
snfi |
|- { 2 } e. Fin |
53 |
|
unfi |
|- ( ( ( ( 1 ... N ) \ Prime ) e. Fin /\ { 2 } e. Fin ) -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin ) |
54 |
51 52 53
|
mp2an |
|- ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin |
55 |
54
|
a1i |
|- ( ph -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin ) |
56 |
13
|
a1i |
|- ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> Lam : NN --> RR ) |
57 |
|
difss |
|- ( ( 1 ... N ) \ Prime ) C_ ( 1 ... N ) |
58 |
57
|
a1i |
|- ( ph -> ( ( 1 ... N ) \ Prime ) C_ ( 1 ... N ) ) |
59 |
|
2nn |
|- 2 e. NN |
60 |
59
|
a1i |
|- ( ph -> 2 e. NN ) |
61 |
|
elfz1b |
|- ( 2 e. ( 1 ... N ) <-> ( 2 e. NN /\ N e. NN /\ 2 <_ N ) ) |
62 |
61
|
biimpri |
|- ( ( 2 e. NN /\ N e. NN /\ 2 <_ N ) -> 2 e. ( 1 ... N ) ) |
63 |
60 2 3 62
|
syl3anc |
|- ( ph -> 2 e. ( 1 ... N ) ) |
64 |
63
|
snssd |
|- ( ph -> { 2 } C_ ( 1 ... N ) ) |
65 |
58 64
|
unssd |
|- ( ph -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) C_ ( 1 ... N ) ) |
66 |
|
fz1ssnn |
|- ( 1 ... N ) C_ NN |
67 |
66
|
a1i |
|- ( ph -> ( 1 ... N ) C_ NN ) |
68 |
65 67
|
sstrd |
|- ( ph -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) C_ NN ) |
69 |
68
|
sselda |
|- ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> i e. NN ) |
70 |
56 69
|
ffvelrnd |
|- ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> ( Lam ` i ) e. RR ) |
71 |
55 70
|
fsumrecl |
|- ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) e. RR ) |
72 |
|
fzfid |
|- ( ph -> ( 1 ... N ) e. Fin ) |
73 |
13
|
a1i |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> Lam : NN --> RR ) |
74 |
67
|
sselda |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> j e. NN ) |
75 |
73 74
|
ffvelrnd |
|- ( ( ph /\ j e. ( 1 ... N ) ) -> ( Lam ` j ) e. RR ) |
76 |
72 75
|
fsumrecl |
|- ( ph -> sum_ j e. ( 1 ... N ) ( Lam ` j ) e. RR ) |
77 |
71 76
|
remulcld |
|- ( ph -> ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) e. RR ) |
78 |
45 77
|
remulcld |
|- ( ph -> ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) e. RR ) |
79 |
2
|
adantr |
|- ( ( ph /\ n e. A ) -> N e. NN ) |
80 |
79
|
nnrpd |
|- ( ( ph /\ n e. A ) -> N e. RR+ ) |
81 |
|
relogcl |
|- ( N e. RR+ -> ( log ` N ) e. RR ) |
82 |
80 81
|
syl |
|- ( ( ph /\ n e. A ) -> ( log ` N ) e. RR ) |
83 |
34 82
|
remulcld |
|- ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) e. RR ) |
84 |
28 83
|
remulcld |
|- ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) ) e. RR ) |
85 |
|
vmage0 |
|- ( ( n ` 0 ) e. NN -> 0 <_ ( Lam ` ( n ` 0 ) ) ) |
86 |
27 85
|
syl |
|- ( ( ph /\ n e. A ) -> 0 <_ ( Lam ` ( n ` 0 ) ) ) |
87 |
|
vmage0 |
|- ( ( n ` 1 ) e. NN -> 0 <_ ( Lam ` ( n ` 1 ) ) ) |
88 |
33 87
|
syl |
|- ( ( ph /\ n e. A ) -> 0 <_ ( Lam ` ( n ` 1 ) ) ) |
89 |
39
|
nnrpd |
|- ( ( ph /\ n e. A ) -> ( n ` 2 ) e. RR+ ) |
90 |
89
|
relogcld |
|- ( ( ph /\ n e. A ) -> ( log ` ( n ` 2 ) ) e. RR ) |
91 |
|
vmalelog |
|- ( ( n ` 2 ) e. NN -> ( Lam ` ( n ` 2 ) ) <_ ( log ` ( n ` 2 ) ) ) |
92 |
39 91
|
syl |
|- ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 2 ) ) <_ ( log ` ( n ` 2 ) ) ) |
93 |
15 17 18 20 38
|
reprle |
|- ( ( ph /\ n e. A ) -> ( n ` 2 ) <_ N ) |
94 |
|
logleb |
|- ( ( ( n ` 2 ) e. RR+ /\ N e. RR+ ) -> ( ( n ` 2 ) <_ N <-> ( log ` ( n ` 2 ) ) <_ ( log ` N ) ) ) |
95 |
94
|
biimpa |
|- ( ( ( ( n ` 2 ) e. RR+ /\ N e. RR+ ) /\ ( n ` 2 ) <_ N ) -> ( log ` ( n ` 2 ) ) <_ ( log ` N ) ) |
96 |
89 80 93 95
|
syl21anc |
|- ( ( ph /\ n e. A ) -> ( log ` ( n ` 2 ) ) <_ ( log ` N ) ) |
97 |
40 90 82 92 96
|
letrd |
|- ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 2 ) ) <_ ( log ` N ) ) |
98 |
40 82 34 88 97
|
lemul2ad |
|- ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) <_ ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) ) |
99 |
41 83 28 86 98
|
lemul2ad |
|- ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) ) ) |
100 |
12 42 84 99
|
fsumle |
|- ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) ) ) |
101 |
2
|
nncnd |
|- ( ph -> N e. CC ) |
102 |
2
|
nnne0d |
|- ( ph -> N =/= 0 ) |
103 |
101 102
|
logcld |
|- ( ph -> ( log ` N ) e. CC ) |
104 |
46
|
recnd |
|- ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) e. CC ) |
105 |
12 103 104
|
fsummulc2 |
|- ( ph -> ( ( log ` N ) x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) = sum_ n e. A ( ( log ` N ) x. ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) ) |
106 |
103
|
adantr |
|- ( ( ph /\ n e. A ) -> ( log ` N ) e. CC ) |
107 |
106 104
|
mulcomd |
|- ( ( ph /\ n e. A ) -> ( ( log ` N ) x. ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) = ( ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) x. ( log ` N ) ) ) |
108 |
28
|
recnd |
|- ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 0 ) ) e. CC ) |
109 |
34
|
recnd |
|- ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 1 ) ) e. CC ) |
110 |
108 109 106
|
mulassd |
|- ( ( ph /\ n e. A ) -> ( ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) x. ( log ` N ) ) = ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) ) ) |
111 |
107 110
|
eqtrd |
|- ( ( ph /\ n e. A ) -> ( ( log ` N ) x. ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) = ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) ) ) |
112 |
111
|
sumeq2dv |
|- ( ph -> sum_ n e. A ( ( log ` N ) x. ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) = sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) ) ) |
113 |
105 112
|
eqtr2d |
|- ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) ) = ( ( log ` N ) x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) ) |
114 |
100 113
|
breqtrd |
|- ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ ( ( log ` N ) x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) ) |
115 |
2
|
nnred |
|- ( ph -> N e. RR ) |
116 |
2
|
nnge1d |
|- ( ph -> 1 <_ N ) |
117 |
115 116
|
logge0d |
|- ( ph -> 0 <_ ( log ` N ) ) |
118 |
|
xpfi |
|- ( ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) e. Fin ) |
119 |
55 72 118
|
syl2anc |
|- ( ph -> ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) e. Fin ) |
120 |
13
|
a1i |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> Lam : NN --> RR ) |
121 |
68
|
adantr |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) C_ NN ) |
122 |
|
xp1st |
|- ( u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) -> ( 1st ` u ) e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) |
123 |
122
|
adantl |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( 1st ` u ) e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) |
124 |
121 123
|
sseldd |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( 1st ` u ) e. NN ) |
125 |
120 124
|
ffvelrnd |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( Lam ` ( 1st ` u ) ) e. RR ) |
126 |
|
xp2nd |
|- ( u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) -> ( 2nd ` u ) e. ( 1 ... N ) ) |
127 |
126
|
adantl |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( 2nd ` u ) e. ( 1 ... N ) ) |
128 |
66 127
|
sselid |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( 2nd ` u ) e. NN ) |
129 |
120 128
|
ffvelrnd |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( Lam ` ( 2nd ` u ) ) e. RR ) |
130 |
125 129
|
remulcld |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) e. RR ) |
131 |
|
vmage0 |
|- ( ( 1st ` u ) e. NN -> 0 <_ ( Lam ` ( 1st ` u ) ) ) |
132 |
124 131
|
syl |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> 0 <_ ( Lam ` ( 1st ` u ) ) ) |
133 |
|
vmage0 |
|- ( ( 2nd ` u ) e. NN -> 0 <_ ( Lam ` ( 2nd ` u ) ) ) |
134 |
128 133
|
syl |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> 0 <_ ( Lam ` ( 2nd ` u ) ) ) |
135 |
125 129 132 134
|
mulge0d |
|- ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> 0 <_ ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) ) |
136 |
|
ssidd |
|- ( ( ph /\ c e. A ) -> NN C_ NN ) |
137 |
16
|
adantr |
|- ( ( ph /\ c e. A ) -> N e. ZZ ) |
138 |
6
|
a1i |
|- ( ( ph /\ c e. A ) -> 3 e. NN0 ) |
139 |
|
simpr |
|- ( ( ph /\ c e. A ) -> c e. A ) |
140 |
10 139
|
sselid |
|- ( ( ph /\ c e. A ) -> c e. ( NN ( repr ` 3 ) N ) ) |
141 |
136 137 138 140
|
reprf |
|- ( ( ph /\ c e. A ) -> c : ( 0 ..^ 3 ) --> NN ) |
142 |
25
|
a1i |
|- ( ( ph /\ c e. A ) -> 0 e. ( 0 ..^ 3 ) ) |
143 |
141 142
|
ffvelrnd |
|- ( ( ph /\ c e. A ) -> ( c ` 0 ) e. NN ) |
144 |
2
|
adantr |
|- ( ( ph /\ c e. A ) -> N e. NN ) |
145 |
136 137 138 140 142
|
reprle |
|- ( ( ph /\ c e. A ) -> ( c ` 0 ) <_ N ) |
146 |
|
elfz1b |
|- ( ( c ` 0 ) e. ( 1 ... N ) <-> ( ( c ` 0 ) e. NN /\ N e. NN /\ ( c ` 0 ) <_ N ) ) |
147 |
146
|
biimpri |
|- ( ( ( c ` 0 ) e. NN /\ N e. NN /\ ( c ` 0 ) <_ N ) -> ( c ` 0 ) e. ( 1 ... N ) ) |
148 |
143 144 145 147
|
syl3anc |
|- ( ( ph /\ c e. A ) -> ( c ` 0 ) e. ( 1 ... N ) ) |
149 |
4
|
rabeq2i |
|- ( c e. A <-> ( c e. ( NN ( repr ` 3 ) N ) /\ -. ( c ` 0 ) e. ( O i^i Prime ) ) ) |
150 |
149
|
simprbi |
|- ( c e. A -> -. ( c ` 0 ) e. ( O i^i Prime ) ) |
151 |
1
|
oddprm2 |
|- ( Prime \ { 2 } ) = ( O i^i Prime ) |
152 |
151
|
eleq2i |
|- ( ( c ` 0 ) e. ( Prime \ { 2 } ) <-> ( c ` 0 ) e. ( O i^i Prime ) ) |
153 |
150 152
|
sylnibr |
|- ( c e. A -> -. ( c ` 0 ) e. ( Prime \ { 2 } ) ) |
154 |
139 153
|
syl |
|- ( ( ph /\ c e. A ) -> -. ( c ` 0 ) e. ( Prime \ { 2 } ) ) |
155 |
148 154
|
jca |
|- ( ( ph /\ c e. A ) -> ( ( c ` 0 ) e. ( 1 ... N ) /\ -. ( c ` 0 ) e. ( Prime \ { 2 } ) ) ) |
156 |
|
eldif |
|- ( ( c ` 0 ) e. ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) <-> ( ( c ` 0 ) e. ( 1 ... N ) /\ -. ( c ` 0 ) e. ( Prime \ { 2 } ) ) ) |
157 |
155 156
|
sylibr |
|- ( ( ph /\ c e. A ) -> ( c ` 0 ) e. ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) ) |
158 |
|
uncom |
|- ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) = ( { 2 } u. ( ( 1 ... N ) \ Prime ) ) |
159 |
|
undif3 |
|- ( { 2 } u. ( ( 1 ... N ) \ Prime ) ) = ( ( { 2 } u. ( 1 ... N ) ) \ ( Prime \ { 2 } ) ) |
160 |
158 159
|
eqtri |
|- ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) = ( ( { 2 } u. ( 1 ... N ) ) \ ( Prime \ { 2 } ) ) |
161 |
|
ssequn1 |
|- ( { 2 } C_ ( 1 ... N ) <-> ( { 2 } u. ( 1 ... N ) ) = ( 1 ... N ) ) |
162 |
64 161
|
sylib |
|- ( ph -> ( { 2 } u. ( 1 ... N ) ) = ( 1 ... N ) ) |
163 |
162
|
difeq1d |
|- ( ph -> ( ( { 2 } u. ( 1 ... N ) ) \ ( Prime \ { 2 } ) ) = ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) ) |
164 |
160 163
|
syl5eq |
|- ( ph -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) = ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) ) |
165 |
164
|
eleq2d |
|- ( ph -> ( ( c ` 0 ) e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) <-> ( c ` 0 ) e. ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) ) ) |
166 |
165
|
adantr |
|- ( ( ph /\ c e. A ) -> ( ( c ` 0 ) e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) <-> ( c ` 0 ) e. ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) ) ) |
167 |
157 166
|
mpbird |
|- ( ( ph /\ c e. A ) -> ( c ` 0 ) e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) |
168 |
31
|
a1i |
|- ( ( ph /\ c e. A ) -> 1 e. ( 0 ..^ 3 ) ) |
169 |
141 168
|
ffvelrnd |
|- ( ( ph /\ c e. A ) -> ( c ` 1 ) e. NN ) |
170 |
136 137 138 140 168
|
reprle |
|- ( ( ph /\ c e. A ) -> ( c ` 1 ) <_ N ) |
171 |
|
elfz1b |
|- ( ( c ` 1 ) e. ( 1 ... N ) <-> ( ( c ` 1 ) e. NN /\ N e. NN /\ ( c ` 1 ) <_ N ) ) |
172 |
171
|
biimpri |
|- ( ( ( c ` 1 ) e. NN /\ N e. NN /\ ( c ` 1 ) <_ N ) -> ( c ` 1 ) e. ( 1 ... N ) ) |
173 |
169 144 170 172
|
syl3anc |
|- ( ( ph /\ c e. A ) -> ( c ` 1 ) e. ( 1 ... N ) ) |
174 |
167 173
|
opelxpd |
|- ( ( ph /\ c e. A ) -> <. ( c ` 0 ) , ( c ` 1 ) >. e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) |
175 |
174
|
ralrimiva |
|- ( ph -> A. c e. A <. ( c ` 0 ) , ( c ` 1 ) >. e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) |
176 |
|
fveq1 |
|- ( d = c -> ( d ` 0 ) = ( c ` 0 ) ) |
177 |
|
fveq1 |
|- ( d = c -> ( d ` 1 ) = ( c ` 1 ) ) |
178 |
176 177
|
opeq12d |
|- ( d = c -> <. ( d ` 0 ) , ( d ` 1 ) >. = <. ( c ` 0 ) , ( c ` 1 ) >. ) |
179 |
178
|
cbvmptv |
|- ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) = ( c e. A |-> <. ( c ` 0 ) , ( c ` 1 ) >. ) |
180 |
179
|
rnmptss |
|- ( A. c e. A <. ( c ` 0 ) , ( c ` 1 ) >. e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) -> ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) C_ ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) |
181 |
175 180
|
syl |
|- ( ph -> ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) C_ ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) |
182 |
119 130 135 181
|
fsumless |
|- ( ph -> sum_ u e. ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) <_ sum_ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) ) |
183 |
|
fvex |
|- ( n ` 0 ) e. _V |
184 |
|
fvex |
|- ( n ` 1 ) e. _V |
185 |
183 184
|
op1std |
|- ( u = <. ( n ` 0 ) , ( n ` 1 ) >. -> ( 1st ` u ) = ( n ` 0 ) ) |
186 |
185
|
fveq2d |
|- ( u = <. ( n ` 0 ) , ( n ` 1 ) >. -> ( Lam ` ( 1st ` u ) ) = ( Lam ` ( n ` 0 ) ) ) |
187 |
183 184
|
op2ndd |
|- ( u = <. ( n ` 0 ) , ( n ` 1 ) >. -> ( 2nd ` u ) = ( n ` 1 ) ) |
188 |
187
|
fveq2d |
|- ( u = <. ( n ` 0 ) , ( n ` 1 ) >. -> ( Lam ` ( 2nd ` u ) ) = ( Lam ` ( n ` 1 ) ) ) |
189 |
186 188
|
oveq12d |
|- ( u = <. ( n ` 0 ) , ( n ` 1 ) >. -> ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) = ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) |
190 |
|
opex |
|- <. ( c ` 0 ) , ( c ` 1 ) >. e. _V |
191 |
190
|
rgenw |
|- A. c e. A <. ( c ` 0 ) , ( c ` 1 ) >. e. _V |
192 |
179
|
fnmpt |
|- ( A. c e. A <. ( c ` 0 ) , ( c ` 1 ) >. e. _V -> ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) Fn A ) |
193 |
191 192
|
mp1i |
|- ( ph -> ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) Fn A ) |
194 |
|
eqidd |
|- ( ph -> ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) = ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ) |
195 |
141
|
ad2antrr |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> c : ( 0 ..^ 3 ) --> NN ) |
196 |
195
|
ffnd |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> c Fn ( 0 ..^ 3 ) ) |
197 |
21
|
ad4ant13 |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> n : ( 0 ..^ 3 ) --> NN ) |
198 |
197
|
ffnd |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> n Fn ( 0 ..^ 3 ) ) |
199 |
|
simpr |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) |
200 |
179
|
a1i |
|- ( ph -> ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) = ( c e. A |-> <. ( c ` 0 ) , ( c ` 1 ) >. ) ) |
201 |
190
|
a1i |
|- ( ( ph /\ c e. A ) -> <. ( c ` 0 ) , ( c ` 1 ) >. e. _V ) |
202 |
200 201
|
fvmpt2d |
|- ( ( ph /\ c e. A ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = <. ( c ` 0 ) , ( c ` 1 ) >. ) |
203 |
202
|
adantr |
|- ( ( ( ph /\ c e. A ) /\ n e. A ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = <. ( c ` 0 ) , ( c ` 1 ) >. ) |
204 |
203
|
adantr |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = <. ( c ` 0 ) , ( c ` 1 ) >. ) |
205 |
|
fveq1 |
|- ( c = n -> ( c ` 0 ) = ( n ` 0 ) ) |
206 |
|
fveq1 |
|- ( c = n -> ( c ` 1 ) = ( n ` 1 ) ) |
207 |
205 206
|
opeq12d |
|- ( c = n -> <. ( c ` 0 ) , ( c ` 1 ) >. = <. ( n ` 0 ) , ( n ` 1 ) >. ) |
208 |
|
opex |
|- <. ( n ` 0 ) , ( n ` 1 ) >. e. _V |
209 |
208
|
a1i |
|- ( ( ph /\ n e. A ) -> <. ( n ` 0 ) , ( n ` 1 ) >. e. _V ) |
210 |
179 207 19 209
|
fvmptd3 |
|- ( ( ph /\ n e. A ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) = <. ( n ` 0 ) , ( n ` 1 ) >. ) |
211 |
210
|
adantlr |
|- ( ( ( ph /\ c e. A ) /\ n e. A ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) = <. ( n ` 0 ) , ( n ` 1 ) >. ) |
212 |
211
|
adantr |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) = <. ( n ` 0 ) , ( n ` 1 ) >. ) |
213 |
199 204 212
|
3eqtr3d |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> <. ( c ` 0 ) , ( c ` 1 ) >. = <. ( n ` 0 ) , ( n ` 1 ) >. ) |
214 |
183 184
|
opth2 |
|- ( <. ( c ` 0 ) , ( c ` 1 ) >. = <. ( n ` 0 ) , ( n ` 1 ) >. <-> ( ( c ` 0 ) = ( n ` 0 ) /\ ( c ` 1 ) = ( n ` 1 ) ) ) |
215 |
213 214
|
sylib |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> ( ( c ` 0 ) = ( n ` 0 ) /\ ( c ` 1 ) = ( n ` 1 ) ) ) |
216 |
215
|
simpld |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> ( c ` 0 ) = ( n ` 0 ) ) |
217 |
216
|
ad2antrr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 0 ) -> ( c ` 0 ) = ( n ` 0 ) ) |
218 |
|
simpr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 0 ) -> i = 0 ) |
219 |
218
|
fveq2d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 0 ) -> ( c ` i ) = ( c ` 0 ) ) |
220 |
218
|
fveq2d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 0 ) -> ( n ` i ) = ( n ` 0 ) ) |
221 |
217 219 220
|
3eqtr4d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 0 ) -> ( c ` i ) = ( n ` i ) ) |
222 |
215
|
simprd |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> ( c ` 1 ) = ( n ` 1 ) ) |
223 |
222
|
ad2antrr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 1 ) -> ( c ` 1 ) = ( n ` 1 ) ) |
224 |
|
simpr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 1 ) -> i = 1 ) |
225 |
224
|
fveq2d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 1 ) -> ( c ` i ) = ( c ` 1 ) ) |
226 |
224
|
fveq2d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 1 ) -> ( n ` i ) = ( n ` 1 ) ) |
227 |
223 225 226
|
3eqtr4d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 1 ) -> ( c ` i ) = ( n ` i ) ) |
228 |
216
|
ad2antrr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( c ` 0 ) = ( n ` 0 ) ) |
229 |
222
|
ad2antrr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( c ` 1 ) = ( n ` 1 ) ) |
230 |
228 229
|
oveq12d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( ( c ` 0 ) + ( c ` 1 ) ) = ( ( n ` 0 ) + ( n ` 1 ) ) ) |
231 |
230
|
oveq2d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( N - ( ( c ` 0 ) + ( c ` 1 ) ) ) = ( N - ( ( n ` 0 ) + ( n ` 1 ) ) ) ) |
232 |
24
|
a1i |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( 0 ..^ 3 ) = { 0 , 1 , 2 } ) |
233 |
232
|
sumeq1d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> sum_ j e. ( 0 ..^ 3 ) ( c ` j ) = sum_ j e. { 0 , 1 , 2 } ( c ` j ) ) |
234 |
|
ssidd |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> NN C_ NN ) |
235 |
137
|
ad4antr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> N e. ZZ ) |
236 |
6
|
a1i |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> 3 e. NN0 ) |
237 |
140
|
ad4antr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> c e. ( NN ( repr ` 3 ) N ) ) |
238 |
234 235 236 237
|
reprsum |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> sum_ j e. ( 0 ..^ 3 ) ( c ` j ) = N ) |
239 |
|
fveq2 |
|- ( j = 0 -> ( c ` j ) = ( c ` 0 ) ) |
240 |
|
fveq2 |
|- ( j = 1 -> ( c ` j ) = ( c ` 1 ) ) |
241 |
|
fveq2 |
|- ( j = 2 -> ( c ` j ) = ( c ` 2 ) ) |
242 |
143
|
nncnd |
|- ( ( ph /\ c e. A ) -> ( c ` 0 ) e. CC ) |
243 |
242
|
ad4antr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( c ` 0 ) e. CC ) |
244 |
169
|
nncnd |
|- ( ( ph /\ c e. A ) -> ( c ` 1 ) e. CC ) |
245 |
244
|
ad4antr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( c ` 1 ) e. CC ) |
246 |
37
|
a1i |
|- ( ( ph /\ c e. A ) -> 2 e. ( 0 ..^ 3 ) ) |
247 |
141 246
|
ffvelrnd |
|- ( ( ph /\ c e. A ) -> ( c ` 2 ) e. NN ) |
248 |
247
|
nncnd |
|- ( ( ph /\ c e. A ) -> ( c ` 2 ) e. CC ) |
249 |
248
|
ad4antr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( c ` 2 ) e. CC ) |
250 |
243 245 249
|
3jca |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( ( c ` 0 ) e. CC /\ ( c ` 1 ) e. CC /\ ( c ` 2 ) e. CC ) ) |
251 |
22 29 35
|
3pm3.2i |
|- ( 0 e. _V /\ 1 e. _V /\ 2 e. _V ) |
252 |
251
|
a1i |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( 0 e. _V /\ 1 e. _V /\ 2 e. _V ) ) |
253 |
|
0ne1 |
|- 0 =/= 1 |
254 |
253
|
a1i |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> 0 =/= 1 ) |
255 |
|
0ne2 |
|- 0 =/= 2 |
256 |
255
|
a1i |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> 0 =/= 2 ) |
257 |
|
1ne2 |
|- 1 =/= 2 |
258 |
257
|
a1i |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> 1 =/= 2 ) |
259 |
239 240 241 250 252 254 256 258
|
sumtp |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> sum_ j e. { 0 , 1 , 2 } ( c ` j ) = ( ( ( c ` 0 ) + ( c ` 1 ) ) + ( c ` 2 ) ) ) |
260 |
233 238 259
|
3eqtr3rd |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( ( ( c ` 0 ) + ( c ` 1 ) ) + ( c ` 2 ) ) = N ) |
261 |
243 245
|
addcld |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( ( c ` 0 ) + ( c ` 1 ) ) e. CC ) |
262 |
101
|
ad5antr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> N e. CC ) |
263 |
261 249 262
|
addrsub |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( ( ( ( c ` 0 ) + ( c ` 1 ) ) + ( c ` 2 ) ) = N <-> ( c ` 2 ) = ( N - ( ( c ` 0 ) + ( c ` 1 ) ) ) ) ) |
264 |
260 263
|
mpbid |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( c ` 2 ) = ( N - ( ( c ` 0 ) + ( c ` 1 ) ) ) ) |
265 |
232
|
sumeq1d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> sum_ j e. ( 0 ..^ 3 ) ( n ` j ) = sum_ j e. { 0 , 1 , 2 } ( n ` j ) ) |
266 |
20
|
ad4ant13 |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> n e. ( NN ( repr ` 3 ) N ) ) |
267 |
266
|
ad2antrr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> n e. ( NN ( repr ` 3 ) N ) ) |
268 |
234 235 236 267
|
reprsum |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> sum_ j e. ( 0 ..^ 3 ) ( n ` j ) = N ) |
269 |
|
fveq2 |
|- ( j = 0 -> ( n ` j ) = ( n ` 0 ) ) |
270 |
|
fveq2 |
|- ( j = 1 -> ( n ` j ) = ( n ` 1 ) ) |
271 |
|
fveq2 |
|- ( j = 2 -> ( n ` j ) = ( n ` 2 ) ) |
272 |
27
|
nncnd |
|- ( ( ph /\ n e. A ) -> ( n ` 0 ) e. CC ) |
273 |
272
|
adantlr |
|- ( ( ( ph /\ c e. A ) /\ n e. A ) -> ( n ` 0 ) e. CC ) |
274 |
273
|
ad3antrrr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( n ` 0 ) e. CC ) |
275 |
33
|
nncnd |
|- ( ( ph /\ n e. A ) -> ( n ` 1 ) e. CC ) |
276 |
275
|
adantlr |
|- ( ( ( ph /\ c e. A ) /\ n e. A ) -> ( n ` 1 ) e. CC ) |
277 |
276
|
ad3antrrr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( n ` 1 ) e. CC ) |
278 |
39
|
nncnd |
|- ( ( ph /\ n e. A ) -> ( n ` 2 ) e. CC ) |
279 |
278
|
adantlr |
|- ( ( ( ph /\ c e. A ) /\ n e. A ) -> ( n ` 2 ) e. CC ) |
280 |
279
|
ad3antrrr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( n ` 2 ) e. CC ) |
281 |
274 277 280
|
3jca |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( ( n ` 0 ) e. CC /\ ( n ` 1 ) e. CC /\ ( n ` 2 ) e. CC ) ) |
282 |
269 270 271 281 252 254 256 258
|
sumtp |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> sum_ j e. { 0 , 1 , 2 } ( n ` j ) = ( ( ( n ` 0 ) + ( n ` 1 ) ) + ( n ` 2 ) ) ) |
283 |
265 268 282
|
3eqtr3rd |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( ( ( n ` 0 ) + ( n ` 1 ) ) + ( n ` 2 ) ) = N ) |
284 |
274 277
|
addcld |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( ( n ` 0 ) + ( n ` 1 ) ) e. CC ) |
285 |
284 280 262
|
addrsub |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( ( ( ( n ` 0 ) + ( n ` 1 ) ) + ( n ` 2 ) ) = N <-> ( n ` 2 ) = ( N - ( ( n ` 0 ) + ( n ` 1 ) ) ) ) ) |
286 |
283 285
|
mpbid |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( n ` 2 ) = ( N - ( ( n ` 0 ) + ( n ` 1 ) ) ) ) |
287 |
231 264 286
|
3eqtr4d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( c ` 2 ) = ( n ` 2 ) ) |
288 |
|
simpr |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> i = 2 ) |
289 |
288
|
fveq2d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( c ` i ) = ( c ` 2 ) ) |
290 |
288
|
fveq2d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( n ` i ) = ( n ` 2 ) ) |
291 |
287 289 290
|
3eqtr4d |
|- ( ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) /\ i = 2 ) -> ( c ` i ) = ( n ` i ) ) |
292 |
|
simpr |
|- ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) -> i e. ( 0 ..^ 3 ) ) |
293 |
292 24
|
eleqtrdi |
|- ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) -> i e. { 0 , 1 , 2 } ) |
294 |
|
vex |
|- i e. _V |
295 |
294
|
eltp |
|- ( i e. { 0 , 1 , 2 } <-> ( i = 0 \/ i = 1 \/ i = 2 ) ) |
296 |
293 295
|
sylib |
|- ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) -> ( i = 0 \/ i = 1 \/ i = 2 ) ) |
297 |
221 227 291 296
|
mpjao3dan |
|- ( ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) /\ i e. ( 0 ..^ 3 ) ) -> ( c ` i ) = ( n ` i ) ) |
298 |
196 198 297
|
eqfnfvd |
|- ( ( ( ( ph /\ c e. A ) /\ n e. A ) /\ ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> c = n ) |
299 |
298
|
ex |
|- ( ( ( ph /\ c e. A ) /\ n e. A ) -> ( ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) -> c = n ) ) |
300 |
299
|
anasss |
|- ( ( ph /\ ( c e. A /\ n e. A ) ) -> ( ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) -> c = n ) ) |
301 |
300
|
ralrimivva |
|- ( ph -> A. c e. A A. n e. A ( ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) -> c = n ) ) |
302 |
|
dff1o6 |
|- ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) : A -1-1-onto-> ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) <-> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) Fn A /\ ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) = ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) /\ A. c e. A A. n e. A ( ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) -> c = n ) ) ) |
303 |
302
|
biimpri |
|- ( ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) Fn A /\ ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) = ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) /\ A. c e. A A. n e. A ( ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) -> c = n ) ) -> ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) : A -1-1-onto-> ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ) |
304 |
193 194 301 303
|
syl3anc |
|- ( ph -> ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) : A -1-1-onto-> ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ) |
305 |
181
|
sselda |
|- ( ( ph /\ u e. ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ) -> u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) |
306 |
305 125
|
syldan |
|- ( ( ph /\ u e. ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ) -> ( Lam ` ( 1st ` u ) ) e. RR ) |
307 |
305 129
|
syldan |
|- ( ( ph /\ u e. ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ) -> ( Lam ` ( 2nd ` u ) ) e. RR ) |
308 |
306 307
|
remulcld |
|- ( ( ph /\ u e. ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ) -> ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) e. RR ) |
309 |
308
|
recnd |
|- ( ( ph /\ u e. ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ) -> ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) e. CC ) |
310 |
189 12 304 210 309
|
fsumf1o |
|- ( ph -> sum_ u e. ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) = sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) |
311 |
76
|
recnd |
|- ( ph -> sum_ j e. ( 1 ... N ) ( Lam ` j ) e. CC ) |
312 |
70
|
recnd |
|- ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> ( Lam ` i ) e. CC ) |
313 |
55 311 312
|
fsummulc1 |
|- ( ph -> ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) = sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) |
314 |
49
|
a1i |
|- ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> ( 1 ... N ) e. Fin ) |
315 |
75
|
adantrl |
|- ( ( ph /\ ( i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) /\ j e. ( 1 ... N ) ) ) -> ( Lam ` j ) e. RR ) |
316 |
315
|
anassrs |
|- ( ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) /\ j e. ( 1 ... N ) ) -> ( Lam ` j ) e. RR ) |
317 |
316
|
recnd |
|- ( ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) /\ j e. ( 1 ... N ) ) -> ( Lam ` j ) e. CC ) |
318 |
314 312 317
|
fsummulc2 |
|- ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> ( ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) = sum_ j e. ( 1 ... N ) ( ( Lam ` i ) x. ( Lam ` j ) ) ) |
319 |
318
|
sumeq2dv |
|- ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) = sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) sum_ j e. ( 1 ... N ) ( ( Lam ` i ) x. ( Lam ` j ) ) ) |
320 |
|
vex |
|- j e. _V |
321 |
294 320
|
op1std |
|- ( u = <. i , j >. -> ( 1st ` u ) = i ) |
322 |
321
|
fveq2d |
|- ( u = <. i , j >. -> ( Lam ` ( 1st ` u ) ) = ( Lam ` i ) ) |
323 |
294 320
|
op2ndd |
|- ( u = <. i , j >. -> ( 2nd ` u ) = j ) |
324 |
323
|
fveq2d |
|- ( u = <. i , j >. -> ( Lam ` ( 2nd ` u ) ) = ( Lam ` j ) ) |
325 |
322 324
|
oveq12d |
|- ( u = <. i , j >. -> ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) = ( ( Lam ` i ) x. ( Lam ` j ) ) ) |
326 |
70
|
adantrr |
|- ( ( ph /\ ( i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) /\ j e. ( 1 ... N ) ) ) -> ( Lam ` i ) e. RR ) |
327 |
326 315
|
remulcld |
|- ( ( ph /\ ( i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) /\ j e. ( 1 ... N ) ) ) -> ( ( Lam ` i ) x. ( Lam ` j ) ) e. RR ) |
328 |
327
|
recnd |
|- ( ( ph /\ ( i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) /\ j e. ( 1 ... N ) ) ) -> ( ( Lam ` i ) x. ( Lam ` j ) ) e. CC ) |
329 |
325 55 72 328
|
fsumxp |
|- ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) sum_ j e. ( 1 ... N ) ( ( Lam ` i ) x. ( Lam ` j ) ) = sum_ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) ) |
330 |
313 319 329
|
3eqtrrd |
|- ( ph -> sum_ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) = ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) |
331 |
182 310 330
|
3brtr3d |
|- ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) <_ ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) |
332 |
47 77 45 117 331
|
lemul2ad |
|- ( ph -> ( ( log ` N ) x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) <_ ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) |
333 |
43 48 78 114 332
|
letrd |
|- ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ ( ( log ` N ) x. ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) ) ) |