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 ⊢A∈ℝ∧0≤A→A1+A<1

Proof

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