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 42491
Description: Lemma for pellex 42492. 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 12280 . . . . . . . 8 (𝜑𝐴 ∈ ℂ)
3 pellex.enn . . . . . . . . 9 (𝜑𝐸 ∈ ℕ)
43nncnd 12280 . . . . . . . 8 (𝜑𝐸 ∈ ℂ)
52, 4mulcld 11284 . . . . . . 7 (𝜑 → (𝐴 · 𝐸) ∈ ℂ)
6 pellex.dnn . . . . . . . . 9 (𝜑𝐷 ∈ ℕ)
76nncnd 12280 . . . . . . . 8 (𝜑𝐷 ∈ ℂ)
8 pellex.bnn . . . . . . . . . 10 (𝜑𝐵 ∈ ℕ)
98nncnd 12280 . . . . . . . . 9 (𝜑𝐵 ∈ ℂ)
10 pellex.fnn . . . . . . . . . 10 (𝜑𝐹 ∈ ℕ)
1110nncnd 12280 . . . . . . . . 9 (𝜑𝐹 ∈ ℂ)
129, 11mulcld 11284 . . . . . . . 8 (𝜑 → (𝐵 · 𝐹) ∈ ℂ)
137, 12mulcld 11284 . . . . . . 7 (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℂ)
145, 13subcld 11621 . . . . . 6 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
15 pellex.cz . . . . . . 7 (𝜑𝐶 ∈ ℤ)
1615zcnd 12719 . . . . . 6 (𝜑𝐶 ∈ ℂ)
17 pellex.cn0 . . . . . 6 (𝜑𝐶 ≠ 0)
1814, 16, 17absdivd 15460 . . . . 5 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)))
195, 13negsubd 11627 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))))
2019eqcomd 2732 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))))
2120oveq1d 7439 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
221nnred 12279 . . . . . . . . . . 11 (𝜑𝐴 ∈ ℝ)
233nnred 12279 . . . . . . . . . . 11 (𝜑𝐸 ∈ ℝ)
2422, 23remulcld 11294 . . . . . . . . . 10 (𝜑 → (𝐴 · 𝐸) ∈ ℝ)
256nnred 12279 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℝ)
268nnred 12279 . . . . . . . . . . . 12 (𝜑𝐵 ∈ ℝ)
2710nnred 12279 . . . . . . . . . . . 12 (𝜑𝐹 ∈ ℝ)
2826, 27remulcld 11294 . . . . . . . . . . 11 (𝜑 → (𝐵 · 𝐹) ∈ ℝ)
2925, 28remulcld 11294 . . . . . . . . . 10 (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
3029renegcld 11691 . . . . . . . . . 10 (𝜑 → -(𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
3116, 17absrpcld 15453 . . . . . . . . . 10 (𝜑 → (abs‘𝐶) ∈ ℝ+)
323nnzd 12637 . . . . . . . . . . . 12 (𝜑𝐸 ∈ ℤ)
33 pellex.xcg . . . . . . . . . . . 12 (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))
34 modmul1 13944 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
3522, 23, 32, 31, 33, 34syl221anc 1378 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
364sqcld 14163 . . . . . . . . . . . . . . 15 (𝜑 → (𝐸↑2) ∈ ℂ)
3711sqcld 14163 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐹↑2) ∈ ℂ)
387, 37mulcld 11284 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℂ)
3936, 38npcand 11625 . . . . . . . . . . . . . 14 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) = (𝐸↑2))
404sqvald 14162 . . . . . . . . . . . . . 14 (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
4139, 40eqtr2d 2767 . . . . . . . . . . . . 13 (𝜑 → (𝐸 · 𝐸) = (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))))
4241oveq1d 7439 . . . . . . . . . . . 12 (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
4323resqcld 14144 . . . . . . . . . . . . . 14 (𝜑 → (𝐸↑2) ∈ ℝ)
4427resqcld 14144 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹↑2) ∈ ℝ)
4525, 44remulcld 11294 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℝ)
4643, 45resubcld 11692 . . . . . . . . . . . . 13 (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ)
47 0red 11267 . . . . . . . . . . . . 13 (𝜑 → 0 ∈ ℝ)
4816abscld 15441 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (abs‘𝐶) ∈ ℝ)
4948recnd 11292 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘𝐶) ∈ ℂ)
5016, 17absne0d 15452 . . . . . . . . . . . . . . . . . 18 (𝜑 → (abs‘𝐶) ≠ 0)
5149, 50dividd 12039 . . . . . . . . . . . . . . . . 17 (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) = 1)
52 1zzd 12645 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ ℤ)
5351, 52eqeltrd 2826 . . . . . . . . . . . . . . . 16 (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ)
54 mod0 13896 . . . . . . . . . . . . . . . . 17 (((abs‘𝐶) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
5548, 31, 54syl2anc 582 . . . . . . . . . . . . . . . 16 (𝜑 → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
5653, 55mpbird 256 . . . . . . . . . . . . . . 15 (𝜑 → ((abs‘𝐶) mod (abs‘𝐶)) = 0)
5715zred 12718 . . . . . . . . . . . . . . . 16 (𝜑𝐶 ∈ ℝ)
58 absmod0 15308 . . . . . . . . . . . . . . . 16 ((𝐶 ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
5957, 31, 58syl2anc 582 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
6056, 59mpbird 256 . . . . . . . . . . . . . 14 (𝜑 → (𝐶 mod (abs‘𝐶)) = 0)
61 pellex.no2 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
6261oveq1d 7439 . . . . . . . . . . . . . 14 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (𝐶 mod (abs‘𝐶)))
63 0mod 13922 . . . . . . . . . . . . . . 15 ((abs‘𝐶) ∈ ℝ+ → (0 mod (abs‘𝐶)) = 0)
6431, 63syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0 mod (abs‘𝐶)) = 0)
6560, 62, 643eqtr4d 2776 . . . . . . . . . . . . 13 (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
66 modadd1 13928 . . . . . . . . . . . . 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 1378 . . . . . . . . . . . 12 (𝜑 → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
6838addlidd 11465 . . . . . . . . . . . . . 14 (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐷 · (𝐹↑2)))
6911sqvald 14162 . . . . . . . . . . . . . . 15 (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
7069oveq2d 7440 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹↑2)) = (𝐷 · (𝐹 · 𝐹)))
717, 11, 11mul12d 11473 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (𝐹 · 𝐹)) = (𝐹 · (𝐷 · 𝐹)))
7268, 70, 713eqtrd 2770 . . . . . . . . . . . . 13 (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐹 · (𝐷 · 𝐹)))
7372oveq1d 7439 . . . . . . . . . . . 12 (𝜑 → ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
7442, 67, 733eqtrd 2770 . . . . . . . . . . 11 (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
756nnzd 12637 . . . . . . . . . . . . . 14 (𝜑𝐷 ∈ ℤ)
7610nnzd 12637 . . . . . . . . . . . . . 14 (𝜑𝐹 ∈ ℤ)
7775, 76zmulcld 12724 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · 𝐹) ∈ ℤ)
78 pellex.ycg . . . . . . . . . . . . . 14 (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))
7978eqcomd 2732 . . . . . . . . . . . . 13 (𝜑 → (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶)))
80 modmul1 13944 . . . . . . . . . . . . 13 (((𝐹 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐷 · 𝐹) ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶))) → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
8127, 26, 77, 31, 79, 80syl221anc 1378 . . . . . . . . . . . 12 (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
829, 7, 11mul12d 11473 . . . . . . . . . . . . 13 (𝜑 → (𝐵 · (𝐷 · 𝐹)) = (𝐷 · (𝐵 · 𝐹)))
8382oveq1d 7439 . . . . . . . . . . . 12 (𝜑 → ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
8481, 83eqtrd 2766 . . . . . . . . . . 11 (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
8535, 74, 843eqtrd 2770 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
86 modadd1 13928 . . . . . . . . . 10 ((((𝐴 · 𝐸) ∈ ℝ ∧ (𝐷 · (𝐵 · 𝐹)) ∈ ℝ) ∧ (-(𝐷 · (𝐵 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) ∧ ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
8724, 29, 30, 31, 85, 86syl221anc 1378 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
8813negidd 11611 . . . . . . . . . 10 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) = 0)
8988oveq1d 7439 . . . . . . . . 9 (𝜑 → (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
9021, 87, 893eqtrd 2770 . . . . . . . 8 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
9190, 64eqtrd 2766 . . . . . . 7 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0)
9224, 29resubcld 11692 . . . . . . . 8 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ)
93 absmod0 15308 . . . . . . . 8 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
9492, 31, 93syl2anc 582 . . . . . . 7 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
9591, 94mpbid 231 . . . . . 6 (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0)
9614abscld 15441 . . . . . . 7 (𝜑 → (abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ)
97 mod0 13896 . . . . . . 7 (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
9896, 31, 97syl2anc 582 . . . . . 6 (𝜑 → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
9995, 98mpbid 231 . . . . 5 (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ)
10018, 99eqeltrd 2826 . . . 4 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ)
10192, 57, 17redivcld 12093 . . . . 5 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ)
102 absz 15316 . . . . 5 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
103101, 102syl 17 . . . 4 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
104100, 103mpbird 256 . . 3 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ)
105 0lt1 11786 . . . . . . . 8 0 < 1
106 0re 11266 . . . . . . . . 9 0 ∈ ℝ
107 1re 11264 . . . . . . . . 9 1 ∈ ℝ
108106, 107ltnlei 11385 . . . . . . . 8 (0 < 1 ↔ ¬ 1 ≤ 0)
109105, 108mpbi 229 . . . . . . 7 ¬ 1 ≤ 0
1109, 4mulcld 11284 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 · 𝐸) ∈ ℂ)
1112, 11mulcld 11284 . . . . . . . . . . . . . 14 (𝜑 → (𝐴 · 𝐹) ∈ ℂ)
112110, 111subcld 11621 . . . . . . . . . . . . 13 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℂ)
113112, 16, 17divcld 12041 . . . . . . . . . . . 12 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℂ)
114113abscld 15441 . . . . . . . . . . 11 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℝ)
115114resqcld 14144 . . . . . . . . . 10 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) ∈ ℝ)
1166nnnn0d 12584 . . . . . . . . . . 11 (𝜑𝐷 ∈ ℕ0)
117116nn0ge0d 12587 . . . . . . . . . 10 (𝜑 → 0 ≤ 𝐷)
118114sqge0d 14156 . . . . . . . . . 10 (𝜑 → 0 ≤ ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
11925, 115, 117, 118mulge0d 11841 . . . . . . . . 9 (𝜑 → 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
12025, 115remulcld 11294 . . . . . . . . . 10 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) ∈ ℝ)
12147, 120suble0d 11855 . . . . . . . . 9 (𝜑 → ((0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0 ↔ 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
122119, 121mpbird 256 . . . . . . . 8 (𝜑 → (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0)
123 breq1 5156 . . . . . . . 8 (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → (1 ≤ 0 ↔ (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0))
124122, 123syl5ibrcom 246 . . . . . . 7 (𝜑 → (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → 1 ≤ 0))
125109, 124mtoi 198 . . . . . 6 (𝜑 → ¬ 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
126 absresq 15307 . . . . . . . . . . . 12 ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
127101, 126syl 17 . . . . . . . . . . 11 (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
12814, 16, 17sqdivd 14178 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)))
12914sqvald 14162 . . . . . . . . . . . 12 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) = (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))))
130129oveq1d 7439 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
131127, 128, 1303eqtrd 2770 . . . . . . . . . 10 (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
13226, 23remulcld 11294 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 · 𝐸) ∈ ℝ)
13322, 27remulcld 11294 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐴 · 𝐹) ∈ ℝ)
134132, 133resubcld 11692 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ)
135134, 57, 17redivcld 12093 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ)
136 absresq 15307 . . . . . . . . . . . . . 14 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
137135, 136syl 17 . . . . . . . . . . . . 13 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
138112, 16, 17sqdivd 14178 . . . . . . . . . . . . 13 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
139137, 138eqtrd 2766 . . . . . . . . . . . 12 (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
140139oveq2d 7440 . . . . . . . . . . 11 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
141112sqcld 14163 . . . . . . . . . . . 12 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) ∈ ℂ)
14216sqcld 14163 . . . . . . . . . . . 12 (𝜑 → (𝐶↑2) ∈ ℂ)
143 sqne0 14142 . . . . . . . . . . . . . 14 (𝐶 ∈ ℂ → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
14416, 143syl 17 . . . . . . . . . . . . 13 (𝜑 → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
14517, 144mpbird 256 . . . . . . . . . . . 12 (𝜑 → (𝐶↑2) ≠ 0)
1467, 141, 142, 145divassd 12076 . . . . . . . . . . 11 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
147112sqvald 14162 . . . . . . . . . . . . 13 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) = (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))
148147oveq2d 7440 . . . . . . . . . . . 12 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) = (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))))
149148oveq1d 7439 . . . . . . . . . . 11 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
150140, 146, 1493eqtr2d 2772 . . . . . . . . . 10 (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
151131, 150oveq12d 7442 . . . . . . . . 9 (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
15214, 14mulcld 11284 . . . . . . . . . 10 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
153112, 112mulcld 11284 . . . . . . . . . . 11 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℂ)
1547, 153mulcld 11284 . . . . . . . . . 10 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) ∈ ℂ)
155152, 154, 142, 145divsubdird 12080 . . . . . . . . 9 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
1565, 13, 5, 13mulsubd 11723 . . . . . . . . . . . 12 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))))
157110, 111, 110, 111mulsubd 11723 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) = ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
158157oveq2d 7440 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
159110, 110mulcld 11284 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) · (𝐵 · 𝐸)) ∈ ℂ)
160111, 111mulcld 11284 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐹) · (𝐴 · 𝐹)) ∈ ℂ)
161159, 160addcld 11283 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
162110, 111mulcld 11284 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 · 𝐸) · (𝐴 · 𝐹)) ∈ ℂ)
163162, 162addcld 11283 . . . . . . . . . . . . . 14 (𝜑 → (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
1647, 161, 163subdid 11720 . . . . . . . . . . . . 13 (𝜑 → (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
1657, 159, 160adddid 11288 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
1667, 162, 162adddid 11288 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
167165, 166oveq12d 7442 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
168158, 164, 1673eqtrd 2770 . . . . . . . . . . . 12 (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
169156, 168oveq12d 7442 . . . . . . . . . . 11 (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
170169oveq1d 7439 . . . . . . . . . 10 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)))
1715, 13mulcomd 11285 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)))
1727, 12, 5mulassd 11287 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)) = (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))))
1732, 4mulcomd 11285 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐴 · 𝐸) = (𝐸 · 𝐴))
174173oveq2d 7440 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐹) · (𝐸 · 𝐴)))
1759, 11, 4, 2mul4d 11476 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹) · (𝐸 · 𝐴)) = ((𝐵 · 𝐸) · (𝐹 · 𝐴)))
17611, 2mulcomd 11285 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝐹 · 𝐴) = (𝐴 · 𝐹))
177176oveq2d 7440 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐸) · (𝐹 · 𝐴)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
178174, 175, 1773eqtrd 2770 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
179178oveq2d 7440 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
180171, 172, 1793eqtrd 2770 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
181180, 180oveq12d 7442 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
182181oveq2d 7440 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
183182oveq1d 7439 . . . . . . . . . . . 12 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
1845, 5mulcld 11284 . . . . . . . . . . . . . 14 (𝜑 → ((𝐴 · 𝐸) · (𝐴 · 𝐸)) ∈ ℂ)
18513, 13mulcld 11284 . . . . . . . . . . . . . 14 (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
186184, 185addcld 11283 . . . . . . . . . . . . 13 (𝜑 → (((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
1877, 159mulcld 11284 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) ∈ ℂ)
1887, 160mulcld 11284 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
189187, 188addcld 11283 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) ∈ ℂ)
1907, 162mulcld 11284 . . . . . . . . . . . . . 14 (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
191190, 190addcld 11283 . . . . . . . . . . . . 13 (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) ∈ ℂ)
192186, 189, 191nnncan2d 11656 . . . . . . . . . . . 12 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
193184, 185, 187, 188addsub4d 11668 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
1945sqvald 14162 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴 · 𝐸) · (𝐴 · 𝐸)))
195110sqvald 14162 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵 · 𝐸) · (𝐵 · 𝐸)))
196195oveq2d 7440 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))))
197194, 196oveq12d 7442 . . . . . . . . . . . . . 14 (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))))
19813sqvald 14162 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))))
199111sqvald 14162 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴 · 𝐹) · (𝐴 · 𝐹)))
200199oveq2d 7440 . . . . . . . . . . . . . . 15 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))
201198, 200oveq12d 7442 . . . . . . . . . . . . . 14 (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
202197, 201oveq12d 7442 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
2032, 4sqmuld 14177 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴↑2) · (𝐸↑2)))
2049, 4sqmuld 14177 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵↑2) · (𝐸↑2)))
205204oveq2d 7440 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
2069sqcld 14163 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐵↑2) ∈ ℂ)
2077, 206, 36mulassd 11287 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐵↑2)) · (𝐸↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
208205, 207eqtr4d 2769 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = ((𝐷 · (𝐵↑2)) · (𝐸↑2)))
209203, 208oveq12d 7442 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
2107sqvald 14162 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷↑2) = (𝐷 · 𝐷))
2119, 11sqmuld 14177 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐵 · 𝐹)↑2) = ((𝐵↑2) · (𝐹↑2)))
212210, 211oveq12d 7442 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷↑2) · ((𝐵 · 𝐹)↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
2137, 12sqmuld 14177 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷↑2) · ((𝐵 · 𝐹)↑2)))
2147, 7mulcld 11284 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · 𝐷) ∈ ℂ)
215214, 206, 37mulassd 11287 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
216212, 213, 2153eqtr4d 2776 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)))
2172, 11sqmuld 14177 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴↑2) · (𝐹↑2)))
218217oveq2d 7440 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
2192sqcld 14163 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐴↑2) ∈ ℂ)
2207, 219, 37mulassd 11287 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐴↑2)) · (𝐹↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
221218, 220eqtr4d 2769 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = ((𝐷 · (𝐴↑2)) · (𝐹↑2)))
222216, 221oveq12d 7442 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
223209, 222oveq12d 7442 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))))
2247, 206mulcld 11284 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · (𝐵↑2)) ∈ ℂ)
225219, 224, 36subdird 11721 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
226 pellex.no1 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)
227226oveq1d 7439 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (𝐶 · (𝐸↑2)))
228225, 227eqtr3d 2768 . . . . . . . . . . . . . . 15 (𝜑 → (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) = (𝐶 · (𝐸↑2)))
2297, 7, 206mulassd 11287 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) = (𝐷 · (𝐷 · (𝐵↑2))))
230229oveq1d 7439 . . . . . . . . . . . . . . . . 17 (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
231230oveq1d 7439 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)))
232214, 206mulcld 11284 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) ∈ ℂ)
2337, 219mulcld 11284 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐷 · (𝐴↑2)) ∈ ℂ)
234232, 233, 37subdird 11721 . . . . . . . . . . . . . . . 16 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
235 subdi 11697 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
236235eqcomd 2732 . . . . . . . . . . . . . . . . . . 19 ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
2377, 224, 219, 236syl3anc 1368 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
238 negsubdi2 11569 . . . . . . . . . . . . . . . . . . . . . 22 (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = ((𝐷 · (𝐵↑2)) − (𝐴↑2)))
239238eqcomd 2732 . . . . . . . . . . . . . . . . . . . . 21 (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
240219, 224, 239syl2anc 582 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
241226negeqd 11504 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = -𝐶)
242240, 241eqtrd 2766 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -𝐶)
243242oveq2d 7440 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = (𝐷 · -𝐶))
2447, 16mulneg2d 11718 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · -𝐶) = -(𝐷 · 𝐶))
245237, 243, 2443eqtrd 2770 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = -(𝐷 · 𝐶))
246245oveq1d 7439 . . . . . . . . . . . . . . . 16 (𝜑 → (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (-(𝐷 · 𝐶) · (𝐹↑2)))
247231, 234, 2463eqtr3d 2774 . . . . . . . . . . . . . . 15 (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))) = (-(𝐷 · 𝐶) · (𝐹↑2)))
248228, 247oveq12d 7442 . . . . . . . . . . . . . 14 (𝜑 → ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))))
2497, 16mulcld 11284 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐷 · 𝐶) ∈ ℂ)
250249, 37mulneg1d 11717 . . . . . . . . . . . . . . . . 17 (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -((𝐷 · 𝐶) · (𝐹↑2)))
2517, 16mulcomd 11285 . . . . . . . . . . . . . . . . . . . 20 (𝜑 → (𝐷 · 𝐶) = (𝐶 · 𝐷))
252251oveq1d 7439 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = ((𝐶 · 𝐷) · (𝐹↑2)))
25316, 7, 37mulassd 11287 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐶 · 𝐷) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
254252, 253eqtrd 2766 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
255254negeqd 11504 . . . . . . . . . . . . . . . . 17 (𝜑 → -((𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
256250, 255eqtrd 2766 . . . . . . . . . . . . . . . 16 (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
257256oveq2d 7440 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))))
25816, 36mulcld 11284 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · (𝐸↑2)) ∈ ℂ)
25916, 38mulcld 11284 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · (𝐷 · (𝐹↑2))) ∈ ℂ)
260258, 259negsubd 11627 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
26161oveq2d 7440 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = (𝐶 · 𝐶))
262 subdi 11697 . . . . . . . . . . . . . . . . . 18 ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
263262eqcomd 2732 . . . . . . . . . . . . . . . . 17 ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
26416, 36, 38, 263syl3anc 1368 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
26516sqvald 14162 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐶↑2) = (𝐶 · 𝐶))
266261, 264, 2653eqtr4d 2776 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶↑2))
267257, 260, 2663eqtrd 2770 . . . . . . . . . . . . . 14 (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = (𝐶↑2))
268223, 248, 2673eqtrd 2770 . . . . . . . . . . . . 13 (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = (𝐶↑2))
269193, 202, 2683eqtr2d 2772 . . . . . . . . . . . 12 (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = (𝐶↑2))
270183, 192, 2693eqtrd 2770 . . . . . . . . . . 11 (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (𝐶↑2))
271270oveq1d 7439 . . . . . . . . . 10 (𝜑 → ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)) = ((𝐶↑2) / (𝐶↑2)))
272142, 145dividd 12039 . . . . . . . . . 10 (𝜑 → ((𝐶↑2) / (𝐶↑2)) = 1)
273170, 271, 2723eqtrd 2770 . . . . . . . . 9 (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = 1)
274151, 155, 2733eqtr2d 2772 . . . . . . . 8 (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
275274adantr 479 . . . . . . 7 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
276 simpr 483 . . . . . . . . . . 11 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
277276fvoveq1d 7446 . . . . . . . . . 10 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = (abs‘(0 / 𝐶)))
27816, 17div0d 12040 . . . . . . . . . . . 12 (𝜑 → (0 / 𝐶) = 0)
279278abs00bd 15296 . . . . . . . . . . 11 (𝜑 → (abs‘(0 / 𝐶)) = 0)
280279adantr 479 . . . . . . . . . 10 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(0 / 𝐶)) = 0)
281277, 280eqtrd 2766 . . . . . . . . 9 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = 0)
282281sq0id 14212 . . . . . . . 8 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = 0)
283282oveq1d 7439 . . . . . . 7 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
284275, 283eqtr3d 2768 . . . . . 6 ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
285125, 284mtand 814 . . . . 5 (𝜑 → ¬ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
286285neqned 2937 . . . 4 (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ≠ 0)
28714, 16, 286, 17divne0d 12057 . . 3 (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0)
288 nnabscl 15330 . . 3 (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ∧ (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
289104, 287, 288syl2anc 582 . 2 (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
290112, 16, 17absdivd 15460 . . . . 5 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) = ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)))
291 negsub 11558 . . . . . . . . . . . 12 (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) + -(𝐴 · 𝐹)) = ((𝐵 · 𝐸) − (𝐴 · 𝐹)))
292291eqcomd 2732 . . . . . . . . . . 11 (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
293110, 111, 292syl2anc 582 . . . . . . . . . 10 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
294293oveq1d 7439 . . . . . . . . 9 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
295133renegcld 11691 . . . . . . . . . 10 (𝜑 → -(𝐴 · 𝐹) ∈ ℝ)
29611, 4mulcomd 11285 . . . . . . . . . . . 12 (𝜑 → (𝐹 · 𝐸) = (𝐸 · 𝐹))
297296oveq1d 7439 . . . . . . . . . . 11 (𝜑 → ((𝐹 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
298 modmul1 13944 . . . . . . . . . . . 12 (((𝐵 ∈ ℝ ∧ 𝐹 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
29926, 27, 32, 31, 78, 298syl221anc 1378 . . . . . . . . . . 11 (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
300 modmul1 13944 . . . . . . . . . . . 12 (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐹 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ+) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
30122, 23, 76, 31, 33, 300syl221anc 1378 . . . . . . . . . . 11 (𝜑 → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
302297, 299, 3013eqtr4d 2776 . . . . . . . . . 10 (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶)))
303 modadd1 13928 . . . . . . . . . 10 ((((𝐵 · 𝐸) ∈ ℝ ∧ (𝐴 · 𝐹) ∈ ℝ) ∧ (-(𝐴 · 𝐹) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) ∧ ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶))) → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
304132, 133, 295, 31, 302, 303syl221anc 1378 . . . . . . . . 9 (𝜑 → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
305111negidd 11611 . . . . . . . . . 10 (𝜑 → ((𝐴 · 𝐹) + -(𝐴 · 𝐹)) = 0)
306305oveq1d 7439 . . . . . . . . 9 (𝜑 → (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
307294, 304, 3063eqtrd 2770 . . . . . . . 8 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
308307, 64eqtrd 2766 . . . . . . 7 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0)
309 absmod0 15308 . . . . . . . 8 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
310134, 31, 309syl2anc 582 . . . . . . 7 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
311308, 310mpbid 231 . . . . . 6 (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0)
312112abscld 15441 . . . . . . 7 (𝜑 → (abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ)
313 mod0 13896 . . . . . . 7 (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ+) → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
314312, 31, 313syl2anc 582 . . . . . 6 (𝜑 → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
315311, 314mpbid 231 . . . . 5 (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ)
316290, 315eqeltrd 2826 . . . 4 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ)
317 absz 15316 . . . . 5 ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
318135, 317syl 17 . . . 4 (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
319316, 318mpbird 256 . . 3 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ)
320 pellex.neq . . . . . . 7 (𝜑 → ¬ (𝐴 = 𝐸𝐵 = 𝐹))
32110nnne0d 12314 . . . . . . . . 9 (𝜑𝐹 ≠ 0)
3223nnne0d 12314 . . . . . . . . 9 (𝜑𝐸 ≠ 0)
3239, 11, 2, 4, 321, 322divmuleqd 12087 . . . . . . . 8 (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) ↔ (𝐵 · 𝐸) = (𝐴 · 𝐹)))
32461adantr 479 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
325324eqcomd 2732 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐸↑2) − (𝐷 · (𝐹↑2))))
326325oveq2d 7440 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
3279, 11, 321divcld 12041 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐹) ∈ ℂ)
328327sqcld 14163 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 𝐹)↑2) ∈ ℂ)
329328adantr 479 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) ∈ ℂ)
33036adantr 479 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ∈ ℂ)
33138adantr 479 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (𝐹↑2)) ∈ ℂ)
332329, 330, 331subdid 11720 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))))
333 oveq1 7431 . . . . . . . . . . . . . . . . 17 ((𝐵 / 𝐹) = (𝐴 / 𝐸) → ((𝐵 / 𝐹)↑2) = ((𝐴 / 𝐸)↑2))
334333oveq1d 7439 . . . . . . . . . . . . . . . 16 ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
335334adantl 480 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
3362adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐴 ∈ ℂ)
3374adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ∈ ℂ)
338322adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ≠ 0)
339336, 337, 338sqdivd 14178 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐴 / 𝐸)↑2) = ((𝐴↑2) / (𝐸↑2)))
340339oveq1d 7439 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴 / 𝐸)↑2) · (𝐸↑2)) = (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)))
341219adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴↑2) ∈ ℂ)
342 sqne0 14142 . . . . . . . . . . . . . . . . . . 19 (𝐸 ∈ ℂ → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
3434, 342syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
344322, 343mpbird 256 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐸↑2) ≠ 0)
345344adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ≠ 0)
346341, 330, 345divcan1d 12042 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)) = (𝐴↑2))
347335, 340, 3463eqtrd 2770 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (𝐴↑2))
3487adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐷 ∈ ℂ)
34937adantr 479 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ∈ ℂ)
350329, 348, 349mul12d 11473 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))))
3519adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐵 ∈ ℂ)
35211adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ∈ ℂ)
353321adantr 479 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ≠ 0)
354351, 352, 353sqdivd 14178 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = ((𝐵↑2) / (𝐹↑2)))
355354oveq1d 7439 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐹↑2)) = (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)))
356355oveq2d 7440 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))) = (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))))
357206adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐵↑2) ∈ ℂ)
358 sqne0 14142 . . . . . . . . . . . . . . . . . . . 20 (𝐹 ∈ ℂ → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
35911, 358syl 17 . . . . . . . . . . . . . . . . . . 19 (𝜑 → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
360321, 359mpbird 256 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝐹↑2) ≠ 0)
361360adantr 479 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ≠ 0)
362357, 349, 361divcan1d 12042 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)) = (𝐵↑2))
363362oveq2d 7440 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
364350, 356, 3633eqtrd 2770 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
365347, 364oveq12d 7442 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
366326, 332, 3653eqtrd 2770 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
367226eqcomd 2732 . . . . . . . . . . . . 13 (𝜑𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
368367adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
369366, 368oveq12d 7442 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))))
37016adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ∈ ℂ)
37117adantr 479 . . . . . . . . . . . 12 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ≠ 0)
372329, 370, 371divcan4d 12047 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = ((𝐵 / 𝐹)↑2))
373226, 226oveq12d 7442 . . . . . . . . . . . . 13 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = (𝐶 / 𝐶))
37416, 17dividd 12039 . . . . . . . . . . . . 13 (𝜑 → (𝐶 / 𝐶) = 1)
375373, 374eqtrd 2766 . . . . . . . . . . . 12 (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
376375adantr 479 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
377369, 372, 3763eqtr3d 2774 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = 1)
37826, 27, 321redivcld 12093 . . . . . . . . . . . . . . . 16 (𝜑 → (𝐵 / 𝐹) ∈ ℝ)
3798nnnn0d 12584 . . . . . . . . . . . . . . . . . 18 (𝜑𝐵 ∈ ℕ0)
380379nn0ge0d 12587 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 ≤ 𝐵)
38110nngt0d 12313 . . . . . . . . . . . . . . . . 17 (𝜑 → 0 < 𝐹)
382 divge0 12135 . . . . . . . . . . . . . . . . 17 (((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ (𝐹 ∈ ℝ ∧ 0 < 𝐹)) → 0 ≤ (𝐵 / 𝐹))
38326, 380, 27, 381, 382syl22anc 837 . . . . . . . . . . . . . . . 16 (𝜑 → 0 ≤ (𝐵 / 𝐹))
384378, 383sqrtsqd 15424 . . . . . . . . . . . . . . 15 (𝜑 → (√‘((𝐵 / 𝐹)↑2)) = (𝐵 / 𝐹))
385384eqcomd 2732 . . . . . . . . . . . . . 14 (𝜑 → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
386385ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
387 fveq2 6901 . . . . . . . . . . . . . 14 (((𝐵 / 𝐹)↑2) = 1 → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
388387adantl 480 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
389 sqrt1 15276 . . . . . . . . . . . . . 14 (√‘1) = 1
390389a1i 11 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘1) = 1)
391386, 388, 3903eqtrd 2770 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = 1)
392391ex 411 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐵 / 𝐹) = 1))
393 simplr 767 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = (𝐴 / 𝐸))
394 simpr 483 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = 1)
395393, 394eqtr3d 2768 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 / 𝐸) = 1)
396395oveq1d 7439 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = (1 · 𝐸))
3972, 4, 322divcan1d 12042 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
398397ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
3994mullidd 11282 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝐸) = 𝐸)
400399ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐸) = 𝐸)
401396, 398, 4003eqtr3d 2774 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐴 = 𝐸)
402394oveq1d 7439 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = (1 · 𝐹))
4039, 11, 321divcan1d 12042 . . . . . . . . . . . . . . 15 (𝜑 → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
404403ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
40511mullidd 11282 . . . . . . . . . . . . . . 15 (𝜑 → (1 · 𝐹) = 𝐹)
406405ad2antrr 724 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐹) = 𝐹)
407402, 404, 4063eqtr3d 2774 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐵 = 𝐹)
408401, 407jca 510 . . . . . . . . . . . 12 (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 = 𝐸𝐵 = 𝐹))
409408ex 411 . . . . . . . . . . 11 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹) = 1 → (𝐴 = 𝐸𝐵 = 𝐹)))
410392, 409syld 47 . . . . . . . . . 10 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐴 = 𝐸𝐵 = 𝐹)))
411377, 410mpd 15 . . . . . . . . 9 ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴 = 𝐸𝐵 = 𝐹))
412411ex 411 . . . . . . . 8 (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (𝐴 = 𝐸𝐵 = 𝐹)))
413323, 412sylbird 259 . . . . . . 7 (𝜑 → ((𝐵 · 𝐸) = (𝐴 · 𝐹) → (𝐴 = 𝐸𝐵 = 𝐹)))
414320, 413mtod 197 . . . . . 6 (𝜑 → ¬ (𝐵 · 𝐸) = (𝐴 · 𝐹))
415414neqned 2937 . . . . 5 (𝜑 → (𝐵 · 𝐸) ≠ (𝐴 · 𝐹))
416110, 111, 415subne0d 11630 . . . 4 (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ≠ 0)
417112, 16, 416, 17divne0d 12057 . . 3 (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0)
418 nnabscl 15330 . . 3 (((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ∧ (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0) → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
419319, 417, 418syl2anc 582 . 2 (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
420 oveq1 7431 . . . . 5 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (𝑎↑2) = ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2))
421420oveq1d 7439 . . . 4 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))))
422421eqeq1d 2728 . . 3 (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1))
423 oveq1 7431 . . . . . 6 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝑏↑2) = ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
424423oveq2d 7440 . . . . 5 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝐷 · (𝑏↑2)) = (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
425424oveq2d 7440 . . . 4 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
426425eqeq1d 2728 . . 3 (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → ((((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1))
427422, 426rspc2ev 3621 . 2 (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ ∧ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ ∧ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
428289, 419, 274, 427syl3anc 1368 1 (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1534  wcel 2099  wne 2930  wrex 3060   class class class wbr 5153  cfv 6554  (class class class)co 7424  cc 11156  cr 11157  0cc0 11158  1c1 11159   + caddc 11161   · cmul 11163   < clt 11298  cle 11299  cmin 11494  -cneg 11495   / cdiv 11921  cn 12264  2c2 12319  cz 12610  cq 12984  +crp 13028   mod cmo 13889  cexp 14081  csqrt 15238  abscabs 15239
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-sep 5304  ax-nul 5311  ax-pow 5369  ax-pr 5433  ax-un 7746  ax-cnex 11214  ax-resscn 11215  ax-1cn 11216  ax-icn 11217  ax-addcl 11218  ax-addrcl 11219  ax-mulcl 11220  ax-mulrcl 11221  ax-mulcom 11222  ax-addass 11223  ax-mulass 11224  ax-distr 11225  ax-i2m1 11226  ax-1ne0 11227  ax-1rid 11228  ax-rnegex 11229  ax-rrecex 11230  ax-cnre 11231  ax-pre-lttri 11232  ax-pre-lttrn 11233  ax-pre-ltadd 11234  ax-pre-mulgt0 11235  ax-pre-sup 11236
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3967  df-nul 4326  df-if 4534  df-pw 4609  df-sn 4634  df-pr 4636  df-op 4640  df-uni 4914  df-iun 5003  df-br 5154  df-opab 5216  df-mpt 5237  df-tr 5271  df-id 5580  df-eprel 5586  df-po 5594  df-so 5595  df-fr 5637  df-we 5639  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-pred 6312  df-ord 6379  df-on 6380  df-lim 6381  df-suc 6382  df-iota 6506  df-fun 6556  df-fn 6557  df-f 6558  df-f1 6559  df-fo 6560  df-f1o 6561  df-fv 6562  df-riota 7380  df-ov 7427  df-oprab 7428  df-mpo 7429  df-om 7877  df-2nd 8004  df-frecs 8296  df-wrecs 8327  df-recs 8401  df-rdg 8440  df-er 8734  df-en 8975  df-dom 8976  df-sdom 8977  df-sup 9485  df-inf 9486  df-pnf 11300  df-mnf 11301  df-xr 11302  df-ltxr 11303  df-le 11304  df-sub 11496  df-neg 11497  df-div 11922  df-nn 12265  df-2 12327  df-3 12328  df-n0 12525  df-z 12611  df-uz 12875  df-rp 13029  df-fl 13812  df-mod 13890  df-seq 14022  df-exp 14082  df-cj 15104  df-re 15105  df-im 15106  df-sqrt 15240  df-abs 15241
This theorem is referenced by:  pellex  42492
  Copyright terms: Public domain W3C validator