Metamath Proof Explorer

Theorem recreclt

Description: Given a positive number A , construct a new positive number less than both A and 1. (Contributed by NM, 28-Dec-2005)

Ref Expression
Assertion recreclt ⊢ A ∈ ℝ ∧ 0 < A → 1 1 + 1 A < 1 ∧ 1 1 + 1 A < A

Proof

Step Hyp Ref Expression
1 recgt0 ⊢ A ∈ ℝ ∧ 0 < A → 0 < 1 A
2 gt0ne0 ⊢ A ∈ ℝ ∧ 0 < A → A ≠ 0
3 rereccl ⊢ A ∈ ℝ ∧ A ≠ 0 → 1 A ∈ ℝ
4 2 3 syldan ⊢ A ∈ ℝ ∧ 0 < A → 1 A ∈ ℝ
5 1re ⊢ 1 ∈ ℝ
6 ltaddpos ⊢ 1 A ∈ ℝ ∧ 1 ∈ ℝ → 0 < 1 A ↔ 1 < 1 + 1 A
7 4 5 6 sylancl ⊢ A ∈ ℝ ∧ 0 < A → 0 < 1 A ↔ 1 < 1 + 1 A
8 1 7 mpbid ⊢ A ∈ ℝ ∧ 0 < A → 1 < 1 + 1 A
9 readdcl ⊢ 1 ∈ ℝ ∧ 1 A ∈ ℝ → 1 + 1 A ∈ ℝ
10 5 4 9 sylancr ⊢ A ∈ ℝ ∧ 0 < A → 1 + 1 A ∈ ℝ
11 0lt1 ⊢ 0 < 1
12 0re ⊢ 0 ∈ ℝ
13 lttr ⊢ 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 1 + 1 A ∈ ℝ → 0 < 1 ∧ 1 < 1 + 1 A → 0 < 1 + 1 A
14 12 5 10 13 mp3an12i ⊢ A ∈ ℝ ∧ 0 < A → 0 < 1 ∧ 1 < 1 + 1 A → 0 < 1 + 1 A
15 11 14 mpani ⊢ A ∈ ℝ ∧ 0 < A → 1 < 1 + 1 A → 0 < 1 + 1 A
16 8 15 mpd ⊢ A ∈ ℝ ∧ 0 < A → 0 < 1 + 1 A
17 recgt1 ⊢ 1 + 1 A ∈ ℝ ∧ 0 < 1 + 1 A → 1 < 1 + 1 A ↔ 1 1 + 1 A < 1
18 10 16 17 syl2anc ⊢ A ∈ ℝ ∧ 0 < A → 1 < 1 + 1 A ↔ 1 1 + 1 A < 1
19 8 18 mpbid ⊢ A ∈ ℝ ∧ 0 < A → 1 1 + 1 A < 1
20 ltaddpos ⊢ 1 ∈ ℝ ∧ 1 A ∈ ℝ → 0 < 1 ↔ 1 A < 1 A + 1
21 5 4 20 sylancr ⊢ A ∈ ℝ ∧ 0 < A → 0 < 1 ↔ 1 A < 1 A + 1
22 11 21 mpbii ⊢ A ∈ ℝ ∧ 0 < A → 1 A < 1 A + 1
23 4 recnd ⊢ A ∈ ℝ ∧ 0 < A → 1 A ∈ ℂ
24 ax-1cn ⊢ 1 ∈ ℂ
25 addcom ⊢ 1 A ∈ ℂ ∧ 1 ∈ ℂ → 1 A + 1 = 1 + 1 A
26 23 24 25 sylancl ⊢ A ∈ ℝ ∧ 0 < A → 1 A + 1 = 1 + 1 A
27 22 26 breqtrd ⊢ A ∈ ℝ ∧ 0 < A → 1 A < 1 + 1 A
28 simpl ⊢ A ∈ ℝ ∧ 0 < A → A ∈ ℝ
29 simpr ⊢ A ∈ ℝ ∧ 0 < A → 0 < A
30 ltrec1 ⊢ A ∈ ℝ ∧ 0 < A ∧ 1 + 1 A ∈ ℝ ∧ 0 < 1 + 1 A → 1 A < 1 + 1 A ↔ 1 1 + 1 A < A
31 28 29 10 16 30 syl22anc ⊢ A ∈ ℝ ∧ 0 < A → 1 A < 1 + 1 A ↔ 1 1 + 1 A < A
32 27 31 mpbid ⊢ A ∈ ℝ ∧ 0 < A → 1 1 + 1 A < A
33 19 32 jca ⊢ A ∈ ℝ ∧ 0 < A → 1 1 + 1 A < 1 ∧ 1 1 + 1 A < A