Metamath Proof Explorer

Theorem sqrlearg

Description: The square compared with its argument. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypothesis sqrlearg.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
Assertion sqrlearg ( 𝜑 → ( ( 𝐴 ↑ 2 ) ≤ 𝐴 ↔ 𝐴 ∈ ( 0 [,] 1 ) ) )

Proof

Step Hyp Ref Expression
1 sqrlearg.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 0re ⊢ 0 ∈ ℝ
3 2 a1i ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → 0 ∈ ℝ )
4 simpr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ≤ 1 ) → ¬ 𝐴 ≤ 1 )
5 1red ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ≤ 1 ) → 1 ∈ ℝ )
6 1 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ≤ 1 ) → 𝐴 ∈ ℝ )
7 5 6 ltnled ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ≤ 1 ) → ( 1 < 𝐴 ↔ ¬ 𝐴 ≤ 1 ) )
8 4 7 mpbird ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ≤ 1 ) → 1 < 𝐴 )
9 1red ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 1 ∈ ℝ )
10 1 adantr ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ )
11 2 a1i ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 0 ∈ ℝ )
12 0lt1 ⊢ 0 < 1
13 12 a1i ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 0 < 1 )
14 simpr ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 1 < 𝐴 )
15 11 9 10 13 14 lttrd ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 0 < 𝐴 )
16 10 15 elrpd ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 𝐴 ∈ ℝ+ )
17 9 10 16 14 ltmul2dd ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ( 𝐴 · 1 ) < ( 𝐴 · 𝐴 ) )
18 1 recnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
19 18 mulid1d ⊢ ( 𝜑 → ( 𝐴 · 1 ) = 𝐴 )
20 19 adantr ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ( 𝐴 · 1 ) = 𝐴 )
21 18 sqvald ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐴 · 𝐴 ) )
22 21 eqcomd ⊢ ( 𝜑 → ( 𝐴 · 𝐴 ) = ( 𝐴 ↑ 2 ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ( 𝐴 · 𝐴 ) = ( 𝐴 ↑ 2 ) )
24 20 23 breq12d ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → ( ( 𝐴 · 1 ) < ( 𝐴 · 𝐴 ) ↔ 𝐴 < ( 𝐴 ↑ 2 ) ) )
25 17 24 mpbid ⊢ ( ( 𝜑 ∧ 1 < 𝐴 ) → 𝐴 < ( 𝐴 ↑ 2 ) )
26 8 25 syldan ⊢ ( ( 𝜑 ∧ ¬ 𝐴 ≤ 1 ) → 𝐴 < ( 𝐴 ↑ 2 ) )
27 26 adantlr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) ∧ ¬ 𝐴 ≤ 1 ) → 𝐴 < ( 𝐴 ↑ 2 ) )
28 simpr ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → ( 𝐴 ↑ 2 ) ≤ 𝐴 )
29 1 resqcld ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℝ )
30 29 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → ( 𝐴 ↑ 2 ) ∈ ℝ )
31 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → 𝐴 ∈ ℝ )
32 30 31 lenltd ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → ( ( 𝐴 ↑ 2 ) ≤ 𝐴 ↔ ¬ 𝐴 < ( 𝐴 ↑ 2 ) ) )
33 28 32 mpbid ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → ¬ 𝐴 < ( 𝐴 ↑ 2 ) )
34 33 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) ∧ ¬ 𝐴 ≤ 1 ) → ¬ 𝐴 < ( 𝐴 ↑ 2 ) )
35 27 34 condan ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → 𝐴 ≤ 1 )
36 1red ⊢ ( ( 𝜑 ∧ 𝐴 ≤ 1 ) → 1 ∈ ℝ )
37 35 36 syldan ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → 1 ∈ ℝ )
38 31 sqge0d ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → 0 ≤ ( 𝐴 ↑ 2 ) )
39 3 30 31 38 28 letrd ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → 0 ≤ 𝐴 )
40 3 37 31 39 35 eliccd ⊢ ( ( 𝜑 ∧ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) → 𝐴 ∈ ( 0 [,] 1 ) )
41 40 ex ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) ≤ 𝐴 → 𝐴 ∈ ( 0 [,] 1 ) ) )
42 unitssre ⊢ ( 0 [,] 1 ) ⊆ ℝ
43 42 sseli ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 𝐴 ∈ ℝ )
44 1red ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 1 ∈ ℝ )
45 0xr ⊢ 0 ∈ ℝ*
46 45 a1i ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 0 ∈ ℝ* )
47 44 rexrd ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 1 ∈ ℝ* )
48 id ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 𝐴 ∈ ( 0 [,] 1 ) )
49 46 47 48 iccgelbd ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 0 ≤ 𝐴 )
50 46 47 48 iccleubd ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → 𝐴 ≤ 1 )
51 43 44 43 49 50 lemul2ad ⊢ ( 𝐴 ∈ ( 0 [,] 1 ) → ( 𝐴 · 𝐴 ) ≤ ( 𝐴 · 1 ) )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 0 [,] 1 ) ) → ( 𝐴 · 𝐴 ) ≤ ( 𝐴 · 1 ) )
53 22 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 0 [,] 1 ) ) → ( 𝐴 · 𝐴 ) = ( 𝐴 ↑ 2 ) )
54 19 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 0 [,] 1 ) ) → ( 𝐴 · 1 ) = 𝐴 )
55 53 54 breq12d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 0 [,] 1 ) ) → ( ( 𝐴 · 𝐴 ) ≤ ( 𝐴 · 1 ) ↔ ( 𝐴 ↑ 2 ) ≤ 𝐴 ) )
56 52 55 mpbid ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ( 0 [,] 1 ) ) → ( 𝐴 ↑ 2 ) ≤ 𝐴 )
57 56 ex ⊢ ( 𝜑 → ( 𝐴 ∈ ( 0 [,] 1 ) → ( 𝐴 ↑ 2 ) ≤ 𝐴 ) )
58 41 57 impbid ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) ≤ 𝐴 ↔ 𝐴 ∈ ( 0 [,] 1 ) ) )