Metamath Proof Explorer

Theorem hgt750lemb

Description: An upper bound on the contribution of the non-prime terms in the Statement 7.50 of Helfgott p. 69. (Contributed by Thierry Arnoux, 28-Dec-2021)

Ref Expression
Hypotheses hgt750leme.o 
|- O = { z e. ZZ | -. 2 || z }
hgt750leme.n 
|- ( ph -> N e. NN )
hgt750lemb.2 
|- ( ph -> 2 <_ N )
hgt750lemb.a 
|- A = { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) }
Assertion hgt750lemb 
|- ( 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 ) ) ) )

Proof

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 ffvelcdmd 
 |-  ( ( ph /\ n e. A ) -> ( n ` 0 ) e. NN )
28 14 27 ffvelcdmd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 0 ) ) e. RR )
29 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
30 29 24 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
31 30 a1i 
 |-  ( ( ph /\ n e. A ) -> 1 e. ( 0 ..^ 3 ) )
32 21 31 ffvelcdmd 
 |-  ( ( ph /\ n e. A ) -> ( n ` 1 ) e. NN )
33 14 32 ffvelcdmd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 1 ) ) e. RR )
34 2ex 
 |-  2 e. _V
35 34 tpid3 
 |-  2 e. { 0 , 1 , 2 }
36 35 24 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
37 36 a1i 
 |-  ( ( ph /\ n e. A ) -> 2 e. ( 0 ..^ 3 ) )
38 21 37 ffvelcdmd 
 |-  ( ( ph /\ n e. A ) -> ( n ` 2 ) e. NN )
39 14 38 ffvelcdmd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 2 ) ) e. RR )
40 33 39 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) e. RR )
41 28 40 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
42 12 41 fsumrecl 
 |-  ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
43 2 nnrpd 
 |-  ( ph -> N e. RR+ )
44 43 relogcld 
 |-  ( ph -> ( log ` N ) e. RR )
45 28 33 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) e. RR )
46 12 45 fsumrecl 
 |-  ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) e. RR )
47 44 46 remulcld 
 |-  ( ph -> ( ( log ` N ) x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) ) e. RR )
48 fzfi 
 |-  ( 1 ... N ) e. Fin
49 diffi 
 |-  ( ( 1 ... N ) e. Fin -> ( ( 1 ... N ) \ Prime ) e. Fin )
50 48 49 ax-mp 
 |-  ( ( 1 ... N ) \ Prime ) e. Fin
51 snfi 
 |-  { 2 } e. Fin
52 unfi 
 |-  ( ( ( ( 1 ... N ) \ Prime ) e. Fin /\ { 2 } e. Fin ) -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin )
53 50 51 52 mp2an 
 |-  ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin
54 53 a1i 
 |-  ( ph -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin )
55 13 a1i 
 |-  ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> Lam : NN --> RR )
56 difss 
 |-  ( ( 1 ... N ) \ Prime ) C_ ( 1 ... N )
57 56 a1i 
 |-  ( ph -> ( ( 1 ... N ) \ Prime ) C_ ( 1 ... N ) )
58 2nn 
 |-  2 e. NN
59 58 a1i 
 |-  ( ph -> 2 e. NN )
60 elfz1b 
 |-  ( 2 e. ( 1 ... N ) <-> ( 2 e. NN /\ N e. NN /\ 2 <_ N ) )
61 60 biimpri 
 |-  ( ( 2 e. NN /\ N e. NN /\ 2 <_ N ) -> 2 e. ( 1 ... N ) )
62 59 2 3 61 syl3anc 
 |-  ( ph -> 2 e. ( 1 ... N ) )
63 62 snssd 
 |-  ( ph -> { 2 } C_ ( 1 ... N ) )
64 57 63 unssd 
 |-  ( ph -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) C_ ( 1 ... N ) )
65 fz1ssnn 
 |-  ( 1 ... N ) C_ NN
66 65 a1i 
 |-  ( ph -> ( 1 ... N ) C_ NN )
67 64 66 sstrd 
 |-  ( ph -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) C_ NN )
68 67 sselda 
 |-  ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> i e. NN )
69 55 68 ffvelcdmd 
 |-  ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> ( Lam ` i ) e. RR )
70 54 69 fsumrecl 
 |-  ( ph -> sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) e. RR )
71 fzfid 
 |-  ( ph -> ( 1 ... N ) e. Fin )
72 13 a1i 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> Lam : NN --> RR )
73 66 sselda 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> j e. NN )
74 72 73 ffvelcdmd 
 |-  ( ( ph /\ j e. ( 1 ... N ) ) -> ( Lam ` j ) e. RR )
75 71 74 fsumrecl 
 |-  ( ph -> sum_ j e. ( 1 ... N ) ( Lam ` j ) e. RR )
76 70 75 remulcld 
 |-  ( ph -> ( sum_ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ( Lam ` i ) x. sum_ j e. ( 1 ... N ) ( Lam ` j ) ) e. RR )
77 44 76 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 )
78 2 adantr 
 |-  ( ( ph /\ n e. A ) -> N e. NN )
79 78 nnrpd 
 |-  ( ( ph /\ n e. A ) -> N e. RR+ )
80 relogcl 
 |-  ( N e. RR+ -> ( log ` N ) e. RR )
81 79 80 syl 
 |-  ( ( ph /\ n e. A ) -> ( log ` N ) e. RR )
82 33 81 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) e. RR )
83 28 82 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) ) e. RR )
84 vmage0 
 |-  ( ( n ` 0 ) e. NN -> 0 <_ ( Lam ` ( n ` 0 ) ) )
85 27 84 syl 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( Lam ` ( n ` 0 ) ) )
86 vmage0 
 |-  ( ( n ` 1 ) e. NN -> 0 <_ ( Lam ` ( n ` 1 ) ) )
87 32 86 syl 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( Lam ` ( n ` 1 ) ) )
88 38 nnrpd 
 |-  ( ( ph /\ n e. A ) -> ( n ` 2 ) e. RR+ )
89 88 relogcld 
 |-  ( ( ph /\ n e. A ) -> ( log ` ( n ` 2 ) ) e. RR )
90 vmalelog 
 |-  ( ( n ` 2 ) e. NN -> ( Lam ` ( n ` 2 ) ) <_ ( log ` ( n ` 2 ) ) )
91 38 90 syl 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 2 ) ) <_ ( log ` ( n ` 2 ) ) )
92 15 17 18 20 37 reprle 
 |-  ( ( ph /\ n e. A ) -> ( n ` 2 ) <_ N )
93 logleb 
 |-  ( ( ( n ` 2 ) e. RR+ /\ N e. RR+ ) -> ( ( n ` 2 ) <_ N <-> ( log ` ( n ` 2 ) ) <_ ( log ` N ) ) )
94 93 biimpa 
 |-  ( ( ( ( n ` 2 ) e. RR+ /\ N e. RR+ ) /\ ( n ` 2 ) <_ N ) -> ( log ` ( n ` 2 ) ) <_ ( log ` N ) )
95 88 79 92 94 syl21anc 
 |-  ( ( ph /\ n e. A ) -> ( log ` ( n ` 2 ) ) <_ ( log ` N ) )
96 39 89 81 91 95 letrd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 2 ) ) <_ ( log ` N ) )
97 39 81 33 87 96 lemul2ad 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) <_ ( ( Lam ` ( n ` 1 ) ) x. ( log ` N ) ) )
98 40 82 28 85 97 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 ) ) ) )
99 12 41 83 98 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 ) ) ) )
100 2 nncnd 
 |-  ( ph -> N e. CC )
101 2 nnne0d 
 |-  ( ph -> N =/= 0 )
102 100 101 logcld 
 |-  ( ph -> ( log ` N ) e. CC )
103 45 recnd 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) e. CC )
104 12 102 103 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 ) ) ) ) )
105 102 adantr 
 |-  ( ( ph /\ n e. A ) -> ( log ` N ) e. CC )
106 105 103 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 ) ) )
107 28 recnd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 0 ) ) e. CC )
108 33 recnd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 1 ) ) e. CC )
109 107 108 105 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 ) ) ) )
110 106 109 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 ) ) ) )
111 110 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 ) ) ) )
112 104 111 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 ) ) ) ) )
113 99 112 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 ) ) ) ) )
114 2 nnred 
 |-  ( ph -> N e. RR )
115 2 nnge1d 
 |-  ( ph -> 1 <_ N )
116 114 115 logge0d 
 |-  ( ph -> 0 <_ ( log ` N ) )
117 xpfi 
 |-  ( ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) e. Fin )
118 54 71 117 syl2anc 
 |-  ( ph -> ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) e. Fin )
119 13 a1i 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> Lam : NN --> RR )
120 67 adantr 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) C_ NN )
121 xp1st 
 |-  ( u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) -> ( 1st ` u ) e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) )
122 121 adantl 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( 1st ` u ) e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) )
123 120 122 sseldd 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( 1st ` u ) e. NN )
124 119 123 ffvelcdmd 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( Lam ` ( 1st ` u ) ) e. RR )
125 xp2nd 
 |-  ( u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) -> ( 2nd ` u ) e. ( 1 ... N ) )
126 125 adantl 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( 2nd ` u ) e. ( 1 ... N ) )
127 65 126 sselid 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( 2nd ` u ) e. NN )
128 119 127 ffvelcdmd 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( Lam ` ( 2nd ` u ) ) e. RR )
129 124 128 remulcld 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) e. RR )
130 vmage0 
 |-  ( ( 1st ` u ) e. NN -> 0 <_ ( Lam ` ( 1st ` u ) ) )
131 123 130 syl 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> 0 <_ ( Lam ` ( 1st ` u ) ) )
132 vmage0 
 |-  ( ( 2nd ` u ) e. NN -> 0 <_ ( Lam ` ( 2nd ` u ) ) )
133 127 132 syl 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> 0 <_ ( Lam ` ( 2nd ` u ) ) )
134 124 128 131 133 mulge0d 
 |-  ( ( ph /\ u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) ) -> 0 <_ ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) )
135 ssidd 
 |-  ( ( ph /\ c e. A ) -> NN C_ NN )
136 16 adantr 
 |-  ( ( ph /\ c e. A ) -> N e. ZZ )
137 6 a1i 
 |-  ( ( ph /\ c e. A ) -> 3 e. NN0 )
138 simpr 
 |-  ( ( ph /\ c e. A ) -> c e. A )
139 10 138 sselid 
 |-  ( ( ph /\ c e. A ) -> c e. ( NN ( repr ` 3 ) N ) )
140 135 136 137 139 reprf 
 |-  ( ( ph /\ c e. A ) -> c : ( 0 ..^ 3 ) --> NN )
141 25 a1i 
 |-  ( ( ph /\ c e. A ) -> 0 e. ( 0 ..^ 3 ) )
142 140 141 ffvelcdmd 
 |-  ( ( ph /\ c e. A ) -> ( c ` 0 ) e. NN )
143 2 adantr 
 |-  ( ( ph /\ c e. A ) -> N e. NN )
144 135 136 137 139 141 reprle 
 |-  ( ( ph /\ c e. A ) -> ( c ` 0 ) <_ N )
145 elfz1b 
 |-  ( ( c ` 0 ) e. ( 1 ... N ) <-> ( ( c ` 0 ) e. NN /\ N e. NN /\ ( c ` 0 ) <_ N ) )
146 145 biimpri 
 |-  ( ( ( c ` 0 ) e. NN /\ N e. NN /\ ( c ` 0 ) <_ N ) -> ( c ` 0 ) e. ( 1 ... N ) )
147 142 143 144 146 syl3anc 
 |-  ( ( ph /\ c e. A ) -> ( c ` 0 ) e. ( 1 ... N ) )
148 4 reqabi 
 |-  ( c e. A <-> ( c e. ( NN ( repr ` 3 ) N ) /\ -. ( c ` 0 ) e. ( O i^i Prime ) ) )
149 148 simprbi 
 |-  ( c e. A -> -. ( c ` 0 ) e. ( O i^i Prime ) )
150 1 oddprm2 
 |-  ( Prime \ { 2 } ) = ( O i^i Prime )
151 150 eleq2i 
 |-  ( ( c ` 0 ) e. ( Prime \ { 2 } ) <-> ( c ` 0 ) e. ( O i^i Prime ) )
152 149 151 sylnibr 
 |-  ( c e. A -> -. ( c ` 0 ) e. ( Prime \ { 2 } ) )
153 138 152 syl 
 |-  ( ( ph /\ c e. A ) -> -. ( c ` 0 ) e. ( Prime \ { 2 } ) )
154 147 153 jca 
 |-  ( ( ph /\ c e. A ) -> ( ( c ` 0 ) e. ( 1 ... N ) /\ -. ( c ` 0 ) e. ( Prime \ { 2 } ) ) )
155 eldif 
 |-  ( ( c ` 0 ) e. ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) <-> ( ( c ` 0 ) e. ( 1 ... N ) /\ -. ( c ` 0 ) e. ( Prime \ { 2 } ) ) )
156 154 155 sylibr 
 |-  ( ( ph /\ c e. A ) -> ( c ` 0 ) e. ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) )
157 uncom 
 |-  ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) = ( { 2 } u. ( ( 1 ... N ) \ Prime ) )
158 undif3 
 |-  ( { 2 } u. ( ( 1 ... N ) \ Prime ) ) = ( ( { 2 } u. ( 1 ... N ) ) \ ( Prime \ { 2 } ) )
159 157 158 eqtri 
 |-  ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) = ( ( { 2 } u. ( 1 ... N ) ) \ ( Prime \ { 2 } ) )
160 ssequn1 
 |-  ( { 2 } C_ ( 1 ... N ) <-> ( { 2 } u. ( 1 ... N ) ) = ( 1 ... N ) )
161 63 160 sylib 
 |-  ( ph -> ( { 2 } u. ( 1 ... N ) ) = ( 1 ... N ) )
162 161 difeq1d 
 |-  ( ph -> ( ( { 2 } u. ( 1 ... N ) ) \ ( Prime \ { 2 } ) ) = ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) )
163 159 162 eqtrid 
 |-  ( ph -> ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) = ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) )
164 163 eleq2d 
 |-  ( ph -> ( ( c ` 0 ) e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) <-> ( c ` 0 ) e. ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) ) )
165 164 adantr 
 |-  ( ( ph /\ c e. A ) -> ( ( c ` 0 ) e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) <-> ( c ` 0 ) e. ( ( 1 ... N ) \ ( Prime \ { 2 } ) ) ) )
166 156 165 mpbird 
 |-  ( ( ph /\ c e. A ) -> ( c ` 0 ) e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) )
167 30 a1i 
 |-  ( ( ph /\ c e. A ) -> 1 e. ( 0 ..^ 3 ) )
168 140 167 ffvelcdmd 
 |-  ( ( ph /\ c e. A ) -> ( c ` 1 ) e. NN )
169 135 136 137 139 167 reprle 
 |-  ( ( ph /\ c e. A ) -> ( c ` 1 ) <_ N )
170 elfz1b 
 |-  ( ( c ` 1 ) e. ( 1 ... N ) <-> ( ( c ` 1 ) e. NN /\ N e. NN /\ ( c ` 1 ) <_ N ) )
171 170 biimpri 
 |-  ( ( ( c ` 1 ) e. NN /\ N e. NN /\ ( c ` 1 ) <_ N ) -> ( c ` 1 ) e. ( 1 ... N ) )
172 168 143 169 171 syl3anc 
 |-  ( ( ph /\ c e. A ) -> ( c ` 1 ) e. ( 1 ... N ) )
173 166 172 opelxpd 
 |-  ( ( ph /\ c e. A ) -> <. ( c ` 0 ) , ( c ` 1 ) >. e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) )
174 173 ralrimiva 
 |-  ( ph -> A. c e. A <. ( c ` 0 ) , ( c ` 1 ) >. e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) )
175 fveq1 
 |-  ( d = c -> ( d ` 0 ) = ( c ` 0 ) )
176 fveq1 
 |-  ( d = c -> ( d ` 1 ) = ( c ` 1 ) )
177 175 176 opeq12d 
 |-  ( d = c -> <. ( d ` 0 ) , ( d ` 1 ) >. = <. ( c ` 0 ) , ( c ` 1 ) >. )
178 177 cbvmptv 
 |-  ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) = ( c e. A |-> <. ( c ` 0 ) , ( c ` 1 ) >. )
179 178 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 ) ) )
180 174 179 syl 
 |-  ( ph -> ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) C_ ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) )
181 118 129 134 180 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 ) ) ) )
182 fvex 
 |-  ( n ` 0 ) e. _V
183 fvex 
 |-  ( n ` 1 ) e. _V
184 182 183 op1std 
 |-  ( u = <. ( n ` 0 ) , ( n ` 1 ) >. -> ( 1st ` u ) = ( n ` 0 ) )
185 184 fveq2d 
 |-  ( u = <. ( n ` 0 ) , ( n ` 1 ) >. -> ( Lam ` ( 1st ` u ) ) = ( Lam ` ( n ` 0 ) ) )
186 182 183 op2ndd 
 |-  ( u = <. ( n ` 0 ) , ( n ` 1 ) >. -> ( 2nd ` u ) = ( n ` 1 ) )
187 186 fveq2d 
 |-  ( u = <. ( n ` 0 ) , ( n ` 1 ) >. -> ( Lam ` ( 2nd ` u ) ) = ( Lam ` ( n ` 1 ) ) )
188 185 187 oveq12d 
 |-  ( u = <. ( n ` 0 ) , ( n ` 1 ) >. -> ( ( Lam ` ( 1st ` u ) ) x. ( Lam ` ( 2nd ` u ) ) ) = ( ( Lam ` ( n ` 0 ) ) x. ( Lam ` ( n ` 1 ) ) ) )
189 opex 
 |-  <. ( c ` 0 ) , ( c ` 1 ) >. e. _V
190 189 rgenw 
 |-  A. c e. A <. ( c ` 0 ) , ( c ` 1 ) >. e. _V
191 178 fnmpt 
 |-  ( A. c e. A <. ( c ` 0 ) , ( c ` 1 ) >. e. _V -> ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) Fn A )
192 190 191 mp1i 
 |-  ( ph -> ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) Fn A )
193 eqidd 
 |-  ( ph -> ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) = ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) )
194 140 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 )
195 194 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 ) )
196 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 )
197 196 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 ) )
198 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 ) )
199 178 a1i 
 |-  ( ph -> ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) = ( c e. A |-> <. ( c ` 0 ) , ( c ` 1 ) >. ) )
200 189 a1i 
 |-  ( ( ph /\ c e. A ) -> <. ( c ` 0 ) , ( c ` 1 ) >. e. _V )
201 199 200 fvmpt2d 
 |-  ( ( ph /\ c e. A ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = <. ( c ` 0 ) , ( c ` 1 ) >. )
202 201 adantr 
 |-  ( ( ( ph /\ c e. A ) /\ n 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 ) = ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` c ) = <. ( c ` 0 ) , ( c ` 1 ) >. )
204 fveq1 
 |-  ( c = n -> ( c ` 0 ) = ( n ` 0 ) )
205 fveq1 
 |-  ( c = n -> ( c ` 1 ) = ( n ` 1 ) )
206 204 205 opeq12d 
 |-  ( c = n -> <. ( c ` 0 ) , ( c ` 1 ) >. = <. ( n ` 0 ) , ( n ` 1 ) >. )
207 opex 
 |-  <. ( n ` 0 ) , ( n ` 1 ) >. e. _V
208 207 a1i 
 |-  ( ( ph /\ n e. A ) -> <. ( n ` 0 ) , ( n ` 1 ) >. e. _V )
209 178 206 19 208 fvmptd3 
 |-  ( ( ph /\ n e. A ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) = <. ( n ` 0 ) , ( n ` 1 ) >. )
210 209 adantlr 
 |-  ( ( ( ph /\ c e. A ) /\ n e. A ) -> ( ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ` n ) = <. ( n ` 0 ) , ( n ` 1 ) >. )
211 210 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 ) >. )
212 198 203 211 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 ) >. )
213 182 183 opth2 
 |-  ( <. ( c ` 0 ) , ( c ` 1 ) >. = <. ( n ` 0 ) , ( n ` 1 ) >. <-> ( ( c ` 0 ) = ( n ` 0 ) /\ ( c ` 1 ) = ( n ` 1 ) ) )
214 212 213 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 ) ) )
215 214 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 ) )
216 215 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 ) )
217 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 )
218 217 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 ) )
219 217 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 ) )
220 216 218 219 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 ) )
221 214 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 ) )
222 221 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 ) )
223 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 )
224 223 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 ) )
225 223 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 ) )
226 222 224 225 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 ) )
227 215 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 ) )
228 221 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 ) )
229 227 228 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 ) ) )
230 229 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 ) ) ) )
231 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 } )
232 231 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 ) )
233 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 )
234 136 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 )
235 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 )
236 139 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 ) )
237 233 234 235 236 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 )
238 fveq2 
 |-  ( j = 0 -> ( c ` j ) = ( c ` 0 ) )
239 fveq2 
 |-  ( j = 1 -> ( c ` j ) = ( c ` 1 ) )
240 fveq2 
 |-  ( j = 2 -> ( c ` j ) = ( c ` 2 ) )
241 142 nncnd 
 |-  ( ( ph /\ c e. A ) -> ( c ` 0 ) e. CC )
242 241 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 )
243 168 nncnd 
 |-  ( ( ph /\ c e. A ) -> ( c ` 1 ) e. CC )
244 243 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 )
245 36 a1i 
 |-  ( ( ph /\ c e. A ) -> 2 e. ( 0 ..^ 3 ) )
246 140 245 ffvelcdmd 
 |-  ( ( ph /\ c e. A ) -> ( c ` 2 ) e. NN )
247 246 nncnd 
 |-  ( ( ph /\ c e. A ) -> ( c ` 2 ) e. CC )
248 247 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 )
249 242 244 248 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 ) )
250 1ex 
 |-  1 e. _V
251 22 250 34 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 238 239 240 249 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 232 237 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 242 244 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 100 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 248 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 231 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 233 234 235 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 32 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 38 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 230 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 220 226 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 195 197 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 192 193 301 303 syl3anc 
 |-  ( ph -> ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) : A -1-1-onto-> ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) )
305 180 sselda 
 |-  ( ( ph /\ u e. ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ) -> u e. ( ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) X. ( 1 ... N ) ) )
306 305 124 syldan 
 |-  ( ( ph /\ u e. ran ( d e. A |-> <. ( d ` 0 ) , ( d ` 1 ) >. ) ) -> ( Lam ` ( 1st ` u ) ) e. RR )
307 305 128 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 188 12 304 209 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 75 recnd 
 |-  ( ph -> sum_ j e. ( 1 ... N ) ( Lam ` j ) e. CC )
312 69 recnd 
 |-  ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> ( Lam ` i ) e. CC )
313 54 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 48 a1i 
 |-  ( ( ph /\ i e. ( ( ( 1 ... N ) \ Prime ) u. { 2 } ) ) -> ( 1 ... N ) e. Fin )
315 74 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 69 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 54 71 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 181 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 46 76 44 116 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 42 47 77 113 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 ) ) ) )