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	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ )
14		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
15	4	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝐻 : ℕ ⟶ ( 0 [,) +∞ ) )
16	15 6	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ∈ ( 0 [,) +∞ ) )
17	14 16	sselid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ∈ ℝ )
18	13 17	remulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 0 ) ) · ( 𝐻 ‘ ( 𝑛 ‘ 0 ) ) ) ∈ ℝ )
19	12 7	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ )
20	5	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → 𝐾 : ℕ ⟶ ( 0 [,) +∞ ) )
21	20 7	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ∈ ( 0 [,) +∞ ) )
22	14 21	sselid	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ∈ ℝ )
23	19 22	remulcld	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( ( Λ ‘ ( 𝑛 ‘ 1 ) ) · ( 𝐾 ‘ ( 𝑛 ‘ 1 ) ) ) ∈ ℝ )
24	12 8	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( Λ ‘ ( 𝑛 ‘ 2 ) ) ∈ ℝ )
25	20 8	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝑛 ‘ 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 ) ) ) ) ) )