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 1ex 
 |-  1 e. _V
34 33 tpid2 
 |-  1 e. { 0 , 1 , 2 }
35 34 28 eleqtrri 
 |-  1 e. ( 0 ..^ 3 )
36 35 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 ) )
37 25 36 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 )
38 18 37 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 )
39 2ex 
 |-  2 e. _V
40 39 tpid3 
 |-  2 e. { 0 , 1 , 2 }
41 40 28 eleqtrri 
 |-  2 e. ( 0 ..^ 3 )
42 41 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 ) )
43 25 42 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 )
44 18 43 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 )
45 38 44 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 )
46 32 45 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 )
47 vmage0 
 |-  ( ( n ` 0 ) e. NN -> 0 <_ ( Lam ` ( n ` 0 ) ) )
48 31 47 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 ) ) )
49 vmage0 
 |-  ( ( n ` 1 ) e. NN -> 0 <_ ( Lam ` ( n ` 1 ) ) )
50 37 49 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 ) ) )
51 vmage0 
 |-  ( ( n ` 2 ) e. NN -> 0 <_ ( Lam ` ( n ` 2 ) ) )
52 43 51 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 ) ) )
53 38 44 50 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 ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) )
54 32 45 48 53 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 ) ) ) ) )
55 7 16 46 54 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 ) ) ) ) )
56 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 ) }
57 inss2 
 |-  ( O i^i Prime ) C_ Prime
58 prmssnn 
 |-  Prime C_ NN
59 57 58 sstri 
 |-  ( O i^i Prime ) C_ NN
60 59 a1i 
 |-  ( ph -> ( O i^i Prime ) C_ NN )
61 56 11 60 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 ) } )
62 61 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 ) ) ) ) )
63 ssrab2 
 |-  { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N )
64 63 a1i 
 |-  ( ph -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } C_ ( NN ( repr ` 3 ) N ) )
65 12 64 ssfid 
 |-  ( ph -> { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } e. Fin )
66 17 a1i 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> Lam : NN --> RR )
67 ssidd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> NN C_ NN )
68 20 adantr 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> N e. ZZ )
69 9 a1i 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 3 e. NN0 )
70 64 sselda 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> n e. ( NN ( repr ` 3 ) N ) )
71 67 68 69 70 reprf 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> n : ( 0 ..^ 3 ) --> NN )
72 29 a1i 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 0 e. ( 0 ..^ 3 ) )
73 71 72 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 0 ) e. NN )
74 66 73 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 0 ) ) e. RR )
75 35 a1i 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 1 e. ( 0 ..^ 3 ) )
76 71 75 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 1 ) e. NN )
77 66 76 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 1 ) ) e. RR )
78 41 a1i 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> 2 e. ( 0 ..^ 3 ) )
79 71 78 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( n ` 2 ) e. NN )
80 66 79 ffvelcdmd 
 |-  ( ( ph /\ n e. { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } ) -> ( Lam ` ( n ` 2 ) ) e. RR )
81 77 80 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 )
82 74 81 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 )
83 65 82 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 )
84 83 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 )
85 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 ) ) ) ) ) )
86 7 84 85 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 ) ) ) ) ) )
87 fveq1 
 |-  ( n = ( F ` e ) -> ( n ` 0 ) = ( ( F ` e ) ` 0 ) )
88 87 fveq2d 
 |-  ( n = ( F ` e ) -> ( Lam ` ( n ` 0 ) ) = ( Lam ` ( ( F ` e ) ` 0 ) ) )
89 fveq1 
 |-  ( n = ( F ` e ) -> ( n ` 1 ) = ( ( F ` e ) ` 1 ) )
90 89 fveq2d 
 |-  ( n = ( F ` e ) -> ( Lam ` ( n ` 1 ) ) = ( Lam ` ( ( F ` e ) ` 1 ) ) )
91 fveq1 
 |-  ( n = ( F ` e ) -> ( n ` 2 ) = ( ( F ` e ) ` 2 ) )
92 91 fveq2d 
 |-  ( n = ( F ` e ) -> ( Lam ` ( n ` 2 ) ) = ( Lam ` ( ( F ` e ) ` 2 ) ) )
93 90 92 oveq12d 
 |-  ( n = ( F ` e ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) = ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) )
94 88 93 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 ) ) ) ) )
95 3nn 
 |-  3 e. NN
96 95 a1i 
 |-  ( ph -> 3 e. NN )
97 96 ralrimivw 
 |-  ( ph -> A. a e. ( 0 ..^ 3 ) 3 e. NN )
98 97 r19.21bi 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> 3 e. NN )
99 20 adantr 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> N e. ZZ )
100 ssidd 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> NN C_ NN )
101 simpr 
 |-  ( ( ph /\ a e. ( 0 ..^ 3 ) ) -> a e. ( 0 ..^ 3 ) )
102 fveq1 
 |-  ( c = d -> ( c ` 0 ) = ( d ` 0 ) )
103 102 eleq1d 
 |-  ( c = d -> ( ( c ` 0 ) e. ( O i^i Prime ) <-> ( d ` 0 ) e. ( O i^i Prime ) ) )
104 103 notbid 
 |-  ( c = d -> ( -. ( c ` 0 ) e. ( O i^i Prime ) <-> -. ( d ` 0 ) e. ( O i^i Prime ) ) )
105 104 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 ) }
106 fveq1 
 |-  ( c = d -> ( c ` a ) = ( d ` a ) )
107 106 eleq1d 
 |-  ( c = d -> ( ( c ` a ) e. ( O i^i Prime ) <-> ( d ` a ) e. ( O i^i Prime ) ) )
108 107 notbid 
 |-  ( c = d -> ( -. ( c ` a ) e. ( O i^i Prime ) <-> -. ( d ` a ) e. ( O i^i Prime ) ) )
109 108 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 ) }
110 eqid 
 |-  if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) ) = if ( a = 0 , ( _I |` ( 0 ..^ 3 ) ) , ( ( pmTrsp ` ( 0 ..^ 3 ) ) ` { a , 0 } ) )
111 98 99 100 101 105 109 110 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 ) } )
112 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 ) )
113 82 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 )
114 113 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 )
115 94 16 111 112 114 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 ) ) ) ) )
116 fveq2 
 |-  ( e = n -> ( F ` e ) = ( F ` n ) )
117 116 fveq1d 
 |-  ( e = n -> ( ( F ` e ) ` 0 ) = ( ( F ` n ) ` 0 ) )
118 117 fveq2d 
 |-  ( e = n -> ( Lam ` ( ( F ` e ) ` 0 ) ) = ( Lam ` ( ( F ` n ) ` 0 ) ) )
119 116 fveq1d 
 |-  ( e = n -> ( ( F ` e ) ` 1 ) = ( ( F ` n ) ` 1 ) )
120 119 fveq2d 
 |-  ( e = n -> ( Lam ` ( ( F ` e ) ` 1 ) ) = ( Lam ` ( ( F ` n ) ` 1 ) ) )
121 116 fveq1d 
 |-  ( e = n -> ( ( F ` e ) ` 2 ) = ( ( F ` n ) ` 2 ) )
122 121 fveq2d 
 |-  ( e = n -> ( Lam ` ( ( F ` e ) ` 2 ) ) = ( Lam ` ( ( F ` n ) ` 2 ) ) )
123 120 122 oveq12d 
 |-  ( e = n -> ( ( Lam ` ( ( F ` e ) ` 1 ) ) x. ( Lam ` ( ( F ` e ) ` 2 ) ) ) = ( ( Lam ` ( ( F ` n ) ` 1 ) ) x. ( Lam ` ( ( F ` n ) ` 2 ) ) ) )
124 118 123 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 ) ) ) ) )
125 124 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 ) ) ) )
126 125 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 ) ) ) ) )
127 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 )
128 101 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 ) )
129 127 128 30 110 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 ) )
130 5 129 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 ) ) ) ) )
131 130 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 ) ) ) ) )
132 115 126 131 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 ) ) ) ) )
133 132 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 ) ) ) ) )
134 hashfzo0 
 |-  ( 3 e. NN0 -> ( # ` ( 0 ..^ 3 ) ) = 3 )
135 9 134 ax-mp 
 |-  ( # ` ( 0 ..^ 3 ) ) = 3
136 135 a1i 
 |-  ( ph -> ( # ` ( 0 ..^ 3 ) ) = 3 )
137 136 eqcomd 
 |-  ( ph -> 3 = ( # ` ( 0 ..^ 3 ) ) )
138 4 a1i 
 |-  ( ph -> A = { c e. ( NN ( repr ` 3 ) N ) | -. ( c ` 0 ) e. ( O i^i Prime ) } )
139 138 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 ) ) ) ) )
140 137 139 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 ) ) ) ) ) )
141 86 133 140 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 ) ) ) ) )
142 55 62 141 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 ) ) ) ) ) )