This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem recp1lt1

Description: Construct a number less than 1 from any nonnegative number. (Contributed by NM, 30-Dec-2005)

Ref Expression
Assertion recp1lt1 ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 / ( 1 + 𝐴 ) ) < 1 )

Proof

Step Hyp Ref Expression
1 ltp1 ⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( 𝐴 + 1 ) )
2 recn ⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
3 ax-1cn ⊢ 1 ∈ ℂ
4 addcom ⊢ ( ( 𝐴 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝐴 + 1 ) = ( 1 + 𝐴 ) )
5 2 3 4 sylancl ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 + 1 ) = ( 1 + 𝐴 ) )
6 1 5 breqtrd ⊢ ( 𝐴 ∈ ℝ → 𝐴 < ( 1 + 𝐴 ) )
7 6 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 < ( 1 + 𝐴 ) )
8 2 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℂ )
9 1re ⊢ 1 ∈ ℝ
10 readdcl ⊢ ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 1 + 𝐴 ) ∈ ℝ )
11 9 10 mpan ⊢ ( 𝐴 ∈ ℝ → ( 1 + 𝐴 ) ∈ ℝ )
12 11 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 1 + 𝐴 ) ∈ ℝ )
13 12 recnd ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 1 + 𝐴 ) ∈ ℂ )
14 0lt1 ⊢ 0 < 1
15 addgtge0 ⊢ ( ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ ( 0 < 1 ∧ 0 ≤ 𝐴 ) ) → 0 < ( 1 + 𝐴 ) )
16 14 15 mpanr1 ⊢ ( ( ( 1 ∈ ℝ ∧ 𝐴 ∈ ℝ ) ∧ 0 ≤ 𝐴 ) → 0 < ( 1 + 𝐴 ) )
17 9 16 mpanl1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 < ( 1 + 𝐴 ) )
18 17 gt0ne0d ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 1 + 𝐴 ) ≠ 0 )
19 8 13 18 divcan1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝐴 / ( 1 + 𝐴 ) ) · ( 1 + 𝐴 ) ) = 𝐴 )
20 11 recnd ⊢ ( 𝐴 ∈ ℝ → ( 1 + 𝐴 ) ∈ ℂ )
21 20 mullidd ⊢ ( 𝐴 ∈ ℝ → ( 1 · ( 1 + 𝐴 ) ) = ( 1 + 𝐴 ) )
22 21 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 1 · ( 1 + 𝐴 ) ) = ( 1 + 𝐴 ) )
23 7 19 22 3brtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝐴 / ( 1 + 𝐴 ) ) · ( 1 + 𝐴 ) ) < ( 1 · ( 1 + 𝐴 ) ) )
24 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
25 24 12 18 redivcld ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 / ( 1 + 𝐴 ) ) ∈ ℝ )
26 ltmul1 ⊢ ( ( ( 𝐴 / ( 1 + 𝐴 ) ) ∈ ℝ ∧ 1 ∈ ℝ ∧ ( ( 1 + 𝐴 ) ∈ ℝ ∧ 0 < ( 1 + 𝐴 ) ) ) → ( ( 𝐴 / ( 1 + 𝐴 ) ) < 1 ↔ ( ( 𝐴 / ( 1 + 𝐴 ) ) · ( 1 + 𝐴 ) ) < ( 1 · ( 1 + 𝐴 ) ) ) )
27 9 26 mp3an2 ⊢ ( ( ( 𝐴 / ( 1 + 𝐴 ) ) ∈ ℝ ∧ ( ( 1 + 𝐴 ) ∈ ℝ ∧ 0 < ( 1 + 𝐴 ) ) ) → ( ( 𝐴 / ( 1 + 𝐴 ) ) < 1 ↔ ( ( 𝐴 / ( 1 + 𝐴 ) ) · ( 1 + 𝐴 ) ) < ( 1 · ( 1 + 𝐴 ) ) ) )
28 25 12 17 27 syl12anc ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝐴 / ( 1 + 𝐴 ) ) < 1 ↔ ( ( 𝐴 / ( 1 + 𝐴 ) ) · ( 1 + 𝐴 ) ) < ( 1 · ( 1 + 𝐴 ) ) ) )
29 23 28 mpbird ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝐴 / ( 1 + 𝐴 ) ) < 1 )