This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
hgt750lemf.p ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
hgt750lemf.q ⊢ ( 𝜑 → 𝑄 ∈ ℝ )
hgt750lemf.h ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 0 [,) +∞ ) )
hgt750lemf.k ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ ( 0 [,) +∞ ) )
hgt750lemf.0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 0 ) ∈ ℕ )
hgt750lemf.1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 1 ) ∈ ℕ )
hgt750lemf.2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 2 ) ∈ ℕ )
hgt750lemf.3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐾 ‘ 𝑚 ) ≤ 𝑃 )
hgt750lemf.4 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) ≤ 𝑄 )
Assertion hgt750lemf ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( 𝑃 ↑ 2 ) · 𝑄 ) · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 hgt750lemf.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 hgt750lemf.p ⊢ ( 𝜑 → 𝑃 ∈ ℝ )
3 hgt750lemf.q ⊢ ( 𝜑 → 𝑄 ∈ ℝ )
4 hgt750lemf.h ⊢ ( 𝜑 → 𝐻 : ℕ ⟶ ( 0 [,) +∞ ) )
5 hgt750lemf.k ⊢ ( 𝜑 → 𝐾 : ℕ ⟶ ( 0 [,) +∞ ) )
6 hgt750lemf.0 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 0 ) ∈ ℕ )
7 hgt750lemf.1 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 1 ) ∈ ℕ )
8 hgt750lemf.2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 ‘ 2 ) ∈ ℕ )
9 hgt750lemf.3 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐾 ‘ 𝑚 ) ≤ 𝑃 )
10 hgt750lemf.4 ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( 𝐻 ‘ 𝑚 ) ≤ 𝑄 )
11 vmaf ⊢ Λ : ℕ ⟶ ℝ
12 11 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → Λ : ℕ ⟶ ℝ )
13 12 6 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ )
14 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
15 4 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝐻 : ℕ ⟶ ( 0 [,) +∞ ) )
16 15 6 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ∈ ( 0 [,) +∞ ) )
17 14 16 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ )
18 13 17 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) ∈ ℝ )
19 12 7 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ )
20 5 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝐾 : ℕ ⟶ ( 0 [,) +∞ ) )
21 20 7 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ∈ ( 0 [,) +∞ ) )
22 14 21 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ )
23 19 22 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) ∈ ℝ )
24 12 8 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ )
25 20 8 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ∈ ( 0 [,) +∞ ) )
26 14 25 sselid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ )
27 24 26 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℝ )
28 23 27 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
29 18 28 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
30 2 resqcld ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℝ )
31 30 3 remulcld ⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) · 𝑄 ) ∈ ℝ )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝑃 ↑ 2 ) · 𝑄 ) ∈ ℝ )
33 19 24 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℝ )
34 13 33 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
35 32 34 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( 𝑃 ↑ 2 ) · 𝑄 ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ∈ ℝ )
36 13 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) ∈ ℂ )
37 33 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℂ )
38 17 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ∈ ℂ )
39 22 26 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℝ )
40 39 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ∈ ℂ )
41 36 37 38 40 mul4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) · ( ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
42 36 37 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℂ )
43 38 40 mulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℂ )
44 42 43 mulcomd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) · ( ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = ( ( ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
45 19 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) ∈ ℂ )
46 24 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ∈ ℂ )
47 22 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ∈ ℂ )
48 26 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ∈ ℂ )
49 45 46 47 48 mul4d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) = ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) )
50 49 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
51 41 44 50 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
52 17 39 remulcld ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℝ )
53 vmage0 ⊢ ( ( 𝑛 ‘ 0 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 0 ) ) )
54 6 53 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 0 ) ) )
55 vmage0 ⊢ ( ( 𝑛 ‘ 1 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 1 ) ) )
56 7 55 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 1 ) ) )
57 vmage0 ⊢ ( ( 𝑛 ‘ 2 ) ∈ ℕ → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 2 ) ) )
58 8 57 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( Λ ‘ ( 𝑛 ‘ 2 ) ) )
59 19 24 56 58 mulge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) )
60 13 33 54 59 mulge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) )
61 3 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝑄 ∈ ℝ )
62 2 2 remulcld ⊢ ( 𝜑 → ( 𝑃 · 𝑃 ) ∈ ℝ )
63 62 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝑃 · 𝑃 ) ∈ ℝ )
64 0xr ⊢ 0 ∈ ℝ*
65 64 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ∈ ℝ* )
66 pnfxr ⊢ +∞ ∈ ℝ*
67 66 a1i ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → +∞ ∈ ℝ* )
68 icogelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ∈ ( 0 [,) +∞ ) ) → 0 ≤ ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) )
69 65 67 16 68 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) )
70 icogelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ∈ ( 0 [,) +∞ ) ) → 0 ≤ ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) )
71 65 67 21 70 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) )
72 icogelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ∈ ( 0 [,) +∞ ) ) → 0 ≤ ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) )
73 65 67 25 72 syl3anc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) )
74 22 26 71 73 mulge0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 0 ≤ ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) )
75 fveq2 ⊢ ( 𝑚 = ( 𝑛 ‘ 0 ) → ( 𝐻 ‘ 𝑚 ) = ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) )
76 75 breq1d ⊢ ( 𝑚 = ( 𝑛 ‘ 0 ) → ( ( 𝐻 ‘ 𝑚 ) ≤ 𝑄 ↔ ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ≤ 𝑄 ) )
77 10 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( 𝐻 ‘ 𝑚 ) ≤ 𝑄 )
78 77 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ∀ 𝑚 ∈ ℕ ( 𝐻 ‘ 𝑚 ) ≤ 𝑄 )
79 76 78 6 rspcdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ≤ 𝑄 )
80 2 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝑃 ∈ ℝ )
81 fveq2 ⊢ ( 𝑚 = ( 𝑛 ‘ 1 ) → ( 𝐾 ‘ 𝑚 ) = ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) )
82 81 breq1d ⊢ ( 𝑚 = ( 𝑛 ‘ 1 ) → ( ( 𝐾 ‘ 𝑚 ) ≤ 𝑃 ↔ ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ≤ 𝑃 ) )
83 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑚 ∈ ℕ ( 𝐾 ‘ 𝑚 ) ≤ 𝑃 )
84 83 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ∀ 𝑚 ∈ ℕ ( 𝐾 ‘ 𝑚 ) ≤ 𝑃 )
85 82 84 7 rspcdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ≤ 𝑃 )
86 fveq2 ⊢ ( 𝑚 = ( 𝑛 ‘ 2 ) → ( 𝐾 ‘ 𝑚 ) = ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) )
87 86 breq1d ⊢ ( 𝑚 = ( 𝑛 ‘ 2 ) → ( ( 𝐾 ‘ 𝑚 ) ≤ 𝑃 ↔ ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ≤ 𝑃 ) )
88 87 84 8 rspcdva ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ≤ 𝑃 )
89 22 80 26 80 71 73 85 88 lemul12ad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ≤ ( 𝑃 · 𝑃 ) )
90 17 61 39 63 69 74 79 89 lemul12ad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( 𝑄 · ( 𝑃 · 𝑃 ) ) )
91 30 recnd ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℂ )
92 3 recnd ⊢ ( 𝜑 → 𝑄 ∈ ℂ )
93 91 92 mulcomd ⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) · 𝑄 ) = ( 𝑄 · ( 𝑃 ↑ 2 ) ) )
94 2 recnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
95 94 sqvald ⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) = ( 𝑃 · 𝑃 ) )
96 95 oveq2d ⊢ ( 𝜑 → ( 𝑄 · ( 𝑃 ↑ 2 ) ) = ( 𝑄 · ( 𝑃 · 𝑃 ) ) )
97 93 96 eqtrd ⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) · 𝑄 ) = ( 𝑄 · ( 𝑃 · 𝑃 ) ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝑃 ↑ 2 ) · 𝑄 ) = ( 𝑄 · ( 𝑃 · 𝑃 ) ) )
99 90 98 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ≤ ( ( 𝑃 ↑ 2 ) · 𝑄 ) )
100 52 32 34 60 99 lemul1ad ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) · ( ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( 𝑃 ↑ 2 ) · 𝑄 ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
101 51 100 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( 𝑃 ↑ 2 ) · 𝑄 ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
102 1 29 35 101 fsumle ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ Σ 𝑛 ∈ 𝐴 ( ( ( 𝑃 ↑ 2 ) · 𝑄 ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
103 31 recnd ⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) · 𝑄 ) ∈ ℂ )
104 34 recnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ∈ ℂ )
105 1 103 104 fsummulc2 ⊢ ( 𝜑 → ( ( ( 𝑃 ↑ 2 ) · 𝑄 ) · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) = Σ 𝑛 ∈ 𝐴 ( ( ( 𝑃 ↑ 2 ) · 𝑄 ) · ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )
106 102 105 breqtrrd ⊢ ( 𝜑 → Σ 𝑛 ∈ 𝐴 ( ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) · ( ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) · ( ( Λ ‘ ( 𝑛 ‘ 2 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 2 ) ) ) ) ) ≤ ( ( ( 𝑃 ↑ 2 ) · 𝑄 ) · Σ 𝑛 ∈ 𝐴 ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( Λ ‘ ( 𝑛 ‘ 2 ) ) ) ) ) )