Metamath Proof Explorer

Theorem 3cubeslem1

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

Ref Expression
Hypothesis 3cubeslem1.a 
|- ( ph -> A e. QQ )
Assertion 3cubeslem1 
|- ( ph -> 0 < ( ( ( A + 1 ) ^ 2 ) - A ) )

Proof

Step Hyp Ref Expression
1 3cubeslem1.a 
 |-  ( ph -> A e. QQ )
2 qre 
 |-  ( A e. QQ -> A e. RR )
3 1 2 syl 
 |-  ( ph -> A e. RR )
4 0red 
 |-  ( ph -> 0 e. RR )
5 3 4 lttri4d 
 |-  ( ph -> ( A < 0 \/ A = 0 \/ 0 < A ) )
6 simpl 
 |-  ( ( A e. RR /\ A < 0 ) -> A e. RR )
7 0red 
 |-  ( ( A e. RR /\ A < 0 ) -> 0 e. RR )
8 peano2re 
 |-  ( A e. RR -> ( A + 1 ) e. RR )
9 8 adantr 
 |-  ( ( A e. RR /\ A < 0 ) -> ( A + 1 ) e. RR )
10 9 resqcld 
 |-  ( ( A e. RR /\ A < 0 ) -> ( ( A + 1 ) ^ 2 ) e. RR )
11 simpr 
 |-  ( ( A e. RR /\ A < 0 ) -> A < 0 )
12 9 sqge0d 
 |-  ( ( A e. RR /\ A < 0 ) -> 0 <_ ( ( A + 1 ) ^ 2 ) )
13 6 7 10 11 12 ltletrd 
 |-  ( ( A e. RR /\ A < 0 ) -> A < ( ( A + 1 ) ^ 2 ) )
14 13 a1i 
 |-  ( ph -> ( ( A e. RR /\ A < 0 ) -> A < ( ( A + 1 ) ^ 2 ) ) )
15 3 14 mpand 
 |-  ( ph -> ( 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 e. CC )
23 1cnd 
 |-  ( A = 0 -> 1 e. CC )
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 
 |-  ( ph -> ( A = 0 -> A < ( ( A + 1 ) ^ 2 ) ) )
31 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
32 31 adantr 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A x. 1 ) = A )
33 simpl 
 |-  ( ( A e. RR /\ 0 < A ) -> A e. RR )
34 1red 
 |-  ( ( A e. RR /\ 0 < A ) -> 1 e. RR )
35 33 34 readdcld 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A + 1 ) e. RR )
36 simpr 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 < A )
37 0red 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 e. RR )
38 ltle 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
39 37 33 38 syl2anc 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 0 < A -> 0 <_ A ) )
40 33 ltp1d 
 |-  ( ( A e. RR /\ 0 < A ) -> A < ( A + 1 ) )
41 39 40 jctird 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 0 < A -> ( 0 <_ A /\ A < ( A + 1 ) ) ) )
42 36 41 mpd 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 0 <_ A /\ A < ( A + 1 ) ) )
43 34 35 jca 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 1 e. RR /\ ( A + 1 ) e. RR ) )
44 0le1 
 |-  0 <_ 1
45 44 a1i 
 |-  ( ( A e. RR /\ 0 < A ) -> 0 <_ 1 )
46 1e0p1 
 |-  1 = ( 0 + 1 )
47 37 33 34 36 ltadd1dd 
 |-  ( ( A e. RR /\ 0 < A ) -> ( 0 + 1 ) < ( A + 1 ) )
48 46 47 eqbrtrid 
 |-  ( ( A e. RR /\ 0 < A ) -> 1 < ( A + 1 ) )
49 43 45 48 jca32 
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( 1 e. RR /\ ( A + 1 ) e. RR ) /\ ( 0 <_ 1 /\ 1 < ( A + 1 ) ) ) )
50 ltmul12a 
 |-  ( ( ( ( A e. RR /\ ( A + 1 ) e. RR ) /\ ( 0 <_ A /\ A < ( A + 1 ) ) ) /\ ( ( 1 e. RR /\ ( A + 1 ) e. RR ) /\ ( 0 <_ 1 /\ 1 < ( A + 1 ) ) ) ) -> ( A x. 1 ) < ( ( A + 1 ) x. ( A + 1 ) ) )
51 33 35 42 49 50 syl1111anc 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A x. 1 ) < ( ( A + 1 ) x. ( A + 1 ) ) )
52 32 51 eqbrtrrd 
 |-  ( ( A e. RR /\ 0 < A ) -> A < ( ( A + 1 ) x. ( A + 1 ) ) )
53 35 recnd 
 |-  ( ( A e. RR /\ 0 < A ) -> ( A + 1 ) e. CC )
54 53 sqvald 
 |-  ( ( A e. RR /\ 0 < A ) -> ( ( A + 1 ) ^ 2 ) = ( ( A + 1 ) x. ( A + 1 ) ) )
55 52 54 breqtrrd 
 |-  ( ( A e. RR /\ 0 < A ) -> A < ( ( A + 1 ) ^ 2 ) )
56 55 a1i 
 |-  ( ph -> ( ( A e. RR /\ 0 < A ) -> A < ( ( A + 1 ) ^ 2 ) ) )
57 3 56 mpand 
 |-  ( ph -> ( 0 < A -> A < ( ( A + 1 ) ^ 2 ) ) )
58 15 30 57 3jaod 
 |-  ( ph -> ( ( A < 0 \/ A = 0 \/ 0 < A ) -> A < ( ( A + 1 ) ^ 2 ) ) )
59 5 58 mpd 
 |-  ( ph -> A < ( ( A + 1 ) ^ 2 ) )
60 3 8 syl 
 |-  ( ph -> ( A + 1 ) e. RR )
61 60 resqcld 
 |-  ( ph -> ( ( A + 1 ) ^ 2 ) e. RR )
62 3 61 posdifd 
 |-  ( ph -> ( A < ( ( A + 1 ) ^ 2 ) <-> 0 < ( ( ( A + 1 ) ^ 2 ) - A ) ) )
63 59 62 mpbid 
 |-  ( ph -> 0 < ( ( ( A + 1 ) ^ 2 ) - A ) )