Theorem rpnnen1lem2

Description: Lemma for rpnnen1 . (Contributed by Mario Carneiro, 12-May-2013)

	Ref	Expression
Hypotheses	rpnnen1lem.1	⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
	rpnnen1lem.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
Assertion	rpnnen1lem2	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℤ )

Proof

Step	Hyp	Ref	Expression
1		rpnnen1lem.1	⊢ 𝑇 = { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 }
2		rpnnen1lem.2	⊢ 𝐹 = ( 𝑥 ∈ ℝ ↦ ( 𝑘 ∈ ℕ ↦ ( sup ( 𝑇 , ℝ , < ) / 𝑘 ) ) )
3	1	ssrab3	⊢ 𝑇 ⊆ ℤ
4		nnre	⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
5		remulcl	⊢ ( ( 𝑘 ∈ ℝ ∧ 𝑥 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
6	5	ancoms	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℝ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
7	4 6	sylan2	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
8		btwnz	⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ( ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ∧ ∃ 𝑛 ∈ ℤ ( 𝑘 · 𝑥 ) < 𝑛 ) )
9	8	simpld	⊢ ( ( 𝑘 · 𝑥 ) ∈ ℝ → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
10	7 9	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) )
11		zre	⊢ ( 𝑛 ∈ ℤ → 𝑛 ∈ ℝ )
12	11	adantl	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑛 ∈ ℝ )
13		simpll	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑥 ∈ ℝ )
14		nngt0	⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
15	4 14	jca	⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
16	15	ad2antlr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
17		ltdivmul	⊢ ( ( 𝑛 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
18	12 13 16 17	syl3anc	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 ↔ 𝑛 < ( 𝑘 · 𝑥 ) ) )
19	18	rexbidva	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 ↔ ∃ 𝑛 ∈ ℤ 𝑛 < ( 𝑘 · 𝑥 ) ) )
20	10 19	mpbird	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
21		rabn0	⊢ ( { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ ↔ ∃ 𝑛 ∈ ℤ ( 𝑛 / 𝑘 ) < 𝑥 )
22	20 21	sylibr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
23	1	neeq1i	⊢ ( 𝑇 ≠ ∅ ↔ { 𝑛 ∈ ℤ ∣ ( 𝑛 / 𝑘 ) < 𝑥 } ≠ ∅ )
24	22 23	sylibr	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → 𝑇 ≠ ∅ )
25	1	rabeq2i	⊢ ( 𝑛 ∈ 𝑇 ↔ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) )
26	4	ad2antlr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → 𝑘 ∈ ℝ )
27	26 13 5	syl2anc	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑘 · 𝑥 ) ∈ ℝ )
28		ltle	⊢ ( ( 𝑛 ∈ ℝ ∧ ( 𝑘 · 𝑥 ) ∈ ℝ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
29	12 27 28	syl2anc	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( 𝑛 < ( 𝑘 · 𝑥 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
30	18 29	sylbid	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ ℤ ) → ( ( 𝑛 / 𝑘 ) < 𝑥 → 𝑛 ≤ ( 𝑘 · 𝑥 ) ) )
31	30	impr	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ℤ ∧ ( 𝑛 / 𝑘 ) < 𝑥 ) ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
32	25 31	sylan2b	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) ∧ 𝑛 ∈ 𝑇 ) → 𝑛 ≤ ( 𝑘 · 𝑥 ) )
33	32	ralrimiva	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) )
34		brralrspcev	⊢ ( ( ( 𝑘 · 𝑥 ) ∈ ℝ ∧ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ ( 𝑘 · 𝑥 ) ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
35	7 33 34	syl2anc	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 )
36		suprzcl	⊢ ( ( 𝑇 ⊆ ℤ ∧ 𝑇 ≠ ∅ ∧ ∃ 𝑦 ∈ ℝ ∀ 𝑛 ∈ 𝑇 𝑛 ≤ 𝑦 ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
37	3 24 35 36	mp3an2i	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ 𝑇 )
38	3 37	sselid	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → sup ( 𝑇 , ℝ , < ) ∈ ℤ )