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 → A 1 + 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 → A 1 + 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 → A 1 + A ⁢ 1 + A < 1 ⁢ 1 + A
24 simpl ⊢ A ∈ ℝ ∧ 0 ≤ A → A ∈ ℝ
25 24 12 18 redivcld ⊢ A ∈ ℝ ∧ 0 ≤ A → A 1 + A ∈ ℝ
26 ltmul1 ⊢ A 1 + A ∈ ℝ ∧ 1 ∈ ℝ ∧ 1 + A ∈ ℝ ∧ 0 < 1 + A → A 1 + A < 1 ↔ A 1 + A ⁢ 1 + A < 1 ⁢ 1 + A
27 9 26 mp3an2 ⊢ A 1 + A ∈ ℝ ∧ 1 + A ∈ ℝ ∧ 0 < 1 + A → A 1 + A < 1 ↔ A 1 + A ⁢ 1 + A < 1 ⁢ 1 + A
28 25 12 17 27 syl12anc ⊢ A ∈ ℝ ∧ 0 ≤ A → A 1 + A < 1 ↔ A 1 + A ⁢ 1 + A < 1 ⁢ 1 + A
29 23 28 mpbird ⊢ A ∈ ℝ ∧ 0 ≤ A → A 1 + A < 1