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 ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( ( 1 / ( 1 + ( 1 / 𝐴 ) ) ) < 1 ∧ ( 1 / ( 1 + ( 1 / 𝐴 ) ) ) < 𝐴 ) )

Proof

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