Metamath Proof Explorer

Theorem hgt750lemf

Description: Lemma for the statement 7.50 of Helfgott p. 69. (Contributed by Thierry Arnoux, 1-Jan-2022)

Ref Expression
Hypotheses hgt750lemf.a 
|- ( ph -> A e. Fin )
hgt750lemf.p 
|- ( ph -> P e. RR )
hgt750lemf.q 
|- ( ph -> Q e. RR )
hgt750lemf.h 
|- ( ph -> H : NN --> ( 0 [,) +oo ) )
hgt750lemf.k 
|- ( ph -> K : NN --> ( 0 [,) +oo ) )
hgt750lemf.0 
|- ( ( ph /\ n e. A ) -> ( n ` 0 ) e. NN )
hgt750lemf.1 
|- ( ( ph /\ n e. A ) -> ( n ` 1 ) e. NN )
hgt750lemf.2 
|- ( ( ph /\ n e. A ) -> ( n ` 2 ) e. NN )
hgt750lemf.3 
|- ( ( ph /\ m e. NN ) -> ( K ` m ) <_ P )
hgt750lemf.4 
|- ( ( ph /\ m e. NN ) -> ( H ` m ) <_ Q )
Assertion hgt750lemf 
|- ( ph -> sum_ n e. A ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) <_ ( ( ( P ^ 2 ) x. Q ) x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hgt750lemf.a 
 |-  ( ph -> A e. Fin )
2 hgt750lemf.p 
 |-  ( ph -> P e. RR )
3 hgt750lemf.q 
 |-  ( ph -> Q e. RR )
4 hgt750lemf.h 
 |-  ( ph -> H : NN --> ( 0 [,) +oo ) )
5 hgt750lemf.k 
 |-  ( ph -> K : NN --> ( 0 [,) +oo ) )
6 hgt750lemf.0 
 |-  ( ( ph /\ n e. A ) -> ( n ` 0 ) e. NN )
7 hgt750lemf.1 
 |-  ( ( ph /\ n e. A ) -> ( n ` 1 ) e. NN )
8 hgt750lemf.2 
 |-  ( ( ph /\ n e. A ) -> ( n ` 2 ) e. NN )
9 hgt750lemf.3 
 |-  ( ( ph /\ m e. NN ) -> ( K ` m ) <_ P )
10 hgt750lemf.4 
 |-  ( ( ph /\ m e. NN ) -> ( H ` m ) <_ Q )
11 vmaf 
 |-  Lam : NN --> RR
12 11 a1i 
 |-  ( ( ph /\ n e. A ) -> Lam : NN --> RR )
13 12 6 ffvelrnd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 0 ) ) e. RR )
14 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
15 4 adantr 
 |-  ( ( ph /\ n e. A ) -> H : NN --> ( 0 [,) +oo ) )
16 15 6 ffvelrnd 
 |-  ( ( ph /\ n e. A ) -> ( H ` ( n ` 0 ) ) e. ( 0 [,) +oo ) )
17 14 16 sselid 
 |-  ( ( ph /\ n e. A ) -> ( H ` ( n ` 0 ) ) e. RR )
18 13 17 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) e. RR )
19 12 7 ffvelrnd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 1 ) ) e. RR )
20 5 adantr 
 |-  ( ( ph /\ n e. A ) -> K : NN --> ( 0 [,) +oo ) )
21 20 7 ffvelrnd 
 |-  ( ( ph /\ n e. A ) -> ( K ` ( n ` 1 ) ) e. ( 0 [,) +oo ) )
22 14 21 sselid 
 |-  ( ( ph /\ n e. A ) -> ( K ` ( n ` 1 ) ) e. RR )
23 19 22 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) e. RR )
24 12 8 ffvelrnd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 2 ) ) e. RR )
25 20 8 ffvelrnd 
 |-  ( ( ph /\ n e. A ) -> ( K ` ( n ` 2 ) ) e. ( 0 [,) +oo ) )
26 14 25 sselid 
 |-  ( ( ph /\ n e. A ) -> ( K ` ( n ` 2 ) ) e. RR )
27 24 26 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) e. RR )
28 23 27 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) e. RR )
29 18 28 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) e. RR )
30 2 resqcld 
 |-  ( ph -> ( P ^ 2 ) e. RR )
31 30 3 remulcld 
 |-  ( ph -> ( ( P ^ 2 ) x. Q ) e. RR )
32 31 adantr 
 |-  ( ( ph /\ n e. A ) -> ( ( P ^ 2 ) x. Q ) e. RR )
33 19 24 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) e. RR )
34 13 33 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. RR )
35 32 34 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( ( P ^ 2 ) x. Q ) x. ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) e. RR )
36 13 recnd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 0 ) ) e. CC )
37 33 recnd 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) e. CC )
38 17 recnd 
 |-  ( ( ph /\ n e. A ) -> ( H ` ( n ` 0 ) ) e. CC )
39 22 26 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) e. RR )
40 39 recnd 
 |-  ( ( ph /\ n e. A ) -> ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) e. CC )
41 36 37 38 40 mul4d 
 |-  ( ( ph /\ n e. A ) -> ( ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) x. ( ( H ` ( n ` 0 ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) = ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) )
42 36 37 mulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. CC )
43 38 40 mulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( H ` ( n ` 0 ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) e. CC )
44 42 43 mulcomd 
 |-  ( ( ph /\ n e. A ) -> ( ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) x. ( ( H ` ( n ` 0 ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) = ( ( ( H ` ( n ` 0 ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) x. ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )
45 19 recnd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 1 ) ) e. CC )
46 24 recnd 
 |-  ( ( ph /\ n e. A ) -> ( Lam ` ( n ` 2 ) ) e. CC )
47 22 recnd 
 |-  ( ( ph /\ n e. A ) -> ( K ` ( n ` 1 ) ) e. CC )
48 26 recnd 
 |-  ( ( ph /\ n e. A ) -> ( K ` ( n ` 2 ) ) e. CC )
49 45 46 47 48 mul4d 
 |-  ( ( ph /\ n e. A ) -> ( ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) = ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) )
50 49 oveq2d 
 |-  ( ( ph /\ n e. A ) -> ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) = ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) )
51 41 44 50 3eqtr3d 
 |-  ( ( ph /\ n e. A ) -> ( ( ( H ` ( n ` 0 ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) x. ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) = ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) )
52 17 39 remulcld 
 |-  ( ( ph /\ n e. A ) -> ( ( H ` ( n ` 0 ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) e. RR )
53 vmage0 
 |-  ( ( n ` 0 ) e. NN -> 0 <_ ( Lam ` ( n ` 0 ) ) )
54 6 53 syl 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( Lam ` ( n ` 0 ) ) )
55 vmage0 
 |-  ( ( n ` 1 ) e. NN -> 0 <_ ( Lam ` ( n ` 1 ) ) )
56 7 55 syl 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( Lam ` ( n ` 1 ) ) )
57 vmage0 
 |-  ( ( n ` 2 ) e. NN -> 0 <_ ( Lam ` ( n ` 2 ) ) )
58 8 57 syl 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( Lam ` ( n ` 2 ) ) )
59 19 24 56 58 mulge0d 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) )
60 13 33 54 59 mulge0d 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) )
61 3 adantr 
 |-  ( ( ph /\ n e. A ) -> Q e. RR )
62 2 2 remulcld 
 |-  ( ph -> ( P x. P ) e. RR )
63 62 adantr 
 |-  ( ( ph /\ n e. A ) -> ( P x. P ) e. RR )
64 0xr 
 |-  0 e. RR*
65 64 a1i 
 |-  ( ( ph /\ n e. A ) -> 0 e. RR* )
66 pnfxr 
 |-  +oo e. RR*
67 66 a1i 
 |-  ( ( ph /\ n e. A ) -> +oo e. RR* )
68 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( H ` ( n ` 0 ) ) e. ( 0 [,) +oo ) ) -> 0 <_ ( H ` ( n ` 0 ) ) )
69 65 67 16 68 syl3anc 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( H ` ( n ` 0 ) ) )
70 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( K ` ( n ` 1 ) ) e. ( 0 [,) +oo ) ) -> 0 <_ ( K ` ( n ` 1 ) ) )
71 65 67 21 70 syl3anc 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( K ` ( n ` 1 ) ) )
72 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ ( K ` ( n ` 2 ) ) e. ( 0 [,) +oo ) ) -> 0 <_ ( K ` ( n ` 2 ) ) )
73 65 67 25 72 syl3anc 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( K ` ( n ` 2 ) ) )
74 22 26 71 73 mulge0d 
 |-  ( ( ph /\ n e. A ) -> 0 <_ ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) )
75 fveq2 
 |-  ( m = ( n ` 0 ) -> ( H ` m ) = ( H ` ( n ` 0 ) ) )
76 75 breq1d 
 |-  ( m = ( n ` 0 ) -> ( ( H ` m ) <_ Q <-> ( H ` ( n ` 0 ) ) <_ Q ) )
77 10 ralrimiva 
 |-  ( ph -> A. m e. NN ( H ` m ) <_ Q )
78 77 adantr 
 |-  ( ( ph /\ n e. A ) -> A. m e. NN ( H ` m ) <_ Q )
79 76 78 6 rspcdva 
 |-  ( ( ph /\ n e. A ) -> ( H ` ( n ` 0 ) ) <_ Q )
80 2 adantr 
 |-  ( ( ph /\ n e. A ) -> P e. RR )
81 fveq2 
 |-  ( m = ( n ` 1 ) -> ( K ` m ) = ( K ` ( n ` 1 ) ) )
82 81 breq1d 
 |-  ( m = ( n ` 1 ) -> ( ( K ` m ) <_ P <-> ( K ` ( n ` 1 ) ) <_ P ) )
83 9 ralrimiva 
 |-  ( ph -> A. m e. NN ( K ` m ) <_ P )
84 83 adantr 
 |-  ( ( ph /\ n e. A ) -> A. m e. NN ( K ` m ) <_ P )
85 82 84 7 rspcdva 
 |-  ( ( ph /\ n e. A ) -> ( K ` ( n ` 1 ) ) <_ P )
86 fveq2 
 |-  ( m = ( n ` 2 ) -> ( K ` m ) = ( K ` ( n ` 2 ) ) )
87 86 breq1d 
 |-  ( m = ( n ` 2 ) -> ( ( K ` m ) <_ P <-> ( K ` ( n ` 2 ) ) <_ P ) )
88 87 84 8 rspcdva 
 |-  ( ( ph /\ n e. A ) -> ( K ` ( n ` 2 ) ) <_ P )
89 22 80 26 80 71 73 85 88 lemul12ad 
 |-  ( ( ph /\ n e. A ) -> ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) <_ ( P x. P ) )
90 17 61 39 63 69 74 79 89 lemul12ad 
 |-  ( ( ph /\ n e. A ) -> ( ( H ` ( n ` 0 ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) <_ ( Q x. ( P x. P ) ) )
91 30 recnd 
 |-  ( ph -> ( P ^ 2 ) e. CC )
92 3 recnd 
 |-  ( ph -> Q e. CC )
93 91 92 mulcomd 
 |-  ( ph -> ( ( P ^ 2 ) x. Q ) = ( Q x. ( P ^ 2 ) ) )
94 2 recnd 
 |-  ( ph -> P e. CC )
95 94 sqvald 
 |-  ( ph -> ( P ^ 2 ) = ( P x. P ) )
96 95 oveq2d 
 |-  ( ph -> ( Q x. ( P ^ 2 ) ) = ( Q x. ( P x. P ) ) )
97 93 96 eqtrd 
 |-  ( ph -> ( ( P ^ 2 ) x. Q ) = ( Q x. ( P x. P ) ) )
98 97 adantr 
 |-  ( ( ph /\ n e. A ) -> ( ( P ^ 2 ) x. Q ) = ( Q x. ( P x. P ) ) )
99 90 98 breqtrrd 
 |-  ( ( ph /\ n e. A ) -> ( ( H ` ( n ` 0 ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) <_ ( ( P ^ 2 ) x. Q ) )
100 52 32 34 60 99 lemul1ad 
 |-  ( ( ph /\ n e. A ) -> ( ( ( H ` ( n ` 0 ) ) x. ( ( K ` ( n ` 1 ) ) x. ( K ` ( n ` 2 ) ) ) ) x. ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) <_ ( ( ( P ^ 2 ) x. Q ) x. ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )
101 51 100 eqbrtrrd 
 |-  ( ( ph /\ n e. A ) -> ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) <_ ( ( ( P ^ 2 ) x. Q ) x. ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )
102 1 29 35 101 fsumle 
 |-  ( ph -> sum_ n e. A ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) <_ sum_ n e. A ( ( ( P ^ 2 ) x. Q ) x. ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )
103 31 recnd 
 |-  ( ph -> ( ( P ^ 2 ) x. Q ) e. CC )
104 34 recnd 
 |-  ( ( ph /\ n e. A ) -> ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) e. CC )
105 1 103 104 fsummulc2 
 |-  ( ph -> ( ( ( P ^ 2 ) x. Q ) x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) = sum_ n e. A ( ( ( P ^ 2 ) x. Q ) x. ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )
106 102 105 breqtrrd 
 |-  ( ph -> sum_ n e. A ( ( ( Lam ` ( n ` 0 ) ) x. ( H ` ( n ` 0 ) ) ) x. ( ( ( Lam ` ( n ` 1 ) ) x. ( K ` ( n ` 1 ) ) ) x. ( ( Lam ` ( n ` 2 ) ) x. ( K ` ( n ` 2 ) ) ) ) ) <_ ( ( ( P ^ 2 ) x. Q ) x. sum_ n e. A ( ( Lam ` ( n ` 0 ) ) x. ( ( Lam ` ( n ` 1 ) ) x. ( Lam ` ( n ` 2 ) ) ) ) ) )