Proof of Theorem sqrlearg
Step | Hyp | Ref
| Expression |
1 | | 0re 9919 |
. . . . 5
⊢ 0 ∈
ℝ |
2 | 1 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 0 ∈ ℝ) |
3 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → ¬ 𝐴 ≤ 1) |
4 | | 1red 9934 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → 1 ∈
ℝ) |
5 | | sqrlearg.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
6 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → 𝐴 ∈ ℝ) |
7 | 4, 6 | ltnled 10063 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → (1 < 𝐴 ↔ ¬ 𝐴 ≤ 1)) |
8 | 3, 7 | mpbird 246 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → 1 < 𝐴) |
9 | | 1red 9934 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < 𝐴) → 1 ∈ ℝ) |
10 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < 𝐴) → 𝐴 ∈ ℝ) |
11 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 1 < 𝐴) → 0 ∈ ℝ) |
12 | | 0lt1 10429 |
. . . . . . . . . . . . 13
⊢ 0 <
1 |
13 | 12 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 1 < 𝐴) → 0 < 1) |
14 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 1 < 𝐴) → 1 < 𝐴) |
15 | 11, 9, 10, 13, 14 | lttrd 10077 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 1 < 𝐴) → 0 < 𝐴) |
16 | 10, 15 | elrpd 11745 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < 𝐴) → 𝐴 ∈
ℝ+) |
17 | 9, 10, 16, 14 | ltmul2dd 11804 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 < 𝐴) → (𝐴 · 1) < (𝐴 · 𝐴)) |
18 | 5 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
19 | 18 | mulid1d 9936 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · 1) = 𝐴) |
20 | 19 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < 𝐴) → (𝐴 · 1) = 𝐴) |
21 | 18 | sqvald 12867 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) |
22 | 21 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · 𝐴) = (𝐴↑2)) |
23 | 22 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < 𝐴) → (𝐴 · 𝐴) = (𝐴↑2)) |
24 | 20, 23 | breq12d 4596 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 1 < 𝐴) → ((𝐴 · 1) < (𝐴 · 𝐴) ↔ 𝐴 < (𝐴↑2))) |
25 | 17, 24 | mpbid 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 1 < 𝐴) → 𝐴 < (𝐴↑2)) |
26 | 8, 25 | syldan 486 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → 𝐴 < (𝐴↑2)) |
27 | 26 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴↑2) ≤ 𝐴) ∧ ¬ 𝐴 ≤ 1) → 𝐴 < (𝐴↑2)) |
28 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → (𝐴↑2) ≤ 𝐴) |
29 | 5 | resqcld 12897 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴↑2) ∈ ℝ) |
30 | 29 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → (𝐴↑2) ∈ ℝ) |
31 | 5 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 𝐴 ∈ ℝ) |
32 | 30, 31 | lenltd 10062 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → ((𝐴↑2) ≤ 𝐴 ↔ ¬ 𝐴 < (𝐴↑2))) |
33 | 28, 32 | mpbid 221 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → ¬ 𝐴 < (𝐴↑2)) |
34 | 33 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝐴↑2) ≤ 𝐴) ∧ ¬ 𝐴 ≤ 1) → ¬ 𝐴 < (𝐴↑2)) |
35 | 27, 34 | condan 831 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 𝐴 ≤ 1) |
36 | | 1red 9934 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 1) → 1 ∈
ℝ) |
37 | 35, 36 | syldan 486 |
. . . 4
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 1 ∈ ℝ) |
38 | 31 | sqge0d 12898 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 0 ≤ (𝐴↑2)) |
39 | 2, 30, 31, 38, 28 | letrd 10073 |
. . . 4
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 0 ≤ 𝐴) |
40 | 2, 37, 31, 39, 35 | eliccd 38573 |
. . 3
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 𝐴 ∈ (0[,]1)) |
41 | 40 | ex 449 |
. 2
⊢ (𝜑 → ((𝐴↑2) ≤ 𝐴 → 𝐴 ∈ (0[,]1))) |
42 | | unitssre 12190 |
. . . . . . 7
⊢ (0[,]1)
⊆ ℝ |
43 | 42 | sseli 3564 |
. . . . . 6
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈
ℝ) |
44 | | 1red 9934 |
. . . . . 6
⊢ (𝐴 ∈ (0[,]1) → 1 ∈
ℝ) |
45 | | 0xr 9965 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
46 | 45 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ (0[,]1) → 0 ∈
ℝ*) |
47 | 44 | rexrd 9968 |
. . . . . . 7
⊢ (𝐴 ∈ (0[,]1) → 1 ∈
ℝ*) |
48 | | id 22 |
. . . . . . 7
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈
(0[,]1)) |
49 | 46, 47, 48 | iccgelbd 38617 |
. . . . . 6
⊢ (𝐴 ∈ (0[,]1) → 0 ≤
𝐴) |
50 | 46, 47, 48 | iccleubd 38622 |
. . . . . 6
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ≤ 1) |
51 | 43, 44, 43, 49, 50 | lemul2ad 10843 |
. . . . 5
⊢ (𝐴 ∈ (0[,]1) → (𝐴 · 𝐴) ≤ (𝐴 · 1)) |
52 | 51 | adantl 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (0[,]1)) → (𝐴 · 𝐴) ≤ (𝐴 · 1)) |
53 | 22 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (0[,]1)) → (𝐴 · 𝐴) = (𝐴↑2)) |
54 | 19 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ (0[,]1)) → (𝐴 · 1) = 𝐴) |
55 | 53, 54 | breq12d 4596 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (0[,]1)) → ((𝐴 · 𝐴) ≤ (𝐴 · 1) ↔ (𝐴↑2) ≤ 𝐴)) |
56 | 52, 55 | mpbid 221 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (0[,]1)) → (𝐴↑2) ≤ 𝐴) |
57 | 56 | ex 449 |
. 2
⊢ (𝜑 → (𝐴 ∈ (0[,]1) → (𝐴↑2) ≤ 𝐴)) |
58 | 41, 57 | impbid 201 |
1
⊢ (𝜑 → ((𝐴↑2) ≤ 𝐴 ↔ 𝐴 ∈ (0[,]1))) |