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 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 ) ) ) )