rpnnen1lem2

	Ref	Expression
Hypotheses	rpnnen1lem.1	$⊢ T = \{n \in ℤ \| \frac{n}{k} < x\}$
	rpnnen1lem.2	$⊢ F = (x \in ℝ ⟼ (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}))$
Assertion	rpnnen1lem2	$⊢ (x \in ℝ \land k \in ℕ) \to sup (T ℝ <) \in ℤ$

Proof

Step	Hyp	Ref	Expression
1		rpnnen1lem.1	$⊢ T = \{n \in ℤ \| \frac{n}{k} < x\}$
2		rpnnen1lem.2	$⊢ F = (x \in ℝ ⟼ (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}))$
3	1	ssrab3	$⊢ T \subseteq ℤ$
4		nnre	$⊢ k \in ℕ \to k \in ℝ$
5		remulcl	$⊢ (k \in ℝ \land x \in ℝ) \to k x \in ℝ$
6	5	ancoms	$⊢ (x \in ℝ \land k \in ℝ) \to k x \in ℝ$
7	4 6	sylan2	$⊢ (x \in ℝ \land k \in ℕ) \to k x \in ℝ$
8		btwnz	$⊢ k x \in ℝ \to (\exists n \in ℤ n < k x \land \exists n \in ℤ k x < n)$
9	8	simpld	$⊢ k x \in ℝ \to \exists n \in ℤ n < k x$
10	7 9	syl	$⊢ (x \in ℝ \land k \in ℕ) \to \exists n \in ℤ n < k x$
11		zre	$⊢ n \in ℤ \to n \in ℝ$
12	11	adantl	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to n \in ℝ$
13		simpll	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to x \in ℝ$
14		nngt0	$⊢ k \in ℕ \to 0 < k$
15	4 14	jca	$⊢ k \in ℕ \to (k \in ℝ \land 0 < k)$
16	15	ad2antlr	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (k \in ℝ \land 0 < k)$
17		ltdivmul	$⊢ (n \in ℝ \land x \in ℝ \land (k \in ℝ \land 0 < k)) \to (\frac{n}{k} < x \leftrightarrow n < k x)$
18	12 13 16 17	syl3anc	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (\frac{n}{k} < x \leftrightarrow n < k x)$
19	18	rexbidva	$⊢ (x \in ℝ \land k \in ℕ) \to (\exists n \in ℤ \frac{n}{k} < x \leftrightarrow \exists n \in ℤ n < k x)$
20	10 19	mpbird	$⊢ (x \in ℝ \land k \in ℕ) \to \exists n \in ℤ \frac{n}{k} < x$
21		rabn0	$⊢ \{n \in ℤ \| \frac{n}{k} < x\} \neq \emptyset \leftrightarrow \exists n \in ℤ \frac{n}{k} < x$
22	20 21	sylibr	$⊢ (x \in ℝ \land k \in ℕ) \to \{n \in ℤ \| \frac{n}{k} < x\} \neq \emptyset$
23	1	neeq1i	$⊢ T \neq \emptyset \leftrightarrow \{n \in ℤ \| \frac{n}{k} < x\} \neq \emptyset$
24	22 23	sylibr	$⊢ (x \in ℝ \land k \in ℕ) \to T \neq \emptyset$
25	1	rabeq2i	$⊢ n \in T \leftrightarrow (n \in ℤ \land \frac{n}{k} < x)$
26	4	ad2antlr	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to k \in ℝ$
27	26 13 5	syl2anc	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to k x \in ℝ$
28		ltle	$⊢ (n \in ℝ \land k x \in ℝ) \to (n < k x \to n \leq k x)$
29	12 27 28	syl2anc	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (n < k x \to n \leq k x)$
30	18 29	sylbid	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (\frac{n}{k} < x \to n \leq k x)$
31	30	impr	$⊢ ((x \in ℝ \land k \in ℕ) \land (n \in ℤ \land \frac{n}{k} < x)) \to n \leq k x$
32	25 31	sylan2b	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in T) \to n \leq k x$
33	32	ralrimiva	$⊢ (x \in ℝ \land k \in ℕ) \to \forall n \in T n \leq k x$
34		brralrspcev	$⊢ (k x \in ℝ \land \forall n \in T n \leq k x) \to \exists y \in ℝ \forall n \in T n \leq y$
35	7 33 34	syl2anc	$⊢ (x \in ℝ \land k \in ℕ) \to \exists y \in ℝ \forall n \in T n \leq y$
36		suprzcl	$⊢ (T \subseteq ℤ \land T \neq \emptyset \land \exists y \in ℝ \forall n \in T n \leq y) \to sup (T ℝ <) \in T$
37	3 24 35 36	mp3an2i	$⊢ (x \in ℝ \land k \in ℕ) \to sup (T ℝ <) \in T$
38	3 37	sseldi	$⊢ (x \in ℝ \land k \in ℕ) \to sup (T ℝ <) \in ℤ$

Metamath Proof Explorer

Theorem rpnnen1lem2

Proof