stoweidlem14

Description: There exists a k as in the proof of Lemma 1 in BrosowskiDeutsh p. 90: k is an integer and 1 < k * δ < 2. D is used to represent δ in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem14.1	$⊢ A = \{j \in ℕ \| \frac{1}{D} < j\}$
	stoweidlem14.2	$⊢ φ \to D \in ℝ^{+}$
	stoweidlem14.3	$⊢ φ \to D < 1$
Assertion	stoweidlem14	$⊢ φ \to \exists k \in ℕ (1 < k D \land \frac{k D}{2} < 1)$

Proof

Step	Hyp	Ref	Expression
1		stoweidlem14.1	$⊢ A = \{j \in ℕ \| \frac{1}{D} < j\}$
2		stoweidlem14.2	$⊢ φ \to D \in ℝ^{+}$
3		stoweidlem14.3	$⊢ φ \to D < 1$
4		ssrab2	$⊢ \{j \in ℕ \| \frac{1}{D} < j\} \subseteq ℕ$
5	4	a1i	$⊢ φ \to \{j \in ℕ \| \frac{1}{D} < j\} \subseteq ℕ$
6	1 5	eqsstrid	$⊢ φ \to A \subseteq ℕ$
7	2	rprecred	$⊢ φ \to \frac{1}{D} \in ℝ$
8		arch	$⊢ \frac{1}{D} \in ℝ \to \exists k \in ℕ \frac{1}{D} < k$
9		breq2	$⊢ j = k \to (\frac{1}{D} < j \leftrightarrow \frac{1}{D} < k)$
10	9	elrab	$⊢ k \in \{j \in ℕ \| \frac{1}{D} < j\} \leftrightarrow (k \in ℕ \land \frac{1}{D} < k)$
11	10	biimpri	$⊢ (k \in ℕ \land \frac{1}{D} < k) \to k \in \{j \in ℕ \| \frac{1}{D} < j\}$
12	11 1	eleqtrrdi	$⊢ (k \in ℕ \land \frac{1}{D} < k) \to k \in A$
13		simpr	$⊢ (k \in ℕ \land \frac{1}{D} < k) \to \frac{1}{D} < k$
14	12 13	jca	$⊢ (k \in ℕ \land \frac{1}{D} < k) \to (k \in A \land \frac{1}{D} < k)$
15	14	reximi2	$⊢ \exists k \in ℕ \frac{1}{D} < k \to \exists k \in A \frac{1}{D} < k$
16		rexn0	$⊢ \exists k \in A \frac{1}{D} < k \to A \neq \emptyset$
17	7 8 15 16	4syl	$⊢ φ \to A \neq \emptyset$
18		nnwo	$⊢ (A \subseteq ℕ \land A \neq \emptyset) \to \exists k \in A \forall z \in A k \leq z$
19	6 17 18	syl2anc	$⊢ φ \to \exists k \in A \forall z \in A k \leq z$
20		df-rex	$⊢ \exists k \in A \forall z \in A k \leq z \leftrightarrow \exists k (k \in A \land \forall z \in A k \leq z)$
21	19 20	sylib	$⊢ φ \to \exists k (k \in A \land \forall z \in A k \leq z)$
22	9 1	elrab2	$⊢ k \in A \leftrightarrow (k \in ℕ \land \frac{1}{D} < k)$
23	22	simplbi	$⊢ k \in A \to k \in ℕ$
24	23	ad2antrl	$⊢ (φ \land (k \in A \land \forall z \in A k \leq z)) \to k \in ℕ$
25		simpl	$⊢ (φ \land (k \in A \land \forall z \in A k \leq z)) \to φ$
26		simprl	$⊢ (φ \land (k \in A \land \forall z \in A k \leq z)) \to k \in A$
27		simprr	$⊢ (φ \land (k \in A \land \forall z \in A k \leq z)) \to \forall z \in A k \leq z$
28		nfcv	$⊢ \underline{Ⅎ} z A$
29		nfrab1	$⊢ \underline{Ⅎ} j \{j \in ℕ \| \frac{1}{D} < j\}$
30	1 29	nfcxfr	$⊢ \underline{Ⅎ} j A$
31		nfv	$⊢ Ⅎ j k \leq z$
32		nfv	$⊢ Ⅎ z k \leq j$
33		breq2	$⊢ z = j \to (k \leq z \leftrightarrow k \leq j)$
34	28 30 31 32 33	cbvralfw	$⊢ \forall z \in A k \leq z \leftrightarrow \forall j \in A k \leq j$
35	27 34	sylib	$⊢ (φ \land (k \in A \land \forall z \in A k \leq z)) \to \forall j \in A k \leq j$
36	22	simprbi	$⊢ k \in A \to \frac{1}{D} < k$
37	36	ad2antrl	$⊢ (φ \land (k \in A \land \forall j \in A k \leq j)) \to \frac{1}{D} < k$
38	23	ad2antrl	$⊢ (φ \land (k \in A \land \forall j \in A k \leq j)) \to k \in ℕ$
39		1red	$⊢ (φ \land k \in ℕ) \to 1 \in ℝ$
40		nnre	$⊢ k \in ℕ \to k \in ℝ$
41	40	adantl	$⊢ (φ \land k \in ℕ) \to k \in ℝ$
42	2	rpregt0d	$⊢ φ \to (D \in ℝ \land 0 < D)$
43	42	adantr	$⊢ (φ \land k \in ℕ) \to (D \in ℝ \land 0 < D)$
44		ltdivmul2	$⊢ (1 \in ℝ \land k \in ℝ \land (D \in ℝ \land 0 < D)) \to (\frac{1}{D} < k \leftrightarrow 1 < k D)$
45	39 41 43 44	syl3anc	$⊢ (φ \land k \in ℕ) \to (\frac{1}{D} < k \leftrightarrow 1 < k D)$
46	38 45	syldan	$⊢ (φ \land (k \in A \land \forall j \in A k \leq j)) \to (\frac{1}{D} < k \leftrightarrow 1 < k D)$
47	37 46	mpbid	$⊢ (φ \land (k \in A \land \forall j \in A k \leq j)) \to 1 < k D$
48	25 26 35 47	syl12anc	$⊢ (φ \land (k \in A \land \forall z \in A k \leq z)) \to 1 < k D$
49		oveq1	$⊢ k = 1 \to k D = 1 D$
50	49	adantl	$⊢ (φ \land k = 1) \to k D = 1 D$
51	2	rpcnd	$⊢ φ \to D \in ℂ$
52	51	adantr	$⊢ (φ \land k = 1) \to D \in ℂ$
53	52	mullidd	$⊢ (φ \land k = 1) \to 1 D = D$
54	50 53	eqtrd	$⊢ (φ \land k = 1) \to k D = D$
55	54	oveq1d	$⊢ (φ \land k = 1) \to \frac{k D}{2} = \frac{D}{2}$
56	2	rpred	$⊢ φ \to D \in ℝ$
57	56	rehalfcld	$⊢ φ \to \frac{D}{2} \in ℝ$
58		halfre	$⊢ \frac{1}{2} \in ℝ$
59	58	a1i	$⊢ φ \to \frac{1}{2} \in ℝ$
60		1red	$⊢ φ \to 1 \in ℝ$
61		2re	$⊢ 2 \in ℝ$
62	61	a1i	$⊢ φ \to 2 \in ℝ$
63		2pos	$⊢ 0 < 2$
64	63	a1i	$⊢ φ \to 0 < 2$
65		ltdiv1	$⊢ (D \in ℝ \land 1 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (D < 1 \leftrightarrow \frac{D}{2} < \frac{1}{2})$
66	56 60 62 64 65	syl112anc	$⊢ φ \to (D < 1 \leftrightarrow \frac{D}{2} < \frac{1}{2})$
67	3 66	mpbid	$⊢ φ \to \frac{D}{2} < \frac{1}{2}$
68		halflt1	$⊢ \frac{1}{2} < 1$
69	68	a1i	$⊢ φ \to \frac{1}{2} < 1$
70	57 59 60 67 69	lttrd	$⊢ φ \to \frac{D}{2} < 1$
71	70	adantr	$⊢ (φ \land k = 1) \to \frac{D}{2} < 1$
72	55 71	eqbrtrd	$⊢ (φ \land k = 1) \to \frac{k D}{2} < 1$
73	72	adantlr	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land k = 1) \to \frac{k D}{2} < 1$
74		simpll	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to φ$
75		simplrl	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to k \in A$
76	75 23	syl	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to k \in ℕ$
77		neqne	$⊢ \neg k = 1 \to k \neq 1$
78	77	adantl	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to k \neq 1$
79		eluz2b3	$⊢ k \in ℤ_{\geq 2} \leftrightarrow (k \in ℕ \land k \neq 1)$
80	76 78 79	sylanbrc	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to k \in ℤ_{\geq 2}$
81		peano2rem	$⊢ k \in ℝ \to k - 1 \in ℝ$
82	75 23 40 81	4syl	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to k - 1 \in ℝ$
83	56	ad2antrr	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to D \in ℝ$
84	2	rpne0d	$⊢ φ \to D \neq 0$
85	84	ad2antrr	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to D \neq 0$
86	83 85	rereccld	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to \frac{1}{D} \in ℝ$
87		1zzd	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to 1 \in ℤ$
88		df-2	$⊢ 2 = 1 + 1$
89	88	fveq2i	$⊢ ℤ_{\geq 2} = ℤ_{\geq (1 + 1)}$
90	89	eleq2i	$⊢ k \in ℤ_{\geq 2} \leftrightarrow k \in ℤ_{\geq (1 + 1)}$
91		eluzsub	$⊢ (1 \in ℤ \land 1 \in ℤ \land k \in ℤ_{\geq (1 + 1)}) \to k - 1 \in ℤ_{\geq 1}$
92	90 91	syl3an3b	$⊢ (1 \in ℤ \land 1 \in ℤ \land k \in ℤ_{\geq 2}) \to k - 1 \in ℤ_{\geq 1}$
93		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
94	92 93	eleqtrrdi	$⊢ (1 \in ℤ \land 1 \in ℤ \land k \in ℤ_{\geq 2}) \to k - 1 \in ℕ$
95	87 87 80 94	syl3anc	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to k - 1 \in ℕ$
96	23 40	syl	$⊢ k \in A \to k \in ℝ$
97	96	adantl	$⊢ (k - 1 \in A \land k \in A) \to k \in ℝ$
98	97 81	syl	$⊢ (k - 1 \in A \land k \in A) \to k - 1 \in ℝ$
99		simpr	$⊢ (k - 1 \in ℝ \land k \in ℝ) \to k \in ℝ$
100	99	ltm1d	$⊢ (k - 1 \in ℝ \land k \in ℝ) \to k - 1 < k$
101		ltnle	$⊢ (k - 1 \in ℝ \land k \in ℝ) \to (k - 1 < k \leftrightarrow \neg k \leq k - 1)$
102	100 101	mpbid	$⊢ (k - 1 \in ℝ \land k \in ℝ) \to \neg k \leq k - 1$
103	98 97 102	syl2anc	$⊢ (k - 1 \in A \land k \in A) \to \neg k \leq k - 1$
104		breq2	$⊢ z = k - 1 \to (k \leq z \leftrightarrow k \leq k - 1)$
105	104	notbid	$⊢ z = k - 1 \to (\neg k \leq z \leftrightarrow \neg k \leq k - 1)$
106	105	rspcev	$⊢ (k - 1 \in A \land \neg k \leq k - 1) \to \exists z \in A \neg k \leq z$
107	103 106	syldan	$⊢ (k - 1 \in A \land k \in A) \to \exists z \in A \neg k \leq z$
108		rexnal	$⊢ \exists z \in A \neg k \leq z \leftrightarrow \neg \forall z \in A k \leq z$
109	107 108	sylib	$⊢ (k - 1 \in A \land k \in A) \to \neg \forall z \in A k \leq z$
110	109	ex	$⊢ k - 1 \in A \to (k \in A \to \neg \forall z \in A k \leq z)$
111		imnan	$⊢ (k \in A \to \neg \forall z \in A k \leq z) \leftrightarrow \neg (k \in A \land \forall z \in A k \leq z)$
112	110 111	sylib	$⊢ k - 1 \in A \to \neg (k \in A \land \forall z \in A k \leq z)$
113	112	con2i	$⊢ (k \in A \land \forall z \in A k \leq z) \to \neg k - 1 \in A$
114	113	ad2antlr	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to \neg k - 1 \in A$
115		breq2	$⊢ j = k - 1 \to (\frac{1}{D} < j \leftrightarrow \frac{1}{D} < k - 1)$
116	115 1	elrab2	$⊢ k - 1 \in A \leftrightarrow (k - 1 \in ℕ \land \frac{1}{D} < k - 1)$
117	114 116	sylnib	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to \neg (k - 1 \in ℕ \land \frac{1}{D} < k - 1)$
118		ianor	$⊢ \neg (k - 1 \in ℕ \land \frac{1}{D} < k - 1) \leftrightarrow (\neg k - 1 \in ℕ \lor \neg \frac{1}{D} < k - 1)$
119	117 118	sylib	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to (\neg k - 1 \in ℕ \lor \neg \frac{1}{D} < k - 1)$
120		imor	$⊢ (k - 1 \in ℕ \to \neg \frac{1}{D} < k - 1) \leftrightarrow (\neg k - 1 \in ℕ \lor \neg \frac{1}{D} < k - 1)$
121	119 120	sylibr	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to (k - 1 \in ℕ \to \neg \frac{1}{D} < k - 1)$
122	95 121	mpd	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to \neg \frac{1}{D} < k - 1$
123	82 86 122	nltled	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to k - 1 \leq \frac{1}{D}$
124		eluzelre	$⊢ k \in ℤ_{\geq 2} \to k \in ℝ$
125	124	adantl	$⊢ (φ \land k \in ℤ_{\geq 2}) \to k \in ℝ$
126	56	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to D \in ℝ$
127	125 126	remulcld	$⊢ (φ \land k \in ℤ_{\geq 2}) \to k D \in ℝ$
128	127	rehalfcld	$⊢ (φ \land k \in ℤ_{\geq 2}) \to \frac{k D}{2} \in ℝ$
129	128	3adant3	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to \frac{k D}{2} \in ℝ$
130	60 56	readdcld	$⊢ φ \to 1 + D \in ℝ$
131	130	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 1 + D \in ℝ$
132	131	rehalfcld	$⊢ (φ \land k \in ℤ_{\geq 2}) \to \frac{1 + D}{2} \in ℝ$
133	132	3adant3	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to \frac{1 + D}{2} \in ℝ$
134		1red	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to 1 \in ℝ$
135		eluzelcn	$⊢ k \in ℤ_{\geq 2} \to k \in ℂ$
136	135	adantl	$⊢ (φ \land k \in ℤ_{\geq 2}) \to k \in ℂ$
137	51	adantr	$⊢ (φ \land k \in ℤ_{\geq 2}) \to D \in ℂ$
138	136 137	mulcld	$⊢ (φ \land k \in ℤ_{\geq 2}) \to k D \in ℂ$
139	138	3adant3	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to k D \in ℂ$
140	51	3ad2ant1	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to D \in ℂ$
141	139 140	npcand	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to k D - D + D = k D$
142	127 126	resubcld	$⊢ (φ \land k \in ℤ_{\geq 2}) \to k D - D \in ℝ$
143	142	3adant3	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to k D - D \in ℝ$
144	56	3ad2ant1	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to D \in ℝ$
145		simp3	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to k - 1 \leq \frac{1}{D}$
146		1red	$⊢ k \in ℤ_{\geq 2} \to 1 \in ℝ$
147	124 146	resubcld	$⊢ k \in ℤ_{\geq 2} \to k - 1 \in ℝ$
148	147	3ad2ant2	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to k - 1 \in ℝ$
149	7	3ad2ant1	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to \frac{1}{D} \in ℝ$
150	42	3ad2ant1	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to (D \in ℝ \land 0 < D)$
151		lemul1	$⊢ (k - 1 \in ℝ \land \frac{1}{D} \in ℝ \land (D \in ℝ \land 0 < D)) \to (k - 1 \leq \frac{1}{D} \leftrightarrow (k - 1) D \leq (\frac{1}{D}) D)$
152	148 149 150 151	syl3anc	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to (k - 1 \leq \frac{1}{D} \leftrightarrow (k - 1) D \leq (\frac{1}{D}) D)$
153	145 152	mpbid	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to (k - 1) D \leq (\frac{1}{D}) D$
154		1cnd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 1 \in ℂ$
155	136 154 137	subdird	$⊢ (φ \land k \in ℤ_{\geq 2}) \to (k - 1) D = k D - 1 D$
156	137	mullidd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to 1 D = D$
157	156	oveq2d	$⊢ (φ \land k \in ℤ_{\geq 2}) \to k D - 1 D = k D - D$
158	155 157	eqtrd	$⊢ (φ \land k \in ℤ_{\geq 2}) \to (k - 1) D = k D - D$
159	158	3adant3	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to (k - 1) D = k D - D$
160		1cnd	$⊢ φ \to 1 \in ℂ$
161	160 51 84	3jca	$⊢ φ \to (1 \in ℂ \land D \in ℂ \land D \neq 0)$
162	161	3ad2ant1	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to (1 \in ℂ \land D \in ℂ \land D \neq 0)$
163		divcan1	$⊢ (1 \in ℂ \land D \in ℂ \land D \neq 0) \to (\frac{1}{D}) D = 1$
164	162 163	syl	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to (\frac{1}{D}) D = 1$
165	153 159 164	3brtr3d	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to k D - D \leq 1$
166	143 134 144 165	leadd1dd	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to k D - D + D \leq 1 + D$
167	141 166	eqbrtrrd	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to k D \leq 1 + D$
168	127	3adant3	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to k D \in ℝ$
169	130	3ad2ant1	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to 1 + D \in ℝ$
170	61 63	pm3.2i	$⊢ (2 \in ℝ \land 0 < 2)$
171	170	a1i	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to (2 \in ℝ \land 0 < 2)$
172		lediv1	$⊢ (k D \in ℝ \land 1 + D \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (k D \leq 1 + D \leftrightarrow \frac{k D}{2} \leq \frac{1 + D}{2})$
173	168 169 171 172	syl3anc	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to (k D \leq 1 + D \leftrightarrow \frac{k D}{2} \leq \frac{1 + D}{2})$
174	167 173	mpbid	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to \frac{k D}{2} \leq \frac{1 + D}{2}$
175	56 60 60 3	ltadd2dd	$⊢ φ \to 1 + D < 1 + 1$
176		1p1e2	$⊢ 1 + 1 = 2$
177	175 176	breqtrdi	$⊢ φ \to 1 + D < 2$
178		ltdiv1	$⊢ (1 + D \in ℝ \land 2 \in ℝ \land (2 \in ℝ \land 0 < 2)) \to (1 + D < 2 \leftrightarrow \frac{1 + D}{2} < \frac{2}{2})$
179	130 62 62 64 178	syl112anc	$⊢ φ \to (1 + D < 2 \leftrightarrow \frac{1 + D}{2} < \frac{2}{2})$
180	177 179	mpbid	$⊢ φ \to \frac{1 + D}{2} < \frac{2}{2}$
181		2div2e1	$⊢ \frac{2}{2} = 1$
182	180 181	breqtrdi	$⊢ φ \to \frac{1 + D}{2} < 1$
183	182	3ad2ant1	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to \frac{1 + D}{2} < 1$
184	129 133 134 174 183	lelttrd	$⊢ (φ \land k \in ℤ_{\geq 2} \land k - 1 \leq \frac{1}{D}) \to \frac{k D}{2} < 1$
185	74 80 123 184	syl3anc	$⊢ ((φ \land (k \in A \land \forall z \in A k \leq z)) \land \neg k = 1) \to \frac{k D}{2} < 1$
186	73 185	pm2.61dan	$⊢ (φ \land (k \in A \land \forall z \in A k \leq z)) \to \frac{k D}{2} < 1$
187	24 48 186	jca32	$⊢ (φ \land (k \in A \land \forall z \in A k \leq z)) \to (k \in ℕ \land (1 < k D \land \frac{k D}{2} < 1))$
188	187	ex	$⊢ φ \to ((k \in A \land \forall z \in A k \leq z) \to (k \in ℕ \land (1 < k D \land \frac{k D}{2} < 1)))$
189	188	eximdv	$⊢ φ \to (\exists k (k \in A \land \forall z \in A k \leq z) \to \exists k (k \in ℕ \land (1 < k D \land \frac{k D}{2} < 1)))$
190	21 189	mpd	$⊢ φ \to \exists k (k \in ℕ \land (1 < k D \land \frac{k D}{2} < 1))$
191		df-rex	$⊢ \exists k \in ℕ (1 < k D \land \frac{k D}{2} < 1) \leftrightarrow \exists k (k \in ℕ \land (1 < k D \land \frac{k D}{2} < 1))$
192	190 191	sylibr	$⊢ φ \to \exists k \in ℕ (1 < k D \land \frac{k D}{2} < 1)$

Metamath Proof Explorer

Theorem stoweidlem14

Proof