Metamath Proof Explorer

Theorem sqrlearg

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

Ref Expression
Hypothesis sqrlearg.1 ⊢φ→A∈ℝ
Assertion sqrlearg ⊢φ→A2≤A↔A∈01

Proof

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