Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  pellexlem6 Structured version   Visualization version   GIF version

Theorem pellexlem6 41143
Description: Lemma for pellex 41144. Doing a field division between near solutions get us to norm 1, and the modularity constraint ensures we still have an integer. Returning NN guarantees that we are not returning the trivial solution (1,0). We are not explicitly defining the Pell-field, Pell-ring, and Pell-norm explicitly because after this construction is done we will never use them. This is mostly basic algebraic number theory and could be simplified if a generic framework for that were in place. (Contributed by Stefan O'Rear, 19-Oct-2014.)
Hypotheses
Ref Expression
pellex.ann (𝜑𝐴 ∈ ℕ)
pellex.bnn (𝜑𝐵 ∈ ℕ)
pellex.cz (𝜑𝐶 ∈ ℤ)
pellex.dnn (𝜑𝐷 ∈ ℕ)
pellex.irr (𝜑 → ¬ (√‘𝐷) ∈ ℚ)
pellex.enn (𝜑𝐸 ∈ ℕ)
pellex.fnn (𝜑𝐹 ∈ ℕ)
pellex.neq (𝜑 → ¬ (𝐴 = 𝐸𝐵 = 𝐹))
pellex.cn0 (𝜑𝐶 ≠ 0)
pellex.no1 (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)
pellex.no2 (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
pellex.xcg (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))
pellex.ycg (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))
Assertion
Ref Expression
pellexlem6 (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
Distinct variable groups:   𝑎,𝑏,𝐴   𝐵,𝑎,𝑏   𝐶,𝑎,𝑏   𝐷,𝑎,𝑏   𝐸,𝑎,𝑏   𝐹,𝑎,𝑏   𝜑,𝑎,𝑏

Proof of Theorem pellexlem6
StepHypRef Expression
1 pellex.ann . . . . . . . . 9 (𝜑𝐴 ∈ ℕ)
21nncnd 12169 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
3 pellex.enn . . . . . . . . 9 (𝜑𝐸 ∈ ℕ)
43nncnd 12169 . . . . . . . 8 (𝜑𝐸 ∈ ℂ)
52, 4mulcld 11175 . . . . . . 7 (𝜑 → (𝐴 · 𝐸) ∈ ℂ)
6 pellex.dnn . . . . . . . . 9 (𝜑𝐷 ∈ ℕ)
76nncnd 12169 . . . . . . . 8 (𝜑𝐷 ∈ ℂ)
8 pellex.bnn . . . . . . . . . 10 (𝜑𝐵 ∈ ℕ)
98nncnd 12169 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
10 pellex.fnn . . . . . . . . . 10 (𝜑𝐹 ∈ ℕ)
1110nncnd 12169 . . . . . . . . 9 (𝜑𝐹 ∈ ℂ)
129, 11mulcld 11175 . . . . . . . 8 (𝜑 → (𝐵 · 𝐹) ∈ ℂ)
137, 12mulcld 11175 . . . . . . 7 (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℂ)
145, 13subcld 11512 . . . . . 6 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
15 pellex.cz . . . . . . 7 (𝜑𝐶 ∈ ℤ)
1615zcnd 12608 . . . . . 6 (𝜑𝐶 ∈ ℂ)
17 pellex.cn0 . . . . . 6 (𝜑𝐶 ≠ 0)
1814, 16, 17absdivd 15340 . . . . 5 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)))
195, 13negsubd 11518 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))))
2019eqcomd 2742 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))))
2120oveq1d 7372 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
221nnred 12168 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
233nnred 12168 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℝ)
2422, 23remulcld 11185 . . . . . . . . . 10 (𝜑 → (𝐴 · 𝐸) ∈ ℝ)
256nnred 12168 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℝ)
268nnred 12168 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
2710nnred 12168 . . . . . . . . . . . 12 (𝜑𝐹 ∈ ℝ)
2826, 27remulcld 11185 . . . . . . . . . . 11 (𝜑 → (𝐵 · 𝐹) ∈ ℝ)
2925, 28remulcld 11185 . . . . . . . . . 10 (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
3029renegcld 11582 . . . . . . . . . 10 (𝜑 → -(𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
3116, 17absrpcld 15333 . . . . . . . . . 10 (𝜑 → (abs‘𝐶) ∈ ℝ+)
323nnzd 12526 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℤ)
33 pellex.xcg . . . . . . . . . . . 12 (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))
34 modmul1 13829 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
3522, 23, 32, 31, 33, 34syl221anc 1381 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
364sqcld 14049 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸↑2) ∈ ℂ)
3711sqcld 14049 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹↑2) ∈ ℂ)
387, 37mulcld 11175 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℂ)
3936, 38npcand 11516 . . . . . . . . . . . . . 14 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) = (𝐸↑2))
404sqvald 14048 . . . . . . . . . . . . . 14 (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
4139, 40eqtr2d 2777 . . . . . . . . . . . . 13 (𝜑 → (𝐸 · 𝐸) = (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))))
4241oveq1d 7372 . . . . . . . . . . . 12 (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
4323resqcld 14030 . . . . . . . . . . . . . 14 (𝜑 → (𝐸↑2) ∈ ℝ)
4427resqcld 14030 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹↑2) ∈ ℝ)
4525, 44remulcld 11185 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℝ)
4643, 45resubcld 11583 . . . . . . . . . . . . 13 (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ)
47 0red 11158 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
4816abscld 15321 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘𝐶) ∈ ℝ)
4948recnd 11183 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘𝐶) ∈ ℂ)
5016, 17absne0d 15332 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘𝐶) ≠ 0)
5149, 50dividd 11929 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) = 1)
52 1zzd 12534 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
5351, 52eqeltrd 2838 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ)
54 mod0 13781 . . . . . . . . . . . . . . . . 17 (((abs‘𝐶) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
5548, 31, 54syl2anc 584 . . . . . . . . . . . . . . . 16 (𝜑 → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
5653, 55mpbird 256 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐶) mod (abs‘𝐶)) = 0)
5715zred 12607 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℝ)
58 absmod0 15188 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
5957, 31, 58syl2anc 584 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
6056, 59mpbird 256 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 mod (abs‘𝐶)) = 0)
61 pellex.no2 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
6261oveq1d 7372 . . . . . . . . . . . . . 14 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (𝐶 mod (abs‘𝐶)))
63 0mod 13807 . . . . . . . . . . . . . . 15 ((abs‘𝐶) ∈ ℝ+ → (0 mod (abs‘𝐶)) = 0)
6431, 63syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0 mod (abs‘𝐶)) = 0)
6560, 62, 643eqtr4d 2786 . . . . . . . . . . . . 13 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
66 modadd1 13813 . . . . . . . . . . . . 13 (((((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ ∧ 0 ∈ ℝ) ∧ ((𝐷 · (𝐹↑2)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶))) → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
6746, 47, 45, 31, 65, 66syl221anc 1381 . . . . . . . . . . . 12 (𝜑 → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
6838addid2d 11356 . . . . . . . . . . . . . 14 (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐷 · (𝐹↑2)))
6911sqvald 14048 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
7069oveq2d 7373 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹↑2)) = (𝐷 · (𝐹 · 𝐹)))
717, 11, 11mul12d 11364 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹 · 𝐹)) = (𝐹 · (𝐷 · 𝐹)))
7268, 70, 713eqtrd 2780 . . . . . . . . . . . . 13 (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐹 · (𝐷 · 𝐹)))
7372oveq1d 7372 . . . . . . . . . . . 12 (𝜑 → ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
7442, 67, 733eqtrd 2780 . . . . . . . . . . 11 (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
756nnzd 12526 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ ℤ)
7610nnzd 12526 . . . . . . . . . . . . . 14 (𝜑𝐹 ∈ ℤ)
7775, 76zmulcld 12613 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · 𝐹) ∈ ℤ)
78 pellex.ycg . . . . . . . . . . . . . 14 (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))
7978eqcomd 2742 . . . . . . . . . . . . 13 (𝜑 → (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶)))
80 modmul1 13829 . . . . . . . . . . . . 13 (((𝐹 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐷 · 𝐹) ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶))) → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
8127, 26, 77, 31, 79, 80syl221anc 1381 . . . . . . . . . . . 12 (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
829, 7, 11mul12d 11364 . . . . . . . . . . . . 13 (𝜑 → (𝐵 · (𝐷 · 𝐹)) = (𝐷 · (𝐵 · 𝐹)))
8382oveq1d 7372 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
8481, 83eqtrd 2776 . . . . . . . . . . 11 (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
8535, 74, 843eqtrd 2780 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
86 modadd1 13813 . . . . . . . . . 10 ((((𝐴 · 𝐸) ∈ ℝ ∧ (𝐷 · (𝐵 · 𝐹)) ∈ ℝ) ∧ (-(𝐷 · (𝐵 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) ∧ ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
8724, 29, 30, 31, 85, 86syl221anc 1381 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
8813negidd 11502 . . . . . . . . . 10 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) = 0)
8988oveq1d 7372 . . . . . . . . 9 (𝜑 → (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
9021, 87, 893eqtrd 2780 . . . . . . . 8 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
9190, 64eqtrd 2776 . . . . . . 7 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0)
9224, 29resubcld 11583 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ)
93 absmod0 15188 . . . . . . . 8 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
9492, 31, 93syl2anc 584 . . . . . . 7 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
9591, 94mpbid 231 . . . . . 6 (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0)
9614abscld 15321 . . . . . . 7 (𝜑 → (abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ)
97 mod0 13781 . . . . . . 7 (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
9896, 31, 97syl2anc 584 . . . . . 6 (𝜑 → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
9995, 98mpbid 231 . . . . 5 (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ)
10018, 99eqeltrd 2838 . . . 4 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ)
10192, 57, 17redivcld 11983 . . . . 5 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ)
102 absz 15196 . . . . 5 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
103101, 102syl 17 . . . 4 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
104100, 103mpbird 256 . . 3 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ)
105 0lt1 11677 . . . . . . . 8 0 < 1
106 0re 11157 . . . . . . . . 9 0 ∈ ℝ
107 1re 11155 . . . . . . . . 9 1 ∈ ℝ
108106, 107ltnlei 11276 . . . . . . . 8 (0 < 1 ↔ ¬ 1 ≤ 0)
109105, 108mpbi 229 . . . . . . 7 ¬ 1 ≤ 0
1109, 4mulcld 11175 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 · 𝐸) ∈ ℂ)
1112, 11mulcld 11175 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐹) ∈ ℂ)
112110, 111subcld 11512 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℂ)
113112, 16, 17divcld 11931 . . . . . . . . . . . 12 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℂ)
114113abscld 15321 . . . . . . . . . . 11 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℝ)
115114resqcld 14030 . . . . . . . . . 10 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) ∈ ℝ)
1166nnnn0d 12473 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℕ0)
117116nn0ge0d 12476 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝐷)
118114sqge0d 14042 . . . . . . . . . 10 (𝜑 → 0 ≤ ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
11925, 115, 117, 118mulge0d 11732 . . . . . . . . 9 (𝜑 → 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
12025, 115remulcld 11185 . . . . . . . . . 10 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) ∈ ℝ)
12147, 120suble0d 11746 . . . . . . . . 9 (𝜑 → ((0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0 ↔ 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
122119, 121mpbird 256 . . . . . . . 8 (𝜑 → (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0)
123 breq1 5108 . . . . . . . 8 (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → (1 ≤ 0 ↔ (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0))
124122, 123syl5ibrcom 246 . . . . . . 7 (𝜑 → (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → 1 ≤ 0))
125109, 124mtoi 198 . . . . . 6 (𝜑 → ¬ 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
126 absresq 15187 . . . . . . . . . . . 12 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
127101, 126syl 17 . . . . . . . . . . 11 (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
12814, 16, 17sqdivd 14064 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)))
12914sqvald 14048 . . . . . . . . . . . 12 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) = (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))))
130129oveq1d 7372 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
131127, 128, 1303eqtrd 2780 . . . . . . . . . 10 (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
13226, 23remulcld 11185 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 · 𝐸) ∈ ℝ)
13322, 27remulcld 11185 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐹) ∈ ℝ)
134132, 133resubcld 11583 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ)
135134, 57, 17redivcld 11983 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ)
136 absresq 15187 . . . . . . . . . . . . . 14 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
137135, 136syl 17 . . . . . . . . . . . . 13 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
138112, 16, 17sqdivd 14064 . . . . . . . . . . . . 13 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
139137, 138eqtrd 2776 . . . . . . . . . . . 12 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
140139oveq2d 7373 . . . . . . . . . . 11 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
141112sqcld 14049 . . . . . . . . . . . 12 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) ∈ ℂ)
14216sqcld 14049 . . . . . . . . . . . 12 (𝜑 → (𝐶↑2) ∈ ℂ)
143 sqne0 14028 . . . . . . . . . . . . . 14 (𝐶 ∈ ℂ → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
14416, 143syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
14517, 144mpbird 256 . . . . . . . . . . . 12 (𝜑 → (𝐶↑2) ≠ 0)
1467, 141, 142, 145divassd 11966 . . . . . . . . . . 11 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
147112sqvald 14048 . . . . . . . . . . . . 13 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) = (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))
148147oveq2d 7373 . . . . . . . . . . . 12 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) = (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))))
149148oveq1d 7372 . . . . . . . . . . 11 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
150140, 146, 1493eqtr2d 2782 . . . . . . . . . 10 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
151131, 150oveq12d 7375 . . . . . . . . 9 (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
15214, 14mulcld 11175 . . . . . . . . . 10 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
153112, 112mulcld 11175 . . . . . . . . . . 11 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℂ)
1547, 153mulcld 11175 . . . . . . . . . 10 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) ∈ ℂ)
155152, 154, 142, 145divsubdird 11970 . . . . . . . . 9 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
1565, 13, 5, 13mulsubd 11614 . . . . . . . . . . . 12 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))))
157110, 111, 110, 111mulsubd 11614 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) = ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
158157oveq2d 7373 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
159110, 110mulcld 11175 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) · (𝐵 · 𝐸)) ∈ ℂ)
160111, 111mulcld 11175 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐹) · (𝐴 · 𝐹)) ∈ ℂ)
161159, 160addcld 11174 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
162110, 111mulcld 11175 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) · (𝐴 · 𝐹)) ∈ ℂ)
163162, 162addcld 11174 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
1647, 161, 163subdid 11611 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
1657, 159, 160adddid 11179 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
1667, 162, 162adddid 11179 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
167165, 166oveq12d 7375 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
168158, 164, 1673eqtrd 2780 . . . . . . . . . . . 12 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
169156, 168oveq12d 7375 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
170169oveq1d 7372 . . . . . . . . . 10 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)))
1715, 13mulcomd 11176 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)))
1727, 12, 5mulassd 11178 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)) = (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))))
1732, 4mulcomd 11176 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 · 𝐸) = (𝐸 · 𝐴))
174173oveq2d 7373 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐹) · (𝐸 · 𝐴)))
1759, 11, 4, 2mul4d 11367 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹) · (𝐸 · 𝐴)) = ((𝐵 · 𝐸) · (𝐹 · 𝐴)))
17611, 2mulcomd 11176 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 · 𝐴) = (𝐴 · 𝐹))
177176oveq2d 7373 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐸) · (𝐹 · 𝐴)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
178174, 175, 1773eqtrd 2780 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
179178oveq2d 7373 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
180171, 172, 1793eqtrd 2780 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
181180, 180oveq12d 7375 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
182181oveq2d 7373 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
183182oveq1d 7372 . . . . . . . . . . . 12 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
1845, 5mulcld 11175 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐸) · (𝐴 · 𝐸)) ∈ ℂ)
18513, 13mulcld 11175 . . . . . . . . . . . . . 14 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
186184, 185addcld 11174 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
1877, 159mulcld 11175 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) ∈ ℂ)
1887, 160mulcld 11175 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
189187, 188addcld 11174 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) ∈ ℂ)
1907, 162mulcld 11175 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
191190, 190addcld 11174 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) ∈ ℂ)
192186, 189, 191nnncan2d 11547 . . . . . . . . . . . 12 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
193184, 185, 187, 188addsub4d 11559 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
1945sqvald 14048 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴 · 𝐸) · (𝐴 · 𝐸)))
195110sqvald 14048 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵 · 𝐸) · (𝐵 · 𝐸)))
196195oveq2d 7373 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))))
197194, 196oveq12d 7375 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))))
19813sqvald 14048 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))))
199111sqvald 14048 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴 · 𝐹) · (𝐴 · 𝐹)))
200199oveq2d 7373 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))
201198, 200oveq12d 7375 . . . . . . . . . . . . . 14 (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
202197, 201oveq12d 7375 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
2032, 4sqmuld 14063 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴↑2) · (𝐸↑2)))
2049, 4sqmuld 14063 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵↑2) · (𝐸↑2)))
205204oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
2069sqcld 14049 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵↑2) ∈ ℂ)
2077, 206, 36mulassd 11178 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐵↑2)) · (𝐸↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
208205, 207eqtr4d 2779 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = ((𝐷 · (𝐵↑2)) · (𝐸↑2)))
209203, 208oveq12d 7375 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
2107sqvald 14048 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷↑2) = (𝐷 · 𝐷))
2119, 11sqmuld 14063 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹)↑2) = ((𝐵↑2) · (𝐹↑2)))
212210, 211oveq12d 7375 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷↑2) · ((𝐵 · 𝐹)↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
2137, 12sqmuld 14063 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷↑2) · ((𝐵 · 𝐹)↑2)))
2147, 7mulcld 11175 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · 𝐷) ∈ ℂ)
215214, 206, 37mulassd 11178 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
216212, 213, 2153eqtr4d 2786 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)))
2172, 11sqmuld 14063 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴↑2) · (𝐹↑2)))
218217oveq2d 7373 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
2192sqcld 14049 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴↑2) ∈ ℂ)
2207, 219, 37mulassd 11178 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐴↑2)) · (𝐹↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
221218, 220eqtr4d 2779 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = ((𝐷 · (𝐴↑2)) · (𝐹↑2)))
222216, 221oveq12d 7375 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
223209, 222oveq12d 7375 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))))
2247, 206mulcld 11175 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · (𝐵↑2)) ∈ ℂ)
225219, 224, 36subdird 11612 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
226 pellex.no1 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)
227226oveq1d 7372 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (𝐶 · (𝐸↑2)))
228225, 227eqtr3d 2778 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) = (𝐶 · (𝐸↑2)))
2297, 7, 206mulassd 11178 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) = (𝐷 · (𝐷 · (𝐵↑2))))
230229oveq1d 7372 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
231230oveq1d 7372 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)))
232214, 206mulcld 11175 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) ∈ ℂ)
2337, 219mulcld 11175 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · (𝐴↑2)) ∈ ℂ)
234232, 233, 37subdird 11612 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
235 subdi 11588 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
236235eqcomd 2742 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
2377, 224, 219, 236syl3anc 1371 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
238 negsubdi2 11460 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = ((𝐷 · (𝐵↑2)) − (𝐴↑2)))
239238eqcomd 2742 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
240219, 224, 239syl2anc 584 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
241226negeqd 11395 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = -𝐶)
242240, 241eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -𝐶)
243242oveq2d 7373 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = (𝐷 · -𝐶))
2447, 16mulneg2d 11609 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · -𝐶) = -(𝐷 · 𝐶))
245237, 243, 2443eqtrd 2780 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = -(𝐷 · 𝐶))
246245oveq1d 7372 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (-(𝐷 · 𝐶) · (𝐹↑2)))
247231, 234, 2463eqtr3d 2784 . . . . . . . . . . . . . . 15 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))) = (-(𝐷 · 𝐶) · (𝐹↑2)))
248228, 247oveq12d 7375 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))))
2497, 16mulcld 11175 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · 𝐶) ∈ ℂ)
250249, 37mulneg1d 11608 . . . . . . . . . . . . . . . . 17 (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -((𝐷 · 𝐶) · (𝐹↑2)))
2517, 16mulcomd 11176 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐷 · 𝐶) = (𝐶 · 𝐷))
252251oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = ((𝐶 · 𝐷) · (𝐹↑2)))
25316, 7, 37mulassd 11178 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐶 · 𝐷) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
254252, 253eqtrd 2776 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
255254negeqd 11395 . . . . . . . . . . . . . . . . 17 (𝜑 → -((𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
256250, 255eqtrd 2776 . . . . . . . . . . . . . . . 16 (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
257256oveq2d 7373 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))))
25816, 36mulcld 11175 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · (𝐸↑2)) ∈ ℂ)
25916, 38mulcld 11175 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · (𝐷 · (𝐹↑2))) ∈ ℂ)
260258, 259negsubd 11518 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
26161oveq2d 7373 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = (𝐶 · 𝐶))
262 subdi 11588 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
263262eqcomd 2742 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
26416, 36, 38, 263syl3anc 1371 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
26516sqvald 14048 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶↑2) = (𝐶 · 𝐶))
266261, 264, 2653eqtr4d 2786 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶↑2))
267257, 260, 2663eqtrd 2780 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = (𝐶↑2))
268223, 248, 2673eqtrd 2780 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = (𝐶↑2))
269193, 202, 2683eqtr2d 2782 . . . . . . . . . . . 12 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = (𝐶↑2))
270183, 192, 2693eqtrd 2780 . . . . . . . . . . 11 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (𝐶↑2))
271270oveq1d 7372 . . . . . . . . . 10 (𝜑 → ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)) = ((𝐶↑2) / (𝐶↑2)))
272142, 145dividd 11929 . . . . . . . . . 10 (𝜑 → ((𝐶↑2) / (𝐶↑2)) = 1)
273170, 271, 2723eqtrd 2780 . . . . . . . . 9 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = 1)
274151, 155, 2733eqtr2d 2782 . . . . . . . 8 (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
275274adantr 481 . . . . . . 7 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
276 simpr 485 . . . . . . . . . . 11 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
277276fvoveq1d 7379 . . . . . . . . . 10 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = (abs‘(0 / 𝐶)))
27816, 17div0d 11930 . . . . . . . . . . . 12 (𝜑 → (0 / 𝐶) = 0)
279278abs00bd 15176 . . . . . . . . . . 11 (𝜑 → (abs‘(0 / 𝐶)) = 0)
280279adantr 481 . . . . . . . . . 10 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(0 / 𝐶)) = 0)
281277, 280eqtrd 2776 . . . . . . . . 9 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = 0)
282281sq0id 14098 . . . . . . . 8 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = 0)
283282oveq1d 7372 . . . . . . 7 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
284275, 283eqtr3d 2778 . . . . . 6 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
285125, 284mtand 814 . . . . 5 (𝜑 → ¬ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
286285neqned 2950 . . . 4 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ≠ 0)
28714, 16, 286, 17divne0d 11947 . . 3 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0)
288 nnabscl 15210 . . 3 (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ∧ (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
289104, 287, 288syl2anc 584 . 2 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
290112, 16, 17absdivd 15340 . . . . 5 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) = ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)))
291 negsub 11449 . . . . . . . . . . . 12 (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) + -(𝐴 · 𝐹)) = ((𝐵 · 𝐸) − (𝐴 · 𝐹)))
292291eqcomd 2742 . . . . . . . . . . 11 (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
293110, 111, 292syl2anc 584 . . . . . . . . . 10 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
294293oveq1d 7372 . . . . . . . . 9 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
295133renegcld 11582 . . . . . . . . . 10 (𝜑 → -(𝐴 · 𝐹) ∈ ℝ)
29611, 4mulcomd 11176 . . . . . . . . . . . 12 (𝜑 → (𝐹 · 𝐸) = (𝐸 · 𝐹))
297296oveq1d 7372 . . . . . . . . . . 11 (𝜑 → ((𝐹 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
298 modmul1 13829 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ 𝐹 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
29926, 27, 32, 31, 78, 298syl221anc 1381 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
300 modmul1 13829 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐹 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
30122, 23, 76, 31, 33, 300syl221anc 1381 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
302297, 299, 3013eqtr4d 2786 . . . . . . . . . 10 (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶)))
303 modadd1 13813 . . . . . . . . . 10 ((((𝐵 · 𝐸) ∈ ℝ ∧ (𝐴 · 𝐹) ∈ ℝ) ∧ (-(𝐴 · 𝐹) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) ∧ ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶))) → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
304132, 133, 295, 31, 302, 303syl221anc 1381 . . . . . . . . 9 (𝜑 → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
305111negidd 11502 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐹) + -(𝐴 · 𝐹)) = 0)
306305oveq1d 7372 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
307294, 304, 3063eqtrd 2780 . . . . . . . 8 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
308307, 64eqtrd 2776 . . . . . . 7 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0)
309 absmod0 15188 . . . . . . . 8 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
310134, 31, 309syl2anc 584 . . . . . . 7 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
311308, 310mpbid 231 . . . . . 6 (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0)
312112abscld 15321 . . . . . . 7 (𝜑 → (abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ)
313 mod0 13781 . . . . . . 7 (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
314312, 31, 313syl2anc 584 . . . . . 6 (𝜑 → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
315311, 314mpbid 231 . . . . 5 (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ)
316290, 315eqeltrd 2838 . . . 4 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ)
317 absz 15196 . . . . 5 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
318135, 317syl 17 . . . 4 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
319316, 318mpbird 256 . . 3 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ)
320 pellex.neq . . . . . . 7 (𝜑 → ¬ (𝐴 = 𝐸𝐵 = 𝐹))
32110nnne0d 12203 . . . . . . . . 9 (𝜑𝐹 ≠ 0)
3223nnne0d 12203 . . . . . . . . 9 (𝜑𝐸 ≠ 0)
3239, 11, 2, 4, 321, 322divmuleqd 11977 . . . . . . . 8 (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) ↔ (𝐵 · 𝐸) = (𝐴 · 𝐹)))
32461adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
325324eqcomd 2742 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐸↑2) − (𝐷 · (𝐹↑2))))
326325oveq2d 7373 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
3279, 11, 321divcld 11931 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐹) ∈ ℂ)
328327sqcld 14049 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 𝐹)↑2) ∈ ℂ)
329328adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) ∈ ℂ)
33036adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ∈ ℂ)
33138adantr 481 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (𝐹↑2)) ∈ ℂ)
332329, 330, 331subdid 11611 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))))
333 oveq1 7364 . . . . . . . . . . . . . . . . 17 ((𝐵 / 𝐹) = (𝐴 / 𝐸) → ((𝐵 / 𝐹)↑2) = ((𝐴 / 𝐸)↑2))
334333oveq1d 7372 . . . . . . . . . . . . . . . 16 ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
335334adantl 482 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
3362adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐴 ∈ ℂ)
3374adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ∈ ℂ)
338322adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ≠ 0)
339336, 337, 338sqdivd 14064 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐴 / 𝐸)↑2) = ((𝐴↑2) / (𝐸↑2)))
340339oveq1d 7372 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴 / 𝐸)↑2) · (𝐸↑2)) = (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)))
341219adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴↑2) ∈ ℂ)
342 sqne0 14028 . . . . . . . . . . . . . . . . . . 19 (𝐸 ∈ ℂ → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
3434, 342syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
344322, 343mpbird 256 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸↑2) ≠ 0)
345344adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ≠ 0)
346341, 330, 345divcan1d 11932 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)) = (𝐴↑2))
347335, 340, 3463eqtrd 2780 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (𝐴↑2))
3487adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐷 ∈ ℂ)
34937adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ∈ ℂ)
350329, 348, 349mul12d 11364 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))))
3519adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐵 ∈ ℂ)
35211adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ∈ ℂ)
353321adantr 481 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ≠ 0)
354351, 352, 353sqdivd 14064 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = ((𝐵↑2) / (𝐹↑2)))
355354oveq1d 7372 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐹↑2)) = (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)))
356355oveq2d 7373 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))) = (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))))
357206adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐵↑2) ∈ ℂ)
358 sqne0 14028 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ ℂ → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
35911, 358syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
360321, 359mpbird 256 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹↑2) ≠ 0)
361360adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ≠ 0)
362357, 349, 361divcan1d 11932 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)) = (𝐵↑2))
363362oveq2d 7373 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
364350, 356, 3633eqtrd 2780 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
365347, 364oveq12d 7375 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
366326, 332, 3653eqtrd 2780 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
367226eqcomd 2742 . . . . . . . . . . . . 13 (𝜑𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
368367adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
369366, 368oveq12d 7375 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))))
37016adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ∈ ℂ)
37117adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ≠ 0)
372329, 370, 371divcan4d 11937 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = ((𝐵 / 𝐹)↑2))
373226, 226oveq12d 7375 . . . . . . . . . . . . 13 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = (𝐶 / 𝐶))
37416, 17dividd 11929 . . . . . . . . . . . . 13 (𝜑 → (𝐶 / 𝐶) = 1)
375373, 374eqtrd 2776 . . . . . . . . . . . 12 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
376375adantr 481 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
377369, 372, 3763eqtr3d 2784 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = 1)
37826, 27, 321redivcld 11983 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐹) ∈ ℝ)
3798nnnn0d 12473 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ ℕ0)
380379nn0ge0d 12476 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 𝐵)
38110nngt0d 12202 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < 𝐹)
382 divge0 12024 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ (𝐹 ∈ ℝ ∧ 0 < 𝐹)) → 0 ≤ (𝐵 / 𝐹))
38326, 380, 27, 381, 382syl22anc 837 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (𝐵 / 𝐹))
384378, 383sqrtsqd 15304 . . . . . . . . . . . . . . 15 (𝜑 → (√‘((𝐵 / 𝐹)↑2)) = (𝐵 / 𝐹))
385384eqcomd 2742 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
386385ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
387 fveq2 6842 . . . . . . . . . . . . . 14 (((𝐵 / 𝐹)↑2) = 1 → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
388387adantl 482 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
389 sqrt1 15156 . . . . . . . . . . . . . 14 (√‘1) = 1
390389a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘1) = 1)
391386, 388, 3903eqtrd 2780 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = 1)
392391ex 413 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐵 / 𝐹) = 1))
393 simplr 767 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = (𝐴 / 𝐸))
394 simpr 485 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = 1)
395393, 394eqtr3d 2778 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 / 𝐸) = 1)
396395oveq1d 7372 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = (1 · 𝐸))
3972, 4, 322divcan1d 11932 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
398397ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
3994mulid2d 11173 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝐸) = 𝐸)
400399ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐸) = 𝐸)
401396, 398, 4003eqtr3d 2784 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐴 = 𝐸)
402394oveq1d 7372 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = (1 · 𝐹))
4039, 11, 321divcan1d 11932 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
404403ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
40511mulid2d 11173 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝐹) = 𝐹)
406405ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐹) = 𝐹)
407402, 404, 4063eqtr3d 2784 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐵 = 𝐹)
408401, 407jca 512 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 = 𝐸𝐵 = 𝐹))
409408ex 413 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹) = 1 → (𝐴 = 𝐸𝐵 = 𝐹)))
410392, 409syld 47 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐴 = 𝐸𝐵 = 𝐹)))
411377, 410mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴 = 𝐸𝐵 = 𝐹))
412411ex 413 . . . . . . . 8 (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (𝐴 = 𝐸𝐵 = 𝐹)))
413323, 412sylbird 259 . . . . . . 7 (𝜑 → ((𝐵 · 𝐸) = (𝐴 · 𝐹) → (𝐴 = 𝐸𝐵 = 𝐹)))
414320, 413mtod 197 . . . . . 6 (𝜑 → ¬ (𝐵 · 𝐸) = (𝐴 · 𝐹))
415414neqned 2950 . . . . 5 (𝜑 → (𝐵 · 𝐸) ≠ (𝐴 · 𝐹))
416110, 111, 415subne0d 11521 . . . 4 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ≠ 0)
417112, 16, 416, 17divne0d 11947 . . 3 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0)
418 nnabscl 15210 . . 3 (((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ∧ (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0) → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
419319, 417, 418syl2anc 584 . 2 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
420 oveq1 7364 . . . . 5 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (𝑎↑2) = ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2))
421420oveq1d 7372 . . . 4 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))))
422421eqeq1d 2738 . . 3 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1))
423 oveq1 7364 . . . . . 6 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝑏↑2) = ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
424423oveq2d 7373 . . . . 5 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝐷 · (𝑏↑2)) = (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
425424oveq2d 7373 . . . 4 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
426425eqeq1d 2738 . . 3 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → ((((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1))
427422, 426rspc2ev 3592 . 2 (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ ∧ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ ∧ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
428289, 419, 274, 427syl3anc 1371 1 (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wrex 3073   class class class wbr 5105  cfv 6496  (class class class)co 7357  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056   < clt 11189  cle 11190  cmin 11385  -cneg 11386   / cdiv 11812  cn 12153  2c2 12208  cz 12499  cq 12873  +crp 12915   mod cmo 13774  cexp 13967  csqrt 15118  abscabs 15119
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-sup 9378  df-inf 9379  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-fl 13697  df-mod 13775  df-seq 13907  df-exp 13968  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121
This theorem is referenced by:  pellex  41144
  Copyright terms: Public domain W3C validator