Proof of Theorem 2sqmod
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2sqmod.6 | . . . . . 6
⊢ (𝜑 → 𝐴 ≤ 𝐵) | 
| 2 | 1 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ≤ 𝐵) | 
| 3 |  | 2sqmod.4 | . . . . . . . 8
⊢ (𝜑 → 𝐶 ∈
ℕ0) | 
| 4 | 3 | nn0red 12590 | . . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℝ) | 
| 5 | 4 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 ∈ ℝ) | 
| 6 |  | 2sqmod.3 | . . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℕ0) | 
| 7 | 6 | nn0red 12590 | . . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℝ) | 
| 8 | 7 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∈ ℝ) | 
| 9 | 3 | nn0ge0d 12592 | . . . . . . 7
⊢ (𝜑 → 0 ≤ 𝐶) | 
| 10 | 9 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐶) | 
| 11 | 6 | nn0ge0d 12592 | . . . . . . 7
⊢ (𝜑 → 0 ≤ 𝐵) | 
| 12 | 11 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐵) | 
| 13 | 3 | nn0cnd 12591 | . . . . . . . . 9
⊢ (𝜑 → 𝐶 ∈ ℂ) | 
| 14 | 13 | sqcld 14185 | . . . . . . . 8
⊢ (𝜑 → (𝐶↑2) ∈ ℂ) | 
| 15 | 14 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) ∈ ℂ) | 
| 16 | 6 | nn0cnd 12591 | . . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) | 
| 17 | 16 | sqcld 14185 | . . . . . . . 8
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) | 
| 18 | 17 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ) | 
| 19 |  | 2sqmod.2 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈
ℕ0) | 
| 20 | 19 | nn0cnd 12591 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 21 | 20 | sqcld 14185 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) | 
| 22 |  | 2sqmod.5 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐷 ∈
ℕ0) | 
| 23 | 22 | nn0cnd 12591 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝐷 ∈ ℂ) | 
| 24 | 23 | sqcld 14185 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐷↑2) ∈ ℂ) | 
| 25 |  | 2sqmod.8 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = 𝑃) | 
| 26 |  | 2sqmod.9 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝐶↑2) + (𝐷↑2)) = 𝑃) | 
| 27 | 25, 26 | eqtr4d 2779 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = ((𝐶↑2) + (𝐷↑2))) | 
| 28 | 21, 17, 14, 24, 27 | subaddeqd 11679 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2))) | 
| 29 | 28 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = ((𝐶↑2) − (𝐵↑2))) | 
| 30 | 19 | nn0zd 12641 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈ ℤ) | 
| 31 | 3 | nn0zd 12641 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ ℤ) | 
| 32 |  | dvdsmul1 16316 | . . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → 𝐴 ∥ (𝐴 · 𝐶)) | 
| 33 | 30, 31, 32 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∥ (𝐴 · 𝐶)) | 
| 34 | 33 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐴 · 𝐶)) | 
| 35 | 20, 13 | mulcld 11282 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℂ) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) ∈ ℂ) | 
| 37 | 16, 23 | mulcld 11282 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 · 𝐷) ∈ ℂ) | 
| 38 | 37 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 · 𝐷) ∈ ℂ) | 
| 39 | 19 | nn0red 12590 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐴 ∈ ℝ) | 
| 40 | 39, 4 | remulcld 11292 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴 · 𝐶) ∈ ℝ) | 
| 41 | 22 | nn0red 12590 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐷 ∈ ℝ) | 
| 42 | 7, 41 | remulcld 11292 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐵 · 𝐷) ∈ ℝ) | 
| 43 | 40, 42 | resubcld 11692 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℝ) | 
| 44 | 43 | recnd 11290 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ) | 
| 45 | 44 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) ∈ ℂ) | 
| 46 | 43 | sqge0d 14178 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2)) | 
| 47 |  | 2sqmod.1 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝑃 ∈ ℙ) | 
| 48 | 6 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝐵 ∈ ℤ) | 
| 49 | 47, 30, 48, 25 | 2sqn0 27479 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐴 ≠ 0) | 
| 50 |  | elnnne0 12542 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐴 ∈ ℕ ↔ (𝐴 ∈ ℕ0
∧ 𝐴 ≠
0)) | 
| 51 | 19, 49, 50 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐴 ∈ ℕ) | 
| 52 | 22 | nn0zd 12641 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → 𝐷 ∈ ℤ) | 
| 53 | 24, 14 | addcomd 11464 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → ((𝐷↑2) + (𝐶↑2)) = ((𝐶↑2) + (𝐷↑2))) | 
| 54 | 53, 26 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → ((𝐷↑2) + (𝐶↑2)) = 𝑃) | 
| 55 | 47, 52, 31, 54 | 2sqn0 27479 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐷 ≠ 0) | 
| 56 |  | elnnne0 12542 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐷 ∈ ℕ ↔ (𝐷 ∈ ℕ0
∧ 𝐷 ≠
0)) | 
| 57 | 22, 55, 56 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐷 ∈ ℕ) | 
| 58 | 51, 57 | nnmulcld 12320 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℕ) | 
| 59 | 47, 31, 52, 26 | 2sqn0 27479 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐶 ≠ 0) | 
| 60 |  | elnnne0 12542 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐶 ∈ ℕ ↔ (𝐶 ∈ ℕ0
∧ 𝐶 ≠
0)) | 
| 61 | 3, 59, 60 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐶 ∈ ℕ) | 
| 62 | 17, 21 | addcomd 11464 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝜑 → ((𝐵↑2) + (𝐴↑2)) = ((𝐴↑2) + (𝐵↑2))) | 
| 63 | 62, 25 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝜑 → ((𝐵↑2) + (𝐴↑2)) = 𝑃) | 
| 64 | 47, 48, 30, 63 | 2sqn0 27479 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝜑 → 𝐵 ≠ 0) | 
| 65 |  | elnnne0 12542 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐵 ∈ ℕ ↔ (𝐵 ∈ ℕ0
∧ 𝐵 ≠
0)) | 
| 66 | 6, 64, 65 | sylanbrc 583 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝜑 → 𝐵 ∈ ℕ) | 
| 67 | 61, 66 | nnmulcld 12320 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝜑 → (𝐶 · 𝐵) ∈ ℕ) | 
| 68 | 58, 67 | nnaddcld 12319 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℕ) | 
| 69 | 68 | nnsqcld 14284 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ) | 
| 70 | 69 | nnred 12282 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℝ) | 
| 71 | 43 | resqcld 14166 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℝ) | 
| 72 | 70, 71 | addge02d 11853 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (0 ≤ (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))) | 
| 73 | 46, 72 | mpbid 232 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))) | 
| 74 | 25, 26 | oveq12d 7450 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = (𝑃 · 𝑃)) | 
| 75 |  | bhmafibid1 15505 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) | 
| 76 | 39, 7, 4, 41, 75 | syl22anc 838 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) | 
| 77 | 74, 76 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) | 
| 78 |  | prmz 16713 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) | 
| 79 | 47, 78 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → 𝑃 ∈ ℤ) | 
| 80 | 79 | zcnd 12725 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → 𝑃 ∈ ℂ) | 
| 81 | 80 | sqvald 14184 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑃↑2) = (𝑃 · 𝑃)) | 
| 82 | 13, 16 | mulcomd 11283 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝜑 → (𝐶 · 𝐵) = (𝐵 · 𝐶)) | 
| 83 | 82 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) = ((𝐴 · 𝐷) + (𝐵 · 𝐶))) | 
| 84 | 83 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2)) | 
| 85 | 84 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐵 · 𝐶))↑2))) | 
| 86 | 77, 81, 85 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))) | 
| 87 | 73, 86 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2)) | 
| 88 | 87 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2)) | 
| 89 | 30, 52 | zmulcld 12730 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℤ) | 
| 90 | 31, 48 | zmulcld 12730 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → (𝐶 · 𝐵) ∈ ℤ) | 
| 91 | 89, 90 | zaddcld 12728 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ) | 
| 92 |  | dvdssqim 16592 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))) | 
| 93 | 79, 91, 92 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))) | 
| 94 |  | zsqcl 14170 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑃 ∈ ℤ → (𝑃↑2) ∈
ℤ) | 
| 95 | 79, 94 | syl 17 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝑃↑2) ∈ ℤ) | 
| 96 |  | dvdsle 16348 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃↑2) ∈ ℤ ∧
(((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))) | 
| 97 | 95, 69, 96 | syl2anc 584 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝑃↑2) ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))) | 
| 98 | 93, 97 | syld 47 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))) | 
| 99 | 98 | imp 406 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) | 
| 100 | 95 | zred 12724 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝑃↑2) ∈ ℝ) | 
| 101 | 70, 100 | letri3d 11404 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))) | 
| 102 | 101 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2) ↔ ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ≤ (𝑃↑2) ∧ (𝑃↑2) ≤ (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)))) | 
| 103 | 88, 99, 102 | mpbir2and 713 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) = (𝑃↑2)) | 
| 104 | 86 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝑃↑2) = ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))) | 
| 105 | 103, 104 | eqtr2d 2777 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) | 
| 106 | 70 | recnd 11290 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) ∈ ℂ) | 
| 107 | 71 | recnd 11290 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ∈ ℂ) | 
| 108 | 106, 106,
107 | subadd2d 11640 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))) | 
| 109 | 108 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) ↔ ((((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2))) | 
| 110 | 105, 109 | mpbird 257 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2)) | 
| 111 | 106 | subidd 11609 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0) | 
| 112 | 111 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2) − (((𝐴 · 𝐷) + (𝐶 · 𝐵))↑2)) = 0) | 
| 113 | 110, 112 | eqtr3d 2778 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴 · 𝐶) − (𝐵 · 𝐷))↑2) = 0) | 
| 114 | 45, 113 | sqeq0d 14186 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 · 𝐶) − (𝐵 · 𝐷)) = 0) | 
| 115 | 36, 38, 114 | subeq0d 11629 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 · 𝐶) = (𝐵 · 𝐷)) | 
| 116 | 34, 115 | breqtrd 5168 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ (𝐵 · 𝐷)) | 
| 117 | 47, 30, 48, 25 | 2sqcoprm 27480 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) | 
| 118 | 117 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 gcd 𝐵) = 1) | 
| 119 |  | coprmdvds 16691 | . . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴 ∥ 𝐷)) | 
| 120 | 30, 48, 52, 119 | syl3anc 1372 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴 ∥ 𝐷)) | 
| 121 | 120 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴 ∥ (𝐵 · 𝐷) ∧ (𝐴 gcd 𝐵) = 1) → 𝐴 ∥ 𝐷)) | 
| 122 | 116, 118,
121 | mp2and 699 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∥ 𝐷) | 
| 123 |  | dvdsle 16348 | . . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℤ ∧ 𝐷 ∈ ℕ) → (𝐴 ∥ 𝐷 → 𝐴 ≤ 𝐷)) | 
| 124 | 30, 57, 123 | syl2anc 584 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∥ 𝐷 → 𝐴 ≤ 𝐷)) | 
| 125 | 124 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 ∥ 𝐷 → 𝐴 ≤ 𝐷)) | 
| 126 | 122, 125 | mpd 15 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ≤ 𝐷) | 
| 127 | 51 | nnrpd 13076 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈
ℝ+) | 
| 128 | 127 | rprege0d 13085 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) | 
| 129 | 22 | nn0ge0d 12592 | . . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ 𝐷) | 
| 130 |  | le2sq 14175 | . . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℝ ∧ 0 ≤
𝐴) ∧ (𝐷 ∈ ℝ ∧ 0 ≤ 𝐷)) → (𝐴 ≤ 𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2))) | 
| 131 | 128, 41, 129, 130 | syl12anc 836 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 ≤ 𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2))) | 
| 132 | 131 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 ≤ 𝐷 ↔ (𝐴↑2) ≤ (𝐷↑2))) | 
| 133 | 126, 132 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ≤ (𝐷↑2)) | 
| 134 | 51 | nnsqcld 14284 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴↑2) ∈ ℕ) | 
| 135 | 134 | nnred 12282 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐴↑2) ∈ ℝ) | 
| 136 |  | zsqcl 14170 | . . . . . . . . . . . . . 14
⊢ (𝐷 ∈ ℤ → (𝐷↑2) ∈
ℤ) | 
| 137 | 52, 136 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷↑2) ∈ ℤ) | 
| 138 | 137 | zred 12724 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐷↑2) ∈ ℝ) | 
| 139 | 135, 138 | suble0d 11855 | . . . . . . . . . . 11
⊢ (𝜑 → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2))) | 
| 140 | 139 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) ≤ 0 ↔ (𝐴↑2) ≤ (𝐷↑2))) | 
| 141 | 133, 140 | mpbird 257 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) ≤ 0) | 
| 142 | 29, 141 | eqbrtrrd 5166 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) ≤ 0) | 
| 143 |  | dvdsmul1 16316 | . . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ) → 𝐵 ∥ (𝐵 · 𝐷)) | 
| 144 | 48, 52, 143 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ∥ (𝐵 · 𝐷)) | 
| 145 | 144 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐵 · 𝐷)) | 
| 146 | 145, 115 | breqtrrd 5170 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ (𝐴 · 𝐶)) | 
| 147 | 30, 48 | gcdcomd 16552 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 gcd 𝐵) = (𝐵 gcd 𝐴)) | 
| 148 | 147, 117 | eqtr3d 2778 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 gcd 𝐴) = 1) | 
| 149 | 148 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 gcd 𝐴) = 1) | 
| 150 |  | coprmdvds 16691 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵 ∥ 𝐶)) | 
| 151 | 48, 30, 31, 150 | syl3anc 1372 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵 ∥ 𝐶)) | 
| 152 | 151 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐵 ∥ (𝐴 · 𝐶) ∧ (𝐵 gcd 𝐴) = 1) → 𝐵 ∥ 𝐶)) | 
| 153 | 146, 149,
152 | mp2and 699 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ∥ 𝐶) | 
| 154 |  | dvdsle 16348 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ) → (𝐵 ∥ 𝐶 → 𝐵 ≤ 𝐶)) | 
| 155 | 48, 61, 154 | syl2anc 584 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∥ 𝐶 → 𝐵 ≤ 𝐶)) | 
| 156 | 155 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 ∥ 𝐶 → 𝐵 ≤ 𝐶)) | 
| 157 | 153, 156 | mpd 15 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐵 ≤ 𝐶) | 
| 158 | 7, 4, 11, 9 | le2sqd 14297 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐵 ≤ 𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2))) | 
| 159 | 158 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵 ≤ 𝐶 ↔ (𝐵↑2) ≤ (𝐶↑2))) | 
| 160 | 157, 159 | mpbid 232 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐵↑2) ≤ (𝐶↑2)) | 
| 161 | 4 | resqcld 14166 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐶↑2) ∈ ℝ) | 
| 162 |  | zsqcl 14170 | . . . . . . . . . . . . 13
⊢ (𝐵 ∈ ℤ → (𝐵↑2) ∈
ℤ) | 
| 163 | 48, 162 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵↑2) ∈ ℤ) | 
| 164 | 163 | zred 12724 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐵↑2) ∈ ℝ) | 
| 165 | 161, 164 | subge0d 11854 | . . . . . . . . . 10
⊢ (𝜑 → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2))) | 
| 166 | 165 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (0 ≤ ((𝐶↑2) − (𝐵↑2)) ↔ (𝐵↑2) ≤ (𝐶↑2))) | 
| 167 | 160, 166 | mpbird 257 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐶↑2) − (𝐵↑2))) | 
| 168 | 135, 138 | resubcld 11692 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐴↑2) − (𝐷↑2)) ∈ ℝ) | 
| 169 | 28, 168 | eqeltrrd 2841 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐶↑2) − (𝐵↑2)) ∈ ℝ) | 
| 170 |  | 0red 11265 | . . . . . . . . . 10
⊢ (𝜑 → 0 ∈
ℝ) | 
| 171 | 169, 170 | letri3d 11404 | . . . . . . . . 9
⊢ (𝜑 → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2))))) | 
| 172 | 171 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐶↑2) − (𝐵↑2)) = 0 ↔ (((𝐶↑2) − (𝐵↑2)) ≤ 0 ∧ 0 ≤ ((𝐶↑2) − (𝐵↑2))))) | 
| 173 | 142, 167,
172 | mpbir2and 713 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐶↑2) − (𝐵↑2)) = 0) | 
| 174 | 15, 18, 173 | subeq0d 11629 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐶↑2) = (𝐵↑2)) | 
| 175 | 5, 8, 10, 12, 174 | sq11d 14298 | . . . . 5
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 = 𝐵) | 
| 176 | 2, 175 | breqtrrd 5170 | . . . 4
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ≤ 𝐶) | 
| 177 |  | 2sqmod.7 | . . . . . 6
⊢ (𝜑 → 𝐶 ≤ 𝐷) | 
| 178 | 177 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 ≤ 𝐷) | 
| 179 | 39 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 ∈ ℝ) | 
| 180 | 41 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐷 ∈ ℝ) | 
| 181 | 19 | nn0ge0d 12592 | . . . . . . 7
⊢ (𝜑 → 0 ≤ 𝐴) | 
| 182 | 181 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐴) | 
| 183 | 129 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ 𝐷) | 
| 184 | 21 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) ∈ ℂ) | 
| 185 | 24 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ) | 
| 186 | 167, 29 | breqtrrd 5170 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 0 ≤ ((𝐴↑2) − (𝐷↑2))) | 
| 187 | 168, 170 | letri3d 11404 | . . . . . . . . 9
⊢ (𝜑 → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2))))) | 
| 188 | 187 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (((𝐴↑2) − (𝐷↑2)) = 0 ↔ (((𝐴↑2) − (𝐷↑2)) ≤ 0 ∧ 0 ≤ ((𝐴↑2) − (𝐷↑2))))) | 
| 189 | 141, 186,
188 | mpbir2and 713 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → ((𝐴↑2) − (𝐷↑2)) = 0) | 
| 190 | 184, 185,
189 | subeq0d 11629 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴↑2) = (𝐷↑2)) | 
| 191 | 179, 180,
182, 183, 190 | sq11d 14298 | . . . . 5
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐷) | 
| 192 | 178, 191 | breqtrrd 5170 | . . . 4
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐶 ≤ 𝐴) | 
| 193 | 39, 4 | letri3d 11404 | . . . . 5
⊢ (𝜑 → (𝐴 = 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴))) | 
| 194 | 193 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → (𝐴 = 𝐶 ↔ (𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴))) | 
| 195 | 176, 192,
194 | mpbir2and 713 | . . 3
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵))) → 𝐴 = 𝐶) | 
| 196 | 20 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 ∈ ℂ) | 
| 197 | 13 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐶 ∈ ℂ) | 
| 198 | 16 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℂ) | 
| 199 | 64 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ≠ 0) | 
| 200 | 41 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 ∈ ℝ) | 
| 201 | 7 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐵 ∈ ℝ) | 
| 202 | 129 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐷) | 
| 203 | 11 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 0 ≤ 𝐵) | 
| 204 | 24 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) ∈ ℂ) | 
| 205 | 17 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐵↑2) ∈ ℂ) | 
| 206 |  | prmnn 16712 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) | 
| 207 | 47, 206 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑃 ∈ ℕ) | 
| 208 | 207 | nnne0d 12317 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑃 ≠ 0) | 
| 209 | 208 | neneqd 2944 | . . . . . . . . . 10
⊢ (𝜑 → ¬ 𝑃 = 0) | 
| 210 | 209 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ¬ 𝑃 = 0) | 
| 211 | 80, 24, 17 | subdid 11720 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2)))) | 
| 212 | 80, 24 | mulcld 11282 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 · (𝐷↑2)) ∈ ℂ) | 
| 213 | 21, 24 | mulcld 11282 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴↑2) · (𝐷↑2)) ∈ ℂ) | 
| 214 | 80, 17 | mulcld 11282 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑃 · (𝐵↑2)) ∈ ℂ) | 
| 215 | 14, 17 | mulcld 11282 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐶↑2) · (𝐵↑2)) ∈ ℂ) | 
| 216 | 17, 24 | mulcomd 11283 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐵↑2) · (𝐷↑2)) = ((𝐷↑2) · (𝐵↑2))) | 
| 217 | 25 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝑃 − (𝐴↑2))) | 
| 218 | 21, 17 | pncan2d 11623 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) − (𝐴↑2)) = (𝐵↑2)) | 
| 219 | 217, 218 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑃 − (𝐴↑2)) = (𝐵↑2)) | 
| 220 | 219 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝐵↑2) · (𝐷↑2))) | 
| 221 | 26 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝑃 − (𝐶↑2))) | 
| 222 | 14, 24 | pncan2d 11623 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐶↑2) + (𝐷↑2)) − (𝐶↑2)) = (𝐷↑2)) | 
| 223 | 221, 222 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑃 − (𝐶↑2)) = (𝐷↑2)) | 
| 224 | 223 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝐷↑2) · (𝐵↑2))) | 
| 225 | 216, 220,
224 | 3eqtr4d 2786 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 − (𝐶↑2)) · (𝐵↑2))) | 
| 226 | 80, 21, 24 | subdird 11721 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑃 − (𝐴↑2)) · (𝐷↑2)) = ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2)))) | 
| 227 | 80, 14, 17 | subdird 11721 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑃 − (𝐶↑2)) · (𝐵↑2)) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2)))) | 
| 228 | 225, 226,
227 | 3eqtr3d 2784 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝑃 · (𝐷↑2)) − ((𝐴↑2) · (𝐷↑2))) = ((𝑃 · (𝐵↑2)) − ((𝐶↑2) · (𝐵↑2)))) | 
| 229 | 212, 213,
214, 215, 228 | subeqxfrd 11673 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝑃 · (𝐷↑2)) − (𝑃 · (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2)))) | 
| 230 | 211, 229 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2)))) | 
| 231 | 20, 23 | sqmuld 14199 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 · 𝐷)↑2) = ((𝐴↑2) · (𝐷↑2))) | 
| 232 | 13, 16 | sqmuld 14199 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐶 · 𝐵)↑2) = ((𝐶↑2) · (𝐵↑2))) | 
| 233 | 231, 232 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴↑2) · (𝐷↑2)) − ((𝐶↑2) · (𝐵↑2)))) | 
| 234 | 20, 23 | mulcld 11282 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℂ) | 
| 235 | 13, 16 | mulcld 11282 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶 · 𝐵) ∈ ℂ) | 
| 236 |  | subsq 14250 | . . . . . . . . . . . . . . 15
⊢ (((𝐴 · 𝐷) ∈ ℂ ∧ (𝐶 · 𝐵) ∈ ℂ) → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵)))) | 
| 237 | 234, 235,
236 | syl2anc 584 | . . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴 · 𝐷)↑2) − ((𝐶 · 𝐵)↑2)) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵)))) | 
| 238 | 230, 233,
237 | 3eqtr2d 2782 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵)))) | 
| 239 | 238 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵)))) | 
| 240 | 234 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) ∈ ℂ) | 
| 241 |  | simpll 766 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → 𝜑) | 
| 242 |  | simpr 484 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) | 
| 243 | 242 | neqned 2946 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) | 
| 244 | 89, 90 | zsubcld 12729 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) | 
| 245 |  | dvdssqim 16592 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))) | 
| 246 | 79, 244, 245 | syl2anc 584 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))) | 
| 247 | 246 | imp 406 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) | 
| 248 | 247 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) | 
| 249 | 95 | adantr 480 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝑃↑2) ∈ ℤ) | 
| 250 | 244 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) | 
| 251 | 234 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ∈ ℂ) | 
| 252 | 235 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐶 · 𝐵) ∈ ℂ) | 
| 253 |  | simpr 484 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) | 
| 254 | 251, 252,
253 | subne0d 11630 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ≠ 0) | 
| 255 | 250, 254 | znsqcld 14203 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ) | 
| 256 |  | dvdsle 16348 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑃↑2) ∈ ℤ ∧
(((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℕ) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))) | 
| 257 | 249, 255,
256 | syl2anc 584 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) → ((𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))) | 
| 258 | 257 | imp 406 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐴 · 𝐷) ≠ (𝐶 · 𝐵)) ∧ (𝑃↑2) ∥ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) | 
| 259 | 241, 243,
248, 258 | syl21anc 837 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) | 
| 260 | 39, 41 | remulcld 11292 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴 · 𝐷) ∈ ℝ) | 
| 261 | 4, 7 | remulcld 11292 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐶 · 𝐵) ∈ ℝ) | 
| 262 | 260, 261 | resubcld 11692 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℝ) | 
| 263 | 262 | resqcld 14166 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) ∈ ℝ) | 
| 264 | 61 | nnrpd 13076 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐶 ∈
ℝ+) | 
| 265 | 127, 264 | rpmulcld 13094 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐴 · 𝐶) ∈
ℝ+) | 
| 266 | 66 | nnrpd 13076 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐵 ∈
ℝ+) | 
| 267 | 57 | nnrpd 13076 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 𝐷 ∈
ℝ+) | 
| 268 | 266, 267 | rpmulcld 13094 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐵 · 𝐷) ∈
ℝ+) | 
| 269 | 265, 268 | rpaddcld 13093 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((𝐴 · 𝐶) + (𝐵 · 𝐷)) ∈
ℝ+) | 
| 270 |  | 2z 12651 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ 2 ∈
ℤ | 
| 271 | 270 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 2 ∈
ℤ) | 
| 272 | 269, 271 | rpexpcld 14287 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) ∈
ℝ+) | 
| 273 | 263, 272 | ltaddrp2d 13112 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))) | 
| 274 |  | bhmafibid2 15506 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ (𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ)) →
(((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))) | 
| 275 | 39, 7, 4, 41, 274 | syl22anc 838 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((𝐴↑2) + (𝐵↑2)) · ((𝐶↑2) + (𝐷↑2))) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))) | 
| 276 | 74, 275 | eqtr3d 2778 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))) | 
| 277 | 82 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = ((𝐴 · 𝐷) − (𝐵 · 𝐶))) | 
| 278 | 277 | oveq1d 7447 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) = (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2)) | 
| 279 | 278 | oveq2d 7448 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐵 · 𝐶))↑2))) | 
| 280 | 276, 279 | eqtr4d 2779 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑃 · 𝑃) = ((((𝐴 · 𝐶) + (𝐵 · 𝐷))↑2) + (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))) | 
| 281 | 273, 280 | breqtrrd 5170 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃 · 𝑃)) | 
| 282 | 281, 81 | breqtrrd 5170 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2)) | 
| 283 | 241, 282 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2)) | 
| 284 | 263, 100 | ltnled 11409 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))) | 
| 285 | 241, 284 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ((((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2) < (𝑃↑2) ↔ ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2))) | 
| 286 | 283, 285 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ∧ ¬ (𝐴 · 𝐷) = (𝐶 · 𝐵)) → ¬ (𝑃↑2) ≤ (((𝐴 · 𝐷) − (𝐶 · 𝐵))↑2)) | 
| 287 | 259, 286 | condan 817 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐶 · 𝐵)) | 
| 288 | 240, 287 | subeq0bd 11690 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐴 · 𝐷) − (𝐶 · 𝐵)) = 0) | 
| 289 | 288 | oveq2d 7448 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) = (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0)) | 
| 290 | 234, 235 | addcld 11281 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℂ) | 
| 291 | 290 | mul01d 11461 | . . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0) | 
| 292 | 291 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · 0) = 0) | 
| 293 | 239, 289,
292 | 3eqtrd 2780 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0) | 
| 294 | 24, 17 | subcld 11621 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℂ) | 
| 295 | 80, 294 | mul0ord 11914 | . . . . . . . . . . . 12
⊢ (𝜑 → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0))) | 
| 296 | 295 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝑃 · ((𝐷↑2) − (𝐵↑2))) = 0 ↔ (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0))) | 
| 297 | 293, 296 | mpbid 232 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝑃 = 0 ∨ ((𝐷↑2) − (𝐵↑2)) = 0)) | 
| 298 | 297 | ord 864 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (¬ 𝑃 = 0 → ((𝐷↑2) − (𝐵↑2)) = 0)) | 
| 299 | 210, 298 | mpd 15 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → ((𝐷↑2) − (𝐵↑2)) = 0) | 
| 300 | 204, 205,
299 | subeq0d 11629 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐷↑2) = (𝐵↑2)) | 
| 301 | 200, 201,
202, 203, 300 | sq11d 14298 | . . . . . 6
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐷 = 𝐵) | 
| 302 | 301 | oveq2d 7448 | . . . . 5
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐷) = (𝐴 · 𝐵)) | 
| 303 | 302, 287 | eqtr3d 2778 | . . . 4
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → (𝐴 · 𝐵) = (𝐶 · 𝐵)) | 
| 304 | 196, 197,
198, 199, 303 | mulcan2ad 11900 | . . 3
⊢ ((𝜑 ∧ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))) → 𝐴 = 𝐶) | 
| 305 | 137, 163 | zsubcld 12729 | . . . . . 6
⊢ (𝜑 → ((𝐷↑2) − (𝐵↑2)) ∈ ℤ) | 
| 306 |  | dvdsmul1 16316 | . . . . . 6
⊢ ((𝑃 ∈ ℤ ∧ ((𝐷↑2) − (𝐵↑2)) ∈ ℤ) →
𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2)))) | 
| 307 | 79, 305, 306 | syl2anc 584 | . . . . 5
⊢ (𝜑 → 𝑃 ∥ (𝑃 · ((𝐷↑2) − (𝐵↑2)))) | 
| 308 | 307, 238 | breqtrd 5168 | . . . 4
⊢ (𝜑 → 𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵)))) | 
| 309 |  | euclemma 16751 | . . . . 5
⊢ ((𝑃 ∈ ℙ ∧ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∈ ℤ ∧ ((𝐴 · 𝐷) − (𝐶 · 𝐵)) ∈ ℤ) → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))))) | 
| 310 | 47, 91, 244, 309 | syl3anc 1372 | . . . 4
⊢ (𝜑 → (𝑃 ∥ (((𝐴 · 𝐷) + (𝐶 · 𝐵)) · ((𝐴 · 𝐷) − (𝐶 · 𝐵))) ↔ (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵))))) | 
| 311 | 308, 310 | mpbid 232 | . . 3
⊢ (𝜑 → (𝑃 ∥ ((𝐴 · 𝐷) + (𝐶 · 𝐵)) ∨ 𝑃 ∥ ((𝐴 · 𝐷) − (𝐶 · 𝐵)))) | 
| 312 | 195, 304,
311 | mpjaodan 960 | . 2
⊢ (𝜑 → 𝐴 = 𝐶) | 
| 313 | 312 | oveq1d 7447 | . . . . 5
⊢ (𝜑 → (𝐴↑2) = (𝐶↑2)) | 
| 314 | 313 | oveq2d 7448 | . . . 4
⊢ (𝜑 → (𝑃 − (𝐴↑2)) = (𝑃 − (𝐶↑2))) | 
| 315 | 314, 219,
223 | 3eqtr3d 2784 | . . 3
⊢ (𝜑 → (𝐵↑2) = (𝐷↑2)) | 
| 316 | 7, 41, 11, 129, 315 | sq11d 14298 | . 2
⊢ (𝜑 → 𝐵 = 𝐷) | 
| 317 | 312, 316 | jca 511 | 1
⊢ (𝜑 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) |