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 / 𝐴 ) ) ) < 𝐴 ) )