Metamath Proof Explorer

Theorem 3cubeslem1

Description: Lemma for 3cubes . (Contributed by Igor Ieskov, 22-Jan-2024)

Ref Expression
Hypothesis 3cubeslem1.a ⊢ φ → A ∈ ℚ
Assertion 3cubeslem1 ⊢ φ → 0 < A + 1 2 − A

Proof

Step Hyp Ref Expression
1 3cubeslem1.a ⊢ φ → A ∈ ℚ
2 qre ⊢ A ∈ ℚ → A ∈ ℝ
3 1 2 syl ⊢ φ → A ∈ ℝ
4 0red ⊢ φ → 0 ∈ ℝ
5 3 4 lttri4d ⊢ φ → A < 0 ∨ A = 0 ∨ 0 < A
6 simpl ⊢ A ∈ ℝ ∧ A < 0 → A ∈ ℝ
7 0red ⊢ A ∈ ℝ ∧ A < 0 → 0 ∈ ℝ
8 peano2re ⊢ A ∈ ℝ → A + 1 ∈ ℝ
9 8 adantr ⊢ A ∈ ℝ ∧ A < 0 → A + 1 ∈ ℝ
10 9 resqcld ⊢ A ∈ ℝ ∧ A < 0 → A + 1 2 ∈ ℝ
11 simpr ⊢ A ∈ ℝ ∧ A < 0 → A < 0
12 9 sqge0d ⊢ A ∈ ℝ ∧ A < 0 → 0 ≤ A + 1 2
13 6 7 10 11 12 ltletrd ⊢ A ∈ ℝ ∧ A < 0 → A < A + 1 2
14 13 a1i ⊢ φ → A ∈ ℝ ∧ A < 0 → A < A + 1 2
15 3 14 mpand ⊢ φ → A < 0 → A < A + 1 2
16 0lt1 ⊢ 0 < 1
17 16 a1i ⊢ A = 0 → 0 < 1
18 id ⊢ A = 0 → A = 0
19 sq1 ⊢ 1 2 = 1
20 19 a1i ⊢ A = 0 → 1 2 = 1
21 17 18 20 3brtr4d ⊢ A = 0 → A < 1 2
22 0cnd ⊢ A = 0 → 0 ∈ ℂ
23 1cnd ⊢ A = 0 → 1 ∈ ℂ
24 18 oveq1d ⊢ A = 0 → A + 1 = 0 + 1
25 22 23 24 comraddd ⊢ A = 0 → A + 1 = 1 + 0
26 1p0e1 ⊢ 1 + 0 = 1
27 25 26 eqtrdi ⊢ A = 0 → A + 1 = 1
28 27 oveq1d ⊢ A = 0 → A + 1 2 = 1 2
29 21 28 breqtrrd ⊢ A = 0 → A < A + 1 2
30 29 a1i ⊢ φ → A = 0 → A < A + 1 2
31 ax-1rid ⊢ A ∈ ℝ → A ⋅ 1 = A
32 31 adantr ⊢ A ∈ ℝ ∧ 0 < A → A ⋅ 1 = A
33 simpl ⊢ A ∈ ℝ ∧ 0 < A → A ∈ ℝ
34 1red ⊢ A ∈ ℝ ∧ 0 < A → 1 ∈ ℝ
35 33 34 readdcld ⊢ A ∈ ℝ ∧ 0 < A → A + 1 ∈ ℝ
36 simpr ⊢ A ∈ ℝ ∧ 0 < A → 0 < A
37 0red ⊢ A ∈ ℝ ∧ 0 < A → 0 ∈ ℝ
38 ltle ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 < A → 0 ≤ A
39 37 33 38 syl2anc ⊢ A ∈ ℝ ∧ 0 < A → 0 < A → 0 ≤ A
40 33 ltp1d ⊢ A ∈ ℝ ∧ 0 < A → A < A + 1
41 39 40 jctird ⊢ A ∈ ℝ ∧ 0 < A → 0 < A → 0 ≤ A ∧ A < A + 1
42 36 41 mpd ⊢ A ∈ ℝ ∧ 0 < A → 0 ≤ A ∧ A < A + 1
43 34 35 jca ⊢ A ∈ ℝ ∧ 0 < A → 1 ∈ ℝ ∧ A + 1 ∈ ℝ
44 0le1 ⊢ 0 ≤ 1
45 44 a1i ⊢ A ∈ ℝ ∧ 0 < A → 0 ≤ 1
46 1e0p1 ⊢ 1 = 0 + 1
47 37 33 34 36 ltadd1dd ⊢ A ∈ ℝ ∧ 0 < A → 0 + 1 < A + 1
48 46 47 eqbrtrid ⊢ A ∈ ℝ ∧ 0 < A → 1 < A + 1
49 43 45 48 jca32 ⊢ A ∈ ℝ ∧ 0 < A → 1 ∈ ℝ ∧ A + 1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < A + 1
50 ltmul12a ⊢ A ∈ ℝ ∧ A + 1 ∈ ℝ ∧ 0 ≤ A ∧ A < A + 1 ∧ 1 ∈ ℝ ∧ A + 1 ∈ ℝ ∧ 0 ≤ 1 ∧ 1 < A + 1 → A ⋅ 1 < A + 1 ⁢ A + 1
51 33 35 42 49 50 syl1111anc ⊢ A ∈ ℝ ∧ 0 < A → A ⋅ 1 < A + 1 ⁢ A + 1
52 32 51 eqbrtrrd ⊢ A ∈ ℝ ∧ 0 < A → A < A + 1 ⁢ A + 1
53 35 recnd ⊢ A ∈ ℝ ∧ 0 < A → A + 1 ∈ ℂ
54 53 sqvald ⊢ A ∈ ℝ ∧ 0 < A → A + 1 2 = A + 1 ⁢ A + 1
55 52 54 breqtrrd ⊢ A ∈ ℝ ∧ 0 < A → A < A + 1 2
56 55 a1i ⊢ φ → A ∈ ℝ ∧ 0 < A → A < A + 1 2
57 3 56 mpand ⊢ φ → 0 < A → A < A + 1 2
58 15 30 57 3jaod ⊢ φ → A < 0 ∨ A = 0 ∨ 0 < A → A < A + 1 2
59 5 58 mpd ⊢ φ → A < A + 1 2
60 3 8 syl ⊢ φ → A + 1 ∈ ℝ
61 60 resqcld ⊢ φ → A + 1 2 ∈ ℝ
62 3 61 posdifd ⊢ φ → A < A + 1 2 ↔ 0 < A + 1 2 − A
63 59 62 mpbid ⊢ φ → 0 < A + 1 2 − A