sqrlearg

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

		Ref	Expression
	Hypothesis	sqrlearg.1	$⊢ φ \to A \in ℝ$
	Assertion	sqrlearg	$⊢ φ \to (A^{2} \leq A \leftrightarrow A \in [0, 1])$

Proof

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

Metamath Proof Explorer

Theorem sqrlearg

Proof