efaddlem20 - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem efaddlem20 7357

Description: Lemma for efadd 7366. Further upper bound for the summation terms on the right-hand side of efaddlem6 7343.

**Hypotheses**
Ref	Expression
efaddlem17.1	⊢ N ∈ ℕ
efaddlem17.2	⊢ A ∈ ℂ
efaddlem17.3	⊢ B ∈ ℂ
efaddlem17.4	⊢ S = (⌊ ‘((N + 1) / 2))
efaddlem17.5	⊢ T = (((⌊ ‘((abs ‘A) + 1)) · (⌊ ‘((abs ‘B) + 1)))↑2)

**Assertion**
Ref	Expression
efaddlem20	⊢ ((N↑2) · ((T↑S) / (! ‘S))) ≤ (((S↑2) · ((4 · T)↑S)) / (! ‘S))

**Proof of Theorem efaddlem20**
Step	Hyp	Ref	Expression
1		efaddlem17.1	. . . . . . 7 ⊢ N ∈ ℕ
2	1	nnsqcl 6661	. . . . . 6 ⊢ (N↑2) ∈ ℕ
3	2	nnre 5933	. . . . 5 ⊢ (N↑2) ∈ ℝ
4		2re 5981	. . . . . . 7 ⊢ 2 ∈ ℝ
5		efaddlem17.4	. . . . . . . . 9 ⊢ S = (⌊ ‘((N + 1) / 2))
6	1, 5	efaddlem8 7345	. . . . . . . 8 ⊢ S ∈ ℕ
7	6	nnre 5933	. . . . . . 7 ⊢ S ∈ ℝ
8	4, 7	remulcl 5347	. . . . . 6 ⊢ (2 · S) ∈ ℝ
9	8	resqcl 6624	. . . . 5 ⊢ ((2 · S)↑2) ∈ ℝ
10		efaddlem17.2	. . . . . . . . 9 ⊢ A ∈ ℂ
11		efaddlem17.3	. . . . . . . . 9 ⊢ B ∈ ℂ
12		efaddlem17.5	. . . . . . . . 9 ⊢ T = (((⌊ ‘((abs ‘A) + 1)) · (⌊ ‘((abs ‘B) + 1)))↑2)
13	10, 11, 12	efaddlem7 7344	. . . . . . . 8 ⊢ T ∈ ℕ
14	13	nnre 5933	. . . . . . 7 ⊢ T ∈ ℝ
15	6	nnnn0 6109	. . . . . . 7 ⊢ S ∈ ℕ₀
16		reexpclt 6581	. . . . . . 7 ⊢ ((T ∈ ℝ ⋀ S ∈ ℕ₀) → (T↑S) ∈ ℝ)
17	14, 15, 16	mp2an 699	. . . . . 6 ⊢ (T↑S) ∈ ℝ
18		facclt 6940	. . . . . . . 8 ⊢ (S ∈ ℕ₀ → (! ‘S) ∈ ℕ)
19	15, 18	ax-mp 7	. . . . . . 7 ⊢ (! ‘S) ∈ ℕ
20	19	nnre 5933	. . . . . 6 ⊢ (! ‘S) ∈ ℝ
21		facne0t 6941	. . . . . . 7 ⊢ (S ∈ ℕ₀ → (! ‘S) ≠ 0)
22	15, 21	ax-mp 7	. . . . . 6 ⊢ (! ‘S) ≠ 0
23	17, 20, 22	redivcl 5800	. . . . 5 ⊢ ((T↑S) / (! ‘S)) ∈ ℝ
24	3, 9, 23	3pm3.2i 820	. . . 4 ⊢ ((N↑2) ∈ ℝ ⋀ ((2 · S)↑2) ∈ ℝ ⋀ ((T↑S) / (! ‘S)) ∈ ℝ)
25	13	nnnn0 6109	. . . . . . . 8 ⊢ T ∈ ℕ₀
26		nn0expclt 6578	. . . . . . . 8 ⊢ ((T ∈ ℕ₀ ⋀ S ∈ ℕ₀) → (T↑S) ∈ ℕ₀)
27	25, 15, 26	mp2an 699	. . . . . . 7 ⊢ (T↑S) ∈ ℕ₀
28	27	nn0ge0 6120	. . . . . 6 ⊢ 0 ≤ (T↑S)
29	19	nngt0 5952	. . . . . 6 ⊢ 0 < (! ‘S)
30	17, 20	divge0 5860	. . . . . 6 ⊢ ((0 ≤ (T↑S) ⋀ 0 < (! ‘S)) → 0 ≤ ((T↑S) / (! ‘S)))
31	28, 29, 30	mp2an 699	. . . . 5 ⊢ 0 ≤ ((T↑S) / (! ‘S))
32	1	nnre 5933	. . . . . . 7 ⊢ N ∈ ℝ
33		0re 5452	. . . . . . . 8 ⊢ 0 ∈ ℝ
34	1	nngt0 5952	. . . . . . . 8 ⊢ 0 < N
35	33, 32, 34	ltlei 5593	. . . . . . 7 ⊢ 0 ≤ N
36	32, 35	pm3.2i 285	. . . . . 6 ⊢ (N ∈ ℝ ⋀ 0 ≤ N)
37		nnzt 6155	. . . . . . . . . 10 ⊢ (N ∈ ℕ → N ∈ ℤ)
38	1, 37	ax-mp 7	. . . . . . . . 9 ⊢ N ∈ ℤ
39		flhalft 6248	. . . . . . . . 9 ⊢ (N ∈ ℤ → N ≤ (2 · (⌊ ‘((N + 1) / 2))))
40	38, 39	ax-mp 7	. . . . . . . 8 ⊢ N ≤ (2 · (⌊ ‘((N + 1) / 2)))
41	5	opreq2i 3978	. . . . . . . 8 ⊢ (2 · S) = (2 · (⌊ ‘((N + 1) / 2)))
42	40, 41	breqtrr 2645	. . . . . . 7 ⊢ N ≤ (2 · S)
43	8, 42	pm3.2i 285	. . . . . 6 ⊢ ((2 · S) ∈ ℝ ⋀ N ≤ (2 · S))
44		le2sqit 6633	. . . . . 6 ⊢ (((N ∈ ℝ ⋀ 0 ≤ N) ⋀ ((2 · S) ∈ ℝ ⋀ N ≤ (2 · S))) → (N↑2) ≤ ((2 · S)↑2))
45	36, 43, 44	mp2an 699	. . . . 5 ⊢ (N↑2) ≤ ((2 · S)↑2)
46	31, 45	pm3.2i 285	. . . 4 ⊢ (0 ≤ ((T↑S) / (! ‘S)) ⋀ (N↑2) ≤ ((2 · S)↑2))
47		lemul1itOLD 5840	. . . 4 ⊢ ((((N↑2) ∈ ℝ ⋀ ((2 · S)↑2) ∈ ℝ ⋀ ((T↑S) / (! ‘S)) ∈ ℝ) ⋀ (0 ≤ ((T↑S) / (! ‘S)) ⋀ (N↑2) ≤ ((2 · S)↑2))) → ((N↑2) · ((T↑S) / (! ‘S))) ≤ (((2 · S)↑2) · ((T↑S) / (! ‘S))))
48	24, 46, 47	mp2an 699	. . 3 ⊢ ((N↑2) · ((T↑S) / (! ‘S))) ≤ (((2 · S)↑2) · ((T↑S) / (! ‘S)))
49	9	recn 5326	. . . 4 ⊢ ((2 · S)↑2) ∈ ℂ
50	17	recn 5326	. . . 4 ⊢ (T↑S) ∈ ℂ
51	19	nncn 5934	. . . 4 ⊢ (! ‘S) ∈ ℂ
52	49, 50, 51, 22	divass 5753	. . 3 ⊢ ((((2 · S)↑2) · (T↑S)) / (! ‘S)) = (((2 · S)↑2) · ((T↑S) / (! ‘S)))
53	48, 52	breqtrr 2645	. 2 ⊢ ((N↑2) · ((T↑S) / (! ‘S))) ≤ ((((2 · S)↑2) · (T↑S)) / (! ‘S))
54		2cn 5982	. . . . . . . 8 ⊢ 2 ∈ ℂ
55	6	nncn 5934	. . . . . . . 8 ⊢ S ∈ ℂ
56	54, 55	sqmul 6618	. . . . . . 7 ⊢ ((2 · S)↑2) = ((2↑2) · (S↑2))
57	54	sqcl 6616	. . . . . . . 8 ⊢ (2↑2) ∈ ℂ
58	6	nnsqcl 6661	. . . . . . . . 9 ⊢ (S↑2) ∈ ℕ
59	58	nncn 5934	. . . . . . . 8 ⊢ (S↑2) ∈ ℂ
60	57, 59	mulcom 5335	. . . . . . 7 ⊢ ((2↑2) · (S↑2)) = ((S↑2) · (2↑2))
61	56, 60	eqtr 1498	. . . . . 6 ⊢ ((2 · S)↑2) = ((S↑2) · (2↑2))
62	61	opreq1i 3977	. . . . 5 ⊢ (((2 · S)↑2) · (T↑S)) = (((S↑2) · (2↑2)) · (T↑S))
63	59, 57, 50	mulass 5337	. . . . 5 ⊢ (((S↑2) · (2↑2)) · (T↑S)) = ((S↑2) · ((2↑2) · (T↑S)))
64	62, 63	eqtr 1498	. . . 4 ⊢ (((2 · S)↑2) · (T↑S)) = ((S↑2) · ((2↑2) · (T↑S)))
65	4	resqcl 6624	. . . . . . 7 ⊢ (2↑2) ∈ ℝ
66	65, 17	remulcl 5347	. . . . . 6 ⊢ ((2↑2) · (T↑S)) ∈ ℝ
67		4re 5984	. . . . . . . 8 ⊢ 4 ∈ ℝ
68	67, 14	remulcl 5347	. . . . . . 7 ⊢ (4 · T) ∈ ℝ
69		reexpclt 6581	. . . . . . 7 ⊢ (((4 · T) ∈ ℝ ⋀ S ∈ ℕ₀) → ((4 · T)↑S) ∈ ℝ)
70	68, 15, 69	mp2an 699	. . . . . 6 ⊢ ((4 · T)↑S) ∈ ℝ
71	58	nnre 5933	. . . . . 6 ⊢ (S↑2) ∈ ℝ
72	66, 70, 71	3pm3.2i 820	. . . . 5 ⊢ (((2↑2) · (T↑S)) ∈ ℝ ⋀ ((4 · T)↑S) ∈ ℝ ⋀ (S↑2) ∈ ℝ)
73	58	nngt0 5952	. . . . . . 7 ⊢ 0 < (S↑2)
74	33, 71, 73	ltlei 5593	. . . . . 6 ⊢ 0 ≤ (S↑2)
75		reexpclt 6581	. . . . . . . . . 10 ⊢ ((4 ∈ ℝ ⋀ S ∈ ℕ₀) → (4↑S) ∈ ℝ)
76	67, 15, 75	mp2an 699	. . . . . . . . 9 ⊢ (4↑S) ∈ ℝ
77	65, 76, 17	3pm3.2i 820	. . . . . . . 8 ⊢ ((2↑2) ∈ ℝ ⋀ (4↑S) ∈ ℝ ⋀ (T↑S) ∈ ℝ)
78		sq2 6639	. . . . . . . . . . 11 ⊢ (2↑2) = 4
79	67	recn 5326	. . . . . . . . . . . 12 ⊢ 4 ∈ ℂ
80		exp1t 6574	. . . . . . . . . . . 12 ⊢ (4 ∈ ℂ → (4↑1) = 4)
81	79, 80	ax-mp 7	. . . . . . . . . . 11 ⊢ (4↑1) = 4
82	78, 81	eqtr4 1501	. . . . . . . . . 10 ⊢ (2↑2) = (4↑1)
83		1nn0 6116	. . . . . . . . . . . 12 ⊢ 1 ∈ ℕ₀
84	67, 83, 15	3pm3.2i 820	. . . . . . . . . . 11 ⊢ (4 ∈ ℝ ⋀ 1 ∈ ℕ₀ ⋀ S ∈ ℕ₀)
85		3re 5983	. . . . . . . . . . . . . . 15 ⊢ 3 ∈ ℝ
86		3pos 5993	. . . . . . . . . . . . . . 15 ⊢ 0 < 3
87	33, 85, 86	ltlei 5593	. . . . . . . . . . . . . 14 ⊢ 0 ≤ 3
88		1re 5447	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℝ
89		addge02t 5685	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℝ ⋀ 3 ∈ ℝ) → (0 ≤ 3 ↔ 1 ≤ (3 + 1)))
90	88, 85, 89	mp2an 699	. . . . . . . . . . . . . 14 ⊢ (0 ≤ 3 ↔ 1 ≤ (3 + 1))
91	87, 90	mpbi 189	. . . . . . . . . . . . 13 ⊢ 1 ≤ (3 + 1)
92		df-4 5974	. . . . . . . . . . . . 13 ⊢ 4 = (3 + 1)
93	91, 92	breqtrr 2645	. . . . . . . . . . . 12 ⊢ 1 ≤ 4
94		nnge1t 5945	. . . . . . . . . . . . 13 ⊢ (S ∈ ℕ → 1 ≤ S)
95	6, 94	ax-mp 7	. . . . . . . . . . . 12 ⊢ 1 ≤ S
96	93, 95	pm3.2i 285	. . . . . . . . . . 11 ⊢ (1 ≤ 4 ⋀ 1 ≤ S)
97		expwordit 6604	. . . . . . . . . . 11 ⊢ (((4 ∈ ℝ ⋀ 1 ∈ ℕ₀ ⋀ S ∈ ℕ₀) ⋀ (1 ≤ 4 ⋀ 1 ≤ S)) → (4↑1) ≤ (4↑S))
98	84, 96, 97	mp2an 699	. . . . . . . . . 10 ⊢ (4↑1) ≤ (4↑S)
99	82, 98	eqbrtr 2639	. . . . . . . . 9 ⊢ (2↑2) ≤ (4↑S)
100	28, 99	pm3.2i 285	. . . . . . . 8 ⊢ (0 ≤ (T↑S) ⋀ (2↑2) ≤ (4↑S))
101		lemul1itOLD 5840	. . . . . . . 8 ⊢ ((((2↑2) ∈ ℝ ⋀ (4↑S) ∈ ℝ ⋀ (T↑S) ∈ ℝ) ⋀ (0 ≤ (T↑S) ⋀ (2↑2) ≤ (4↑S))) → ((2↑2) · (T↑S)) ≤ ((4↑S) · (T↑S)))
102	77, 100, 101	mp2an 699	. . . . . . 7 ⊢ ((2↑2) · (T↑S)) ≤ ((4↑S) · (T↑S))
103	13	nncn 5934	. . . . . . . 8 ⊢ T ∈ ℂ
104		mulexpt 6595	. . . . . . . 8 ⊢ ((4 ∈ ℂ ⋀ T ∈ ℂ ⋀ S ∈ ℕ₀) → ((4 · T)↑S) = ((4↑S) · (T↑S)))
105	79, 103, 15, 104	mp3an 918	. . . . . . 7 ⊢ ((4 · T)↑S) = ((4↑S) · (T↑S))
106	102, 105	breqtrr 2645	. . . . . 6 ⊢ ((2↑2) · (T↑S)) ≤ ((4 · T)↑S)
107	74, 106	pm3.2i 285	. . . . 5 ⊢ (0 ≤ (S↑2) ⋀ ((2↑2) · (T↑S)) ≤ ((4 · T)↑S))
108		lemul2itOLD 5842	. . . . 5 ⊢ (((((2↑2) · (T↑S)) ∈ ℝ ⋀ ((4 · T)↑S) ∈ ℝ ⋀ (S↑2) ∈ ℝ) ⋀ (0 ≤ (S↑2) ⋀ ((2↑2) · (T↑S)) ≤ ((4 · T)↑S))) → ((S↑2) · ((2↑2) · (T↑S))) ≤ ((S↑2) · ((4 · T)↑S)))
109	72, 107, 108	mp2an 699	. . . 4 ⊢ ((S↑2) · ((2↑2) · (T↑S))) ≤ ((S↑2) · ((4 · T)↑S))
110	64, 109	eqbrtr 2639	. . 3 ⊢ (((2 · S)↑2) · (T↑S)) ≤ ((S↑2) · ((4 · T)↑S))
111	9, 17	remulcl 5347	. . . 4 ⊢ (((2 · S)↑2) · (T↑S)) ∈ ℝ
112	71, 70	remulcl 5347	. . . 4 ⊢ ((S↑2) · ((4 · T)↑S)) ∈ ℝ
113		lediv1tOLD 5854	. . . . 5 ⊢ ((((((2 · S)↑2) · (T↑S)) ∈ ℝ ⋀ ((S↑2) · ((4 · T)↑S)) ∈ ℝ ⋀ (! ‘S) ∈ ℝ) ⋀ 0 < (! ‘S)) → ((((2 · S)↑2) · (T↑S)) ≤ ((S↑2) · ((4 · T)↑S)) ↔ ((((2 · S)↑2) · (T↑S)) / (! ‘S)) ≤ (((S↑2) · ((4 · T)↑S)) / (! ‘S))))
114	29, 113	mpan2 698	. . . 4 ⊢ (((((2 · S)↑2) · (T↑S)) ∈ ℝ ⋀ ((S↑2) · ((4 · T)↑S)) ∈ ℝ ⋀ (! ‘S) ∈ ℝ) → ((((2 · S)↑2) · (T↑S)) ≤ ((S↑2) · ((4 · T)↑S)) ↔ ((((2 · S)↑2) · (T↑S)) / (! ‘S)) ≤ (((S↑2) · ((4 · T)↑S)) / (! ‘S))))
115	111, 112, 20, 114	mp3an 918	. . 3 ⊢ ((((2 · S)↑2) · (T↑S)) ≤ ((S↑2) · ((4 · T)↑S)) ↔ ((((2 · S)↑2) · (T↑S)) / (! ‘S)) ≤ (((S↑2) · ((4 · T)↑S)) / (! ‘S)))
116	110, 115	mpbi 189	. 2 ⊢ ((((2 · S)↑2) · (T↑S)) / (! ‘S)) ≤ (((S↑2) · ((4 · T)↑S)) / (! ‘S))
117	3, 23	remulcl 5347	. . 3 ⊢ ((N↑2) · ((T↑S) / (! ‘S))) ∈ ℝ
118	111, 20, 22	redivcl 5800	. . 3 ⊢ ((((2 · S)↑2) · (T↑S)) / (! ‘S)) ∈ ℝ
119	112, 20, 22	redivcl 5800	. . 3 ⊢ (((S↑2) · ((4 · T)↑S)) / (! ‘S)) ∈ ℝ
120	117, 118, 119	letr 5600	. 2 ⊢ ((((N↑2) · ((T↑S) / (! ‘S))) ≤ ((((2 · S)↑2) · (T↑S)) / (! ‘S)) ⋀ ((((2 · S)↑2) · (T↑S)) / (! ‘S)) ≤ (((S↑2) · ((4 · T)↑S)) / (! ‘S))) → ((N↑2) · ((T↑S) / (! ‘S))) ≤ (((S↑2) · ((4 · T)↑S)) / (! ‘S)))
121	53, 116, 120	mp2an 699	1 ⊢ ((N↑2) · ((T↑S) / (! ‘S))) ≤ (((S↑2) · ((4 · T)↑S)) / (! ‘S))

Colors of variables: wff set class

Syntax hints: ↔ wb 146 ⋀ wa 223 ⋀ w3a 777 = wceq 958 ∈ wcel 960 ≠ wne 1588 class class class wbr 2624 ‘cfv 3188 (class class class)co 3969 ℂcc 5244 ℝcr 5245 0cc0 5246 1c1 5247 + caddc 5249 · cmul 5251 / cdiv 5306 ≤ cle 5307 ℕcn 5308 ℕ₀cn0 5309 ℤcz 5310 < clt 5498 2c2 5963 3c3 5964 4c4 5965 ⌊cfl 6225 ↑cexp 6569 abscabs 6751 !cfa 6931

This theorem is referenced by: efaddlem22 7359

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 964 ax-gen 965 ax-8 966 ax-9 967 ax-10 968 ax-11 969 ax-12 970 ax-13 971 ax-14 972 ax-17 973 ax-4 975 ax-5o 977 ax-6o 980 ax-9o 1125 ax-10o 1142 ax-16 1212 ax-11o 1220 ax-ext 1462 ax-rep 2698 ax-sep 2708 ax-nul 2715 ax-pow 2748 ax-pr 2785 ax-un 2872 ax-inf2 4634

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-3or 778 df-3an 779 df-ex 983 df-sb 1174 df-eu 1384 df-mo 1385 df-clab 1467 df-cleq 1472 df-clel 1475 df-ne 1590 df-nel 1591 df-ral 1652 df-rex 1653 df-reu 1654 df-rab 1655 df-v 1815 df-sbc 1945 df-csb 2005 df-dif 2052 df-un 2053 df-in 2054 df-ss 2056 df-pss 2058 df-nul 2284 df-if 2366 df-pw 2406 df-sn 2416 df-pr 2417 df-tp 2419 df-op 2420 df-uni 2508 df-int 2538 df-iun 2572 df-br 2625 df-opab 2672 df-tr 2686 df-eprel 2838 df-id 2841 df-po 2846 df-so 2856 df-fr 2923 df-we 2940 df-ord 2957 df-on 2958 df-lim 2959 df-suc 2960 df-om 3138 df-xp 3190 df-rel 3191 df-cnv 3192 df-co 3193 df-dm 3194 df-rn 3195 df-res 3196 df-ima 3197 df-fun 3198 df-fn 3199 df-f 3200 df-f1 3201 df-fo 3202 df-f1o 3203 df-fv 3204 df-rdg 3938 df-opr 3971 df-oprab 3972 df-1st 4085 df-2nd 4086 df-1o 4139 df-oadd 4141 df-omul 4142 df-er 4267 df-ec 4269 df-qs 4272 df-en 4374 df-dom 4375 df-sdom 4376 df-sup 4583 df-ni 5012 df-pli 5013 df-mi 5014 df-lti 5015 df-plpq 5047 df-mpq 5048 df-enq 5049 df-nq 5050 df-plq 5051 df-mq 5052 df-rq 5053 df-ltq 5054 df-1q 5055 df-np 5098 df-1p 5099 df-plp 5100 df-mp 5101 df-ltp 5102 df-plpr 5176 df-mpr 5177 df-enr 5178 df-nr 5179 df-plr 5180 df-mr 5181 df-ltr 5182 df-0r 5183 df-1r 5184 df-m1r 5185 df-c 5252 df-0 5253 df-1 5254 df-i 5255 df-r 5256 df-plus 5257 df-mul 5258 df-lt 5259 df-sub 5368 df-neg 5370 df-pnf 5499 df-mnf 5500 df-xr 5501 df-ltxr 5502 df-le 5503 df-div 5715 df-n 5927 df-2 5972 df-3 5973 df-4 5974 df-n0 6102 df-z 6138 df-fl 6226 df-seq1 6309 df-exp 6570 df-sqr 6671 df-re 6752 df-im 6753 df-cj 6754 df-abs 6755 df-fac 6932