Metamath Proof Explorer

Theorem hgt750lema

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, 1-Jan-2022)

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 ) }
hgt750lema.f 
|- F = ( d e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } |-> ( d o. if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) ) )
Assertion hgt750lema 
|- ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ ( 3 x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )

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 hgt750lema.f 
 |-  F = ( d e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } |-> ( d o. if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) ) )
6 fzofi 
 |-  ( 0 ..^ 3 ) e. Fin
7 6 a1i 
 |-  ( ph -> ( 0 ..^ 3 ) e. Fin )
8 2 nnnn0d 
 |-  ( ph -> N e. NN0 )
9 3nn0 
 |-  3 e. NN0
10 9 a1i 
 |-  ( ph -> 3 e. NN0 )
11 ssidd 
 |-  ( ph -> NN C_ NN )
12 8 10 11 reprfi2 
 |-  ( ph -> ( NN ( repr ` 3 ) N ) e. Fin )
13 ssrab2 
 |-  { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N )
14 13 a1i 
 |-  ( ph -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N ) )
15 12 14 ssfid 
 |-  ( ph -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } e. Fin )
16 15 adantr 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } e. Fin )
17 vmaf 
 |-  Lam : NN --> RR
18 17 a1i 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> Lam : NN --> RR )
19 ssidd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> NN C_ NN )
20 8 nn0zd 
 |-  ( ph -> N e. ZZ )
21 20 ad2antrr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> N e. ZZ )
22 9 a1i 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 3 e. NN0 )
23 simpr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } )
24 13 23 sselid 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> n e. ( NN ( repr ` 3 ) N ) )
25 19 21 22 24 reprf 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> n : ( 0 ..^ 3 ) --> NN )
26 c0ex 
 |-  0 e. _V
27 26 tpid1 
 |-  0 e. { 0 , 1 , 2 }
28 fzo0to3tp 
 |-  ( 0 ..^ 3 ) = { 0 , 1 , 2 }
29 27 28 eleqtrri 
 |-  0 e. ( 0 ..^ 3 )
30 29 a1i 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 e. ( 0 ..^ 3 ) )
31 25 30 ffvelcdmd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( n ` 0 ) e. NN )
32 18 31 ffvelcdmd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 0 ) ) e. RR )
33 1eltp012 
 |-  1 e. { 0 , 1 , 2 }
34 33 28 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
35 34 a1i 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 1 e. ( 0 ..^ 3 ) )
36 25 35 ffvelcdmd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( n ` 1 ) e. NN )
37 18 36 ffvelcdmd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 1 ) ) e. RR )
38 2ex 
 |-  2 e. _V
39 38 tpid3 
 |-  2 e. { 0 , 1 , 2 }
40 39 28 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
41 40 a1i 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 2 e. ( 0 ..^ 3 ) )
42 25 41 ffvelcdmd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( n ` 2 ) e. NN )
43 18 42 ffvelcdmd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 2 ) ) e. RR )
44 37 43 remulcld 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) e. RR )
45 32 44 remulcld 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
46 vmage0 
 |-  ( ( n ` 0 ) e. NN -> 0 <_ ( Lam ` ( n ` 0 ) ) )
47 31 46 syl 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 <_ ( Lam ` ( n ` 0 ) ) )
48 vmage0 
 |-  ( ( n ` 1 ) e. NN -> 0 <_ ( Lam ` ( n ` 1 ) ) )
49 36 48 syl 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 <_ ( Lam ` ( n ` 1 ) ) )
50 vmage0 
 |-  ( ( n ` 2 ) e. NN -> 0 <_ ( Lam ` ( n ` 2 ) ) )
51 42 50 syl 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 <_ ( Lam ` ( n ` 2 ) ) )
52 37 43 49 51 mulge0d 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 <_ ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) )
53 32 44 47 52 mulge0d 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> 0 <_ ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
54 7 16 45 53 fsumiunle 
 |-  ( ph -> sum_ n e. U_ a e. ( 0 ..^ 3 ) { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
55 eqid 
 |-  { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } = { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) }
56 inss2 
 |-  ( O i^i Prime ) C_ Prime
57 prmssnn 
 |-  Prime C_ NN
58 56 57 sstri 
 |-  ( O i^i Prime ) C_ NN
59 58 a1i 
 |-  ( ph -> ( O i^i Prime ) C_ NN )
60 55 11 59 8 10 reprdifc 
 |-  ( ph -> ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) = U_ a e. ( 0 ..^ 3 ) { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } )
61 60 sumeq1d 
 |-  ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = sum_ n e. U_ a e. ( 0 ..^ 3 ) { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
62 ssrab2 
 |-  { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N )
63 62 a1i 
 |-  ( ph -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N ) )
64 12 63 ssfid 
 |-  ( ph -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } e. Fin )
65 17 a1i 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> Lam : NN --> RR )
66 ssidd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> NN C_ NN )
67 20 adantr 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> N e. ZZ )
68 9 a1i 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 3 e. NN0 )
69 63 sselda 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> n e. ( NN ( repr ` 3 ) N ) )
70 66 67 68 69 reprf 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> n : ( 0 ..^ 3 ) --> NN )
71 29 a1i 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 0 e. ( 0 ..^ 3 ) )
72 70 71 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 0 ) e. NN )
73 65 72 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 0 ) ) e. RR )
74 34 a1i 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 1 e. ( 0 ..^ 3 ) )
75 70 74 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 1 ) e. NN )
76 65 75 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 1 ) ) e. RR )
77 40 a1i 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 2 e. ( 0 ..^ 3 ) )
78 70 77 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 2 ) e. NN )
79 65 78 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 2 ) ) e. RR )
80 76 79 remulcld 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) e. RR )
81 73 80 remulcld 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
82 64 81 fsumrecl 
 |-  ( ph -> sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
83 82 recnd 
 |-  ( ph -> sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. CC )
84 fsumconst 
 |-  ( ( ( 0 ..^ 3 ) e. Fin /\ sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. CC ) -> sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = ( ( # ` ( 0 ..^ 3 ) ) x. sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )
85 7 83 84 syl2anc 
 |-  ( ph -> sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = ( ( # ` ( 0 ..^ 3 ) ) x. sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )
86 fveq1 
 |-  ( n = ( F ` e ) -> ( n ` 0 ) = ( ( F ` e ) ` 0 ) )
87 86 fveq2d 
 |-  ( n = ( F ` e ) -> ( Lam ` ( n ` 0 ) ) = ( Lam ` ( ( F ` e ) ` 0 ) ) )
88 fveq1 
 |-  ( n = ( F ` e ) -> ( n ` 1 ) = ( ( F ` e ) ` 1 ) )
89 88 fveq2d 
 |-  ( n = ( F ` e ) -> ( Lam ` ( n ` 1 ) ) = ( Lam ` ( ( F ` e ) ` 1 ) ) )
90 fveq1 
 |-  ( n = ( F ` e ) -> ( n ` 2 ) = ( ( F ` e ) ` 2 ) )
91 90 fveq2d 
 |-  ( n = ( F ` e ) -> ( Lam ` ( n ` 2 ) ) = ( Lam ` ( ( F ` e ) ` 2 ) ) )
92 89 91 oveq12d 
 |-  ( n = ( F ` e ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) = ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) )
93 87 92 oveq12d 
 |-  ( n = ( F ` e ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = ( ( Lam ` ( ( F ` e ) ` 0 ) ) x. ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) )
94 3nn 
 |-  3 e. NN
95 94 a1i 
 |-  ( ph -> 3 e. NN )
96 95 ralrimivw 
 |-  ( ph -> A. a e. ( 0 ..^ 3 ) 3 e. NN )
97 96 r19.21bi 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> 3 e. NN )
98 20 adantr 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> N e. ZZ )
99 ssidd 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> NN C_ NN )
100 simpr 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> a e. ( 0 ..^ 3 ) )
101 fveq1 
 |-  ( c = d -> ( c ` 0 ) = ( d ` 0 ) )
102 101 eleq1d 
 |-  ( c = d -> ( ( c ` 0 ) e. ( O i^i Prime ) <-> ( d ` 0 ) e. ( O i^i Prime ) ) )
103 102 notbid 
 |-  ( c = d -> ( -. ( c ` 0 ) e. ( O i^i Prime ) <-> -. ( d ` 0 ) e. ( O i^i Prime ) ) )
104 103 cbvrabv 
 |-  { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } = { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` 0 ) e. ( O i^i Prime ) }
105 fveq1 
 |-  ( c = d -> ( c ` a ) = ( d ` a ) )
106 105 eleq1d 
 |-  ( c = d -> ( ( c ` a ) e. ( O i^i Prime ) <-> ( d ` a ) e. ( O i^i Prime ) ) )
107 106 notbid 
 |-  ( c = d -> ( -. ( c ` a ) e. ( O i^i Prime ) <-> -. ( d ` a ) e. ( O i^i Prime ) ) )
108 107 cbvrabv 
 |-  { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } = { d e. ( NN ( repr ` 3 ) N ) | -. ( d ` a ) e. ( O i^i Prime ) }
109 eqid 
 |-  if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) = if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) )
110 97 98 99 100 104 108 109 5 reprpmtf1o 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> F : { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } -1-1-onto-> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } )
111 eqidd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ e e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( F ` e ) = ( F ` e ) )
112 81 adantlr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
113 112 recnd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. CC )
114 93 16 110 111 113 fsumf1o 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = sum_ e e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` e ) ` 0 ) ) x. ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) )
115 fveq2 
 |-  ( e = n -> ( F ` e ) = ( F ` n ) )
116 115 fveq1d 
 |-  ( e = n -> ( ( F ` e ) ` 0 ) = ( ( F ` n ) ` 0 ) )
117 116 fveq2d 
 |-  ( e = n -> ( Lam ` ( ( F ` e ) ` 0 ) ) = ( Lam ` ( ( F ` n ) ` 0 ) ) )
118 115 fveq1d 
 |-  ( e = n -> ( ( F ` e ) ` 1 ) = ( ( F ` n ) ` 1 ) )
119 118 fveq2d 
 |-  ( e = n -> ( Lam ` ( ( F ` e ) ` 1 ) ) = ( Lam ` ( ( F ` n ) ` 1 ) ) )
120 115 fveq1d 
 |-  ( e = n -> ( ( F ` e ) ` 2 ) = ( ( F ` n ) ` 2 ) )
121 120 fveq2d 
 |-  ( e = n -> ( Lam ` ( ( F ` e ) ` 2 ) ) = ( Lam ` ( ( F ` n ) ` 2 ) ) )
122 119 121 oveq12d 
 |-  ( e = n -> ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) = ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) )
123 117 122 oveq12d 
 |-  ( e = n -> ( ( Lam ` ( ( F ` e ) ` 0 ) ) x. ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) = ( ( Lam ` ( ( F ` n ) ` 0 ) ) x. ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) ) )
124 123 cbvsumv 
 |-  sum_ e e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` e ) ` 0 ) ) x. ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) = sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` n ) ` 0 ) ) x. ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) )
125 124 a1i 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> sum_ e e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` e ) ` 0 ) ) x. ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) ) = sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` n ) ` 0 ) ) x. ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) ) )
126 ovexd 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( 0 ..^ 3 ) e. _V )
127 100 adantr 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> a e. ( 0 ..^ 3 ) )
128 126 127 30 109 pmtridf1o 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) : ( 0 ..^ 3 ) -1-1-onto-> ( 0 ..^ 3 ) )
129 5 128 25 18 23 hgt750lemg 
 |-  ( ( ( ph /\ a e. ( 0 ..^ 3 ) ) /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ) -> ( ( Lam ` ( ( F ` n ) ` 0 ) ) x. ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) ) = ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
130 129 sumeq2dv 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( ( F ` n ) ` 0 ) ) x. ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) ) = sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
131 114 125 130 3eqtrrd 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
132 131 sumeq2dv 
 |-  ( ph -> sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
133 hashfzo0 
 |-  ( 3 e. NN0 -> ( # ` ( 0 ..^ 3 ) ) = 3 )
134 9 133 ax-mp 
 |-  ( # ` ( 0 ..^ 3 ) ) = 3
135 134 a1i 
 |-  ( ph -> ( # ` ( 0 ..^ 3 ) ) = 3 )
136 135 eqcomd 
 |-  ( ph -> 3 = ( # ` ( 0 ..^ 3 ) ) )
137 4 a1i 
 |-  ( ph -> A = { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } )
138 137 sumeq1d 
 |-  ( ph -> sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) = sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
139 136 138 oveq12d 
 |-  ( ph -> ( 3 x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) = ( ( # ` ( 0 ..^ 3 ) ) x. sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )
140 85 132 139 3eqtr4rd 
 |-  ( ph -> ( 3 x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) = sum_ a e. ( 0 ..^ 3 ) sum_ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` a ) e. ( O i^i Prime ) } ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
141 54 61 140 3brtr4d 
 |-  ( ph -> sum_ n e. ( ( NN ( repr ` 3 ) N ) \ ( ( O i^i Prime ) ( repr ` 3 ) N ) ) ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) <_ ( 3 x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )