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	mulridd	⊢ ( 𝜑 → ( 𝐴 · 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 ) ) )