Metamath Proof Explorer

Theorem rpgtrecnn

Description: Any positive real number is greater than the reciprocal of a positive integer. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Assertion rpgtrecnn ( 𝐴 ∈ ℝ+ → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝐴 )

Proof

Step Hyp Ref Expression
1 rpreccl ⊢ ( 𝐴 ∈ ℝ+ → ( 1 / 𝐴 ) ∈ ℝ+ )
2 1 rpred ⊢ ( 𝐴 ∈ ℝ+ → ( 1 / 𝐴 ) ∈ ℝ )
3 1 rpge0d ⊢ ( 𝐴 ∈ ℝ+ → 0 ≤ ( 1 / 𝐴 ) )
4 flge0nn0 ⊢ ( ( ( 1 / 𝐴 ) ∈ ℝ ∧ 0 ≤ ( 1 / 𝐴 ) ) → ( ⌊ ‘ ( 1 / 𝐴 ) ) ∈ ℕ0 )
5 2 3 4 syl2anc ⊢ ( 𝐴 ∈ ℝ+ → ( ⌊ ‘ ( 1 / 𝐴 ) ) ∈ ℕ0 )
6 nn0p1nn ⊢ ( ( ⌊ ‘ ( 1 / 𝐴 ) ) ∈ ℕ0 → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℕ )
7 5 6 syl ⊢ ( 𝐴 ∈ ℝ+ → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℕ )
8 flltp1 ⊢ ( ( 1 / 𝐴 ) ∈ ℝ → ( 1 / 𝐴 ) < ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) )
9 2 8 syl ⊢ ( 𝐴 ∈ ℝ+ → ( 1 / 𝐴 ) < ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) )
10 7 nnrpd ⊢ ( 𝐴 ∈ ℝ+ → ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℝ+ )
11 1 10 ltrecd ⊢ ( 𝐴 ∈ ℝ+ → ( ( 1 / 𝐴 ) < ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ↔ ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) < ( 1 / ( 1 / 𝐴 ) ) ) )
12 9 11 mpbid ⊢ ( 𝐴 ∈ ℝ+ → ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) < ( 1 / ( 1 / 𝐴 ) ) )
13 rpcn ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
14 rpne0 ⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 )
15 13 14 recrecd ⊢ ( 𝐴 ∈ ℝ+ → ( 1 / ( 1 / 𝐴 ) ) = 𝐴 )
16 12 15 breqtrd ⊢ ( 𝐴 ∈ ℝ+ → ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) < 𝐴 )
17 oveq2 ⊢ ( 𝑛 = ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) → ( 1 / 𝑛 ) = ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) )
18 17 breq1d ⊢ ( 𝑛 = ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) → ( ( 1 / 𝑛 ) < 𝐴 ↔ ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) < 𝐴 ) )
19 18 rspcev ⊢ ( ( ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ∈ ℕ ∧ ( 1 / ( ( ⌊ ‘ ( 1 / 𝐴 ) ) + 1 ) ) < 𝐴 ) → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝐴 )
20 7 16 19 syl2anc ⊢ ( 𝐴 ∈ ℝ+ → ∃ 𝑛 ∈ ℕ ( 1 / 𝑛 ) < 𝐴 )