pellexlem6 - Mathbox for Stefan O'Rear

	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 43262

Description: Lemma for pellex 43263. 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**
Step	Hyp	Ref	Expression
1		pellex.ann	. . . . . . . . 9 ⊢ (𝜑 → 𝐴 ∈ ℕ)
2	1	nncnd 12190	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		pellex.enn	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ ℕ)
4	3	nncnd 12190	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ℂ)
5	2, 4	mulcld 11165	. . . . . . 7 ⊢ (𝜑 → (𝐴 · 𝐸) ∈ ℂ)
6		pellex.dnn	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℕ)
7	6	nncnd 12190	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℂ)
8		pellex.bnn	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℕ)
9	8	nncnd 12190	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℂ)
10		pellex.fnn	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℕ)
11	10	nncnd 12190	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ℂ)
12	9, 11	mulcld 11165	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℂ)
13	7, 12	mulcld 11165	. . . . . . 7 ⊢ (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℂ)
14	5, 13	subcld 11505	. . . . . 6 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
15		pellex.cz	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℤ)
16	15	zcnd 12634	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ℂ)
17		pellex.cn0	. . . . . 6 ⊢ (𝜑 → 𝐶 ≠ 0)
18	14, 16, 17	absdivd 15420	. . . . 5 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)))
19	5, 13	negsubd 11511	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))))
20	19	eqcomd 2742	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))))
21	20	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
22	1	nnred 12189	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
23	3	nnred 12189	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℝ)
24	22, 23	remulcld 11175	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · 𝐸) ∈ ℝ)
25	6	nnred 12189	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
26	8	nnred 12189	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ)
27	10	nnred 12189	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ ℝ)
28	26, 27	remulcld 11175	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℝ)
29	25, 28	remulcld 11175	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
30	29	renegcld 11577	. . . . . . . . . 10 ⊢ (𝜑 → -(𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
31	16, 17	absrpcld 15413	. . . . . . . . . 10 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ⁺)
32	3	nnzd 12550	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ ℤ)
33		pellex.xcg	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))
34		modmul1 13886	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
35	22, 23, 32, 31, 33, 34	syl221anc 1384	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
36	4	sqcld 14106	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
37	11	sqcld 14106	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
38	7, 37	mulcld 11165	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℂ)
39	36, 38	npcand 11509	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) = (𝐸↑2))
40	4	sqvald 14105	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
41	39, 40	eqtr2d 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 · 𝐸) = (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))))
42	41	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
43	23	resqcld 14087	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸↑2) ∈ ℝ)
44	27	resqcld 14087	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹↑2) ∈ ℝ)
45	25, 44	remulcld 11175	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℝ)
46	43, 45	resubcld 11578	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ)
47		0red 11147	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
48	16	abscld 15401	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ)
49	48	recnd 11173	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘𝐶) ∈ ℂ)
50	16, 17	absne0d 15412	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘𝐶) ≠ 0)
51	49, 50	dividd 11929	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) = 1)
52		1zzd 12558	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℤ)
53	51, 52	eqeltrd 2836	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ)
54		mod0 13835	. . . . . . . . . . . . . . . . 17 ⊢ (((abs‘𝐶) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
55	48, 31, 54	syl2anc 585	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
56	53, 55	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘𝐶) mod (abs‘𝐶)) = 0)
57	15	zred 12633	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ℝ)
58		absmod0 15265	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
59	57, 31, 58	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
60	56, 59	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 mod (abs‘𝐶)) = 0)
61		pellex.no2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
62	61	oveq1d 7382	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (𝐶 mod (abs‘𝐶)))
63		0mod 13861	. . . . . . . . . . . . . . 15 ⊢ ((abs‘𝐶) ∈ ℝ⁺ → (0 mod (abs‘𝐶)) = 0)
64	31, 63	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 mod (abs‘𝐶)) = 0)
65	60, 62, 64	3eqtr4d 2781	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
66		modadd1 13867	. . . . . . . . . . . . 13 ⊢ (((((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ ∧ 0 ∈ ℝ) ∧ ((𝐷 · (𝐹↑2)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶))) → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
67	46, 47, 45, 31, 65, 66	syl221anc 1384	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
68	38	addlidd 11347	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐷 · (𝐹↑2)))
69	11	sqvald 14105	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
70	69	oveq2d 7383	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) = (𝐷 · (𝐹 · 𝐹)))
71	7, 11, 11	mul12d 11355	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹 · 𝐹)) = (𝐹 · (𝐷 · 𝐹)))
72	68, 70, 71	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐹 · (𝐷 · 𝐹)))
73	72	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝜑 → ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
74	42, 67, 73	3eqtrd 2775	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
75	6	nnzd 12550	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ ℤ)
76	10	nnzd 12550	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ ℤ)
77	75, 76	zmulcld 12639	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · 𝐹) ∈ ℤ)
78		pellex.ycg	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))
79	78	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶)))
80		modmul1 13886	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐷 · 𝐹) ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶))) → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
81	27, 26, 77, 31, 79, 80	syl221anc 1384	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
82	9, 7, 11	mul12d 11355	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 · (𝐷 · 𝐹)) = (𝐷 · (𝐵 · 𝐹)))
83	82	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
84	81, 83	eqtrd 2771	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
85	35, 74, 84	3eqtrd 2775	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
86		modadd1 13867	. . . . . . . . . 10 ⊢ ((((𝐴 · 𝐸) ∈ ℝ ∧ (𝐷 · (𝐵 · 𝐹)) ∈ ℝ) ∧ (-(𝐷 · (𝐵 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
87	24, 29, 30, 31, 85, 86	syl221anc 1384	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
88	13	negidd 11495	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) = 0)
89	88	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
90	21, 87, 89	3eqtrd 2775	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
91	90, 64	eqtrd 2771	. . . . . . 7 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0)
92	24, 29	resubcld 11578	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ)
93		absmod0 15265	. . . . . . . 8 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
94	92, 31, 93	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
95	91, 94	mpbid 232	. . . . . 6 ⊢ (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0)
96	14	abscld 15401	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ)
97		mod0 13835	. . . . . . 7 ⊢ (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
98	96, 31, 97	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
99	95, 98	mpbid 232	. . . . 5 ⊢ (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ)
100	18, 99	eqeltrd 2836	. . . 4 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ)
101	92, 57, 17	redivcld 11983	. . . . 5 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ)
102		absz 15273	. . . . 5 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
103	101, 102	syl 17	. . . 4 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
104	100, 103	mpbird 257	. . 3 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ)
105		0lt1 11672	. . . . . . . 8 ⊢ 0 < 1
106		0re 11146	. . . . . . . . 9 ⊢ 0 ∈ ℝ
107		1re 11144	. . . . . . . . 9 ⊢ 1 ∈ ℝ
108	106, 107	ltnlei 11267	. . . . . . . 8 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
109	105, 108	mpbi 230	. . . . . . 7 ⊢ ¬ 1 ≤ 0
110	9, 4	mulcld 11165	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 · 𝐸) ∈ ℂ)
111	2, 11	mulcld 11165	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐹) ∈ ℂ)
112	110, 111	subcld 11505	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℂ)
113	112, 16, 17	divcld 11931	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℂ)
114	113	abscld 15401	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℝ)
115	114	resqcld 14087	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) ∈ ℝ)
116	6	nnnn0d 12498	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ₀)
117	116	nn0ge0d 12501	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝐷)
118	114	sqge0d 14099	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
119	25, 115, 117, 118	mulge0d 11727	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
120	25, 115	remulcld 11175	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) ∈ ℝ)
121	47, 120	suble0d 11741	. . . . . . . . 9 ⊢ (𝜑 → ((0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0 ↔ 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
122	119, 121	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0)
123		breq1 5088	. . . . . . . 8 ⊢ (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → (1 ≤ 0 ↔ (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0))
124	122, 123	syl5ibrcom 247	. . . . . . 7 ⊢ (𝜑 → (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → 1 ≤ 0))
125	109, 124	mtoi 199	. . . . . 6 ⊢ (𝜑 → ¬ 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
126		absresq 15264	. . . . . . . . . . . 12 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
127	101, 126	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
128	14, 16, 17	sqdivd 14121	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)))
129	14	sqvald 14105	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) = (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))))
130	129	oveq1d 7382	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
131	127, 128, 130	3eqtrd 2775	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
132	26, 23	remulcld 11175	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 · 𝐸) ∈ ℝ)
133	22, 27	remulcld 11175	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 𝐹) ∈ ℝ)
134	132, 133	resubcld 11578	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ)
135	134, 57, 17	redivcld 11983	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ)
136		absresq 15264	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
137	135, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
138	112, 16, 17	sqdivd 14121	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
139	137, 138	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
140	139	oveq2d 7383	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
141	112	sqcld 14106	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) ∈ ℂ)
142	16	sqcld 14106	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
143		sqne0 14085	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ ℂ → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
144	16, 143	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
145	17, 144	mpbird 257	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶↑2) ≠ 0)
146	7, 141, 142, 145	divassd 11966	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
147	112	sqvald 14105	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) = (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))
148	147	oveq2d 7383	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) = (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))))
149	148	oveq1d 7382	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
150	140, 146, 149	3eqtr2d 2777	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
151	131, 150	oveq12d 7385	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
152	14, 14	mulcld 11165	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
153	112, 112	mulcld 11165	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℂ)
154	7, 153	mulcld 11165	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) ∈ ℂ)
155	152, 154, 142, 145	divsubdird 11970	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
156	5, 13, 5, 13	mulsubd 11609	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))))
157	110, 111, 110, 111	mulsubd 11609	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) = ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
158	157	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
159	110, 110	mulcld 11165	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐵 · 𝐸)) ∈ ℂ)
160	111, 111	mulcld 11165	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐹) · (𝐴 · 𝐹)) ∈ ℂ)
161	159, 160	addcld 11164	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
162	110, 111	mulcld 11165	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐴 · 𝐹)) ∈ ℂ)
163	162, 162	addcld 11164	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
164	7, 161, 163	subdid 11606	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
165	7, 159, 160	adddid 11169	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
166	7, 162, 162	adddid 11169	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
167	165, 166	oveq12d 7385	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
168	158, 164, 167	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
169	156, 168	oveq12d 7385	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
170	169	oveq1d 7382	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)))
171	5, 13	mulcomd 11166	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)))
172	7, 12, 5	mulassd 11168	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)) = (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))))
173	2, 4	mulcomd 11166	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 · 𝐸) = (𝐸 · 𝐴))
174	173	oveq2d 7383	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐹) · (𝐸 · 𝐴)))
175	9, 11, 4, 2	mul4d 11358	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐸 · 𝐴)) = ((𝐵 · 𝐸) · (𝐹 · 𝐴)))
176	11, 2	mulcomd 11166	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐹 · 𝐴) = (𝐴 · 𝐹))
177	176	oveq2d 7383	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐹 · 𝐴)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
178	174, 175, 177	3eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
179	178	oveq2d 7383	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
180	171, 172, 179	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
181	180, 180	oveq12d 7385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
182	181	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
183	182	oveq1d 7382	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
184	5, 5	mulcld 11165	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐴 · 𝐸)) ∈ ℂ)
185	13, 13	mulcld 11165	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
186	184, 185	addcld 11164	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
187	7, 159	mulcld 11165	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) ∈ ℂ)
188	7, 160	mulcld 11165	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
189	187, 188	addcld 11164	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) ∈ ℂ)
190	7, 162	mulcld 11165	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
191	190, 190	addcld 11164	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) ∈ ℂ)
192	186, 189, 191	nnncan2d 11540	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
193	184, 185, 187, 188	addsub4d 11552	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
194	5	sqvald 14105	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴 · 𝐸) · (𝐴 · 𝐸)))
195	110	sqvald 14105	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵 · 𝐸) · (𝐵 · 𝐸)))
196	195	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))))
197	194, 196	oveq12d 7385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))))
198	13	sqvald 14105	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))))
199	111	sqvald 14105	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴 · 𝐹) · (𝐴 · 𝐹)))
200	199	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))
201	198, 200	oveq12d 7385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
202	197, 201	oveq12d 7385	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
203	2, 4	sqmuld 14120	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴↑2) · (𝐸↑2)))
204	9, 4	sqmuld 14120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵↑2) · (𝐸↑2)))
205	204	oveq2d 7383	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
206	9	sqcld 14106	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
207	7, 206, 36	mulassd 11168	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) · (𝐸↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
208	205, 207	eqtr4d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = ((𝐷 · (𝐵↑2)) · (𝐸↑2)))
209	203, 208	oveq12d 7385	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
210	7	sqvald 14105	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷↑2) = (𝐷 · 𝐷))
211	9, 11	sqmuld 14120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹)↑2) = ((𝐵↑2) · (𝐹↑2)))
212	210, 211	oveq12d 7385	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷↑2) · ((𝐵 · 𝐹)↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
213	7, 12	sqmuld 14120	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷↑2) · ((𝐵 · 𝐹)↑2)))
214	7, 7	mulcld 11165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · 𝐷) ∈ ℂ)
215	214, 206, 37	mulassd 11168	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
216	212, 213, 215	3eqtr4d 2781	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)))
217	2, 11	sqmuld 14120	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴↑2) · (𝐹↑2)))
218	217	oveq2d 7383	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
219	2	sqcld 14106	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
220	7, 219, 37	mulassd 11168	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐴↑2)) · (𝐹↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
221	218, 220	eqtr4d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = ((𝐷 · (𝐴↑2)) · (𝐹↑2)))
222	216, 221	oveq12d 7385	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
223	209, 222	oveq12d 7385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))))
224	7, 206	mulcld 11165	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · (𝐵↑2)) ∈ ℂ)
225	219, 224, 36	subdird 11607	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
226		pellex.no1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)
227	226	oveq1d 7382	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (𝐶 · (𝐸↑2)))
228	225, 227	eqtr3d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) = (𝐶 · (𝐸↑2)))
229	7, 7, 206	mulassd 11168	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) = (𝐷 · (𝐷 · (𝐵↑2))))
230	229	oveq1d 7382	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
231	230	oveq1d 7382	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)))
232	214, 206	mulcld 11165	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) ∈ ℂ)
233	7, 219	mulcld 11165	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · (𝐴↑2)) ∈ ℂ)
234	232, 233, 37	subdird 11607	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
235		subdi 11583	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
236	235	eqcomd 2742	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
237	7, 224, 219, 236	syl3anc 1374	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
238		negsubdi2 11453	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = ((𝐷 · (𝐵↑2)) − (𝐴↑2)))
239	238	eqcomd 2742	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
240	219, 224, 239	syl2anc 585	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
241	226	negeqd 11387	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = -𝐶)
242	240, 241	eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -𝐶)
243	242	oveq2d 7383	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = (𝐷 · -𝐶))
244	7, 16	mulneg2d 11604	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · -𝐶) = -(𝐷 · 𝐶))
245	237, 243, 244	3eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = -(𝐷 · 𝐶))
246	245	oveq1d 7382	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (-(𝐷 · 𝐶) · (𝐹↑2)))
247	231, 234, 246	3eqtr3d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))) = (-(𝐷 · 𝐶) · (𝐹↑2)))
248	228, 247	oveq12d 7385	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))))
249	7, 16	mulcld 11165	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · 𝐶) ∈ ℂ)
250	249, 37	mulneg1d 11603	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -((𝐷 · 𝐶) · (𝐹↑2)))
251	7, 16	mulcomd 11166	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐷 · 𝐶) = (𝐶 · 𝐷))
252	251	oveq1d 7382	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = ((𝐶 · 𝐷) · (𝐹↑2)))
253	16, 7, 37	mulassd 11168	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐶 · 𝐷) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
254	252, 253	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
255	254	negeqd 11387	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -((𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
256	250, 255	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
257	256	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))))
258	16, 36	mulcld 11165	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · (𝐸↑2)) ∈ ℂ)
259	16, 38	mulcld 11165	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · (𝐷 · (𝐹↑2))) ∈ ℂ)
260	258, 259	negsubd 11511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
261	61	oveq2d 7383	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = (𝐶 · 𝐶))
262		subdi 11583	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
263	262	eqcomd 2742	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
264	16, 36, 38, 263	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
265	16	sqvald 14105	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶↑2) = (𝐶 · 𝐶))
266	261, 264, 265	3eqtr4d 2781	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶↑2))
267	257, 260, 266	3eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = (𝐶↑2))
268	223, 248, 267	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = (𝐶↑2))
269	193, 202, 268	3eqtr2d 2777	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = (𝐶↑2))
270	183, 192, 269	3eqtrd 2775	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (𝐶↑2))
271	270	oveq1d 7382	. . . . . . . . . 10 ⊢ (𝜑 → ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)) = ((𝐶↑2) / (𝐶↑2)))
272	142, 145	dividd 11929	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑2) / (𝐶↑2)) = 1)
273	170, 271, 272	3eqtrd 2775	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = 1)
274	151, 155, 273	3eqtr2d 2777	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
275	274	adantr 480	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
276		simpr 484	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
277	276	fvoveq1d 7389	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = (abs‘(0 / 𝐶)))
278	16, 17	div0d 11930	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 / 𝐶) = 0)
279	278	abs00bd 15253	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(0 / 𝐶)) = 0)
280	279	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(0 / 𝐶)) = 0)
281	277, 280	eqtrd 2771	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = 0)
282	281	sq0id 14156	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = 0)
283	282	oveq1d 7382	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
284	275, 283	eqtr3d 2773	. . . . . 6 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
285	125, 284	mtand 816	. . . . 5 ⊢ (𝜑 → ¬ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
286	285	neqned 2939	. . . 4 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ≠ 0)
287	14, 16, 286, 17	divne0d 11947	. . 3 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0)
288		nnabscl 15288	. . 3 ⊢ (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ∧ (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
289	104, 287, 288	syl2anc 585	. 2 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
290	112, 16, 17	absdivd 15420	. . . . 5 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) = ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)))
291		negsub 11442	. . . . . . . . . . . 12 ⊢ (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) + -(𝐴 · 𝐹)) = ((𝐵 · 𝐸) − (𝐴 · 𝐹)))
292	291	eqcomd 2742	. . . . . . . . . . 11 ⊢ (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
293	110, 111, 292	syl2anc 585	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
294	293	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
295	133	renegcld 11577	. . . . . . . . . 10 ⊢ (𝜑 → -(𝐴 · 𝐹) ∈ ℝ)
296	11, 4	mulcomd 11166	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 · 𝐸) = (𝐸 · 𝐹))
297	296	oveq1d 7382	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
298		modmul1 13886	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℝ ∧ 𝐹 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
299	26, 27, 32, 31, 78, 298	syl221anc 1384	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
300		modmul1 13886	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐹 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
301	22, 23, 76, 31, 33, 300	syl221anc 1384	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
302	297, 299, 301	3eqtr4d 2781	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶)))
303		modadd1 13867	. . . . . . . . . 10 ⊢ ((((𝐵 · 𝐸) ∈ ℝ ∧ (𝐴 · 𝐹) ∈ ℝ) ∧ (-(𝐴 · 𝐹) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶))) → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
304	132, 133, 295, 31, 302, 303	syl221anc 1384	. . . . . . . . 9 ⊢ (𝜑 → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
305	111	negidd 11495	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐹) + -(𝐴 · 𝐹)) = 0)
306	305	oveq1d 7382	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
307	294, 304, 306	3eqtrd 2775	. . . . . . . 8 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
308	307, 64	eqtrd 2771	. . . . . . 7 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0)
309		absmod0 15265	. . . . . . . 8 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
310	134, 31, 309	syl2anc 585	. . . . . . 7 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
311	308, 310	mpbid 232	. . . . . 6 ⊢ (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0)
312	112	abscld 15401	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ)
313		mod0 13835	. . . . . . 7 ⊢ (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
314	312, 31, 313	syl2anc 585	. . . . . 6 ⊢ (𝜑 → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
315	311, 314	mpbid 232	. . . . 5 ⊢ (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ)
316	290, 315	eqeltrd 2836	. . . 4 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ)
317		absz 15273	. . . . 5 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
318	135, 317	syl 17	. . . 4 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
319	316, 318	mpbird 257	. . 3 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ)
320		pellex.neq	. . . . . . 7 ⊢ (𝜑 → ¬ (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))
321	10	nnne0d 12227	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ≠ 0)
322	3	nnne0d 12227	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ≠ 0)
323	9, 11, 2, 4, 321, 322	divmuleqd 11977	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) ↔ (𝐵 · 𝐸) = (𝐴 · 𝐹)))
324	61	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
325	324	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐸↑2) − (𝐷 · (𝐹↑2))))
326	325	oveq2d 7383	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
327	9, 11, 321	divcld 11931	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / 𝐹) ∈ ℂ)
328	327	sqcld 14106	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐹)↑2) ∈ ℂ)
329	328	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) ∈ ℂ)
330	36	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ∈ ℂ)
331	38	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (𝐹↑2)) ∈ ℂ)
332	329, 330, 331	subdid 11606	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))))
333		oveq1 7374	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 / 𝐹) = (𝐴 / 𝐸) → ((𝐵 / 𝐹)↑2) = ((𝐴 / 𝐸)↑2))
334	333	oveq1d 7382	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
335	334	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
336	2	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐴 ∈ ℂ)
337	4	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ∈ ℂ)
338	322	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ≠ 0)
339	336, 337, 338	sqdivd 14121	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐴 / 𝐸)↑2) = ((𝐴↑2) / (𝐸↑2)))
340	339	oveq1d 7382	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴 / 𝐸)↑2) · (𝐸↑2)) = (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)))
341	219	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴↑2) ∈ ℂ)
342		sqne0 14085	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐸 ∈ ℂ → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
343	4, 342	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
344	322, 343	mpbird 257	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸↑2) ≠ 0)
345	344	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ≠ 0)
346	341, 330, 345	divcan1d 11932	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)) = (𝐴↑2))
347	335, 340, 346	3eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (𝐴↑2))
348	7	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐷 ∈ ℂ)
349	37	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ∈ ℂ)
350	329, 348, 349	mul12d 11355	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))))
351	9	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐵 ∈ ℂ)
352	11	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ∈ ℂ)
353	321	adantr 480	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ≠ 0)
354	351, 352, 353	sqdivd 14121	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = ((𝐵↑2) / (𝐹↑2)))
355	354	oveq1d 7382	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐹↑2)) = (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)))
356	355	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))) = (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))))
357	206	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐵↑2) ∈ ℂ)
358		sqne0 14085	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 ∈ ℂ → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
359	11, 358	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
360	321, 359	mpbird 257	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹↑2) ≠ 0)
361	360	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ≠ 0)
362	357, 349, 361	divcan1d 11932	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)) = (𝐵↑2))
363	362	oveq2d 7383	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
364	350, 356, 363	3eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
365	347, 364	oveq12d 7385	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
366	326, 332, 365	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
367	226	eqcomd 2742	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
368	367	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
369	366, 368	oveq12d 7385	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))))
370	16	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ∈ ℂ)
371	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ≠ 0)
372	329, 370, 371	divcan4d 11937	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = ((𝐵 / 𝐹)↑2))
373	226, 226	oveq12d 7385	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = (𝐶 / 𝐶))
374	16, 17	dividd 11929	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 / 𝐶) = 1)
375	373, 374	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
376	375	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
377	369, 372, 376	3eqtr3d 2779	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = 1)
378	26, 27, 321	redivcld 11983	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / 𝐹) ∈ ℝ)
379	8	nnnn0d 12498	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℕ₀)
380	379	nn0ge0d 12501	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 𝐵)
381	10	nngt0d 12226	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝐹)
382		divge0 12025	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ (𝐹 ∈ ℝ ∧ 0 < 𝐹)) → 0 ≤ (𝐵 / 𝐹))
383	26, 380, 27, 381, 382	syl22anc 839	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ (𝐵 / 𝐹))
384	378, 383	sqrtsqd 15382	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (√‘((𝐵 / 𝐹)↑2)) = (𝐵 / 𝐹))
385	384	eqcomd 2742	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
386	385	ad2antrr 727	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
387		fveq2 6840	. . . . . . . . . . . . . 14 ⊢ (((𝐵 / 𝐹)↑2) = 1 → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
388	387	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
389		sqrt1 15233	. . . . . . . . . . . . . 14 ⊢ (√‘1) = 1
390	389	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘1) = 1)
391	386, 388, 390	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = 1)
392	391	ex 412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐵 / 𝐹) = 1))
393		simplr 769	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = (𝐴 / 𝐸))
394		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = 1)
395	393, 394	eqtr3d 2773	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 / 𝐸) = 1)
396	395	oveq1d 7382	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = (1 · 𝐸))
397	2, 4, 322	divcan1d 11932	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
398	397	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
399	4	mullidd 11163	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
400	399	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐸) = 𝐸)
401	396, 398, 400	3eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐴 = 𝐸)
402	394	oveq1d 7382	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = (1 · 𝐹))
403	9, 11, 321	divcan1d 11932	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
404	403	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
405	11	mullidd 11163	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · 𝐹) = 𝐹)
406	405	ad2antrr 727	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐹) = 𝐹)
407	402, 404, 406	3eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐵 = 𝐹)
408	401, 407	jca 511	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))
409	408	ex 412	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹) = 1 → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
410	392, 409	syld 47	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
411	377, 410	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))
412	411	ex 412	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
413	323, 412	sylbird 260	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · 𝐸) = (𝐴 · 𝐹) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
414	320, 413	mtod 198	. . . . . 6 ⊢ (𝜑 → ¬ (𝐵 · 𝐸) = (𝐴 · 𝐹))
415	414	neqned 2939	. . . . 5 ⊢ (𝜑 → (𝐵 · 𝐸) ≠ (𝐴 · 𝐹))
416	110, 111, 415	subne0d 11514	. . . 4 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ≠ 0)
417	112, 16, 416, 17	divne0d 11947	. . 3 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0)
418		nnabscl 15288	. . 3 ⊢ (((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ∧ (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0) → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
419	319, 417, 418	syl2anc 585	. 2 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
420		oveq1 7374	. . . . 5 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (𝑎↑2) = ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2))
421	420	oveq1d 7382	. . . 4 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))))
422	421	eqeq1d 2738	. . 3 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1))
423		oveq1 7374	. . . . . 6 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝑏↑2) = ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
424	423	oveq2d 7383	. . . . 5 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝐷 · (𝑏↑2)) = (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
425	424	oveq2d 7383	. . . 4 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
426	425	eqeq1d 2738	. . 3 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → ((((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1))
427	422, 426	rspc2ev 3577	. 2 ⊢ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ ∧ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ ∧ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
428	289, 419, 274, 427	syl3anc 1374	1 ⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1542 ∈ wcel 2114 ≠ wne 2932 ∃wrex 3061 class class class wbr 5085 ‘cfv 6498 (class class class)co 7367 ℂcc 11036 ℝcr 11037 0cc0 11038 1c1 11039 + caddc 11041 · cmul 11043 < clt 11179 ≤ cle 11180 − cmin 11377 -cneg 11378 / cdiv 11807 ℕcn 12174 2c2 12236 ℤcz 12524 ℚcq 12898 ℝ⁺crp 12942 mod cmo 13828 ↑cexp 14023 √csqrt 15195 abscabs 15196

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2708 ax-sep 5231 ax-nul 5241 ax-pow 5307 ax-pr 5375 ax-un 7689 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-pre-sup 11116

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3062 df-rmo 3342 df-reu 3343 df-rab 3390 df-v 3431 df-sbc 3729 df-csb 3838 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3909 df-nul 4274 df-if 4467 df-pw 4543 df-sn 4568 df-pr 4570 df-op 4574 df-uni 4851 df-iun 4935 df-br 5086 df-opab 5148 df-mpt 5167 df-tr 5193 df-id 5526 df-eprel 5531 df-po 5539 df-so 5540 df-fr 5584 df-we 5586 df-xp 5637 df-rel 5638 df-cnv 5639 df-co 5640 df-dm 5641 df-rn 5642 df-res 5643 df-ima 5644 df-pred 6265 df-ord 6326 df-on 6327 df-lim 6328 df-suc 6329 df-iota 6454 df-fun 6500 df-fn 6501 df-f 6502 df-f1 6503 df-fo 6504 df-f1o 6505 df-fv 6506 df-riota 7324 df-ov 7370 df-oprab 7371 df-mpo 7372 df-om 7818 df-2nd 7943 df-frecs 8231 df-wrecs 8262 df-recs 8311 df-rdg 8349 df-er 8643 df-en 8894 df-dom 8895 df-sdom 8896 df-sup 9355 df-inf 9356 df-pnf 11181 df-mnf 11182 df-xr 11183 df-ltxr 11184 df-le 11185 df-sub 11379 df-neg 11380 df-div 11808 df-nn 12175 df-2 12244 df-3 12245 df-n0 12438 df-z 12525 df-uz 12789 df-rp 12943 df-fl 13751 df-mod 13829 df-seq 13964 df-exp 14024 df-cj 15061 df-re 15062 df-im 15063 df-sqrt 15197 df-abs 15198

This theorem is referenced by: pellex 43263

W3C validator