stoweidlem1

Description: Lemma for stoweid . This lemma is used by Lemma 1 in BrosowskiDeutsh p. 90; the key step uses Bernoulli's inequality bernneq . (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem1.1	$⊢ φ \to N \in ℕ$
	stoweidlem1.2	$⊢ φ \to K \in ℕ$
	stoweidlem1.3	$⊢ φ \to D \in ℝ^{+}$
	stoweidlem1.5	$⊢ φ \to A \in ℝ^{+}$
	stoweidlem1.6	$⊢ φ \to 0 \leq A$
	stoweidlem1.7	$⊢ φ \to A \leq 1$
	stoweidlem1.8	$⊢ φ \to D \leq A$
Assertion	stoweidlem1	$⊢ φ \to {(1 - A^{N})}^{K^{N}} \leq \frac{1}{{K D}^{N}}$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem1.1	$⊢ φ \to N \in ℕ$
2		stoweidlem1.2	$⊢ φ \to K \in ℕ$
3		stoweidlem1.3	$⊢ φ \to D \in ℝ^{+}$
4		stoweidlem1.5	$⊢ φ \to A \in ℝ^{+}$
5		stoweidlem1.6	$⊢ φ \to 0 \leq A$
6		stoweidlem1.7	$⊢ φ \to A \leq 1$
7		stoweidlem1.8	$⊢ φ \to D \leq A$
8		1re	$⊢ 1 \in ℝ$
9	8	a1i	$⊢ φ \to 1 \in ℝ$
10	4	rpred	$⊢ φ \to A \in ℝ$
11	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
12	10 11	reexpcld	$⊢ φ \to A^{N} \in ℝ$
13	9 12	resubcld	$⊢ φ \to 1 - A^{N} \in ℝ$
14	2	nnnn0d	$⊢ φ \to K \in ℕ_{0}$
15	14 11	nn0expcld	$⊢ φ \to K^{N} \in ℕ_{0}$
16	13 15	reexpcld	$⊢ φ \to {(1 - A^{N})}^{K^{N}} \in ℝ$
17		2nn0	$⊢ 2 \in ℕ_{0}$
18	17	a1i	$⊢ φ \to 2 \in ℕ_{0}$
19	18 11	nn0mulcld	$⊢ φ \to 2 \cdot N \in ℕ_{0}$
20	10 19	reexpcld	$⊢ φ \to A^{2 \cdot N} \in ℝ$
21	9 20	resubcld	$⊢ φ \to 1 - A^{2 \cdot N} \in ℝ$
22	21 15	reexpcld	$⊢ φ \to {(1 - A^{2 \cdot N})}^{K^{N}} \in ℝ$
23	2	nnred	$⊢ φ \to K \in ℝ$
24	23 10	remulcld	$⊢ φ \to K A \in ℝ$
25	24 11	reexpcld	$⊢ φ \to {K A}^{N} \in ℝ$
26	2	nncnd	$⊢ φ \to K \in ℂ$
27	4	rpcnd	$⊢ φ \to A \in ℂ$
28	2	nnne0d	$⊢ φ \to K \neq 0$
29	4	rpne0d	$⊢ φ \to A \neq 0$
30	26 27 28 29	mulne0d	$⊢ φ \to K A \neq 0$
31	26 27	mulcld	$⊢ φ \to K A \in ℂ$
32		expne0	$⊢ (K A \in ℂ \land N \in ℕ) \to ({K A}^{N} \neq 0 \leftrightarrow K A \neq 0)$
33	31 1 32	syl2anc	$⊢ φ \to ({K A}^{N} \neq 0 \leftrightarrow K A \neq 0)$
34	30 33	mpbird	$⊢ φ \to {K A}^{N} \neq 0$
35	22 25 34	redivcld	$⊢ φ \to \frac{{(1 - A^{2 \cdot N})}^{K^{N}}}{{K A}^{N}} \in ℝ$
36	3	rpred	$⊢ φ \to D \in ℝ$
37	23 36	remulcld	$⊢ φ \to K D \in ℝ$
38	37 11	reexpcld	$⊢ φ \to {K D}^{N} \in ℝ$
39	3	rpcnd	$⊢ φ \to D \in ℂ$
40	3	rpne0d	$⊢ φ \to D \neq 0$
41	26 39 28 40	mulne0d	$⊢ φ \to K D \neq 0$
42	26 39	mulcld	$⊢ φ \to K D \in ℂ$
43		expne0	$⊢ (K D \in ℂ \land N \in ℕ) \to ({K D}^{N} \neq 0 \leftrightarrow K D \neq 0)$
44	42 1 43	syl2anc	$⊢ φ \to ({K D}^{N} \neq 0 \leftrightarrow K D \neq 0)$
45	41 44	mpbird	$⊢ φ \to {K D}^{N} \neq 0$
46	9 38 45	redivcld	$⊢ φ \to \frac{1}{{K D}^{N}} \in ℝ$
47	23 11	reexpcld	$⊢ φ \to K^{N} \in ℝ$
48	47 12	remulcld	$⊢ φ \to K^{N} A^{N} \in ℝ$
49	9 48	readdcld	$⊢ φ \to 1 + K^{N} A^{N} \in ℝ$
50	16 49	remulcld	$⊢ φ \to {(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N}) \in ℝ$
51	50 25 34	redivcld	$⊢ φ \to \frac{{(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N})}{{K A}^{N}} \in ℝ$
52	9 12	readdcld	$⊢ φ \to 1 + A^{N} \in ℝ$
53	52 15	reexpcld	$⊢ φ \to {(1 + A^{N})}^{K^{N}} \in ℝ$
54	16 53	remulcld	$⊢ φ \to {(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}} \in ℝ$
55	54 25 34	redivcld	$⊢ φ \to \frac{{(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}}}{{K A}^{N}} \in ℝ$
56	49 25 34	redivcld	$⊢ φ \to \frac{1 + K^{N} A^{N}}{{K A}^{N}} \in ℝ$
57		exple1	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land N \in ℕ_{0}) \to A^{N} \leq 1$
58	10 5 6 11 57	syl31anc	$⊢ φ \to A^{N} \leq 1$
59	9 12	subge0d	$⊢ φ \to (0 \leq 1 - A^{N} \leftrightarrow A^{N} \leq 1)$
60	58 59	mpbird	$⊢ φ \to 0 \leq 1 - A^{N}$
61	13 15 60	expge0d	$⊢ φ \to 0 \leq {(1 - A^{N})}^{K^{N}}$
62	31 11	expcld	$⊢ φ \to {K A}^{N} \in ℂ$
63	62 34	dividd	$⊢ φ \to \frac{{K A}^{N}}{{K A}^{N}} = 1$
64	62	addid2d	$⊢ φ \to 0 + {K A}^{N} = {K A}^{N}$
65		0red	$⊢ φ \to 0 \in ℝ$
66		0le1	$⊢ 0 \leq 1$
67	66	a1i	$⊢ φ \to 0 \leq 1$
68	65 9 25 67	leadd1dd	$⊢ φ \to 0 + {K A}^{N} \leq 1 + {K A}^{N}$
69	64 68	eqbrtrrd	$⊢ φ \to {K A}^{N} \leq 1 + {K A}^{N}$
70	9 25	readdcld	$⊢ φ \to 1 + {K A}^{N} \in ℝ$
71	1	nnzd	$⊢ φ \to N \in ℤ$
72	2	nngt0d	$⊢ φ \to 0 < K$
73	4	rpgt0d	$⊢ φ \to 0 < A$
74	23 10 72 73	mulgt0d	$⊢ φ \to 0 < K A$
75		expgt0	$⊢ (K A \in ℝ \land N \in ℤ \land 0 < K A) \to 0 < {K A}^{N}$
76	24 71 74 75	syl3anc	$⊢ φ \to 0 < {K A}^{N}$
77		lediv1	$⊢ ({K A}^{N} \in ℝ \land 1 + {K A}^{N} \in ℝ \land ({K A}^{N} \in ℝ \land 0 < {K A}^{N})) \to ({K A}^{N} \leq 1 + {K A}^{N} \leftrightarrow \frac{{K A}^{N}}{{K A}^{N}} \leq \frac{1 + {K A}^{N}}{{K A}^{N}})$
78	25 70 25 76 77	syl112anc	$⊢ φ \to ({K A}^{N} \leq 1 + {K A}^{N} \leftrightarrow \frac{{K A}^{N}}{{K A}^{N}} \leq \frac{1 + {K A}^{N}}{{K A}^{N}})$
79	69 78	mpbid	$⊢ φ \to \frac{{K A}^{N}}{{K A}^{N}} \leq \frac{1 + {K A}^{N}}{{K A}^{N}}$
80	63 79	eqbrtrrd	$⊢ φ \to 1 \leq \frac{1 + {K A}^{N}}{{K A}^{N}}$
81	26 27 11	mulexpd	$⊢ φ \to {K A}^{N} = K^{N} A^{N}$
82	81	oveq2d	$⊢ φ \to 1 + {K A}^{N} = 1 + K^{N} A^{N}$
83	82	oveq1d	$⊢ φ \to \frac{1 + {K A}^{N}}{{K A}^{N}} = \frac{1 + K^{N} A^{N}}{{K A}^{N}}$
84	80 83	breqtrd	$⊢ φ \to 1 \leq \frac{1 + K^{N} A^{N}}{{K A}^{N}}$
85	16 56 61 84	lemulge11d	$⊢ φ \to {(1 - A^{N})}^{K^{N}} \leq {(1 - A^{N})}^{K^{N}} (\frac{1 + K^{N} A^{N}}{{K A}^{N}})$
86		1cnd	$⊢ φ \to 1 \in ℂ$
87	27 11	expcld	$⊢ φ \to A^{N} \in ℂ$
88	86 87	subcld	$⊢ φ \to 1 - A^{N} \in ℂ$
89	88 15	expcld	$⊢ φ \to {(1 - A^{N})}^{K^{N}} \in ℂ$
90	26 11	expcld	$⊢ φ \to K^{N} \in ℂ$
91	90 87	mulcld	$⊢ φ \to K^{N} A^{N} \in ℂ$
92	86 91	addcld	$⊢ φ \to 1 + K^{N} A^{N} \in ℂ$
93	89 92 62 34	divassd	$⊢ φ \to \frac{{(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N})}{{K A}^{N}} = {(1 - A^{N})}^{K^{N}} (\frac{1 + K^{N} A^{N}}{{K A}^{N}})$
94	85 93	breqtrrd	$⊢ φ \to {(1 - A^{N})}^{K^{N}} \leq \frac{{(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N})}{{K A}^{N}}$
95	90 87	mulcomd	$⊢ φ \to K^{N} A^{N} = A^{N} K^{N}$
96	95	oveq2d	$⊢ φ \to 1 + K^{N} A^{N} = 1 + A^{N} K^{N}$
97	9	renegcld	$⊢ φ \to - 1 \in ℝ$
98		le0neg2	$⊢ 1 \in ℝ \to (0 \leq 1 \leftrightarrow - 1 \leq 0)$
99	8 98	ax-mp	$⊢ 0 \leq 1 \leftrightarrow - 1 \leq 0$
100	66 99	mpbi	$⊢ - 1 \leq 0$
101	100	a1i	$⊢ φ \to - 1 \leq 0$
102	10 11 5	expge0d	$⊢ φ \to 0 \leq A^{N}$
103	97 65 12 101 102	letrd	$⊢ φ \to - 1 \leq A^{N}$
104		bernneq	$⊢ (A^{N} \in ℝ \land K^{N} \in ℕ_{0} \land - 1 \leq A^{N}) \to 1 + A^{N} K^{N} \leq {(1 + A^{N})}^{K^{N}}$
105	12 15 103 104	syl3anc	$⊢ φ \to 1 + A^{N} K^{N} \leq {(1 + A^{N})}^{K^{N}}$
106	96 105	eqbrtrd	$⊢ φ \to 1 + K^{N} A^{N} \leq {(1 + A^{N})}^{K^{N}}$
107	49 53 16 61 106	lemul2ad	$⊢ φ \to {(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N}) \leq {(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}}$
108		lediv1	$⊢ ({(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N}) \in ℝ \land {(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}} \in ℝ \land ({K A}^{N} \in ℝ \land 0 < {K A}^{N})) \to ({(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N}) \leq {(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}} \leftrightarrow \frac{{(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N})}{{K A}^{N}} \leq \frac{{(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}}}{{K A}^{N}})$
109	50 54 25 76 108	syl112anc	$⊢ φ \to ({(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N}) \leq {(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}} \leftrightarrow \frac{{(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N})}{{K A}^{N}} \leq \frac{{(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}}}{{K A}^{N}})$
110	107 109	mpbid	$⊢ φ \to \frac{{(1 - A^{N})}^{K^{N}} (1 + K^{N} A^{N})}{{K A}^{N}} \leq \frac{{(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}}}{{K A}^{N}}$
111	16 51 55 94 110	letrd	$⊢ φ \to {(1 - A^{N})}^{K^{N}} \leq \frac{{(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}}}{{K A}^{N}}$
112	86 87	addcld	$⊢ φ \to 1 + A^{N} \in ℂ$
113	88 112	mulcomd	$⊢ φ \to (1 - A^{N}) (1 + A^{N}) = (1 + A^{N}) (1 - A^{N})$
114	113	oveq1d	$⊢ φ \to {(1 - A^{N}) (1 + A^{N})}^{K^{N}} = {(1 + A^{N}) (1 - A^{N})}^{K^{N}}$
115	88 112 15	mulexpd	$⊢ φ \to {(1 - A^{N}) (1 + A^{N})}^{K^{N}} = {(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}}$
116		subsq	$⊢ (1 \in ℂ \land A^{N} \in ℂ) \to 1^{2} - {(A^{N})}^{2} = (1 + A^{N}) (1 - A^{N})$
117	86 87 116	syl2anc	$⊢ φ \to 1^{2} - {(A^{N})}^{2} = (1 + A^{N}) (1 - A^{N})$
118		sq1	$⊢ 1^{2} = 1$
119	118	a1i	$⊢ φ \to 1^{2} = 1$
120	27 18 11	expmuld	$⊢ φ \to A^{N \cdot 2} = {(A^{N})}^{2}$
121	1	nncnd	$⊢ φ \to N \in ℂ$
122		2cnd	$⊢ φ \to 2 \in ℂ$
123	121 122	mulcomd	$⊢ φ \to N \cdot 2 = 2 \cdot N$
124	123	oveq2d	$⊢ φ \to A^{N \cdot 2} = A^{2 \cdot N}$
125	120 124	eqtr3d	$⊢ φ \to {(A^{N})}^{2} = A^{2 \cdot N}$
126	119 125	oveq12d	$⊢ φ \to 1^{2} - {(A^{N})}^{2} = 1 - A^{2 \cdot N}$
127	117 126	eqtr3d	$⊢ φ \to (1 + A^{N}) (1 - A^{N}) = 1 - A^{2 \cdot N}$
128	127	oveq1d	$⊢ φ \to {(1 + A^{N}) (1 - A^{N})}^{K^{N}} = {(1 - A^{2 \cdot N})}^{K^{N}}$
129	114 115 128	3eqtr3d	$⊢ φ \to {(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}} = {(1 - A^{2 \cdot N})}^{K^{N}}$
130	129	oveq1d	$⊢ φ \to \frac{{(1 - A^{N})}^{K^{N}} {(1 + A^{N})}^{K^{N}}}{{K A}^{N}} = \frac{{(1 - A^{2 \cdot N})}^{K^{N}}}{{K A}^{N}}$
131	111 130	breqtrd	$⊢ φ \to {(1 - A^{N})}^{K^{N}} \leq \frac{{(1 - A^{2 \cdot N})}^{K^{N}}}{{K A}^{N}}$
132	22 9	jca	$⊢ φ \to ({(1 - A^{2 \cdot N})}^{K^{N}} \in ℝ \land 1 \in ℝ)$
133		exple1	$⊢ ((A \in ℝ \land 0 \leq A \land A \leq 1) \land 2 \cdot N \in ℕ_{0}) \to A^{2 \cdot N} \leq 1$
134	10 5 6 19 133	syl31anc	$⊢ φ \to A^{2 \cdot N} \leq 1$
135	9 20	subge0d	$⊢ φ \to (0 \leq 1 - A^{2 \cdot N} \leftrightarrow A^{2 \cdot N} \leq 1)$
136	134 135	mpbird	$⊢ φ \to 0 \leq 1 - A^{2 \cdot N}$
137	21 15 136	expge0d	$⊢ φ \to 0 \leq {(1 - A^{2 \cdot N})}^{K^{N}}$
138		1m1e0	$⊢ 1 - 1 = 0$
139	10 19 5	expge0d	$⊢ φ \to 0 \leq A^{2 \cdot N}$
140	138 139	eqbrtrid	$⊢ φ \to 1 - 1 \leq A^{2 \cdot N}$
141	9 9 20 140	subled	$⊢ φ \to 1 - A^{2 \cdot N} \leq 1$
142		exple1	$⊢ ((1 - A^{2 \cdot N} \in ℝ \land 0 \leq 1 - A^{2 \cdot N} \land 1 - A^{2 \cdot N} \leq 1) \land K^{N} \in ℕ_{0}) \to {(1 - A^{2 \cdot N})}^{K^{N}} \leq 1$
143	21 136 141 15 142	syl31anc	$⊢ φ \to {(1 - A^{2 \cdot N})}^{K^{N}} \leq 1$
144	132 137 143	jca32	$⊢ φ \to (({(1 - A^{2 \cdot N})}^{K^{N}} \in ℝ \land 1 \in ℝ) \land (0 \leq {(1 - A^{2 \cdot N})}^{K^{N}} \land {(1 - A^{2 \cdot N})}^{K^{N}} \leq 1))$
145	38 25	jca	$⊢ φ \to ({K D}^{N} \in ℝ \land {K A}^{N} \in ℝ)$
146	3	rpgt0d	$⊢ φ \to 0 < D$
147	23 36 72 146	mulgt0d	$⊢ φ \to 0 < K D$
148		expgt0	$⊢ (K D \in ℝ \land N \in ℤ \land 0 < K D) \to 0 < {K D}^{N}$
149	37 71 147 148	syl3anc	$⊢ φ \to 0 < {K D}^{N}$
150	65 23 72	ltled	$⊢ φ \to 0 \leq K$
151	65 36 146	ltled	$⊢ φ \to 0 \leq D$
152	23 36 150 151	mulge0d	$⊢ φ \to 0 \leq K D$
153	36 10 23 150 7	lemul2ad	$⊢ φ \to K D \leq K A$
154		leexp1a	$⊢ ((K D \in ℝ \land K A \in ℝ \land N \in ℕ_{0}) \land (0 \leq K D \land K D \leq K A)) \to {K D}^{N} \leq {K A}^{N}$
155	37 24 11 152 153 154	syl32anc	$⊢ φ \to {K D}^{N} \leq {K A}^{N}$
156	149 155	jca	$⊢ φ \to (0 < {K D}^{N} \land {K D}^{N} \leq {K A}^{N})$
157		lediv12a	$⊢ ((({(1 - A^{2 \cdot N})}^{K^{N}} \in ℝ \land 1 \in ℝ) \land (0 \leq {(1 - A^{2 \cdot N})}^{K^{N}} \land {(1 - A^{2 \cdot N})}^{K^{N}} \leq 1)) \land (({K D}^{N} \in ℝ \land {K A}^{N} \in ℝ) \land (0 < {K D}^{N} \land {K D}^{N} \leq {K A}^{N}))) \to \frac{{(1 - A^{2 \cdot N})}^{K^{N}}}{{K A}^{N}} \leq \frac{1}{{K D}^{N}}$
158	144 145 156 157	syl12anc	$⊢ φ \to \frac{{(1 - A^{2 \cdot N})}^{K^{N}}}{{K A}^{N}} \leq \frac{1}{{K D}^{N}}$
159	16 35 46 131 158	letrd	$⊢ φ \to {(1 - A^{N})}^{K^{N}} \leq \frac{1}{{K D}^{N}}$

Metamath Proof Explorer

Theorem stoweidlem1

Proof