Proof of Theorem pellexlem6
Step | Hyp | Ref
| Expression |
1 | | pellex.ann |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℕ) |
2 | 1 | nncnd 10913 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ ℂ) |
3 | | pellex.enn |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ∈ ℕ) |
4 | 3 | nncnd 10913 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ℂ) |
5 | 2, 4 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → (𝐴 · 𝐸) ∈ ℂ) |
6 | | pellex.dnn |
. . . . . . . . 9
⊢ (𝜑 → 𝐷 ∈ ℕ) |
7 | 6 | nncnd 10913 |
. . . . . . . 8
⊢ (𝜑 → 𝐷 ∈ ℂ) |
8 | | pellex.bnn |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ ℕ) |
9 | 8 | nncnd 10913 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ ℂ) |
10 | | pellex.fnn |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℕ) |
11 | 10 | nncnd 10913 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ℂ) |
12 | 9, 11 | mulcld 9939 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℂ) |
13 | 7, 12 | mulcld 9939 |
. . . . . . 7
⊢ (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℂ) |
14 | 5, 13 | subcld 10271 |
. . . . . 6
⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℂ) |
15 | | pellex.cz |
. . . . . . 7
⊢ (𝜑 → 𝐶 ∈ ℤ) |
16 | 15 | zcnd 11359 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ ℂ) |
17 | | pellex.cn0 |
. . . . . 6
⊢ (𝜑 → 𝐶 ≠ 0) |
18 | 14, 16, 17 | absdivd 14042 |
. . . . 5
⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶))) |
19 | 5, 13 | negsubd 10277 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) |
20 | 19 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹)))) |
21 | 20 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶))) |
22 | 1 | nnred 10912 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℝ) |
23 | 3 | nnred 10912 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐸 ∈ ℝ) |
24 | 22, 23 | remulcld 9949 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 · 𝐸) ∈ ℝ) |
25 | 6 | nnred 10912 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈ ℝ) |
26 | 8 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℝ) |
27 | 10 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ ℝ) |
28 | 26, 27 | remulcld 9949 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℝ) |
29 | 25, 28 | remulcld 9949 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℝ) |
30 | 29 | renegcld 10336 |
. . . . . . . . . 10
⊢ (𝜑 → -(𝐷 · (𝐵 · 𝐹)) ∈ ℝ) |
31 | 16, 17 | absrpcld 14035 |
. . . . . . . . . 10
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ+) |
32 | 3 | nnzd 11357 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐸 ∈ ℤ) |
33 | | pellex.xcg |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) |
34 | | modmul1 12585 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧
(abs‘𝐶) ∈
ℝ+) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶))) |
35 | 22, 23, 32, 31, 33, 34 | syl221anc 1329 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶))) |
36 | 4 | sqcld 12868 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) |
37 | 11 | sqcld 12868 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐹↑2) ∈ ℂ) |
38 | 7, 37 | mulcld 9939 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℂ) |
39 | 36, 38 | npcand 10275 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) = (𝐸↑2)) |
40 | 4 | sqvald 12867 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸↑2) = (𝐸 · 𝐸)) |
41 | 39, 40 | eqtr2d 2645 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐸 · 𝐸) = (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2)))) |
42 | 41 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶))) |
43 | 23 | resqcld 12897 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐸↑2) ∈ ℝ) |
44 | 27 | resqcld 12897 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹↑2) ∈ ℝ) |
45 | 25, 44 | remulcld 9949 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℝ) |
46 | 43, 45 | resubcld 10337 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ) |
47 | | 0red 9920 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ∈
ℝ) |
48 | 16 | abscld 14023 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (abs‘𝐶) ∈
ℝ) |
49 | 48 | recnd 9947 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (abs‘𝐶) ∈
ℂ) |
50 | 16, 17 | absne0d 14034 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (abs‘𝐶) ≠ 0) |
51 | 49, 50 | dividd 10678 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) = 1) |
52 | | 1zzd 11285 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈
ℤ) |
53 | 51, 52 | eqeltrd 2688 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ) |
54 | | mod0 12537 |
. . . . . . . . . . . . . . . . 17
⊢
(((abs‘𝐶)
∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) →
(((abs‘𝐶) mod
(abs‘𝐶)) = 0 ↔
((abs‘𝐶) /
(abs‘𝐶)) ∈
ℤ)) |
55 | 48, 31, 54 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ)) |
56 | 53, 55 | mpbird 246 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((abs‘𝐶) mod (abs‘𝐶)) = 0) |
57 | 15 | zred 11358 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ ℝ) |
58 | | absmod0 13891 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐶 ∈ ℝ ∧
(abs‘𝐶) ∈
ℝ+) → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0)) |
59 | 57, 31, 58 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0)) |
60 | 56, 59 | mpbird 246 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐶 mod (abs‘𝐶)) = 0) |
61 | | pellex.no2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶) |
62 | 61 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (𝐶 mod (abs‘𝐶))) |
63 | | 0mod 12563 |
. . . . . . . . . . . . . . 15
⊢
((abs‘𝐶)
∈ ℝ+ → (0 mod (abs‘𝐶)) = 0) |
64 | 31, 63 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0 mod (abs‘𝐶)) = 0) |
65 | 60, 62, 64 | 3eqtr4d 2654 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶))) |
66 | | modadd1 12569 |
. . . . . . . . . . . . 13
⊢
(((((𝐸↑2)
− (𝐷 · (𝐹↑2))) ∈ ℝ ∧
0 ∈ ℝ) ∧ ((𝐷
· (𝐹↑2)) ∈
ℝ ∧ (abs‘𝐶)
∈ ℝ+) ∧ (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶))) → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶))) |
67 | 46, 47, 45, 31, 65, 66 | syl221anc 1329 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶))) |
68 | 38 | addid2d 10116 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐷 · (𝐹↑2))) |
69 | 11 | sqvald 12867 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐹↑2) = (𝐹 · 𝐹)) |
70 | 69 | oveq2d 6565 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷 · (𝐹↑2)) = (𝐷 · (𝐹 · 𝐹))) |
71 | 7, 11, 11 | mul12d 10124 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷 · (𝐹 · 𝐹)) = (𝐹 · (𝐷 · 𝐹))) |
72 | 68, 70, 71 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐹 · (𝐷 · 𝐹))) |
73 | 72 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶))) |
74 | 42, 67, 73 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶))) |
75 | 6 | nnzd 11357 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐷 ∈ ℤ) |
76 | 10 | nnzd 11357 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹 ∈ ℤ) |
77 | 75, 76 | zmulcld 11364 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷 · 𝐹) ∈ ℤ) |
78 | | pellex.ycg |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) |
79 | 78 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶))) |
80 | | modmul1 12585 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐷 · 𝐹) ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+)
∧ (𝐹 mod
(abs‘𝐶)) = (𝐵 mod (abs‘𝐶))) → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶))) |
81 | 27, 26, 77, 31, 79, 80 | syl221anc 1329 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶))) |
82 | 9, 7, 11 | mul12d 10124 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐵 · (𝐷 · 𝐹)) = (𝐷 · (𝐵 · 𝐹))) |
83 | 82 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) |
84 | 81, 83 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) |
85 | 35, 74, 84 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) |
86 | | modadd1 12569 |
. . . . . . . . . 10
⊢ ((((𝐴 · 𝐸) ∈ ℝ ∧ (𝐷 · (𝐵 · 𝐹)) ∈ ℝ) ∧ (-(𝐷 · (𝐵 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+)
∧ ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶))) |
87 | 24, 29, 30, 31, 85, 86 | syl221anc 1329 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶))) |
88 | 13 | negidd 10261 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) = 0) |
89 | 88 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶))) |
90 | 21, 87, 89 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶))) |
91 | 90, 64 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0) |
92 | 24, 29 | resubcld 10337 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ) |
93 | | absmod0 13891 |
. . . . . . . 8
⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+)
→ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0)) |
94 | 92, 31, 93 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0)) |
95 | 91, 94 | mpbid 221 |
. . . . . 6
⊢ (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0) |
96 | 14 | abscld 14023 |
. . . . . . 7
⊢ (𝜑 → (abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ) |
97 | | mod0 12537 |
. . . . . . 7
⊢
(((abs‘((𝐴
· 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+)
→ (((abs‘((𝐴
· 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ)) |
98 | 96, 31, 97 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ)) |
99 | 95, 98 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ) |
100 | 18, 99 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ) |
101 | 92, 57, 17 | redivcld 10732 |
. . . . 5
⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ) |
102 | | absz 13899 |
. . . . 5
⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ)) |
103 | 101, 102 | syl 17 |
. . . 4
⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ)) |
104 | 100, 103 | mpbird 246 |
. . 3
⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ) |
105 | | 0lt1 10429 |
. . . . . . . 8
⊢ 0 <
1 |
106 | | 0re 9919 |
. . . . . . . . 9
⊢ 0 ∈
ℝ |
107 | | 1re 9918 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
108 | 106, 107 | ltnlei 10037 |
. . . . . . . 8
⊢ (0 < 1
↔ ¬ 1 ≤ 0) |
109 | 105, 108 | mpbi 219 |
. . . . . . 7
⊢ ¬ 1
≤ 0 |
110 | 9, 4 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 · 𝐸) ∈ ℂ) |
111 | 2, 11 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴 · 𝐹) ∈ ℂ) |
112 | 110, 111 | subcld 10271 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℂ) |
113 | 112, 16, 17 | divcld 10680 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℂ) |
114 | 113 | abscld 14023 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℝ) |
115 | 114 | resqcld 12897 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) ∈ ℝ) |
116 | 6 | nnnn0d 11228 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
117 | 116 | nn0ge0d 11231 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ 𝐷) |
118 | 114 | sqge0d 12898 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤
((abs‘(((𝐵 ·
𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) |
119 | 25, 115, 117, 118 | mulge0d 10483 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) |
120 | 25, 115 | remulcld 9949 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) ∈ ℝ) |
121 | 47, 120 | suble0d 10497 |
. . . . . . . . 9
⊢ (𝜑 → ((0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0 ↔ 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))) |
122 | 119, 121 | mpbird 246 |
. . . . . . . 8
⊢ (𝜑 → (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0) |
123 | | breq1 4586 |
. . . . . . . 8
⊢ (1 = (0
− (𝐷 ·
((abs‘(((𝐵 ·
𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → (1 ≤ 0 ↔ (0
− (𝐷 ·
((abs‘(((𝐵 ·
𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0)) |
124 | 122, 123 | syl5ibrcom 236 |
. . . . . . 7
⊢ (𝜑 → (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → 1 ≤
0)) |
125 | 109, 124 | mtoi 189 |
. . . . . 6
⊢ (𝜑 → ¬ 1 = (0 −
(𝐷 ·
((abs‘(((𝐵 ·
𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))) |
126 | | absresq 13890 |
. . . . . . . . . . . 12
⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2)) |
127 | 101, 126 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2)) |
128 | 14, 16, 17 | sqdivd 12883 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2))) |
129 | 14 | sqvald 12867 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) = (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))))) |
130 | 129 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2))) |
131 | 127, 128,
130 | 3eqtrd 2648 |
. . . . . . . . . 10
⊢ (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2))) |
132 | 26, 23 | remulcld 9949 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 · 𝐸) ∈ ℝ) |
133 | 22, 27 | remulcld 9949 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐴 · 𝐹) ∈ ℝ) |
134 | 132, 133 | resubcld 10337 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ) |
135 | 134, 57, 17 | redivcld 10732 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ) |
136 | | absresq 13890 |
. . . . . . . . . . . . . 14
⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2)) |
137 | 135, 136 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2)) |
138 | 112, 16, 17 | sqdivd 12883 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))) |
139 | 137, 138 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))) |
140 | 139 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))) |
141 | 112 | sqcld 12868 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) ∈ ℂ) |
142 | 16 | sqcld 12868 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶↑2) ∈ ℂ) |
143 | | sqne0 12792 |
. . . . . . . . . . . . . 14
⊢ (𝐶 ∈ ℂ → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0)) |
144 | 16, 143 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0)) |
145 | 17, 144 | mpbird 246 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶↑2) ≠ 0) |
146 | 7, 141, 142, 145 | divassd 10715 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))) |
147 | 112 | sqvald 12867 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) = (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) |
148 | 147 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) = (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) |
149 | 148 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))) |
150 | 140, 146,
149 | 3eqtr2d 2650 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))) |
151 | 131, 150 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))) |
152 | 14, 14 | mulcld 9939 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ) |
153 | 112, 112 | mulcld 9939 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℂ) |
154 | 7, 153 | mulcld 9939 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) ∈ ℂ) |
155 | 152, 154,
142, 145 | divsubdird 10719 |
. . . . . . . . 9
⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))) |
156 | 5, 13, 5, 13 | mulsubd 10369 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹)))))) |
157 | 110, 111,
110, 111 | mulsubd 10369 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) = ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) |
158 | 157 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) |
159 | 110, 110 | mulcld 9939 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐵 · 𝐸)) ∈ ℂ) |
160 | 111, 111 | mulcld 9939 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 · 𝐹) · (𝐴 · 𝐹)) ∈ ℂ) |
161 | 159, 160 | addcld 9938 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ) |
162 | 110, 111 | mulcld 9939 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐴 · 𝐹)) ∈ ℂ) |
163 | 162, 162 | addcld 9938 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ) |
164 | 7, 161, 163 | subdid 10365 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) |
165 | 7, 159, 160 | adddid 9943 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) |
166 | 7, 162, 162 | adddid 9943 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) |
167 | 165, 166 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) |
168 | 158, 164,
167 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) |
169 | 156, 168 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))) |
170 | 169 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2))) |
171 | 5, 13 | mulcomd 9940 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸))) |
172 | 7, 12, 5 | mulassd 9942 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)) = (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸)))) |
173 | 2, 4 | mulcomd 9940 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐴 · 𝐸) = (𝐸 · 𝐴)) |
174 | 173 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐹) · (𝐸 · 𝐴))) |
175 | 9, 11, 4, 2 | mul4d 10127 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐸 · 𝐴)) = ((𝐵 · 𝐸) · (𝐹 · 𝐴))) |
176 | 11, 2 | mulcomd 9940 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐹 · 𝐴) = (𝐴 · 𝐹)) |
177 | 176 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐹 · 𝐴)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹))) |
178 | 174, 175,
177 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹))) |
179 | 178 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) |
180 | 171, 172,
179 | 3eqtrd 2648 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) |
181 | 180, 180 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) |
182 | 181 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) |
183 | 182 | oveq1d 6564 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))) |
184 | 5, 5 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐴 · 𝐸)) ∈ ℂ) |
185 | 13, 13 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) ∈ ℂ) |
186 | 184, 185 | addcld 9938 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ) |
187 | 7, 159 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) ∈ ℂ) |
188 | 7, 160 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ) |
189 | 187, 188 | addcld 9938 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) ∈ ℂ) |
190 | 7, 162 | mulcld 9939 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ) |
191 | 190, 190 | addcld 9938 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) ∈ ℂ) |
192 | 186, 189,
191 | nnncan2d 10306 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))) |
193 | 184, 185,
187, 188 | addsub4d 10318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))) |
194 | 5 | sqvald 12867 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴 · 𝐸) · (𝐴 · 𝐸))) |
195 | 110 | sqvald 12867 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵 · 𝐸) · (𝐵 · 𝐸))) |
196 | 195 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) |
197 | 194, 196 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))))) |
198 | 13 | sqvald 12867 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) |
199 | 111 | sqvald 12867 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴 · 𝐹) · (𝐴 · 𝐹))) |
200 | 199 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) |
201 | 198, 200 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) |
202 | 197, 201 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))) |
203 | 2, 4 | sqmuld 12882 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴↑2) · (𝐸↑2))) |
204 | 9, 4 | sqmuld 12882 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵↑2) · (𝐸↑2))) |
205 | 204 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2)))) |
206 | 9 | sqcld 12868 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐵↑2) ∈ ℂ) |
207 | 7, 206, 36 | mulassd 9942 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐷 · (𝐵↑2)) · (𝐸↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2)))) |
208 | 205, 207 | eqtr4d 2647 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = ((𝐷 · (𝐵↑2)) · (𝐸↑2))) |
209 | 203, 208 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2)))) |
210 | 7 | sqvald 12867 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐷↑2) = (𝐷 · 𝐷)) |
211 | 9, 11 | sqmuld 12882 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐵 · 𝐹)↑2) = ((𝐵↑2) · (𝐹↑2))) |
212 | 210, 211 | oveq12d 6567 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐷↑2) · ((𝐵 · 𝐹)↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2)))) |
213 | 7, 12 | sqmuld 12882 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷↑2) · ((𝐵 · 𝐹)↑2))) |
214 | 7, 7 | mulcld 9939 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐷 · 𝐷) ∈ ℂ) |
215 | 214, 206,
37 | mulassd 9942 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2)))) |
216 | 212, 213,
215 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2))) |
217 | 2, 11 | sqmuld 12882 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴↑2) · (𝐹↑2))) |
218 | 217 | oveq2d 6565 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2)))) |
219 | 2 | sqcld 12868 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
220 | 7, 219, 37 | mulassd 9942 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐷 · (𝐴↑2)) · (𝐹↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2)))) |
221 | 218, 220 | eqtr4d 2647 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = ((𝐷 · (𝐴↑2)) · (𝐹↑2))) |
222 | 216, 221 | oveq12d 6567 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) |
223 | 209, 222 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))) |
224 | 7, 206 | mulcld 9939 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷 · (𝐵↑2)) ∈ ℂ) |
225 | 219, 224,
36 | subdird 10366 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2)))) |
226 | | pellex.no1 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶) |
227 | 226 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (𝐶 · (𝐸↑2))) |
228 | 225, 227 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) = (𝐶 · (𝐸↑2))) |
229 | 7, 7, 206 | mulassd 9942 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) = (𝐷 · (𝐷 · (𝐵↑2)))) |
230 | 229 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2)))) |
231 | 230 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2))) |
232 | 214, 206 | mulcld 9939 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) ∈ ℂ) |
233 | 7, 219 | mulcld 9939 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐷 · (𝐴↑2)) ∈ ℂ) |
234 | 232, 233,
37 | subdird 10366 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) |
235 | | subdi 10342 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) →
(𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2)))) |
236 | 235 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) →
((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2)))) |
237 | 7, 224, 219, 236 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2)))) |
238 | | negsubdi2 10219 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐴↑2) ∈ ℂ ∧
(𝐷 · (𝐵↑2)) ∈ ℂ) →
-((𝐴↑2) − (𝐷 · (𝐵↑2))) = ((𝐷 · (𝐵↑2)) − (𝐴↑2))) |
239 | 238 | eqcomd 2616 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴↑2) ∈ ℂ ∧
(𝐷 · (𝐵↑2)) ∈ ℂ) →
((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2)))) |
240 | 219, 224,
239 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2)))) |
241 | 226 | negeqd 10154 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = -𝐶) |
242 | 240, 241 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -𝐶) |
243 | 242 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = (𝐷 · -𝐶)) |
244 | 7, 16 | mulneg2d 10363 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐷 · -𝐶) = -(𝐷 · 𝐶)) |
245 | 237, 243,
244 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = -(𝐷 · 𝐶)) |
246 | 245 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (-(𝐷 · 𝐶) · (𝐹↑2))) |
247 | 231, 234,
246 | 3eqtr3d 2652 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))) = (-(𝐷 · 𝐶) · (𝐹↑2))) |
248 | 228, 247 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2)))) |
249 | 7, 16 | mulcld 9939 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐷 · 𝐶) ∈ ℂ) |
250 | 249, 37 | mulneg1d 10362 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -((𝐷 · 𝐶) · (𝐹↑2))) |
251 | 7, 16 | mulcomd 9940 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐷 · 𝐶) = (𝐶 · 𝐷)) |
252 | 251 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = ((𝐶 · 𝐷) · (𝐹↑2))) |
253 | 16, 7, 37 | mulassd 9942 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐶 · 𝐷) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2)))) |
254 | 252, 253 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2)))) |
255 | 254 | negeqd 10154 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → -((𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2)))) |
256 | 250, 255 | eqtrd 2644 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2)))) |
257 | 256 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2))))) |
258 | 16, 36 | mulcld 9939 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶 · (𝐸↑2)) ∈ ℂ) |
259 | 16, 38 | mulcld 9939 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶 · (𝐷 · (𝐹↑2))) ∈ ℂ) |
260 | 258, 259 | negsubd 10277 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2))))) |
261 | 61 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = (𝐶 · 𝐶)) |
262 | | subdi 10342 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧
(𝐷 · (𝐹↑2)) ∈ ℂ) →
(𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2))))) |
263 | 262 | eqcomd 2616 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧
(𝐷 · (𝐹↑2)) ∈ ℂ) →
((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2))))) |
264 | 16, 36, 38, 263 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2))))) |
265 | 16 | sqvald 12867 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐶↑2) = (𝐶 · 𝐶)) |
266 | 261, 264,
265 | 3eqtr4d 2654 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶↑2)) |
267 | 257, 260,
266 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = (𝐶↑2)) |
268 | 223, 248,
267 | 3eqtrd 2648 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = (𝐶↑2)) |
269 | 193, 202,
268 | 3eqtr2d 2650 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = (𝐶↑2)) |
270 | 183, 192,
269 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (𝐶↑2)) |
271 | 270 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝜑 → ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)) = ((𝐶↑2) / (𝐶↑2))) |
272 | 142, 145 | dividd 10678 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶↑2) / (𝐶↑2)) = 1) |
273 | 170, 271,
272 | 3eqtrd 2648 |
. . . . . . . . 9
⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = 1) |
274 | 151, 155,
273 | 3eqtr2d 2650 |
. . . . . . . 8
⊢ (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) |
275 | 274 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) |
276 | | simpr 476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) |
277 | 276 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) = (0 / 𝐶)) |
278 | 277 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = (abs‘(0 / 𝐶))) |
279 | 16, 17 | div0d 10679 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0 / 𝐶) = 0) |
280 | 279 | abs00bd 13879 |
. . . . . . . . . . 11
⊢ (𝜑 → (abs‘(0 / 𝐶)) = 0) |
281 | 280 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(0 / 𝐶)) = 0) |
282 | 278, 281 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = 0) |
283 | 282 | sq0id 12819 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = 0) |
284 | 283 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))) |
285 | 275, 284 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))) |
286 | 125, 285 | mtand 689 |
. . . . 5
⊢ (𝜑 → ¬ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) |
287 | 286 | neqned 2789 |
. . . 4
⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ≠ 0) |
288 | 14, 16, 287, 17 | divne0d 10696 |
. . 3
⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0) |
289 | | nnabscl 13913 |
. . 3
⊢
(((((𝐴 ·
𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ∧ (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ) |
290 | 104, 288,
289 | syl2anc 691 |
. 2
⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ) |
291 | 112, 16, 17 | absdivd 14042 |
. . . . 5
⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) = ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶))) |
292 | | negsub 10208 |
. . . . . . . . . . . 12
⊢ (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) + -(𝐴 · 𝐹)) = ((𝐵 · 𝐸) − (𝐴 · 𝐹))) |
293 | 292 | eqcomd 2616 |
. . . . . . . . . . 11
⊢ (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹))) |
294 | 110, 111,
293 | syl2anc 691 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹))) |
295 | 294 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶))) |
296 | 133 | renegcld 10336 |
. . . . . . . . . 10
⊢ (𝜑 → -(𝐴 · 𝐹) ∈ ℝ) |
297 | 11, 4 | mulcomd 9940 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 · 𝐸) = (𝐸 · 𝐹)) |
298 | 297 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐹 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶))) |
299 | | modmul1 12585 |
. . . . . . . . . . . 12
⊢ (((𝐵 ∈ ℝ ∧ 𝐹 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧
(abs‘𝐶) ∈
ℝ+) ∧ (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶))) |
300 | 26, 27, 32, 31, 78, 299 | syl221anc 1329 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶))) |
301 | | modmul1 12585 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐹 ∈ ℤ ∧
(abs‘𝐶) ∈
ℝ+) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶))) |
302 | 22, 23, 76, 31, 33, 301 | syl221anc 1329 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶))) |
303 | 298, 300,
302 | 3eqtr4d 2654 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶))) |
304 | | modadd1 12569 |
. . . . . . . . . 10
⊢ ((((𝐵 · 𝐸) ∈ ℝ ∧ (𝐴 · 𝐹) ∈ ℝ) ∧ (-(𝐴 · 𝐹) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+)
∧ ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶))) → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶))) |
305 | 132, 133,
296, 31, 303, 304 | syl221anc 1329 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶))) |
306 | 111 | negidd 10261 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 · 𝐹) + -(𝐴 · 𝐹)) = 0) |
307 | 306 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶))) |
308 | 295, 305,
307 | 3eqtrd 2648 |
. . . . . . . 8
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶))) |
309 | 308, 64 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0) |
310 | | absmod0 13891 |
. . . . . . . 8
⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+)
→ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0)) |
311 | 134, 31, 310 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0)) |
312 | 309, 311 | mpbid 221 |
. . . . . 6
⊢ (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0) |
313 | 112 | abscld 14023 |
. . . . . . 7
⊢ (𝜑 → (abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ) |
314 | | mod0 12537 |
. . . . . . 7
⊢
(((abs‘((𝐵
· 𝐸) − (𝐴 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+)
→ (((abs‘((𝐵
· 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ)) |
315 | 313, 31, 314 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ)) |
316 | 312, 315 | mpbid 221 |
. . . . 5
⊢ (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ) |
317 | 291, 316 | eqeltrd 2688 |
. . . 4
⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ) |
318 | | absz 13899 |
. . . . 5
⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ)) |
319 | 135, 318 | syl 17 |
. . . 4
⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ)) |
320 | 317, 319 | mpbird 246 |
. . 3
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ) |
321 | | pellex.neq |
. . . . . . 7
⊢ (𝜑 → ¬ (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)) |
322 | 10 | nnne0d 10942 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ≠ 0) |
323 | 3 | nnne0d 10942 |
. . . . . . . . 9
⊢ (𝜑 → 𝐸 ≠ 0) |
324 | 9, 11, 2, 4, 322, 323 | divmuleqd 10726 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) ↔ (𝐵 · 𝐸) = (𝐴 · 𝐹))) |
325 | 61 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶) |
326 | 325 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐸↑2) − (𝐷 · (𝐹↑2)))) |
327 | 326 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2))))) |
328 | 9, 11, 322 | divcld 10680 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 / 𝐹) ∈ ℂ) |
329 | 328 | sqcld 12868 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 / 𝐹)↑2) ∈ ℂ) |
330 | 329 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) ∈ ℂ) |
331 | 36 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ∈ ℂ) |
332 | 38 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (𝐹↑2)) ∈ ℂ) |
333 | 330, 331,
332 | subdid 10365 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))))) |
334 | | oveq1 6556 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 / 𝐹) = (𝐴 / 𝐸) → ((𝐵 / 𝐹)↑2) = ((𝐴 / 𝐸)↑2)) |
335 | 334 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2))) |
336 | 335 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2))) |
337 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐴 ∈ ℂ) |
338 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ∈ ℂ) |
339 | 323 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ≠ 0) |
340 | 337, 338,
339 | sqdivd 12883 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐴 / 𝐸)↑2) = ((𝐴↑2) / (𝐸↑2))) |
341 | 340 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴 / 𝐸)↑2) · (𝐸↑2)) = (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2))) |
342 | 219 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴↑2) ∈ ℂ) |
343 | | sqne0 12792 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐸 ∈ ℂ → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0)) |
344 | 4, 343 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0)) |
345 | 323, 344 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐸↑2) ≠ 0) |
346 | 345 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ≠ 0) |
347 | 342, 331,
346 | divcan1d 10681 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)) = (𝐴↑2)) |
348 | 336, 341,
347 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (𝐴↑2)) |
349 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐷 ∈ ℂ) |
350 | 37 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ∈ ℂ) |
351 | 330, 349,
350 | mul12d 10124 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2)))) |
352 | 9 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐵 ∈ ℂ) |
353 | 11 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ∈ ℂ) |
354 | 322 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ≠ 0) |
355 | 352, 353,
354 | sqdivd 12883 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = ((𝐵↑2) / (𝐹↑2))) |
356 | 355 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐹↑2)) = (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))) |
357 | 356 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))) = (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)))) |
358 | 206 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐵↑2) ∈ ℂ) |
359 | | sqne0 12792 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 ∈ ℂ → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0)) |
360 | 11, 359 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0)) |
361 | 322, 360 | mpbird 246 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐹↑2) ≠ 0) |
362 | 361 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ≠ 0) |
363 | 358, 350,
362 | divcan1d 10681 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)) = (𝐵↑2)) |
364 | 363 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))) = (𝐷 · (𝐵↑2))) |
365 | 351, 357,
364 | 3eqtrd 2648 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (𝐵↑2))) |
366 | 348, 365 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))) = ((𝐴↑2) − (𝐷 · (𝐵↑2)))) |
367 | 327, 333,
366 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = ((𝐴↑2) − (𝐷 · (𝐵↑2)))) |
368 | 226 | eqcomd 2616 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2)))) |
369 | 368 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2)))) |
370 | 367, 369 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2))))) |
371 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ∈ ℂ) |
372 | 17 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ≠ 0) |
373 | 330, 371,
372 | divcan4d 10686 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = ((𝐵 / 𝐹)↑2)) |
374 | 226, 226 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = (𝐶 / 𝐶)) |
375 | 16, 17 | dividd 10678 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶 / 𝐶) = 1) |
376 | 374, 375 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1) |
377 | 376 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1) |
378 | 370, 373,
377 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = 1) |
379 | 26, 27, 322 | redivcld 10732 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝐵 / 𝐹) ∈ ℝ) |
380 | 8 | nnnn0d 11228 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
381 | 380 | nn0ge0d 11231 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 ≤ 𝐵) |
382 | 10 | nngt0d 10941 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 0 < 𝐹) |
383 | | divge0 10771 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 ∈ ℝ ∧ 0 ≤
𝐵) ∧ (𝐹 ∈ ℝ ∧ 0 < 𝐹)) → 0 ≤ (𝐵 / 𝐹)) |
384 | 26, 381, 27, 382, 383 | syl22anc 1319 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ (𝐵 / 𝐹)) |
385 | 379, 384 | sqrtsqd 14006 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (√‘((𝐵 / 𝐹)↑2)) = (𝐵 / 𝐹)) |
386 | 385 | eqcomd 2616 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2))) |
387 | 386 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2))) |
388 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (((𝐵 / 𝐹)↑2) = 1 → (√‘((𝐵 / 𝐹)↑2)) =
(√‘1)) |
389 | 388 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘((𝐵 / 𝐹)↑2)) =
(√‘1)) |
390 | | sqrt1 13860 |
. . . . . . . . . . . . . 14
⊢
(√‘1) = 1 |
391 | 390 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘1) =
1) |
392 | 387, 389,
391 | 3eqtrd 2648 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = 1) |
393 | 392 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐵 / 𝐹) = 1)) |
394 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = (𝐴 / 𝐸)) |
395 | | simpr 476 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = 1) |
396 | 394, 395 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 / 𝐸) = 1) |
397 | 396 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = (1 · 𝐸)) |
398 | 2, 4, 323 | divcan1d 10681 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐴 / 𝐸) · 𝐸) = 𝐴) |
399 | 398 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = 𝐴) |
400 | 4 | mulid2d 9937 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 · 𝐸) = 𝐸) |
401 | 400 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐸) = 𝐸) |
402 | 397, 399,
401 | 3eqtr3d 2652 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐴 = 𝐸) |
403 | 395 | oveq1d 6564 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = (1 · 𝐹)) |
404 | 9, 11, 322 | divcan1d 10681 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ((𝐵 / 𝐹) · 𝐹) = 𝐵) |
405 | 404 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = 𝐵) |
406 | 11 | mulid2d 9937 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (1 · 𝐹) = 𝐹) |
407 | 406 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐹) = 𝐹) |
408 | 403, 405,
407 | 3eqtr3d 2652 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐵 = 𝐹) |
409 | 402, 408 | jca 553 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)) |
410 | 409 | ex 449 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹) = 1 → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))) |
411 | 393, 410 | syld 46 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))) |
412 | 378, 411 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)) |
413 | 412 | ex 449 |
. . . . . . . 8
⊢ (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))) |
414 | 324, 413 | sylbird 249 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 · 𝐸) = (𝐴 · 𝐹) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))) |
415 | 321, 414 | mtod 188 |
. . . . . 6
⊢ (𝜑 → ¬ (𝐵 · 𝐸) = (𝐴 · 𝐹)) |
416 | 415 | neqned 2789 |
. . . . 5
⊢ (𝜑 → (𝐵 · 𝐸) ≠ (𝐴 · 𝐹)) |
417 | 110, 111,
416 | subne0d 10280 |
. . . 4
⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ≠ 0) |
418 | 112, 16, 417, 17 | divne0d 10696 |
. . 3
⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0) |
419 | | nnabscl 13913 |
. . 3
⊢
(((((𝐵 ·
𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ∧ (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0) → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ) |
420 | 320, 418,
419 | syl2anc 691 |
. 2
⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ) |
421 | | oveq1 6556 |
. . . . 5
⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (𝑎↑2) = ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2)) |
422 | 421 | oveq1d 6564 |
. . . 4
⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2)))) |
423 | 422 | eqeq1d 2612 |
. . 3
⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1)) |
424 | | oveq1 6556 |
. . . . . 6
⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝑏↑2) = ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) |
425 | 424 | oveq2d 6565 |
. . . . 5
⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝐷 · (𝑏↑2)) = (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) |
426 | 425 | oveq2d 6565 |
. . . 4
⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))) |
427 | 426 | eqeq1d 2612 |
. . 3
⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → ((((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)) |
428 | 423, 427 | rspc2ev 3295 |
. 2
⊢
(((abs‘(((𝐴
· 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ ∧ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ ∧
(((abs‘(((𝐴 ·
𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) |
429 | 290, 420,
274, 428 | syl3anc 1318 |
1
⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) |