rpnnen1lem1

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013) (Revised by NM, 13-Aug-2021) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	rpnnen1lem.1	$⊢ T = \{n \in ℤ \| \frac{n}{k} < x\}$
	rpnnen1lem.2	$⊢ F = (x \in ℝ ⟼ (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}))$
	rpnnen1lem.n	$⊢ ℕ \in V$
	rpnnen1lem.q	$⊢ ℚ \in V$
Assertion	rpnnen1lem1	$⊢ x \in ℝ \to F (x) \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		rpnnen1lem.n	$⊢ ℕ \in V$
4		rpnnen1lem.q	$⊢ ℚ \in V$
5	3	mptex	$⊢ (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) \in V$
6	2	fvmpt2	$⊢ (x \in ℝ \land (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) \in V) \to F (x) = (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k})$
7	5 6	mpan2	$⊢ x \in ℝ \to F (x) = (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k})$
8		ssrab2	$⊢ \{n \in ℤ \| \frac{n}{k} < x\} \subseteq ℤ$
9	1 8	eqsstri	$⊢ T \subseteq ℤ$
10	9	a1i	$⊢ (x \in ℝ \land k \in ℕ) \to T \subseteq ℤ$
11		nnre	$⊢ k \in ℕ \to k \in ℝ$
12		remulcl	$⊢ (k \in ℝ \land x \in ℝ) \to k x \in ℝ$
13	12	ancoms	$⊢ (x \in ℝ \land k \in ℝ) \to k x \in ℝ$
14	11 13	sylan2	$⊢ (x \in ℝ \land k \in ℕ) \to k x \in ℝ$
15		btwnz	$⊢ k x \in ℝ \to (\exists n \in ℤ n < k x \land \exists n \in ℤ k x < n)$
16	15	simpld	$⊢ k x \in ℝ \to \exists n \in ℤ n < k x$
17	14 16	syl	$⊢ (x \in ℝ \land k \in ℕ) \to \exists n \in ℤ n < k x$
18		zre	$⊢ n \in ℤ \to n \in ℝ$
19	18	adantl	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to n \in ℝ$
20		simpll	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to x \in ℝ$
21		nngt0	$⊢ k \in ℕ \to 0 < k$
22	11 21	jca	$⊢ k \in ℕ \to (k \in ℝ \land 0 < k)$
23	22	ad2antlr	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (k \in ℝ \land 0 < k)$
24		ltdivmul	$⊢ (n \in ℝ \land x \in ℝ \land (k \in ℝ \land 0 < k)) \to (\frac{n}{k} < x \leftrightarrow n < k x)$
25	19 20 23 24	syl3anc	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (\frac{n}{k} < x \leftrightarrow n < k x)$
26	25	rexbidva	$⊢ (x \in ℝ \land k \in ℕ) \to (\exists n \in ℤ \frac{n}{k} < x \leftrightarrow \exists n \in ℤ n < k x)$
27	17 26	mpbird	$⊢ (x \in ℝ \land k \in ℕ) \to \exists n \in ℤ \frac{n}{k} < x$
28		rabn0	$⊢ \{n \in ℤ \| \frac{n}{k} < x\} \neq \emptyset \leftrightarrow \exists n \in ℤ \frac{n}{k} < x$
29	27 28	sylibr	$⊢ (x \in ℝ \land k \in ℕ) \to \{n \in ℤ \| \frac{n}{k} < x\} \neq \emptyset$
30	1	neeq1i	$⊢ T \neq \emptyset \leftrightarrow \{n \in ℤ \| \frac{n}{k} < x\} \neq \emptyset$
31	29 30	sylibr	$⊢ (x \in ℝ \land k \in ℕ) \to T \neq \emptyset$
32	1	rabeq2i	$⊢ n \in T \leftrightarrow (n \in ℤ \land \frac{n}{k} < x)$
33	11	ad2antlr	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to k \in ℝ$
34	33 20 12	syl2anc	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to k x \in ℝ$
35		ltle	$⊢ (n \in ℝ \land k x \in ℝ) \to (n < k x \to n \leq k x)$
36	19 34 35	syl2anc	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (n < k x \to n \leq k x)$
37	25 36	sylbid	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (\frac{n}{k} < x \to n \leq k x)$
38	37	impr	$⊢ ((x \in ℝ \land k \in ℕ) \land (n \in ℤ \land \frac{n}{k} < x)) \to n \leq k x$
39	32 38	sylan2b	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in T) \to n \leq k x$
40	39	ralrimiva	$⊢ (x \in ℝ \land k \in ℕ) \to \forall n \in T n \leq k x$
41		breq2	$⊢ y = k x \to (n \leq y \leftrightarrow n \leq k x)$
42	41	ralbidv	$⊢ y = k x \to (\forall n \in T n \leq y \leftrightarrow \forall n \in T n \leq k x)$
43	42	rspcev	$⊢ (k x \in ℝ \land \forall n \in T n \leq k x) \to \exists y \in ℝ \forall n \in T n \leq y$
44	14 40 43	syl2anc	$⊢ (x \in ℝ \land k \in ℕ) \to \exists y \in ℝ \forall n \in T n \leq y$
45		suprzcl	$⊢ (T \subseteq ℤ \land T \neq \emptyset \land \exists y \in ℝ \forall n \in T n \leq y) \to sup (T ℝ <) \in T$
46	10 31 44 45	syl3anc	$⊢ (x \in ℝ \land k \in ℕ) \to sup (T ℝ <) \in T$
47	9 46	sselid	$⊢ (x \in ℝ \land k \in ℕ) \to sup (T ℝ <) \in ℤ$
48		znq	$⊢ (sup (T ℝ <) \in ℤ \land k \in ℕ) \to \frac{sup (T ℝ <)}{k} \in ℚ$
49	47 48	sylancom	$⊢ (x \in ℝ \land k \in ℕ) \to \frac{sup (T ℝ <)}{k} \in ℚ$
50		eqid	$⊢ (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) = (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k})$
51	49 50	fmptd	$⊢ x \in ℝ \to (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) : ℕ ⟶ ℚ$
52	4 3	elmap	$⊢ (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) \in (ℚ^{ℕ}) \leftrightarrow (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) : ℕ ⟶ ℚ$
53	51 52	sylibr	$⊢ x \in ℝ \to (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) \in (ℚ^{ℕ})$
54	7 53	eqeltrd	$⊢ x \in ℝ \to F (x) \in (ℚ^{ℕ})$

Metamath Proof Explorer

Theorem rpnnen1lem1

Proof