recnnltrp

Description: N is a natural number large enough that its reciprocal is smaller than the given positive E . (Contributed by Glauco Siliprandi, 8-Apr-2021)

		Ref	Expression
	Hypothesis	recnnltrp.1	⊢ 𝑁 = ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 )
	Assertion	recnnltrp	⊢ ( 𝐸 ∈ ℝ⁺ → ( 𝑁 ∈ ℕ ∧ ( 1 / 𝑁 ) < 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		recnnltrp.1	⊢ 𝑁 = ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 )
2		rpreccl	⊢ ( 𝐸 ∈ ℝ⁺ → ( 1 / 𝐸 ) ∈ ℝ⁺ )
3	2	rpred	⊢ ( 𝐸 ∈ ℝ⁺ → ( 1 / 𝐸 ) ∈ ℝ )
4	2	rpge0d	⊢ ( 𝐸 ∈ ℝ⁺ → 0 ≤ ( 1 / 𝐸 ) )
5		flge0nn0	⊢ ( ( ( 1 / 𝐸 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐸 ) ) → ( ⌊ ‘ ( 1 / 𝐸 ) ) ∈ ℕ₀ )
6	3 4 5	syl2anc	⊢ ( 𝐸 ∈ ℝ⁺ → ( ⌊ ‘ ( 1 / 𝐸 ) ) ∈ ℕ₀ )
7		nn0p1nn	⊢ ( ( ⌊ ‘ ( 1 / 𝐸 ) ) ∈ ℕ₀ → ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 ) ∈ ℕ )
8	6 7	syl	⊢ ( 𝐸 ∈ ℝ⁺ → ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 ) ∈ ℕ )
9	1 8	eqeltrid	⊢ ( 𝐸 ∈ ℝ⁺ → 𝑁 ∈ ℕ )
10		flltp1	⊢ ( ( 1 / 𝐸 ) ∈ ℝ → ( 1 / 𝐸 ) < ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 ) )
11	3 10	syl	⊢ ( 𝐸 ∈ ℝ⁺ → ( 1 / 𝐸 ) < ( ( ⌊ ‘ ( 1 / 𝐸 ) ) + 1 ) )
12	11 1	breqtrrdi	⊢ ( 𝐸 ∈ ℝ⁺ → ( 1 / 𝐸 ) < 𝑁 )
13	9	nnrpd	⊢ ( 𝐸 ∈ ℝ⁺ → 𝑁 ∈ ℝ⁺ )
14	2 13	ltrecd	⊢ ( 𝐸 ∈ ℝ⁺ → ( ( 1 / 𝐸 ) < 𝑁 ↔ ( 1 / 𝑁 ) < ( 1 / ( 1 / 𝐸 ) ) ) )
15	12 14	mpbid	⊢ ( 𝐸 ∈ ℝ⁺ → ( 1 / 𝑁 ) < ( 1 / ( 1 / 𝐸 ) ) )
16		rpcn	⊢ ( 𝐸 ∈ ℝ⁺ → 𝐸 ∈ ℂ )
17		rpne0	⊢ ( 𝐸 ∈ ℝ⁺ → 𝐸 ≠ 0 )
18	16 17	recrecd	⊢ ( 𝐸 ∈ ℝ⁺ → ( 1 / ( 1 / 𝐸 ) ) = 𝐸 )
19	15 18	breqtrd	⊢ ( 𝐸 ∈ ℝ⁺ → ( 1 / 𝑁 ) < 𝐸 )
20	9 19	jca	⊢ ( 𝐸 ∈ ℝ⁺ → ( 𝑁 ∈ ℕ ∧ ( 1 / 𝑁 ) < 𝐸 ) )

Metamath Proof Explorer

Theorem recnnltrp

Proof