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