Proof of Theorem itscnhlinecirc02plem1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 4re 12350 | . . . . 5
⊢ 4 ∈
ℝ | 
| 2 | 1 | a1i 11 | . . . 4
⊢ (𝜑 → 4 ∈
ℝ) | 
| 3 |  | 2itscp.d | . . . . . . . 8
⊢ 𝐷 = (𝑋 − 𝐴) | 
| 4 |  | 2itscp.x | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ ℝ) | 
| 5 |  | 2itscp.a | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 6 | 4, 5 | resubcld 11691 | . . . . . . . 8
⊢ (𝜑 → (𝑋 − 𝐴) ∈ ℝ) | 
| 7 | 3, 6 | eqeltrid 2845 | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 8 | 7 | resqcld 14165 | . . . . . 6
⊢ (𝜑 → (𝐷↑2) ∈ ℝ) | 
| 9 |  | 2itscp.c | . . . . . . . 8
⊢ 𝐶 = ((𝐷 · 𝐵) + (𝐸 · 𝐴)) | 
| 10 |  | 2itscp.b | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 11 | 7, 10 | remulcld 11291 | . . . . . . . . 9
⊢ (𝜑 → (𝐷 · 𝐵) ∈ ℝ) | 
| 12 |  | 2itscp.e | . . . . . . . . . . 11
⊢ 𝐸 = (𝐵 − 𝑌) | 
| 13 |  | 2itscp.y | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑌 ∈ ℝ) | 
| 14 | 10, 13 | resubcld 11691 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐵 − 𝑌) ∈ ℝ) | 
| 15 | 12, 14 | eqeltrid 2845 | . . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℝ) | 
| 16 | 15, 5 | remulcld 11291 | . . . . . . . . 9
⊢ (𝜑 → (𝐸 · 𝐴) ∈ ℝ) | 
| 17 | 11, 16 | readdcld 11290 | . . . . . . . 8
⊢ (𝜑 → ((𝐷 · 𝐵) + (𝐸 · 𝐴)) ∈ ℝ) | 
| 18 | 9, 17 | eqeltrid 2845 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 19 | 18 | resqcld 14165 | . . . . . 6
⊢ (𝜑 → (𝐶↑2) ∈ ℝ) | 
| 20 | 8, 19 | remulcld 11291 | . . . . 5
⊢ (𝜑 → ((𝐷↑2) · (𝐶↑2)) ∈ ℝ) | 
| 21 | 15 | resqcld 14165 | . . . . . . 7
⊢ (𝜑 → (𝐸↑2) ∈ ℝ) | 
| 22 | 21, 8 | readdcld 11290 | . . . . . 6
⊢ (𝜑 → ((𝐸↑2) + (𝐷↑2)) ∈ ℝ) | 
| 23 |  | 2itscp.r | . . . . . . . . 9
⊢ (𝜑 → 𝑅 ∈ ℝ) | 
| 24 | 23 | resqcld 14165 | . . . . . . . 8
⊢ (𝜑 → (𝑅↑2) ∈ ℝ) | 
| 25 | 21, 24 | remulcld 11291 | . . . . . . 7
⊢ (𝜑 → ((𝐸↑2) · (𝑅↑2)) ∈ ℝ) | 
| 26 | 19, 25 | resubcld 11691 | . . . . . 6
⊢ (𝜑 → ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))) ∈ ℝ) | 
| 27 | 22, 26 | remulcld 11291 | . . . . 5
⊢ (𝜑 → (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))) ∈ ℝ) | 
| 28 | 20, 27 | resubcld 11691 | . . . 4
⊢ (𝜑 → (((𝐷↑2) · (𝐶↑2)) − (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))) ∈
ℝ) | 
| 29 |  | 4pos 12373 | . . . . 5
⊢ 0 <
4 | 
| 30 | 29 | a1i 11 | . . . 4
⊢ (𝜑 → 0 < 4) | 
| 31 | 8, 24 | remulcld 11291 | . . . . . . . . 9
⊢ (𝜑 → ((𝐷↑2) · (𝑅↑2)) ∈ ℝ) | 
| 32 | 25, 31 | readdcld 11290 | . . . . . . . 8
⊢ (𝜑 → (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) ∈ ℝ) | 
| 33 | 32, 19 | resubcld 11691 | . . . . . . 7
⊢ (𝜑 → ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (𝐶↑2)) ∈ ℝ) | 
| 34 | 12 | a1i 11 | . . . . . . . . 9
⊢ (𝜑 → 𝐸 = (𝐵 − 𝑌)) | 
| 35 | 10 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 36 | 13 | recnd 11289 | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ ℂ) | 
| 37 |  | itscnhlinecirc02plem1.n | . . . . . . . . . 10
⊢ (𝜑 → 𝐵 ≠ 𝑌) | 
| 38 | 35, 36, 37 | subne0d 11629 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 − 𝑌) ≠ 0) | 
| 39 | 34, 38 | eqnetrd 3008 | . . . . . . . 8
⊢ (𝜑 → 𝐸 ≠ 0) | 
| 40 | 15, 39 | sqgt0d 14289 | . . . . . . 7
⊢ (𝜑 → 0 < (𝐸↑2)) | 
| 41 |  | 2itscp.l | . . . . . . . . 9
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) < (𝑅↑2)) | 
| 42 | 37 | orcd 874 | . . . . . . . . 9
⊢ (𝜑 → (𝐵 ≠ 𝑌 ∨ 𝐴 ≠ 𝑋)) | 
| 43 |  | eqid 2737 | . . . . . . . . 9
⊢ ((𝐸↑2) + (𝐷↑2)) = ((𝐸↑2) + (𝐷↑2)) | 
| 44 |  | eqid 2737 | . . . . . . . . 9
⊢ (((𝑅↑2) · ((𝐸↑2) + (𝐷↑2))) − (𝐶↑2)) = (((𝑅↑2) · ((𝐸↑2) + (𝐷↑2))) − (𝐶↑2)) | 
| 45 | 5, 10, 4, 13, 3, 12, 9, 23, 41, 42, 43, 44 | 2itscp 48702 | . . . . . . . 8
⊢ (𝜑 → 0 < (((𝑅↑2) · ((𝐸↑2) + (𝐷↑2))) − (𝐶↑2))) | 
| 46 | 21 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) | 
| 47 | 8 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) | 
| 48 | 24 | recnd 11289 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑅↑2) ∈ ℂ) | 
| 49 | 46, 47, 48 | adddird 11286 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐸↑2) + (𝐷↑2)) · (𝑅↑2)) = (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2)))) | 
| 50 | 46, 47 | addcld 11280 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐸↑2) + (𝐷↑2)) ∈ ℂ) | 
| 51 | 50, 48 | mulcomd 11282 | . . . . . . . . . 10
⊢ (𝜑 → (((𝐸↑2) + (𝐷↑2)) · (𝑅↑2)) = ((𝑅↑2) · ((𝐸↑2) + (𝐷↑2)))) | 
| 52 | 49, 51 | eqtr3d 2779 | . . . . . . . . 9
⊢ (𝜑 → (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) = ((𝑅↑2) · ((𝐸↑2) + (𝐷↑2)))) | 
| 53 | 52 | oveq1d 7446 | . . . . . . . 8
⊢ (𝜑 → ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (𝐶↑2)) = (((𝑅↑2) · ((𝐸↑2) + (𝐷↑2))) − (𝐶↑2))) | 
| 54 | 45, 53 | breqtrrd 5171 | . . . . . . 7
⊢ (𝜑 → 0 < ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (𝐶↑2))) | 
| 55 | 21, 33, 40, 54 | mulgt0d 11416 | . . . . . 6
⊢ (𝜑 → 0 < ((𝐸↑2) · ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (𝐶↑2)))) | 
| 56 | 47, 46, 48 | mul12d 11470 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐷↑2) · ((𝐸↑2) · (𝑅↑2))) = ((𝐸↑2) · ((𝐷↑2) · (𝑅↑2)))) | 
| 57 | 56 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → (((𝐸↑2) · ((𝐸↑2) · (𝑅↑2))) + ((𝐷↑2) · ((𝐸↑2) · (𝑅↑2)))) = (((𝐸↑2) · ((𝐸↑2) · (𝑅↑2))) + ((𝐸↑2) · ((𝐷↑2) · (𝑅↑2))))) | 
| 58 | 46, 48 | mulcld 11281 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐸↑2) · (𝑅↑2)) ∈ ℂ) | 
| 59 | 47, 48 | mulcld 11281 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐷↑2) · (𝑅↑2)) ∈ ℂ) | 
| 60 | 46, 58, 59 | adddid 11285 | . . . . . . . . 9
⊢ (𝜑 → ((𝐸↑2) · (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2)))) = (((𝐸↑2) · ((𝐸↑2) · (𝑅↑2))) + ((𝐸↑2) · ((𝐷↑2) · (𝑅↑2))))) | 
| 61 | 57, 60 | eqtr4d 2780 | . . . . . . . 8
⊢ (𝜑 → (((𝐸↑2) · ((𝐸↑2) · (𝑅↑2))) + ((𝐷↑2) · ((𝐸↑2) · (𝑅↑2)))) = ((𝐸↑2) · (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))))) | 
| 62 | 61 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → ((((𝐸↑2) · ((𝐸↑2) · (𝑅↑2))) + ((𝐷↑2) · ((𝐸↑2) · (𝑅↑2)))) − ((𝐸↑2) · (𝐶↑2))) = (((𝐸↑2) · (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2)))) − ((𝐸↑2) · (𝐶↑2)))) | 
| 63 | 58, 59 | addcld 11280 | . . . . . . . 8
⊢ (𝜑 → (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) ∈ ℂ) | 
| 64 | 19 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → (𝐶↑2) ∈ ℂ) | 
| 65 | 46, 63, 64 | subdid 11719 | . . . . . . 7
⊢ (𝜑 → ((𝐸↑2) · ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (𝐶↑2))) = (((𝐸↑2) · (((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2)))) − ((𝐸↑2) · (𝐶↑2)))) | 
| 66 | 62, 65 | eqtr4d 2780 | . . . . . 6
⊢ (𝜑 → ((((𝐸↑2) · ((𝐸↑2) · (𝑅↑2))) + ((𝐷↑2) · ((𝐸↑2) · (𝑅↑2)))) − ((𝐸↑2) · (𝐶↑2))) = ((𝐸↑2) · ((((𝐸↑2) · (𝑅↑2)) + ((𝐷↑2) · (𝑅↑2))) − (𝐶↑2)))) | 
| 67 | 55, 66 | breqtrrd 5171 | . . . . 5
⊢ (𝜑 → 0 < ((((𝐸↑2) · ((𝐸↑2) · (𝑅↑2))) + ((𝐷↑2) · ((𝐸↑2) · (𝑅↑2)))) − ((𝐸↑2) · (𝐶↑2)))) | 
| 68 | 15 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℂ) | 
| 69 | 68 | sqcld 14184 | . . . . . 6
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) | 
| 70 | 7 | recnd 11289 | . . . . . . 7
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 71 | 70 | sqcld 14184 | . . . . . 6
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) | 
| 72 | 25 | recnd 11289 | . . . . . 6
⊢ (𝜑 → ((𝐸↑2) · (𝑅↑2)) ∈ ℂ) | 
| 73 |  | mulsubaddmulsub 11727 | . . . . . 6
⊢ ((((𝐸↑2) ∈ ℂ ∧
(𝐷↑2) ∈ ℂ)
∧ ((𝐶↑2) ∈
ℂ ∧ ((𝐸↑2)
· (𝑅↑2)) ∈
ℂ)) → (((𝐷↑2) · (𝐶↑2)) − (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))) = ((((𝐸↑2) · ((𝐸↑2) · (𝑅↑2))) + ((𝐷↑2) · ((𝐸↑2) · (𝑅↑2)))) − ((𝐸↑2) · (𝐶↑2)))) | 
| 74 | 69, 71, 64, 72, 73 | syl22anc 839 | . . . . 5
⊢ (𝜑 → (((𝐷↑2) · (𝐶↑2)) − (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))) = ((((𝐸↑2) · ((𝐸↑2) · (𝑅↑2))) + ((𝐷↑2) · ((𝐸↑2) · (𝑅↑2)))) − ((𝐸↑2) · (𝐶↑2)))) | 
| 75 | 67, 74 | breqtrrd 5171 | . . . 4
⊢ (𝜑 → 0 < (((𝐷↑2) · (𝐶↑2)) − (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))) | 
| 76 | 2, 28, 30, 75 | mulgt0d 11416 | . . 3
⊢ (𝜑 → 0 < (4 ·
(((𝐷↑2) ·
(𝐶↑2)) −
(((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | 
| 77 |  | 4cn 12351 | . . . . 5
⊢ 4 ∈
ℂ | 
| 78 | 77 | a1i 11 | . . . 4
⊢ (𝜑 → 4 ∈
ℂ) | 
| 79 | 18 | recnd 11289 | . . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 80 | 79 | sqcld 14184 | . . . . 5
⊢ (𝜑 → (𝐶↑2) ∈ ℂ) | 
| 81 | 71, 80 | mulcld 11281 | . . . 4
⊢ (𝜑 → ((𝐷↑2) · (𝐶↑2)) ∈ ℂ) | 
| 82 | 69, 71 | addcld 11280 | . . . . 5
⊢ (𝜑 → ((𝐸↑2) + (𝐷↑2)) ∈ ℂ) | 
| 83 | 23 | recnd 11289 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ∈ ℂ) | 
| 84 | 83 | sqcld 14184 | . . . . . . 7
⊢ (𝜑 → (𝑅↑2) ∈ ℂ) | 
| 85 | 69, 84 | mulcld 11281 | . . . . . 6
⊢ (𝜑 → ((𝐸↑2) · (𝑅↑2)) ∈ ℂ) | 
| 86 | 80, 85 | subcld 11620 | . . . . 5
⊢ (𝜑 → ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))) ∈ ℂ) | 
| 87 | 82, 86 | mulcld 11281 | . . . 4
⊢ (𝜑 → (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))) ∈ ℂ) | 
| 88 | 78, 81, 87 | subdid 11719 | . . 3
⊢ (𝜑 → (4 · (((𝐷↑2) · (𝐶↑2)) − (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))) = ((4 · ((𝐷↑2) · (𝐶↑2))) − (4 ·
(((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | 
| 89 | 76, 88 | breqtrd 5169 | . 2
⊢ (𝜑 → 0 < ((4 ·
((𝐷↑2) · (𝐶↑2))) − (4 ·
(((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | 
| 90 |  | 2cnd 12344 | . . . . . 6
⊢ (𝜑 → 2 ∈
ℂ) | 
| 91 | 70, 79 | mulcld 11281 | . . . . . 6
⊢ (𝜑 → (𝐷 · 𝐶) ∈ ℂ) | 
| 92 | 90, 91 | mulcld 11281 | . . . . 5
⊢ (𝜑 → (2 · (𝐷 · 𝐶)) ∈ ℂ) | 
| 93 |  | sqneg 14156 | . . . . 5
⊢ ((2
· (𝐷 · 𝐶)) ∈ ℂ → (-(2
· (𝐷 · 𝐶))↑2) = ((2 · (𝐷 · 𝐶))↑2)) | 
| 94 | 92, 93 | syl 17 | . . . 4
⊢ (𝜑 → (-(2 · (𝐷 · 𝐶))↑2) = ((2 · (𝐷 · 𝐶))↑2)) | 
| 95 | 90, 91 | sqmuld 14198 | . . . 4
⊢ (𝜑 → ((2 · (𝐷 · 𝐶))↑2) = ((2↑2) · ((𝐷 · 𝐶)↑2))) | 
| 96 |  | sq2 14236 | . . . . . 6
⊢
(2↑2) = 4 | 
| 97 | 96 | a1i 11 | . . . . 5
⊢ (𝜑 → (2↑2) =
4) | 
| 98 | 70, 79 | sqmuld 14198 | . . . . 5
⊢ (𝜑 → ((𝐷 · 𝐶)↑2) = ((𝐷↑2) · (𝐶↑2))) | 
| 99 | 97, 98 | oveq12d 7449 | . . . 4
⊢ (𝜑 → ((2↑2) ·
((𝐷 · 𝐶)↑2)) = (4 · ((𝐷↑2) · (𝐶↑2)))) | 
| 100 | 94, 95, 99 | 3eqtrd 2781 | . . 3
⊢ (𝜑 → (-(2 · (𝐷 · 𝐶))↑2) = (4 · ((𝐷↑2) · (𝐶↑2)))) | 
| 101 | 100 | oveq1d 7446 | . 2
⊢ (𝜑 → ((-(2 · (𝐷 · 𝐶))↑2) − (4 · (((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2)))))) = ((4 · ((𝐷↑2) · (𝐶↑2))) − (4 ·
(((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) | 
| 102 | 89, 101 | breqtrrd 5171 | 1
⊢ (𝜑 → 0 < ((-(2 ·
(𝐷 · 𝐶))↑2) − (4 ·
(((𝐸↑2) + (𝐷↑2)) · ((𝐶↑2) − ((𝐸↑2) · (𝑅↑2))))))) |