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	mulid2d	⊢ ( 𝐴 ∈ ℝ → ( 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 )