hgt750lemf

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

	Ref	Expression
Hypotheses	hgt750lemf.a	$⊢ φ \to A \in Fin$
	hgt750lemf.p	$⊢ φ \to P \in ℝ$
	hgt750lemf.q	$⊢ φ \to Q \in ℝ$
	hgt750lemf.h	$⊢ φ \to H : ℕ ⟶ [0, +∞)$
	hgt750lemf.k	$⊢ φ \to K : ℕ ⟶ [0, +∞)$
	hgt750lemf.0	$⊢ (φ \land n \in A) \to n (0) \in ℕ$
	hgt750lemf.1	$⊢ (φ \land n \in A) \to n (1) \in ℕ$
	hgt750lemf.2	$⊢ (φ \land n \in A) \to n (2) \in ℕ$
	hgt750lemf.3	$⊢ (φ \land m \in ℕ) \to K (m) \leq P$
	hgt750lemf.4	$⊢ (φ \land m \in ℕ) \to H (m) \leq Q$
Assertion	hgt750lemf	$⊢ φ \to \sum_{n \in A} Λ (n (0)) H (n (0)) Λ (n (1)) K (n (1)) Λ (n (2)) K (n (2)) \leq P^{2} Q \sum_{n \in A} Λ (n (0)) Λ (n (1)) Λ (n (2))$

Proof

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

Metamath Proof Explorer

Theorem hgt750lemf

Proof