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 37897
Description: Lemma for pellex 37898. 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 11317 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
3 pellex.enn . . . . . . . . 9 (𝜑𝐸 ∈ ℕ)
43nncnd 11317 . . . . . . . 8 (𝜑𝐸 ∈ ℂ)
52, 4mulcld 10341 . . . . . . 7 (𝜑 → (𝐴 · 𝐸) ∈ ℂ)
6 pellex.dnn . . . . . . . . 9 (𝜑𝐷 ∈ ℕ)
76nncnd 11317 . . . . . . . 8 (𝜑𝐷 ∈ ℂ)
8 pellex.bnn . . . . . . . . . 10 (𝜑𝐵 ∈ ℕ)
98nncnd 11317 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
10 pellex.fnn . . . . . . . . . 10 (𝜑𝐹 ∈ ℕ)
1110nncnd 11317 . . . . . . . . 9 (𝜑𝐹 ∈ ℂ)
129, 11mulcld 10341 . . . . . . . 8 (𝜑 → (𝐵 · 𝐹) ∈ ℂ)
137, 12mulcld 10341 . . . . . . 7 (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℂ)
145, 13subcld 10673 . . . . . 6 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
15 pellex.cz . . . . . . 7 (𝜑𝐶 ∈ ℤ)
1615zcnd 11745 . . . . . 6 (𝜑𝐶 ∈ ℂ)
17 pellex.cn0 . . . . . 6 (𝜑𝐶 ≠ 0)
1814, 16, 17absdivd 14413 . . . . 5 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)))
195, 13negsubd 10679 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))))
2019eqcomd 2812 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))))
2120oveq1d 6885 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
221nnred 11316 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
233nnred 11316 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℝ)
2422, 23remulcld 10351 . . . . . . . . . 10 (𝜑 → (𝐴 · 𝐸) ∈ ℝ)
256nnred 11316 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℝ)
268nnred 11316 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
2710nnred 11316 . . . . . . . . . . . 12 (𝜑𝐹 ∈ ℝ)
2826, 27remulcld 10351 . . . . . . . . . . 11 (𝜑 → (𝐵 · 𝐹) ∈ ℝ)
2925, 28remulcld 10351 . . . . . . . . . 10 (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
3029renegcld 10738 . . . . . . . . . 10 (𝜑 → -(𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
3116, 17absrpcld 14406 . . . . . . . . . 10 (𝜑 → (abs‘𝐶) ∈ ℝ+)
323nnzd 11743 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℤ)
33 pellex.xcg . . . . . . . . . . . 12 (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))
34 modmul1 12943 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
3522, 23, 32, 31, 33, 34syl221anc 1493 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
364sqcld 13225 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸↑2) ∈ ℂ)
3711sqcld 13225 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹↑2) ∈ ℂ)
387, 37mulcld 10341 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℂ)
3936, 38npcand 10677 . . . . . . . . . . . . . 14 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) = (𝐸↑2))
404sqvald 13224 . . . . . . . . . . . . . 14 (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
4139, 40eqtr2d 2841 . . . . . . . . . . . . 13 (𝜑 → (𝐸 · 𝐸) = (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))))
4241oveq1d 6885 . . . . . . . . . . . 12 (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
4323resqcld 13254 . . . . . . . . . . . . . 14 (𝜑 → (𝐸↑2) ∈ ℝ)
4427resqcld 13254 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹↑2) ∈ ℝ)
4525, 44remulcld 10351 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℝ)
4643, 45resubcld 10739 . . . . . . . . . . . . 13 (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ)
47 0red 10324 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
4816abscld 14394 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘𝐶) ∈ ℝ)
4948recnd 10349 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘𝐶) ∈ ℂ)
5016, 17absne0d 14405 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘𝐶) ≠ 0)
5149, 50dividd 11080 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) = 1)
52 1zzd 11670 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
5351, 52eqeltrd 2885 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ)
54 mod0 12895 . . . . . . . . . . . . . . . . 17 (((abs‘𝐶) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
5548, 31, 54syl2anc 575 . . . . . . . . . . . . . . . 16 (𝜑 → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
5653, 55mpbird 248 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐶) mod (abs‘𝐶)) = 0)
5715zred 11744 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℝ)
58 absmod0 14262 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
5957, 31, 58syl2anc 575 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
6056, 59mpbird 248 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 mod (abs‘𝐶)) = 0)
61 pellex.no2 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
6261oveq1d 6885 . . . . . . . . . . . . . 14 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (𝐶 mod (abs‘𝐶)))
63 0mod 12921 . . . . . . . . . . . . . . 15 ((abs‘𝐶) ∈ ℝ+ → (0 mod (abs‘𝐶)) = 0)
6431, 63syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0 mod (abs‘𝐶)) = 0)
6560, 62, 643eqtr4d 2850 . . . . . . . . . . . . 13 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
66 modadd1 12927 . . . . . . . . . . . . 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 1493 . . . . . . . . . . . 12 (𝜑 → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
6838addid2d 10518 . . . . . . . . . . . . . 14 (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐷 · (𝐹↑2)))
6911sqvald 13224 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
7069oveq2d 6886 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹↑2)) = (𝐷 · (𝐹 · 𝐹)))
717, 11, 11mul12d 10526 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹 · 𝐹)) = (𝐹 · (𝐷 · 𝐹)))
7268, 70, 713eqtrd 2844 . . . . . . . . . . . . 13 (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐹 · (𝐷 · 𝐹)))
7372oveq1d 6885 . . . . . . . . . . . 12 (𝜑 → ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
7442, 67, 733eqtrd 2844 . . . . . . . . . . 11 (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
756nnzd 11743 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ ℤ)
7610nnzd 11743 . . . . . . . . . . . . . 14 (𝜑𝐹 ∈ ℤ)
7775, 76zmulcld 11750 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · 𝐹) ∈ ℤ)
78 pellex.ycg . . . . . . . . . . . . . 14 (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))
7978eqcomd 2812 . . . . . . . . . . . . 13 (𝜑 → (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶)))
80 modmul1 12943 . . . . . . . . . . . . 13 (((𝐹 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐷 · 𝐹) ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶))) → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
8127, 26, 77, 31, 79, 80syl221anc 1493 . . . . . . . . . . . 12 (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
829, 7, 11mul12d 10526 . . . . . . . . . . . . 13 (𝜑 → (𝐵 · (𝐷 · 𝐹)) = (𝐷 · (𝐵 · 𝐹)))
8382oveq1d 6885 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
8481, 83eqtrd 2840 . . . . . . . . . . 11 (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
8535, 74, 843eqtrd 2844 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
86 modadd1 12927 . . . . . . . . . 10 ((((𝐴 · 𝐸) ∈ ℝ ∧ (𝐷 · (𝐵 · 𝐹)) ∈ ℝ) ∧ (-(𝐷 · (𝐵 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) ∧ ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
8724, 29, 30, 31, 85, 86syl221anc 1493 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
8813negidd 10663 . . . . . . . . . 10 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) = 0)
8988oveq1d 6885 . . . . . . . . 9 (𝜑 → (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
9021, 87, 893eqtrd 2844 . . . . . . . 8 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
9190, 64eqtrd 2840 . . . . . . 7 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0)
9224, 29resubcld 10739 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ)
93 absmod0 14262 . . . . . . . 8 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
9492, 31, 93syl2anc 575 . . . . . . 7 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
9591, 94mpbid 223 . . . . . 6 (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0)
9614abscld 14394 . . . . . . 7 (𝜑 → (abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ)
97 mod0 12895 . . . . . . 7 (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
9896, 31, 97syl2anc 575 . . . . . 6 (𝜑 → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
9995, 98mpbid 223 . . . . 5 (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ)
10018, 99eqeltrd 2885 . . . 4 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ)
10192, 57, 17redivcld 11134 . . . . 5 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ)
102 absz 14270 . . . . 5 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
103101, 102syl 17 . . . 4 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
104100, 103mpbird 248 . . 3 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ)
105 0lt1 10831 . . . . . . . 8 0 < 1
106 0re 10323 . . . . . . . . 9 0 ∈ ℝ
107 1re 10321 . . . . . . . . 9 1 ∈ ℝ
108106, 107ltnlei 10439 . . . . . . . 8 (0 < 1 ↔ ¬ 1 ≤ 0)
109105, 108mpbi 221 . . . . . . 7 ¬ 1 ≤ 0
1109, 4mulcld 10341 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 · 𝐸) ∈ ℂ)
1112, 11mulcld 10341 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐹) ∈ ℂ)
112110, 111subcld 10673 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℂ)
113112, 16, 17divcld 11082 . . . . . . . . . . . 12 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℂ)
114113abscld 14394 . . . . . . . . . . 11 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℝ)
115114resqcld 13254 . . . . . . . . . 10 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) ∈ ℝ)
1166nnnn0d 11613 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℕ0)
117116nn0ge0d 11616 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝐷)
118114sqge0d 13255 . . . . . . . . . 10 (𝜑 → 0 ≤ ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
11925, 115, 117, 118mulge0d 10885 . . . . . . . . 9 (𝜑 → 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
12025, 115remulcld 10351 . . . . . . . . . 10 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) ∈ ℝ)
12147, 120suble0d 10899 . . . . . . . . 9 (𝜑 → ((0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0 ↔ 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
122119, 121mpbird 248 . . . . . . . 8 (𝜑 → (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0)
123 breq1 4847 . . . . . . . 8 (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → (1 ≤ 0 ↔ (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0))
124122, 123syl5ibrcom 238 . . . . . . 7 (𝜑 → (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → 1 ≤ 0))
125109, 124mtoi 190 . . . . . 6 (𝜑 → ¬ 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
126 absresq 14261 . . . . . . . . . . . 12 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
127101, 126syl 17 . . . . . . . . . . 11 (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
12814, 16, 17sqdivd 13240 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)))
12914sqvald 13224 . . . . . . . . . . . 12 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) = (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))))
130129oveq1d 6885 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
131127, 128, 1303eqtrd 2844 . . . . . . . . . 10 (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
13226, 23remulcld 10351 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 · 𝐸) ∈ ℝ)
13322, 27remulcld 10351 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐹) ∈ ℝ)
134132, 133resubcld 10739 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ)
135134, 57, 17redivcld 11134 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ)
136 absresq 14261 . . . . . . . . . . . . . 14 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
137135, 136syl 17 . . . . . . . . . . . . 13 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
138112, 16, 17sqdivd 13240 . . . . . . . . . . . . 13 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
139137, 138eqtrd 2840 . . . . . . . . . . . 12 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
140139oveq2d 6886 . . . . . . . . . . 11 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
141112sqcld 13225 . . . . . . . . . . . 12 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) ∈ ℂ)
14216sqcld 13225 . . . . . . . . . . . 12 (𝜑 → (𝐶↑2) ∈ ℂ)
143 sqne0 13149 . . . . . . . . . . . . . 14 (𝐶 ∈ ℂ → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
14416, 143syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
14517, 144mpbird 248 . . . . . . . . . . . 12 (𝜑 → (𝐶↑2) ≠ 0)
1467, 141, 142, 145divassd 11117 . . . . . . . . . . 11 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
147112sqvald 13224 . . . . . . . . . . . . 13 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) = (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))
148147oveq2d 6886 . . . . . . . . . . . 12 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) = (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))))
149148oveq1d 6885 . . . . . . . . . . 11 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
150140, 146, 1493eqtr2d 2846 . . . . . . . . . 10 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
151131, 150oveq12d 6888 . . . . . . . . 9 (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
15214, 14mulcld 10341 . . . . . . . . . 10 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
153112, 112mulcld 10341 . . . . . . . . . . 11 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℂ)
1547, 153mulcld 10341 . . . . . . . . . 10 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) ∈ ℂ)
155152, 154, 142, 145divsubdird 11121 . . . . . . . . 9 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
1565, 13, 5, 13mulsubd 10771 . . . . . . . . . . . 12 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))))
157110, 111, 110, 111mulsubd 10771 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) = ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
158157oveq2d 6886 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
159110, 110mulcld 10341 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) · (𝐵 · 𝐸)) ∈ ℂ)
160111, 111mulcld 10341 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐹) · (𝐴 · 𝐹)) ∈ ℂ)
161159, 160addcld 10340 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
162110, 111mulcld 10341 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) · (𝐴 · 𝐹)) ∈ ℂ)
163162, 162addcld 10340 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
1647, 161, 163subdid 10767 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
1657, 159, 160adddid 10345 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
1667, 162, 162adddid 10345 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
167165, 166oveq12d 6888 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
168158, 164, 1673eqtrd 2844 . . . . . . . . . . . 12 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
169156, 168oveq12d 6888 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
170169oveq1d 6885 . . . . . . . . . 10 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)))
1715, 13mulcomd 10342 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)))
1727, 12, 5mulassd 10344 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)) = (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))))
1732, 4mulcomd 10342 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 · 𝐸) = (𝐸 · 𝐴))
174173oveq2d 6886 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐹) · (𝐸 · 𝐴)))
1759, 11, 4, 2mul4d 10529 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹) · (𝐸 · 𝐴)) = ((𝐵 · 𝐸) · (𝐹 · 𝐴)))
17611, 2mulcomd 10342 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 · 𝐴) = (𝐴 · 𝐹))
177176oveq2d 6886 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐸) · (𝐹 · 𝐴)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
178174, 175, 1773eqtrd 2844 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
179178oveq2d 6886 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
180171, 172, 1793eqtrd 2844 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
181180, 180oveq12d 6888 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
182181oveq2d 6886 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
183182oveq1d 6885 . . . . . . . . . . . 12 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
1845, 5mulcld 10341 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐸) · (𝐴 · 𝐸)) ∈ ℂ)
18513, 13mulcld 10341 . . . . . . . . . . . . . 14 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
186184, 185addcld 10340 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
1877, 159mulcld 10341 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) ∈ ℂ)
1887, 160mulcld 10341 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
189187, 188addcld 10340 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) ∈ ℂ)
1907, 162mulcld 10341 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
191190, 190addcld 10340 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) ∈ ℂ)
192186, 189, 191nnncan2d 10708 . . . . . . . . . . . 12 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
193184, 185, 187, 188addsub4d 10720 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
1945sqvald 13224 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴 · 𝐸) · (𝐴 · 𝐸)))
195110sqvald 13224 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵 · 𝐸) · (𝐵 · 𝐸)))
196195oveq2d 6886 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))))
197194, 196oveq12d 6888 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))))
19813sqvald 13224 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))))
199111sqvald 13224 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴 · 𝐹) · (𝐴 · 𝐹)))
200199oveq2d 6886 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))
201198, 200oveq12d 6888 . . . . . . . . . . . . . 14 (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
202197, 201oveq12d 6888 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
2032, 4sqmuld 13239 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴↑2) · (𝐸↑2)))
2049, 4sqmuld 13239 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵↑2) · (𝐸↑2)))
205204oveq2d 6886 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
2069sqcld 13225 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵↑2) ∈ ℂ)
2077, 206, 36mulassd 10344 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐵↑2)) · (𝐸↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
208205, 207eqtr4d 2843 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = ((𝐷 · (𝐵↑2)) · (𝐸↑2)))
209203, 208oveq12d 6888 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
2107sqvald 13224 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷↑2) = (𝐷 · 𝐷))
2119, 11sqmuld 13239 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹)↑2) = ((𝐵↑2) · (𝐹↑2)))
212210, 211oveq12d 6888 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷↑2) · ((𝐵 · 𝐹)↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
2137, 12sqmuld 13239 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷↑2) · ((𝐵 · 𝐹)↑2)))
2147, 7mulcld 10341 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · 𝐷) ∈ ℂ)
215214, 206, 37mulassd 10344 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
216212, 213, 2153eqtr4d 2850 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)))
2172, 11sqmuld 13239 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴↑2) · (𝐹↑2)))
218217oveq2d 6886 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
2192sqcld 13225 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴↑2) ∈ ℂ)
2207, 219, 37mulassd 10344 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐴↑2)) · (𝐹↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
221218, 220eqtr4d 2843 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = ((𝐷 · (𝐴↑2)) · (𝐹↑2)))
222216, 221oveq12d 6888 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
223209, 222oveq12d 6888 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))))
2247, 206mulcld 10341 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · (𝐵↑2)) ∈ ℂ)
225219, 224, 36subdird 10768 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
226 pellex.no1 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)
227226oveq1d 6885 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (𝐶 · (𝐸↑2)))
228225, 227eqtr3d 2842 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) = (𝐶 · (𝐸↑2)))
2297, 7, 206mulassd 10344 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) = (𝐷 · (𝐷 · (𝐵↑2))))
230229oveq1d 6885 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
231230oveq1d 6885 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)))
232214, 206mulcld 10341 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) ∈ ℂ)
2337, 219mulcld 10341 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · (𝐴↑2)) ∈ ℂ)
234232, 233, 37subdird 10768 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
235 subdi 10744 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
236235eqcomd 2812 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
2377, 224, 219, 236syl3anc 1483 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
238 negsubdi2 10621 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = ((𝐷 · (𝐵↑2)) − (𝐴↑2)))
239238eqcomd 2812 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
240219, 224, 239syl2anc 575 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
241226negeqd 10556 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = -𝐶)
242240, 241eqtrd 2840 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -𝐶)
243242oveq2d 6886 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = (𝐷 · -𝐶))
2447, 16mulneg2d 10765 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · -𝐶) = -(𝐷 · 𝐶))
245237, 243, 2443eqtrd 2844 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = -(𝐷 · 𝐶))
246245oveq1d 6885 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (-(𝐷 · 𝐶) · (𝐹↑2)))
247231, 234, 2463eqtr3d 2848 . . . . . . . . . . . . . . 15 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))) = (-(𝐷 · 𝐶) · (𝐹↑2)))
248228, 247oveq12d 6888 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))))
2497, 16mulcld 10341 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · 𝐶) ∈ ℂ)
250249, 37mulneg1d 10764 . . . . . . . . . . . . . . . . 17 (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -((𝐷 · 𝐶) · (𝐹↑2)))
2517, 16mulcomd 10342 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐷 · 𝐶) = (𝐶 · 𝐷))
252251oveq1d 6885 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = ((𝐶 · 𝐷) · (𝐹↑2)))
25316, 7, 37mulassd 10344 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐶 · 𝐷) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
254252, 253eqtrd 2840 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
255254negeqd 10556 . . . . . . . . . . . . . . . . 17 (𝜑 → -((𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
256250, 255eqtrd 2840 . . . . . . . . . . . . . . . 16 (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
257256oveq2d 6886 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))))
25816, 36mulcld 10341 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · (𝐸↑2)) ∈ ℂ)
25916, 38mulcld 10341 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · (𝐷 · (𝐹↑2))) ∈ ℂ)
260258, 259negsubd 10679 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
26161oveq2d 6886 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = (𝐶 · 𝐶))
262 subdi 10744 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
263262eqcomd 2812 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
26416, 36, 38, 263syl3anc 1483 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
26516sqvald 13224 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶↑2) = (𝐶 · 𝐶))
266261, 264, 2653eqtr4d 2850 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶↑2))
267257, 260, 2663eqtrd 2844 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = (𝐶↑2))
268223, 248, 2673eqtrd 2844 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = (𝐶↑2))
269193, 202, 2683eqtr2d 2846 . . . . . . . . . . . 12 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = (𝐶↑2))
270183, 192, 2693eqtrd 2844 . . . . . . . . . . 11 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (𝐶↑2))
271270oveq1d 6885 . . . . . . . . . 10 (𝜑 → ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)) = ((𝐶↑2) / (𝐶↑2)))
272142, 145dividd 11080 . . . . . . . . . 10 (𝜑 → ((𝐶↑2) / (𝐶↑2)) = 1)
273170, 271, 2723eqtrd 2844 . . . . . . . . 9 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = 1)
274151, 155, 2733eqtr2d 2846 . . . . . . . 8 (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
275274adantr 468 . . . . . . 7 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
276 simpr 473 . . . . . . . . . . 11 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
277276fvoveq1d 6892 . . . . . . . . . 10 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = (abs‘(0 / 𝐶)))
27816, 17div0d 11081 . . . . . . . . . . . 12 (𝜑 → (0 / 𝐶) = 0)
279278abs00bd 14250 . . . . . . . . . . 11 (𝜑 → (abs‘(0 / 𝐶)) = 0)
280279adantr 468 . . . . . . . . . 10 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(0 / 𝐶)) = 0)
281277, 280eqtrd 2840 . . . . . . . . 9 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = 0)
282281sq0id 13176 . . . . . . . 8 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = 0)
283282oveq1d 6885 . . . . . . 7 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
284275, 283eqtr3d 2842 . . . . . 6 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
285125, 284mtand 841 . . . . 5 (𝜑 → ¬ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
286285neqned 2985 . . . 4 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ≠ 0)
28714, 16, 286, 17divne0d 11098 . . 3 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0)
288 nnabscl 14284 . . 3 (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ∧ (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
289104, 287, 288syl2anc 575 . 2 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
290112, 16, 17absdivd 14413 . . . . 5 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) = ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)))
291 negsub 10610 . . . . . . . . . . . 12 (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) + -(𝐴 · 𝐹)) = ((𝐵 · 𝐸) − (𝐴 · 𝐹)))
292291eqcomd 2812 . . . . . . . . . . 11 (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
293110, 111, 292syl2anc 575 . . . . . . . . . 10 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
294293oveq1d 6885 . . . . . . . . 9 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
295133renegcld 10738 . . . . . . . . . 10 (𝜑 → -(𝐴 · 𝐹) ∈ ℝ)
29611, 4mulcomd 10342 . . . . . . . . . . . 12 (𝜑 → (𝐹 · 𝐸) = (𝐸 · 𝐹))
297296oveq1d 6885 . . . . . . . . . . 11 (𝜑 → ((𝐹 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
298 modmul1 12943 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ 𝐹 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
29926, 27, 32, 31, 78, 298syl221anc 1493 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
300 modmul1 12943 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐹 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
30122, 23, 76, 31, 33, 300syl221anc 1493 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
302297, 299, 3013eqtr4d 2850 . . . . . . . . . 10 (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶)))
303 modadd1 12927 . . . . . . . . . 10 ((((𝐵 · 𝐸) ∈ ℝ ∧ (𝐴 · 𝐹) ∈ ℝ) ∧ (-(𝐴 · 𝐹) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) ∧ ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶))) → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
304132, 133, 295, 31, 302, 303syl221anc 1493 . . . . . . . . 9 (𝜑 → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
305111negidd 10663 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐹) + -(𝐴 · 𝐹)) = 0)
306305oveq1d 6885 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
307294, 304, 3063eqtrd 2844 . . . . . . . 8 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
308307, 64eqtrd 2840 . . . . . . 7 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0)
309 absmod0 14262 . . . . . . . 8 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
310134, 31, 309syl2anc 575 . . . . . . 7 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
311308, 310mpbid 223 . . . . . 6 (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0)
312112abscld 14394 . . . . . . 7 (𝜑 → (abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ)
313 mod0 12895 . . . . . . 7 (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
314312, 31, 313syl2anc 575 . . . . . 6 (𝜑 → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
315311, 314mpbid 223 . . . . 5 (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ)
316290, 315eqeltrd 2885 . . . 4 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ)
317 absz 14270 . . . . 5 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
318135, 317syl 17 . . . 4 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
319316, 318mpbird 248 . . 3 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ)
320 pellex.neq . . . . . . 7 (𝜑 → ¬ (𝐴 = 𝐸𝐵 = 𝐹))
32110nnne0d 11347 . . . . . . . . 9 (𝜑𝐹 ≠ 0)
3223nnne0d 11347 . . . . . . . . 9 (𝜑𝐸 ≠ 0)
3239, 11, 2, 4, 321, 322divmuleqd 11128 . . . . . . . 8 (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) ↔ (𝐵 · 𝐸) = (𝐴 · 𝐹)))
32461adantr 468 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
325324eqcomd 2812 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐸↑2) − (𝐷 · (𝐹↑2))))
326325oveq2d 6886 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
3279, 11, 321divcld 11082 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐹) ∈ ℂ)
328327sqcld 13225 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 𝐹)↑2) ∈ ℂ)
329328adantr 468 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) ∈ ℂ)
33036adantr 468 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ∈ ℂ)
33138adantr 468 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (𝐹↑2)) ∈ ℂ)
332329, 330, 331subdid 10767 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))))
333 oveq1 6877 . . . . . . . . . . . . . . . . 17 ((𝐵 / 𝐹) = (𝐴 / 𝐸) → ((𝐵 / 𝐹)↑2) = ((𝐴 / 𝐸)↑2))
334333oveq1d 6885 . . . . . . . . . . . . . . . 16 ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
335334adantl 469 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
3362adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐴 ∈ ℂ)
3374adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ∈ ℂ)
338322adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ≠ 0)
339336, 337, 338sqdivd 13240 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐴 / 𝐸)↑2) = ((𝐴↑2) / (𝐸↑2)))
340339oveq1d 6885 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴 / 𝐸)↑2) · (𝐸↑2)) = (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)))
341219adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴↑2) ∈ ℂ)
342 sqne0 13149 . . . . . . . . . . . . . . . . . . 19 (𝐸 ∈ ℂ → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
3434, 342syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
344322, 343mpbird 248 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸↑2) ≠ 0)
345344adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ≠ 0)
346341, 330, 345divcan1d 11083 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)) = (𝐴↑2))
347335, 340, 3463eqtrd 2844 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (𝐴↑2))
3487adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐷 ∈ ℂ)
34937adantr 468 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ∈ ℂ)
350329, 348, 349mul12d 10526 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))))
3519adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐵 ∈ ℂ)
35211adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ∈ ℂ)
353321adantr 468 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ≠ 0)
354351, 352, 353sqdivd 13240 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = ((𝐵↑2) / (𝐹↑2)))
355354oveq1d 6885 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐹↑2)) = (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)))
356355oveq2d 6886 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))) = (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))))
357206adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐵↑2) ∈ ℂ)
358 sqne0 13149 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ ℂ → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
35911, 358syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
360321, 359mpbird 248 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹↑2) ≠ 0)
361360adantr 468 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ≠ 0)
362357, 349, 361divcan1d 11083 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)) = (𝐵↑2))
363362oveq2d 6886 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
364350, 356, 3633eqtrd 2844 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
365347, 364oveq12d 6888 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
366326, 332, 3653eqtrd 2844 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
367226eqcomd 2812 . . . . . . . . . . . . 13 (𝜑𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
368367adantr 468 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
369366, 368oveq12d 6888 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))))
37016adantr 468 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ∈ ℂ)
37117adantr 468 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ≠ 0)
372329, 370, 371divcan4d 11088 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = ((𝐵 / 𝐹)↑2))
373226, 226oveq12d 6888 . . . . . . . . . . . . 13 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = (𝐶 / 𝐶))
37416, 17dividd 11080 . . . . . . . . . . . . 13 (𝜑 → (𝐶 / 𝐶) = 1)
375373, 374eqtrd 2840 . . . . . . . . . . . 12 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
376375adantr 468 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
377369, 372, 3763eqtr3d 2848 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = 1)
37826, 27, 321redivcld 11134 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐹) ∈ ℝ)
3798nnnn0d 11613 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ ℕ0)
380379nn0ge0d 11616 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 𝐵)
38110nngt0d 11346 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < 𝐹)
382 divge0 11173 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ (𝐹 ∈ ℝ ∧ 0 < 𝐹)) → 0 ≤ (𝐵 / 𝐹))
38326, 380, 27, 381, 382syl22anc 858 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (𝐵 / 𝐹))
384378, 383sqrtsqd 14377 . . . . . . . . . . . . . . 15 (𝜑 → (√‘((𝐵 / 𝐹)↑2)) = (𝐵 / 𝐹))
385384eqcomd 2812 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
386385ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
387 fveq2 6404 . . . . . . . . . . . . . 14 (((𝐵 / 𝐹)↑2) = 1 → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
388387adantl 469 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
389 sqrt1 14231 . . . . . . . . . . . . . 14 (√‘1) = 1
390389a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘1) = 1)
391386, 388, 3903eqtrd 2844 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = 1)
392391ex 399 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐵 / 𝐹) = 1))
393 simplr 776 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = (𝐴 / 𝐸))
394 simpr 473 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = 1)
395393, 394eqtr3d 2842 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 / 𝐸) = 1)
396395oveq1d 6885 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = (1 · 𝐸))
3972, 4, 322divcan1d 11083 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
398397ad2antrr 708 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
3994mulid2d 10339 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝐸) = 𝐸)
400399ad2antrr 708 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐸) = 𝐸)
401396, 398, 4003eqtr3d 2848 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐴 = 𝐸)
402394oveq1d 6885 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = (1 · 𝐹))
4039, 11, 321divcan1d 11083 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
404403ad2antrr 708 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
40511mulid2d 10339 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝐹) = 𝐹)
406405ad2antrr 708 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐹) = 𝐹)
407402, 404, 4063eqtr3d 2848 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐵 = 𝐹)
408401, 407jca 503 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 = 𝐸𝐵 = 𝐹))
409408ex 399 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹) = 1 → (𝐴 = 𝐸𝐵 = 𝐹)))
410392, 409syld 47 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐴 = 𝐸𝐵 = 𝐹)))
411377, 410mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴 = 𝐸𝐵 = 𝐹))
412411ex 399 . . . . . . . 8 (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (𝐴 = 𝐸𝐵 = 𝐹)))
413323, 412sylbird 251 . . . . . . 7 (𝜑 → ((𝐵 · 𝐸) = (𝐴 · 𝐹) → (𝐴 = 𝐸𝐵 = 𝐹)))
414320, 413mtod 189 . . . . . 6 (𝜑 → ¬ (𝐵 · 𝐸) = (𝐴 · 𝐹))
415414neqned 2985 . . . . 5 (𝜑 → (𝐵 · 𝐸) ≠ (𝐴 · 𝐹))
416110, 111, 415subne0d 10682 . . . 4 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ≠ 0)
417112, 16, 416, 17divne0d 11098 . . 3 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0)
418 nnabscl 14284 . . 3 (((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ∧ (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0) → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
419319, 417, 418syl2anc 575 . 2 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
420 oveq1 6877 . . . . 5 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (𝑎↑2) = ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2))
421420oveq1d 6885 . . . 4 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))))
422421eqeq1d 2808 . . 3 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1))
423 oveq1 6877 . . . . . 6 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝑏↑2) = ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
424423oveq2d 6886 . . . . 5 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝐷 · (𝑏↑2)) = (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
425424oveq2d 6886 . . . 4 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
426425eqeq1d 2808 . . 3 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → ((((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1))
427422, 426rspc2ev 3517 . 2 (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ ∧ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ ∧ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
428289, 419, 274, 427syl3anc 1483 1 (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wne 2978  wrex 3097   class class class wbr 4844  cfv 6097  (class class class)co 6870  cc 10215  cr 10216  0cc0 10217  1c1 10218   + caddc 10220   · cmul 10222   < clt 10355  cle 10356  cmin 10547  -cneg 10548   / cdiv 10965  cn 11301  2c2 11352  cz 11639  cq 12003  +crp 12042   mod cmo 12888  cexp 13079  csqrt 14192  abscabs 14193
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-iun 4714  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-om 7292  df-2nd 7395  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-er 7975  df-en 8189  df-dom 8190  df-sdom 8191  df-sup 8583  df-inf 8584  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-3 11361  df-n0 11556  df-z 11640  df-uz 11901  df-rp 12043  df-fl 12813  df-mod 12889  df-seq 13021  df-exp 13080  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195
This theorem is referenced by:  pellex  37898
  Copyright terms: Public domain W3C validator