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 φ A 2 A A 0 1

Proof

Step Hyp Ref Expression
1 sqrlearg.1 φ A
2 0re 0
3 2 a1i φ A 2 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 mulid1d φ A 1 = A
20 19 adantr φ 1 < A A 1 = A
21 18 sqvald φ A 2 = A A
22 21 eqcomd φ A A = A 2
23 22 adantr φ 1 < A A A = A 2
24 20 23 breq12d φ 1 < A A 1 < A A A < A 2
25 17 24 mpbid φ 1 < A A < A 2
26 8 25 syldan φ ¬ A 1 A < A 2
27 26 adantlr φ A 2 A ¬ A 1 A < A 2
28 simpr φ A 2 A A 2 A
29 1 resqcld φ A 2
30 29 adantr φ A 2 A A 2
31 1 adantr φ A 2 A A
32 30 31 lenltd φ A 2 A A 2 A ¬ A < A 2
33 28 32 mpbid φ A 2 A ¬ A < A 2
34 33 adantr φ A 2 A ¬ A 1 ¬ A < A 2
35 27 34 condan φ A 2 A A 1
36 1red φ A 1 1
37 35 36 syldan φ A 2 A 1
38 31 sqge0d φ A 2 A 0 A 2
39 3 30 31 38 28 letrd φ A 2 A 0 A
40 3 37 31 39 35 eliccd φ A 2 A A 0 1
41 40 ex φ A 2 A A 0 1
42 unitssre 0 1
43 42 sseli A 0 1 A
44 1red A 0 1 1
45 0xr 0 *
46 45 a1i A 0 1 0 *
47 44 rexrd A 0 1 1 *
48 id A 0 1 A 0 1
49 46 47 48 iccgelbd A 0 1 0 A
50 46 47 48 iccleubd A 0 1 A 1
51 43 44 43 49 50 lemul2ad A 0 1 A A A 1
52 51 adantl φ A 0 1 A A A 1
53 22 adantr φ A 0 1 A A = A 2
54 19 adantr φ A 0 1 A 1 = A
55 53 54 breq12d φ A 0 1 A A A 1 A 2 A
56 52 55 mpbid φ A 0 1 A 2 A
57 56 ex φ A 0 1 A 2 A
58 41 57 impbid φ A 2 A A 0 1