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 38856
Description: Lemma for pellex 38857. 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 11455 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
3 pellex.enn . . . . . . . . 9 (𝜑𝐸 ∈ ℕ)
43nncnd 11455 . . . . . . . 8 (𝜑𝐸 ∈ ℂ)
52, 4mulcld 10458 . . . . . . 7 (𝜑 → (𝐴 · 𝐸) ∈ ℂ)
6 pellex.dnn . . . . . . . . 9 (𝜑𝐷 ∈ ℕ)
76nncnd 11455 . . . . . . . 8 (𝜑𝐷 ∈ ℂ)
8 pellex.bnn . . . . . . . . . 10 (𝜑𝐵 ∈ ℕ)
98nncnd 11455 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
10 pellex.fnn . . . . . . . . . 10 (𝜑𝐹 ∈ ℕ)
1110nncnd 11455 . . . . . . . . 9 (𝜑𝐹 ∈ ℂ)
129, 11mulcld 10458 . . . . . . . 8 (𝜑 → (𝐵 · 𝐹) ∈ ℂ)
137, 12mulcld 10458 . . . . . . 7 (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℂ)
145, 13subcld 10796 . . . . . 6 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
15 pellex.cz . . . . . . 7 (𝜑𝐶 ∈ ℤ)
1615zcnd 11899 . . . . . 6 (𝜑𝐶 ∈ ℂ)
17 pellex.cn0 . . . . . 6 (𝜑𝐶 ≠ 0)
1814, 16, 17absdivd 14674 . . . . 5 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)))
195, 13negsubd 10802 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))))
2019eqcomd 2778 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))))
2120oveq1d 6989 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
221nnred 11454 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
233nnred 11454 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℝ)
2422, 23remulcld 10468 . . . . . . . . . 10 (𝜑 → (𝐴 · 𝐸) ∈ ℝ)
256nnred 11454 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℝ)
268nnred 11454 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
2710nnred 11454 . . . . . . . . . . . 12 (𝜑𝐹 ∈ ℝ)
2826, 27remulcld 10468 . . . . . . . . . . 11 (𝜑 → (𝐵 · 𝐹) ∈ ℝ)
2925, 28remulcld 10468 . . . . . . . . . 10 (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
3029renegcld 10866 . . . . . . . . . 10 (𝜑 → -(𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
3116, 17absrpcld 14667 . . . . . . . . . 10 (𝜑 → (abs‘𝐶) ∈ ℝ+)
323nnzd 11897 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℤ)
33 pellex.xcg . . . . . . . . . . . 12 (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))
34 modmul1 13105 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
3522, 23, 32, 31, 33, 34syl221anc 1361 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
364sqcld 13321 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸↑2) ∈ ℂ)
3711sqcld 13321 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹↑2) ∈ ℂ)
387, 37mulcld 10458 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℂ)
3936, 38npcand 10800 . . . . . . . . . . . . . 14 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) = (𝐸↑2))
404sqvald 13320 . . . . . . . . . . . . . 14 (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
4139, 40eqtr2d 2809 . . . . . . . . . . . . 13 (𝜑 → (𝐸 · 𝐸) = (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))))
4241oveq1d 6989 . . . . . . . . . . . 12 (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
4323resqcld 13424 . . . . . . . . . . . . . 14 (𝜑 → (𝐸↑2) ∈ ℝ)
4427resqcld 13424 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹↑2) ∈ ℝ)
4525, 44remulcld 10468 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℝ)
4643, 45resubcld 10867 . . . . . . . . . . . . 13 (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ)
47 0red 10441 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
4816abscld 14655 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘𝐶) ∈ ℝ)
4948recnd 10466 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘𝐶) ∈ ℂ)
5016, 17absne0d 14666 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘𝐶) ≠ 0)
5149, 50dividd 11213 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) = 1)
52 1zzd 11824 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
5351, 52eqeltrd 2860 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ)
54 mod0 13057 . . . . . . . . . . . . . . . . 17 (((abs‘𝐶) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
5548, 31, 54syl2anc 576 . . . . . . . . . . . . . . . 16 (𝜑 → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
5653, 55mpbird 249 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐶) mod (abs‘𝐶)) = 0)
5715zred 11898 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℝ)
58 absmod0 14522 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
5957, 31, 58syl2anc 576 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
6056, 59mpbird 249 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 mod (abs‘𝐶)) = 0)
61 pellex.no2 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
6261oveq1d 6989 . . . . . . . . . . . . . 14 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (𝐶 mod (abs‘𝐶)))
63 0mod 13083 . . . . . . . . . . . . . . 15 ((abs‘𝐶) ∈ ℝ+ → (0 mod (abs‘𝐶)) = 0)
6431, 63syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0 mod (abs‘𝐶)) = 0)
6560, 62, 643eqtr4d 2818 . . . . . . . . . . . . 13 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
66 modadd1 13089 . . . . . . . . . . . . 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 1361 . . . . . . . . . . . 12 (𝜑 → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
6838addid2d 10639 . . . . . . . . . . . . . 14 (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐷 · (𝐹↑2)))
6911sqvald 13320 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
7069oveq2d 6990 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹↑2)) = (𝐷 · (𝐹 · 𝐹)))
717, 11, 11mul12d 10647 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹 · 𝐹)) = (𝐹 · (𝐷 · 𝐹)))
7268, 70, 713eqtrd 2812 . . . . . . . . . . . . 13 (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐹 · (𝐷 · 𝐹)))
7372oveq1d 6989 . . . . . . . . . . . 12 (𝜑 → ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
7442, 67, 733eqtrd 2812 . . . . . . . . . . 11 (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
756nnzd 11897 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ ℤ)
7610nnzd 11897 . . . . . . . . . . . . . 14 (𝜑𝐹 ∈ ℤ)
7775, 76zmulcld 11904 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · 𝐹) ∈ ℤ)
78 pellex.ycg . . . . . . . . . . . . . 14 (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))
7978eqcomd 2778 . . . . . . . . . . . . 13 (𝜑 → (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶)))
80 modmul1 13105 . . . . . . . . . . . . 13 (((𝐹 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐷 · 𝐹) ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶))) → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
8127, 26, 77, 31, 79, 80syl221anc 1361 . . . . . . . . . . . 12 (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
829, 7, 11mul12d 10647 . . . . . . . . . . . . 13 (𝜑 → (𝐵 · (𝐷 · 𝐹)) = (𝐷 · (𝐵 · 𝐹)))
8382oveq1d 6989 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
8481, 83eqtrd 2808 . . . . . . . . . . 11 (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
8535, 74, 843eqtrd 2812 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
86 modadd1 13089 . . . . . . . . . 10 ((((𝐴 · 𝐸) ∈ ℝ ∧ (𝐷 · (𝐵 · 𝐹)) ∈ ℝ) ∧ (-(𝐷 · (𝐵 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) ∧ ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
8724, 29, 30, 31, 85, 86syl221anc 1361 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
8813negidd 10786 . . . . . . . . . 10 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) = 0)
8988oveq1d 6989 . . . . . . . . 9 (𝜑 → (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
9021, 87, 893eqtrd 2812 . . . . . . . 8 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
9190, 64eqtrd 2808 . . . . . . 7 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0)
9224, 29resubcld 10867 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ)
93 absmod0 14522 . . . . . . . 8 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
9492, 31, 93syl2anc 576 . . . . . . 7 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
9591, 94mpbid 224 . . . . . 6 (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0)
9614abscld 14655 . . . . . . 7 (𝜑 → (abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ)
97 mod0 13057 . . . . . . 7 (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
9896, 31, 97syl2anc 576 . . . . . 6 (𝜑 → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
9995, 98mpbid 224 . . . . 5 (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ)
10018, 99eqeltrd 2860 . . . 4 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ)
10192, 57, 17redivcld 11267 . . . . 5 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ)
102 absz 14530 . . . . 5 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
103101, 102syl 17 . . . 4 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
104100, 103mpbird 249 . . 3 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ)
105 0lt1 10961 . . . . . . . 8 0 < 1
106 0re 10439 . . . . . . . . 9 0 ∈ ℝ
107 1re 10437 . . . . . . . . 9 1 ∈ ℝ
108106, 107ltnlei 10559 . . . . . . . 8 (0 < 1 ↔ ¬ 1 ≤ 0)
109105, 108mpbi 222 . . . . . . 7 ¬ 1 ≤ 0
1109, 4mulcld 10458 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 · 𝐸) ∈ ℂ)
1112, 11mulcld 10458 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐹) ∈ ℂ)
112110, 111subcld 10796 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℂ)
113112, 16, 17divcld 11215 . . . . . . . . . . . 12 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℂ)
114113abscld 14655 . . . . . . . . . . 11 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℝ)
115114resqcld 13424 . . . . . . . . . 10 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) ∈ ℝ)
1166nnnn0d 11765 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℕ0)
117116nn0ge0d 11768 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝐷)
118114sqge0d 13425 . . . . . . . . . 10 (𝜑 → 0 ≤ ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
11925, 115, 117, 118mulge0d 11016 . . . . . . . . 9 (𝜑 → 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
12025, 115remulcld 10468 . . . . . . . . . 10 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) ∈ ℝ)
12147, 120suble0d 11030 . . . . . . . . 9 (𝜑 → ((0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0 ↔ 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
122119, 121mpbird 249 . . . . . . . 8 (𝜑 → (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0)
123 breq1 4928 . . . . . . . 8 (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → (1 ≤ 0 ↔ (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0))
124122, 123syl5ibrcom 239 . . . . . . 7 (𝜑 → (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → 1 ≤ 0))
125109, 124mtoi 191 . . . . . 6 (𝜑 → ¬ 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
126 absresq 14521 . . . . . . . . . . . 12 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
127101, 126syl 17 . . . . . . . . . . 11 (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
12814, 16, 17sqdivd 13336 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)))
12914sqvald 13320 . . . . . . . . . . . 12 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) = (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))))
130129oveq1d 6989 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
131127, 128, 1303eqtrd 2812 . . . . . . . . . 10 (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
13226, 23remulcld 10468 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 · 𝐸) ∈ ℝ)
13322, 27remulcld 10468 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐹) ∈ ℝ)
134132, 133resubcld 10867 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ)
135134, 57, 17redivcld 11267 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ)
136 absresq 14521 . . . . . . . . . . . . . 14 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
137135, 136syl 17 . . . . . . . . . . . . 13 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
138112, 16, 17sqdivd 13336 . . . . . . . . . . . . 13 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
139137, 138eqtrd 2808 . . . . . . . . . . . 12 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
140139oveq2d 6990 . . . . . . . . . . 11 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
141112sqcld 13321 . . . . . . . . . . . 12 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) ∈ ℂ)
14216sqcld 13321 . . . . . . . . . . . 12 (𝜑 → (𝐶↑2) ∈ ℂ)
143 sqne0 13302 . . . . . . . . . . . . . 14 (𝐶 ∈ ℂ → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
14416, 143syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
14517, 144mpbird 249 . . . . . . . . . . . 12 (𝜑 → (𝐶↑2) ≠ 0)
1467, 141, 142, 145divassd 11250 . . . . . . . . . . 11 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
147112sqvald 13320 . . . . . . . . . . . . 13 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) = (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))
148147oveq2d 6990 . . . . . . . . . . . 12 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) = (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))))
149148oveq1d 6989 . . . . . . . . . . 11 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
150140, 146, 1493eqtr2d 2814 . . . . . . . . . 10 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
151131, 150oveq12d 6992 . . . . . . . . 9 (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
15214, 14mulcld 10458 . . . . . . . . . 10 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
153112, 112mulcld 10458 . . . . . . . . . . 11 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℂ)
1547, 153mulcld 10458 . . . . . . . . . 10 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) ∈ ℂ)
155152, 154, 142, 145divsubdird 11254 . . . . . . . . 9 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
1565, 13, 5, 13mulsubd 10898 . . . . . . . . . . . 12 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))))
157110, 111, 110, 111mulsubd 10898 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) = ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
158157oveq2d 6990 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
159110, 110mulcld 10458 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) · (𝐵 · 𝐸)) ∈ ℂ)
160111, 111mulcld 10458 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐹) · (𝐴 · 𝐹)) ∈ ℂ)
161159, 160addcld 10457 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
162110, 111mulcld 10458 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) · (𝐴 · 𝐹)) ∈ ℂ)
163162, 162addcld 10457 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
1647, 161, 163subdid 10895 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
1657, 159, 160adddid 10462 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
1667, 162, 162adddid 10462 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
167165, 166oveq12d 6992 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
168158, 164, 1673eqtrd 2812 . . . . . . . . . . . 12 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
169156, 168oveq12d 6992 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
170169oveq1d 6989 . . . . . . . . . 10 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)))
1715, 13mulcomd 10459 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)))
1727, 12, 5mulassd 10461 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)) = (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))))
1732, 4mulcomd 10459 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 · 𝐸) = (𝐸 · 𝐴))
174173oveq2d 6990 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐹) · (𝐸 · 𝐴)))
1759, 11, 4, 2mul4d 10650 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹) · (𝐸 · 𝐴)) = ((𝐵 · 𝐸) · (𝐹 · 𝐴)))
17611, 2mulcomd 10459 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 · 𝐴) = (𝐴 · 𝐹))
177176oveq2d 6990 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐸) · (𝐹 · 𝐴)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
178174, 175, 1773eqtrd 2812 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
179178oveq2d 6990 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
180171, 172, 1793eqtrd 2812 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
181180, 180oveq12d 6992 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
182181oveq2d 6990 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
183182oveq1d 6989 . . . . . . . . . . . 12 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
1845, 5mulcld 10458 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐸) · (𝐴 · 𝐸)) ∈ ℂ)
18513, 13mulcld 10458 . . . . . . . . . . . . . 14 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
186184, 185addcld 10457 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
1877, 159mulcld 10458 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) ∈ ℂ)
1887, 160mulcld 10458 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
189187, 188addcld 10457 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) ∈ ℂ)
1907, 162mulcld 10458 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
191190, 190addcld 10457 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) ∈ ℂ)
192186, 189, 191nnncan2d 10831 . . . . . . . . . . . 12 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
193184, 185, 187, 188addsub4d 10843 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
1945sqvald 13320 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴 · 𝐸) · (𝐴 · 𝐸)))
195110sqvald 13320 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵 · 𝐸) · (𝐵 · 𝐸)))
196195oveq2d 6990 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))))
197194, 196oveq12d 6992 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))))
19813sqvald 13320 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))))
199111sqvald 13320 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴 · 𝐹) · (𝐴 · 𝐹)))
200199oveq2d 6990 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))
201198, 200oveq12d 6992 . . . . . . . . . . . . . 14 (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
202197, 201oveq12d 6992 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
2032, 4sqmuld 13335 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴↑2) · (𝐸↑2)))
2049, 4sqmuld 13335 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵↑2) · (𝐸↑2)))
205204oveq2d 6990 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
2069sqcld 13321 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵↑2) ∈ ℂ)
2077, 206, 36mulassd 10461 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐵↑2)) · (𝐸↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
208205, 207eqtr4d 2811 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = ((𝐷 · (𝐵↑2)) · (𝐸↑2)))
209203, 208oveq12d 6992 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
2107sqvald 13320 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷↑2) = (𝐷 · 𝐷))
2119, 11sqmuld 13335 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹)↑2) = ((𝐵↑2) · (𝐹↑2)))
212210, 211oveq12d 6992 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷↑2) · ((𝐵 · 𝐹)↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
2137, 12sqmuld 13335 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷↑2) · ((𝐵 · 𝐹)↑2)))
2147, 7mulcld 10458 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · 𝐷) ∈ ℂ)
215214, 206, 37mulassd 10461 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
216212, 213, 2153eqtr4d 2818 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)))
2172, 11sqmuld 13335 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴↑2) · (𝐹↑2)))
218217oveq2d 6990 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
2192sqcld 13321 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴↑2) ∈ ℂ)
2207, 219, 37mulassd 10461 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐴↑2)) · (𝐹↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
221218, 220eqtr4d 2811 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = ((𝐷 · (𝐴↑2)) · (𝐹↑2)))
222216, 221oveq12d 6992 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
223209, 222oveq12d 6992 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))))
2247, 206mulcld 10458 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · (𝐵↑2)) ∈ ℂ)
225219, 224, 36subdird 10896 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
226 pellex.no1 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)
227226oveq1d 6989 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (𝐶 · (𝐸↑2)))
228225, 227eqtr3d 2810 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) = (𝐶 · (𝐸↑2)))
2297, 7, 206mulassd 10461 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) = (𝐷 · (𝐷 · (𝐵↑2))))
230229oveq1d 6989 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
231230oveq1d 6989 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)))
232214, 206mulcld 10458 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) ∈ ℂ)
2337, 219mulcld 10458 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · (𝐴↑2)) ∈ ℂ)
234232, 233, 37subdird 10896 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
235 subdi 10872 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
236235eqcomd 2778 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
2377, 224, 219, 236syl3anc 1351 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
238 negsubdi2 10744 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = ((𝐷 · (𝐵↑2)) − (𝐴↑2)))
239238eqcomd 2778 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
240219, 224, 239syl2anc 576 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
241226negeqd 10678 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = -𝐶)
242240, 241eqtrd 2808 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -𝐶)
243242oveq2d 6990 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = (𝐷 · -𝐶))
2447, 16mulneg2d 10893 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · -𝐶) = -(𝐷 · 𝐶))
245237, 243, 2443eqtrd 2812 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = -(𝐷 · 𝐶))
246245oveq1d 6989 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (-(𝐷 · 𝐶) · (𝐹↑2)))
247231, 234, 2463eqtr3d 2816 . . . . . . . . . . . . . . 15 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))) = (-(𝐷 · 𝐶) · (𝐹↑2)))
248228, 247oveq12d 6992 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))))
2497, 16mulcld 10458 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · 𝐶) ∈ ℂ)
250249, 37mulneg1d 10892 . . . . . . . . . . . . . . . . 17 (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -((𝐷 · 𝐶) · (𝐹↑2)))
2517, 16mulcomd 10459 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐷 · 𝐶) = (𝐶 · 𝐷))
252251oveq1d 6989 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = ((𝐶 · 𝐷) · (𝐹↑2)))
25316, 7, 37mulassd 10461 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐶 · 𝐷) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
254252, 253eqtrd 2808 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
255254negeqd 10678 . . . . . . . . . . . . . . . . 17 (𝜑 → -((𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
256250, 255eqtrd 2808 . . . . . . . . . . . . . . . 16 (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
257256oveq2d 6990 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))))
25816, 36mulcld 10458 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · (𝐸↑2)) ∈ ℂ)
25916, 38mulcld 10458 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · (𝐷 · (𝐹↑2))) ∈ ℂ)
260258, 259negsubd 10802 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
26161oveq2d 6990 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = (𝐶 · 𝐶))
262 subdi 10872 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
263262eqcomd 2778 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
26416, 36, 38, 263syl3anc 1351 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
26516sqvald 13320 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶↑2) = (𝐶 · 𝐶))
266261, 264, 2653eqtr4d 2818 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶↑2))
267257, 260, 2663eqtrd 2812 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = (𝐶↑2))
268223, 248, 2673eqtrd 2812 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = (𝐶↑2))
269193, 202, 2683eqtr2d 2814 . . . . . . . . . . . 12 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = (𝐶↑2))
270183, 192, 2693eqtrd 2812 . . . . . . . . . . 11 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (𝐶↑2))
271270oveq1d 6989 . . . . . . . . . 10 (𝜑 → ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)) = ((𝐶↑2) / (𝐶↑2)))
272142, 145dividd 11213 . . . . . . . . . 10 (𝜑 → ((𝐶↑2) / (𝐶↑2)) = 1)
273170, 271, 2723eqtrd 2812 . . . . . . . . 9 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = 1)
274151, 155, 2733eqtr2d 2814 . . . . . . . 8 (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
275274adantr 473 . . . . . . 7 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
276 simpr 477 . . . . . . . . . . 11 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
277276fvoveq1d 6996 . . . . . . . . . 10 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = (abs‘(0 / 𝐶)))
27816, 17div0d 11214 . . . . . . . . . . . 12 (𝜑 → (0 / 𝐶) = 0)
279278abs00bd 14510 . . . . . . . . . . 11 (𝜑 → (abs‘(0 / 𝐶)) = 0)
280279adantr 473 . . . . . . . . . 10 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(0 / 𝐶)) = 0)
281277, 280eqtrd 2808 . . . . . . . . 9 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = 0)
282281sq0id 13370 . . . . . . . 8 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = 0)
283282oveq1d 6989 . . . . . . 7 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
284275, 283eqtr3d 2810 . . . . . 6 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
285125, 284mtand 803 . . . . 5 (𝜑 → ¬ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
286285neqned 2968 . . . 4 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ≠ 0)
28714, 16, 286, 17divne0d 11231 . . 3 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0)
288 nnabscl 14544 . . 3 (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ∧ (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
289104, 287, 288syl2anc 576 . 2 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
290112, 16, 17absdivd 14674 . . . . 5 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) = ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)))
291 negsub 10733 . . . . . . . . . . . 12 (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) + -(𝐴 · 𝐹)) = ((𝐵 · 𝐸) − (𝐴 · 𝐹)))
292291eqcomd 2778 . . . . . . . . . . 11 (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
293110, 111, 292syl2anc 576 . . . . . . . . . 10 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
294293oveq1d 6989 . . . . . . . . 9 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
295133renegcld 10866 . . . . . . . . . 10 (𝜑 → -(𝐴 · 𝐹) ∈ ℝ)
29611, 4mulcomd 10459 . . . . . . . . . . . 12 (𝜑 → (𝐹 · 𝐸) = (𝐸 · 𝐹))
297296oveq1d 6989 . . . . . . . . . . 11 (𝜑 → ((𝐹 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
298 modmul1 13105 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ 𝐹 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
29926, 27, 32, 31, 78, 298syl221anc 1361 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
300 modmul1 13105 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐹 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
30122, 23, 76, 31, 33, 300syl221anc 1361 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
302297, 299, 3013eqtr4d 2818 . . . . . . . . . 10 (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶)))
303 modadd1 13089 . . . . . . . . . 10 ((((𝐵 · 𝐸) ∈ ℝ ∧ (𝐴 · 𝐹) ∈ ℝ) ∧ (-(𝐴 · 𝐹) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) ∧ ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶))) → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
304132, 133, 295, 31, 302, 303syl221anc 1361 . . . . . . . . 9 (𝜑 → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
305111negidd 10786 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐹) + -(𝐴 · 𝐹)) = 0)
306305oveq1d 6989 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
307294, 304, 3063eqtrd 2812 . . . . . . . 8 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
308307, 64eqtrd 2808 . . . . . . 7 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0)
309 absmod0 14522 . . . . . . . 8 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
310134, 31, 309syl2anc 576 . . . . . . 7 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
311308, 310mpbid 224 . . . . . 6 (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0)
312112abscld 14655 . . . . . . 7 (𝜑 → (abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ)
313 mod0 13057 . . . . . . 7 (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
314312, 31, 313syl2anc 576 . . . . . 6 (𝜑 → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
315311, 314mpbid 224 . . . . 5 (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ)
316290, 315eqeltrd 2860 . . . 4 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ)
317 absz 14530 . . . . 5 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
318135, 317syl 17 . . . 4 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
319316, 318mpbird 249 . . 3 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ)
320 pellex.neq . . . . . . 7 (𝜑 → ¬ (𝐴 = 𝐸𝐵 = 𝐹))
32110nnne0d 11488 . . . . . . . . 9 (𝜑𝐹 ≠ 0)
3223nnne0d 11488 . . . . . . . . 9 (𝜑𝐸 ≠ 0)
3239, 11, 2, 4, 321, 322divmuleqd 11261 . . . . . . . 8 (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) ↔ (𝐵 · 𝐸) = (𝐴 · 𝐹)))
32461adantr 473 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
325324eqcomd 2778 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐸↑2) − (𝐷 · (𝐹↑2))))
326325oveq2d 6990 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
3279, 11, 321divcld 11215 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐹) ∈ ℂ)
328327sqcld 13321 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 𝐹)↑2) ∈ ℂ)
329328adantr 473 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) ∈ ℂ)
33036adantr 473 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ∈ ℂ)
33138adantr 473 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (𝐹↑2)) ∈ ℂ)
332329, 330, 331subdid 10895 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))))
333 oveq1 6981 . . . . . . . . . . . . . . . . 17 ((𝐵 / 𝐹) = (𝐴 / 𝐸) → ((𝐵 / 𝐹)↑2) = ((𝐴 / 𝐸)↑2))
334333oveq1d 6989 . . . . . . . . . . . . . . . 16 ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
335334adantl 474 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
3362adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐴 ∈ ℂ)
3374adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ∈ ℂ)
338322adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ≠ 0)
339336, 337, 338sqdivd 13336 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐴 / 𝐸)↑2) = ((𝐴↑2) / (𝐸↑2)))
340339oveq1d 6989 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴 / 𝐸)↑2) · (𝐸↑2)) = (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)))
341219adantr 473 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴↑2) ∈ ℂ)
342 sqne0 13302 . . . . . . . . . . . . . . . . . . 19 (𝐸 ∈ ℂ → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
3434, 342syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
344322, 343mpbird 249 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸↑2) ≠ 0)
345344adantr 473 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ≠ 0)
346341, 330, 345divcan1d 11216 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)) = (𝐴↑2))
347335, 340, 3463eqtrd 2812 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (𝐴↑2))
3487adantr 473 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐷 ∈ ℂ)
34937adantr 473 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ∈ ℂ)
350329, 348, 349mul12d 10647 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))))
3519adantr 473 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐵 ∈ ℂ)
35211adantr 473 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ∈ ℂ)
353321adantr 473 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ≠ 0)
354351, 352, 353sqdivd 13336 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = ((𝐵↑2) / (𝐹↑2)))
355354oveq1d 6989 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐹↑2)) = (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)))
356355oveq2d 6990 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))) = (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))))
357206adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐵↑2) ∈ ℂ)
358 sqne0 13302 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ ℂ → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
35911, 358syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
360321, 359mpbird 249 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹↑2) ≠ 0)
361360adantr 473 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ≠ 0)
362357, 349, 361divcan1d 11216 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)) = (𝐵↑2))
363362oveq2d 6990 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
364350, 356, 3633eqtrd 2812 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
365347, 364oveq12d 6992 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
366326, 332, 3653eqtrd 2812 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
367226eqcomd 2778 . . . . . . . . . . . . 13 (𝜑𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
368367adantr 473 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
369366, 368oveq12d 6992 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))))
37016adantr 473 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ∈ ℂ)
37117adantr 473 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ≠ 0)
372329, 370, 371divcan4d 11221 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = ((𝐵 / 𝐹)↑2))
373226, 226oveq12d 6992 . . . . . . . . . . . . 13 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = (𝐶 / 𝐶))
37416, 17dividd 11213 . . . . . . . . . . . . 13 (𝜑 → (𝐶 / 𝐶) = 1)
375373, 374eqtrd 2808 . . . . . . . . . . . 12 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
376375adantr 473 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
377369, 372, 3763eqtr3d 2816 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = 1)
37826, 27, 321redivcld 11267 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐹) ∈ ℝ)
3798nnnn0d 11765 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ ℕ0)
380379nn0ge0d 11768 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 𝐵)
38110nngt0d 11487 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < 𝐹)
382 divge0 11308 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ (𝐹 ∈ ℝ ∧ 0 < 𝐹)) → 0 ≤ (𝐵 / 𝐹))
38326, 380, 27, 381, 382syl22anc 826 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (𝐵 / 𝐹))
384378, 383sqrtsqd 14638 . . . . . . . . . . . . . . 15 (𝜑 → (√‘((𝐵 / 𝐹)↑2)) = (𝐵 / 𝐹))
385384eqcomd 2778 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
386385ad2antrr 713 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
387 fveq2 6496 . . . . . . . . . . . . . 14 (((𝐵 / 𝐹)↑2) = 1 → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
388387adantl 474 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
389 sqrt1 14490 . . . . . . . . . . . . . 14 (√‘1) = 1
390389a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘1) = 1)
391386, 388, 3903eqtrd 2812 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = 1)
392391ex 405 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐵 / 𝐹) = 1))
393 simplr 756 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = (𝐴 / 𝐸))
394 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = 1)
395393, 394eqtr3d 2810 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 / 𝐸) = 1)
396395oveq1d 6989 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = (1 · 𝐸))
3972, 4, 322divcan1d 11216 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
398397ad2antrr 713 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
3994mulid2d 10456 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝐸) = 𝐸)
400399ad2antrr 713 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐸) = 𝐸)
401396, 398, 4003eqtr3d 2816 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐴 = 𝐸)
402394oveq1d 6989 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = (1 · 𝐹))
4039, 11, 321divcan1d 11216 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
404403ad2antrr 713 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
40511mulid2d 10456 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝐹) = 𝐹)
406405ad2antrr 713 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐹) = 𝐹)
407402, 404, 4063eqtr3d 2816 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐵 = 𝐹)
408401, 407jca 504 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 = 𝐸𝐵 = 𝐹))
409408ex 405 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹) = 1 → (𝐴 = 𝐸𝐵 = 𝐹)))
410392, 409syld 47 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐴 = 𝐸𝐵 = 𝐹)))
411377, 410mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴 = 𝐸𝐵 = 𝐹))
412411ex 405 . . . . . . . 8 (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (𝐴 = 𝐸𝐵 = 𝐹)))
413323, 412sylbird 252 . . . . . . 7 (𝜑 → ((𝐵 · 𝐸) = (𝐴 · 𝐹) → (𝐴 = 𝐸𝐵 = 𝐹)))
414320, 413mtod 190 . . . . . 6 (𝜑 → ¬ (𝐵 · 𝐸) = (𝐴 · 𝐹))
415414neqned 2968 . . . . 5 (𝜑 → (𝐵 · 𝐸) ≠ (𝐴 · 𝐹))
416110, 111, 415subne0d 10805 . . . 4 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ≠ 0)
417112, 16, 416, 17divne0d 11231 . . 3 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0)
418 nnabscl 14544 . . 3 (((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ∧ (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0) → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
419319, 417, 418syl2anc 576 . 2 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
420 oveq1 6981 . . . . 5 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (𝑎↑2) = ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2))
421420oveq1d 6989 . . . 4 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))))
422421eqeq1d 2774 . . 3 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1))
423 oveq1 6981 . . . . . 6 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝑏↑2) = ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
424423oveq2d 6990 . . . . 5 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝐷 · (𝑏↑2)) = (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
425424oveq2d 6990 . . . 4 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
426425eqeq1d 2774 . . 3 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → ((((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1))
427422, 426rspc2ev 3544 . 2 (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ ∧ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ ∧ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
428289, 419, 274, 427syl3anc 1351 1 (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 387  w3a 1068   = wceq 1507  wcel 2050  wne 2961  wrex 3083   class class class wbr 4925  cfv 6185  (class class class)co 6974  cc 10331  cr 10332  0cc0 10333  1c1 10334   + caddc 10336   · cmul 10338   < clt 10472  cle 10473  cmin 10668  -cneg 10669   / cdiv 11096  cn 11437  2c2 11493  cz 11791  cq 12160  +crp 12202   mod cmo 13050  cexp 13242  csqrt 14451  abscabs 14452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277  ax-cnex 10389  ax-resscn 10390  ax-1cn 10391  ax-icn 10392  ax-addcl 10393  ax-addrcl 10394  ax-mulcl 10395  ax-mulrcl 10396  ax-mulcom 10397  ax-addass 10398  ax-mulass 10399  ax-distr 10400  ax-i2m1 10401  ax-1ne0 10402  ax-1rid 10403  ax-rnegex 10404  ax-rrecex 10405  ax-cnre 10406  ax-pre-lttri 10407  ax-pre-lttrn 10408  ax-pre-ltadd 10409  ax-pre-mulgt0 10410  ax-pre-sup 10411
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3676  df-csb 3781  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-pss 3839  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4709  df-iun 4790  df-br 4926  df-opab 4988  df-mpt 5005  df-tr 5027  df-id 5308  df-eprel 5313  df-po 5322  df-so 5323  df-fr 5362  df-we 5364  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-pred 5983  df-ord 6029  df-on 6030  df-lim 6031  df-suc 6032  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-f1 6190  df-fo 6191  df-f1o 6192  df-fv 6193  df-riota 6935  df-ov 6977  df-oprab 6978  df-mpo 6979  df-om 7395  df-2nd 7500  df-wrecs 7748  df-recs 7810  df-rdg 7848  df-er 8087  df-en 8305  df-dom 8306  df-sdom 8307  df-sup 8699  df-inf 8700  df-pnf 10474  df-mnf 10475  df-xr 10476  df-ltxr 10477  df-le 10478  df-sub 10670  df-neg 10671  df-div 11097  df-nn 11438  df-2 11501  df-3 11502  df-n0 11706  df-z 11792  df-uz 12057  df-rp 12203  df-fl 12975  df-mod 13051  df-seq 13183  df-exp 13243  df-cj 14317  df-re 14318  df-im 14319  df-sqrt 14453  df-abs 14454
This theorem is referenced by:  pellex  38857
  Copyright terms: Public domain W3C validator