rpnnen1lem3

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	rpnnen1lem3	$⊢ x \in ℝ \to \forall n \in ran F (x) n \leq x$

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	7	fveq1d	$⊢ x \in ℝ \to F (x) (k) = (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) (k)$
9		ovex	$⊢ \frac{sup (T ℝ <)}{k} \in V$
10		eqid	$⊢ (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) = (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k})$
11	10	fvmpt2	$⊢ (k \in ℕ \land \frac{sup (T ℝ <)}{k} \in V) \to (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) (k) = \frac{sup (T ℝ <)}{k}$
12	9 11	mpan2	$⊢ k \in ℕ \to (k \in ℕ ⟼ \frac{sup (T ℝ <)}{k}) (k) = \frac{sup (T ℝ <)}{k}$
13	8 12	sylan9eq	$⊢ (x \in ℝ \land k \in ℕ) \to F (x) (k) = \frac{sup (T ℝ <)}{k}$
14	1	reqabi	$⊢ n \in T \leftrightarrow (n \in ℤ \land \frac{n}{k} < x)$
15		zre	$⊢ n \in ℤ \to n \in ℝ$
16	15	adantl	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to n \in ℝ$
17		simpll	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to x \in ℝ$
18		nnre	$⊢ k \in ℕ \to k \in ℝ$
19		nngt0	$⊢ k \in ℕ \to 0 < k$
20	18 19	jca	$⊢ k \in ℕ \to (k \in ℝ \land 0 < k)$
21	20	ad2antlr	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (k \in ℝ \land 0 < k)$
22		ltdivmul	$⊢ (n \in ℝ \land x \in ℝ \land (k \in ℝ \land 0 < k)) \to (\frac{n}{k} < x \leftrightarrow n < k x)$
23	16 17 21 22	syl3anc	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (\frac{n}{k} < x \leftrightarrow n < k x)$
24	18	ad2antlr	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to k \in ℝ$
25		remulcl	$⊢ (k \in ℝ \land x \in ℝ) \to k x \in ℝ$
26	24 17 25	syl2anc	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to k x \in ℝ$
27		ltle	$⊢ (n \in ℝ \land k x \in ℝ) \to (n < k x \to n \leq k x)$
28	16 26 27	syl2anc	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (n < k x \to n \leq k x)$
29	23 28	sylbid	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in ℤ) \to (\frac{n}{k} < x \to n \leq k x)$
30	29	impr	$⊢ ((x \in ℝ \land k \in ℕ) \land (n \in ℤ \land \frac{n}{k} < x)) \to n \leq k x$
31	14 30	sylan2b	$⊢ ((x \in ℝ \land k \in ℕ) \land n \in T) \to n \leq k x$
32	31	ralrimiva	$⊢ (x \in ℝ \land k \in ℕ) \to \forall n \in T n \leq k x$
33		ssrab2	$⊢ \{n \in ℤ \| \frac{n}{k} < x\} \subseteq ℤ$
34	1 33	eqsstri	$⊢ T \subseteq ℤ$
35		zssre	$⊢ ℤ \subseteq ℝ$
36	34 35	sstri	$⊢ T \subseteq ℝ$
37	36	a1i	$⊢ (x \in ℝ \land k \in ℕ) \to T \subseteq ℝ$
38	25	ancoms	$⊢ (x \in ℝ \land k \in ℝ) \to k x \in ℝ$
39	18 38	sylan2	$⊢ (x \in ℝ \land k \in ℕ) \to k x \in ℝ$
40		btwnz	$⊢ k x \in ℝ \to (\exists n \in ℤ n < k x \land \exists n \in ℤ k x < n)$
41	40	simpld	$⊢ k x \in ℝ \to \exists n \in ℤ n < k x$
42	39 41	syl	$⊢ (x \in ℝ \land k \in ℕ) \to \exists n \in ℤ n < k x$
43	23	rexbidva	$⊢ (x \in ℝ \land k \in ℕ) \to (\exists n \in ℤ \frac{n}{k} < x \leftrightarrow \exists n \in ℤ n < k x)$
44	42 43	mpbird	$⊢ (x \in ℝ \land k \in ℕ) \to \exists n \in ℤ \frac{n}{k} < x$
45		rabn0	$⊢ \{n \in ℤ \| \frac{n}{k} < x\} \neq \emptyset \leftrightarrow \exists n \in ℤ \frac{n}{k} < x$
46	44 45	sylibr	$⊢ (x \in ℝ \land k \in ℕ) \to \{n \in ℤ \| \frac{n}{k} < x\} \neq \emptyset$
47	1	neeq1i	$⊢ T \neq \emptyset \leftrightarrow \{n \in ℤ \| \frac{n}{k} < x\} \neq \emptyset$
48	46 47	sylibr	$⊢ (x \in ℝ \land k \in ℕ) \to T \neq \emptyset$
49		breq2	$⊢ y = k x \to (n \leq y \leftrightarrow n \leq k x)$
50	49	ralbidv	$⊢ y = k x \to (\forall n \in T n \leq y \leftrightarrow \forall n \in T n \leq k x)$
51	50	rspcev	$⊢ (k x \in ℝ \land \forall n \in T n \leq k x) \to \exists y \in ℝ \forall n \in T n \leq y$
52	39 32 51	syl2anc	$⊢ (x \in ℝ \land k \in ℕ) \to \exists y \in ℝ \forall n \in T n \leq y$
53		suprleub	$⊢ ((T \subseteq ℝ \land T \neq \emptyset \land \exists y \in ℝ \forall n \in T n \leq y) \land k x \in ℝ) \to (sup (T ℝ <) \leq k x \leftrightarrow \forall n \in T n \leq k x)$
54	37 48 52 39 53	syl31anc	$⊢ (x \in ℝ \land k \in ℕ) \to (sup (T ℝ <) \leq k x \leftrightarrow \forall n \in T n \leq k x)$
55	32 54	mpbird	$⊢ (x \in ℝ \land k \in ℕ) \to sup (T ℝ <) \leq k x$
56	1 2	rpnnen1lem2	$⊢ (x \in ℝ \land k \in ℕ) \to sup (T ℝ <) \in ℤ$
57	56	zred	$⊢ (x \in ℝ \land k \in ℕ) \to sup (T ℝ <) \in ℝ$
58		simpl	$⊢ (x \in ℝ \land k \in ℕ) \to x \in ℝ$
59	20	adantl	$⊢ (x \in ℝ \land k \in ℕ) \to (k \in ℝ \land 0 < k)$
60		ledivmul	$⊢ (sup (T ℝ <) \in ℝ \land x \in ℝ \land (k \in ℝ \land 0 < k)) \to (\frac{sup (T ℝ <)}{k} \leq x \leftrightarrow sup (T ℝ <) \leq k x)$
61	57 58 59 60	syl3anc	$⊢ (x \in ℝ \land k \in ℕ) \to (\frac{sup (T ℝ <)}{k} \leq x \leftrightarrow sup (T ℝ <) \leq k x)$
62	55 61	mpbird	$⊢ (x \in ℝ \land k \in ℕ) \to \frac{sup (T ℝ <)}{k} \leq x$
63	13 62	eqbrtrd	$⊢ (x \in ℝ \land k \in ℕ) \to F (x) (k) \leq x$
64	63	ralrimiva	$⊢ x \in ℝ \to \forall k \in ℕ F (x) (k) \leq x$
65	1 2 3 4	rpnnen1lem1	$⊢ x \in ℝ \to F (x) \in (ℚ^{ℕ})$
66	4 3	elmap	$⊢ F (x) \in (ℚ^{ℕ}) \leftrightarrow F (x) : ℕ ⟶ ℚ$
67	65 66	sylib	$⊢ x \in ℝ \to F (x) : ℕ ⟶ ℚ$
68		ffn	$⊢ F (x) : ℕ ⟶ ℚ \to F (x) Fn ℕ$
69		breq1	$⊢ n = F (x) (k) \to (n \leq x \leftrightarrow F (x) (k) \leq x)$
70	69	ralrn	$⊢ F (x) Fn ℕ \to (\forall n \in ran F (x) n \leq x \leftrightarrow \forall k \in ℕ F (x) (k) \leq x)$
71	67 68 70	3syl	$⊢ x \in ℝ \to (\forall n \in ran F (x) n \leq x \leftrightarrow \forall k \in ℕ F (x) (k) \leq x)$
72	64 71	mpbird	$⊢ x \in ℝ \to \forall n \in ran F (x) n \leq x$

Metamath Proof Explorer

Theorem rpnnen1lem3

Proof