Theorem 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	⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
	rpnnen1lem.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
	rpnnen1lem.n	⊢ ℕ ∈ V
	rpnnen1lem.q	⊢ ℚ ∈ V
Assertion	rpnnen1lem1	⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) )

Proof

Step	Hyp	Ref	Expression
1		rpnnen1lem.1	⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
2		rpnnen1lem.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
3		rpnnen1lem.n	⊢ ℕ ∈ V
4		rpnnen1lem.q	⊢ ℚ ∈ V
5	3	mptex	⊢ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ∈ V
6	2	fvmpt2	⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ∈ V ) → ( 𝐹 ‘ 𝑥 ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
7	5 6	mpan2	⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
8		ssrab2	⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ⊆ ℤ
9	1 8	eqsstri	⊢ 𝑇 ⊆ ℤ
10	9	a1i	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ⊆ ℤ )
11		nnre	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
12		remulcl	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
13	12	ancoms	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
14	11 13	sylan2	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
15		btwnz	⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ( ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑘 · 𝑥 ) < 𝑛 ) )
16	15	simpld	⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
17	14 16	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
18		zre	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℝ )
19	18	adantl	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℝ )
20		simpll	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℝ )
21		nngt0	⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
22	11 21	jca	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
23	22	ad2antlr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
24		ltdivmul	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
25	19 20 23 24	syl3anc	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
26	25	rexbidva	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 ↔ ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ) )
27	17 26	mpbird	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
28		rabn0	⊢ ( { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
29	27 28	sylibr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
30	1	neeq1i	⊢ ( 𝑇 ≠ ∅ ↔ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
31	29 30	sylibr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ≠ ∅ )
32	1	rabeq2i	⊢ ( 𝑛 ∈ 𝑇 ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) )
33	11	ad2antlr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑘 ∈ ℝ )
34	33 20 12	syl2anc	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
35		ltle	⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑘 · 𝑥 ) ∈ ℝ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
36	19 34 35	syl2anc	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
37	25 36	sylbid	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
38	37	impr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
39	32 38	sylan2b	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑇 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
40	39	ralrimiva	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) )
41		breq2	⊢ ( 𝑦 = ( 𝑘 · 𝑥 ) → ( 𝑛 ≤ 𝑦 ↔ 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
42	41	ralbidv	⊢ ( 𝑦 = ( 𝑘 · 𝑥 ) → ( ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
43	42	rspcev	⊢ ( ( ( 𝑘 · 𝑥 ) ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
44	14 40 43	syl2anc	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
45		suprzcl	⊢ ( ( 𝑇 ⊆ ℤ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
46	10 31 44 45	syl3anc	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
47	9 46	sselid	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℤ )
48		znq	⊢ ( ( sup ( 𝑇 , ℝ , < ) ∈ ℤ ∧ 𝑘 ∈ ℕ ) → ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ∈ ℚ )
49	47 48	sylancom	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ∈ ℚ )
50		eqid	⊢ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
51	49 50	fmptd	⊢ ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) : ℕ ⟶ ℚ )
52	4 3	elmap	⊢ ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ∈ ( ℚ ↑m ℕ ) ↔ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) : ℕ ⟶ ℚ )
53	51 52	sylibr	⊢ ( 𝑥 ∈ ℝ → ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ∈ ( ℚ ↑m ℕ ) )
54	7 53	eqeltrd	⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) )