Proof of Theorem sqrlearg
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0re 11264 | . . . . 5
⊢ 0 ∈
ℝ | 
| 2 | 1 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 0 ∈ ℝ) | 
| 3 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → ¬ 𝐴 ≤ 1) | 
| 4 |  | 1red 11263 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → 1 ∈
ℝ) | 
| 5 |  | sqrlearg.1 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 6 | 5 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → 𝐴 ∈ ℝ) | 
| 7 | 4, 6 | ltnled 11409 | . . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → (1 < 𝐴 ↔ ¬ 𝐴 ≤ 1)) | 
| 8 | 3, 7 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → 1 < 𝐴) | 
| 9 |  | 1red 11263 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < 𝐴) → 1 ∈ ℝ) | 
| 10 | 5 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < 𝐴) → 𝐴 ∈ ℝ) | 
| 11 | 1 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 1 < 𝐴) → 0 ∈ ℝ) | 
| 12 |  | 0lt1 11786 | . . . . . . . . . . . . 13
⊢ 0 <
1 | 
| 13 | 12 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 1 < 𝐴) → 0 < 1) | 
| 14 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 1 < 𝐴) → 1 < 𝐴) | 
| 15 | 11, 9, 10, 13, 14 | lttrd 11423 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 1 < 𝐴) → 0 < 𝐴) | 
| 16 | 10, 15 | elrpd 13075 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < 𝐴) → 𝐴 ∈
ℝ+) | 
| 17 | 9, 10, 16, 14 | ltmul2dd 13134 | . . . . . . . . 9
⊢ ((𝜑 ∧ 1 < 𝐴) → (𝐴 · 1) < (𝐴 · 𝐴)) | 
| 18 | 5 | recnd 11290 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 19 | 18 | mulridd 11279 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · 1) = 𝐴) | 
| 20 | 19 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < 𝐴) → (𝐴 · 1) = 𝐴) | 
| 21 | 18 | sqvald 14184 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) | 
| 22 | 21 | eqcomd 2742 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴 · 𝐴) = (𝐴↑2)) | 
| 23 | 22 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 1 < 𝐴) → (𝐴 · 𝐴) = (𝐴↑2)) | 
| 24 | 20, 23 | breq12d 5155 | . . . . . . . . 9
⊢ ((𝜑 ∧ 1 < 𝐴) → ((𝐴 · 1) < (𝐴 · 𝐴) ↔ 𝐴 < (𝐴↑2))) | 
| 25 | 17, 24 | mpbid 232 | . . . . . . . 8
⊢ ((𝜑 ∧ 1 < 𝐴) → 𝐴 < (𝐴↑2)) | 
| 26 | 8, 25 | syldan 591 | . . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝐴 ≤ 1) → 𝐴 < (𝐴↑2)) | 
| 27 | 26 | adantlr 715 | . . . . . 6
⊢ (((𝜑 ∧ (𝐴↑2) ≤ 𝐴) ∧ ¬ 𝐴 ≤ 1) → 𝐴 < (𝐴↑2)) | 
| 28 |  | simpr 484 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → (𝐴↑2) ≤ 𝐴) | 
| 29 | 5 | resqcld 14166 | . . . . . . . . . 10
⊢ (𝜑 → (𝐴↑2) ∈ ℝ) | 
| 30 | 29 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → (𝐴↑2) ∈ ℝ) | 
| 31 | 5 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 𝐴 ∈ ℝ) | 
| 32 | 30, 31 | lenltd 11408 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → ((𝐴↑2) ≤ 𝐴 ↔ ¬ 𝐴 < (𝐴↑2))) | 
| 33 | 28, 32 | mpbid 232 | . . . . . . 7
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → ¬ 𝐴 < (𝐴↑2)) | 
| 34 | 33 | adantr 480 | . . . . . 6
⊢ (((𝜑 ∧ (𝐴↑2) ≤ 𝐴) ∧ ¬ 𝐴 ≤ 1) → ¬ 𝐴 < (𝐴↑2)) | 
| 35 | 27, 34 | condan 817 | . . . . 5
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 𝐴 ≤ 1) | 
| 36 |  | 1red 11263 | . . . . 5
⊢ ((𝜑 ∧ 𝐴 ≤ 1) → 1 ∈
ℝ) | 
| 37 | 35, 36 | syldan 591 | . . . 4
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 1 ∈ ℝ) | 
| 38 | 31 | sqge0d 14178 | . . . . 5
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 0 ≤ (𝐴↑2)) | 
| 39 | 2, 30, 31, 38, 28 | letrd 11419 | . . . 4
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 0 ≤ 𝐴) | 
| 40 | 2, 37, 31, 39, 35 | eliccd 45522 | . . 3
⊢ ((𝜑 ∧ (𝐴↑2) ≤ 𝐴) → 𝐴 ∈ (0[,]1)) | 
| 41 | 40 | ex 412 | . 2
⊢ (𝜑 → ((𝐴↑2) ≤ 𝐴 → 𝐴 ∈ (0[,]1))) | 
| 42 |  | unitssre 13540 | . . . . . . 7
⊢ (0[,]1)
⊆ ℝ | 
| 43 | 42 | sseli 3978 | . . . . . 6
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈
ℝ) | 
| 44 |  | 1red 11263 | . . . . . 6
⊢ (𝐴 ∈ (0[,]1) → 1 ∈
ℝ) | 
| 45 |  | 0xr 11309 | . . . . . . . 8
⊢ 0 ∈
ℝ* | 
| 46 | 45 | a1i 11 | . . . . . . 7
⊢ (𝐴 ∈ (0[,]1) → 0 ∈
ℝ*) | 
| 47 | 44 | rexrd 11312 | . . . . . . 7
⊢ (𝐴 ∈ (0[,]1) → 1 ∈
ℝ*) | 
| 48 |  | id 22 | . . . . . . 7
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ∈
(0[,]1)) | 
| 49 | 46, 47, 48 | iccgelbd 45561 | . . . . . 6
⊢ (𝐴 ∈ (0[,]1) → 0 ≤
𝐴) | 
| 50 | 46, 47, 48 | iccleubd 45566 | . . . . . 6
⊢ (𝐴 ∈ (0[,]1) → 𝐴 ≤ 1) | 
| 51 | 43, 44, 43, 49, 50 | lemul2ad 12209 | . . . . 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 5155 | . . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ (0[,]1)) → ((𝐴 · 𝐴) ≤ (𝐴 · 1) ↔ (𝐴↑2) ≤ 𝐴)) | 
| 56 | 52, 55 | mpbid 232 | . . 3
⊢ ((𝜑 ∧ 𝐴 ∈ (0[,]1)) → (𝐴↑2) ≤ 𝐴) | 
| 57 | 56 | ex 412 | . 2
⊢ (𝜑 → (𝐴 ∈ (0[,]1) → (𝐴↑2) ≤ 𝐴)) | 
| 58 | 41, 57 | impbid 212 | 1
⊢ (𝜑 → ((𝐴↑2) ≤ 𝐴 ↔ 𝐴 ∈ (0[,]1))) |