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

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	7	fveq1d	⊢ ( 𝑥 ∈ ℝ → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) = ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ‘ 𝑘 ) )
9		ovex	⊢ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ∈ V
10		eqid	⊢ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) = ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
11	10	fvmpt2	⊢ ( ( 𝑘 ∈ ℕ ∧ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ∈ V ) → ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ‘ 𝑘 ) = ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
12	9 11	mpan2	⊢ ( 𝑘 ∈ ℕ → ( ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) ‘ 𝑘 ) = ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
13	8 12	sylan9eq	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) = ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) )
14	1	rabeq2i	⊢ ( 𝑛 ∈ 𝑇 ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) )
15		zre	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℝ )
16	15	adantl	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℝ )
17		simpll	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℝ )
18		nnre	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
19		nngt0	⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
20	18 19	jca	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
21	20	ad2antlr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
22		ltdivmul	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
23	16 17 21 22	syl3anc	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
24	18	ad2antlr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑘 ∈ ℝ )
25		remulcl	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
26	24 17 25	syl2anc	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
27		ltle	⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑘 · 𝑥 ) ∈ ℝ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
28	16 26 27	syl2anc	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
29	23 28	sylbid	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
30	29	impr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
31	14 30	sylan2b	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑇 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
32	31	ralrimiva	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) )
33		ssrab2	⊢ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ⊆ ℤ
34	1 33	eqsstri	⊢ 𝑇 ⊆ ℤ
35		zssre	⊢ ℤ ⊆ ℝ
36	34 35	sstri	⊢ 𝑇 ⊆ ℝ
37	36	a1i	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ⊆ ℝ )
38	25	ancoms	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
39	18 38	sylan2	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
40		btwnz	⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ( ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑘 · 𝑥 ) < 𝑛 ) )
41	40	simpld	⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
42	39 41	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
43	23	rexbidva	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 ↔ ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ) )
44	42 43	mpbird	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
45		rabn0	⊢ ( { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
46	44 45	sylibr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
47	1	neeq1i	⊢ ( 𝑇 ≠ ∅ ↔ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
48	46 47	sylibr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ≠ ∅ )
49		breq2	⊢ ( 𝑦 = ( 𝑘 · 𝑥 ) → ( 𝑛 ≤ 𝑦 ↔ 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
50	49	ralbidv	⊢ ( 𝑦 = ( 𝑘 · 𝑥 ) → ( ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ↔ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
51	50	rspcev	⊢ ( ( ( 𝑘 · 𝑥 ) ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
52	39 32 51	syl2anc	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
53		suprleub	⊢ ( ( ( 𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ) ∧ ( 𝑘 · 𝑥 ) ∈ ℝ ) → ( sup ( 𝑇 , ℝ , < ) ≤ ( 𝑘 · 𝑥 ) ↔ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
54	37 48 52 39 53	syl31anc	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( sup ( 𝑇 , ℝ , < ) ≤ ( 𝑘 · 𝑥 ) ↔ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
55	32 54	mpbird	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ≤ ( 𝑘 · 𝑥 ) )
56	1 2	rpnnen1lem2	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℤ )
57	56	zred	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℝ )
58		simpl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑥 ∈ ℝ )
59	20	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
60		ledivmul	⊢ ( ( sup ( 𝑇 , ℝ , < ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ≤ 𝑥 ↔ sup ( 𝑇 , ℝ , < ) ≤ ( 𝑘 · 𝑥 ) ) )
61	57 58 59 60	syl3anc	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ≤ 𝑥 ↔ sup ( 𝑇 , ℝ , < ) ≤ ( 𝑘 · 𝑥 ) ) )
62	55 61	mpbird	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ≤ 𝑥 )
63	13 62	eqbrtrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ 𝑥 )
64	63	ralrimiva	⊢ ( 𝑥 ∈ ℝ → ∀ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ 𝑥 )
65	1 2 3 4	rpnnen1lem1	⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) )
66	4 3	elmap	⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ ( ℚ ↑m ℕ ) ↔ ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ )
67	65 66	sylib	⊢ ( 𝑥 ∈ ℝ → ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ )
68		ffn	⊢ ( ( 𝐹 ‘ 𝑥 ) : ℕ ⟶ ℚ → ( 𝐹 ‘ 𝑥 ) Fn ℕ )
69		breq1	⊢ ( 𝑛 = ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) → ( 𝑛 ≤ 𝑥 ↔ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ 𝑥 ) )
70	69	ralrn	⊢ ( ( 𝐹 ‘ 𝑥 ) Fn ℕ → ( ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ 𝑥 ) )
71	67 68 70	3syl	⊢ ( 𝑥 ∈ ℝ → ( ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 ↔ ∀ 𝑘 ∈ ℕ ( ( 𝐹 ‘ 𝑥 ) ‘ 𝑘 ) ≤ 𝑥 ) )
72	64 71	mpbird	⊢ ( 𝑥 ∈ ℝ → ∀ 𝑛 ∈ ran ( 𝐹 ‘ 𝑥 ) 𝑛 ≤ 𝑥 )