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 41875

Description: Lemma for pellex 41876. 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 12233	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		pellex.enn	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ ℕ)
4	3	nncnd 12233	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ℂ)
5	2, 4	mulcld 11239	. . . . . . 7 ⊢ (𝜑 → (𝐴 · 𝐸) ∈ ℂ)
6		pellex.dnn	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℕ)
7	6	nncnd 12233	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℂ)
8		pellex.bnn	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℕ)
9	8	nncnd 12233	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℂ)
10		pellex.fnn	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℕ)
11	10	nncnd 12233	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ℂ)
12	9, 11	mulcld 11239	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℂ)
13	7, 12	mulcld 11239	. . . . . . 7 ⊢ (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℂ)
14	5, 13	subcld 11576	. . . . . 6 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
15		pellex.cz	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℤ)
16	15	zcnd 12672	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ℂ)
17		pellex.cn0	. . . . . 6 ⊢ (𝜑 → 𝐶 ≠ 0)
18	14, 16, 17	absdivd 15407	. . . . 5 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)))
19	5, 13	negsubd 11582	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))))
20	19	eqcomd 2737	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))))
21	20	oveq1d 7427	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
22	1	nnred 12232	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
23	3	nnred 12232	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℝ)
24	22, 23	remulcld 11249	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · 𝐸) ∈ ℝ)
25	6	nnred 12232	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
26	8	nnred 12232	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ)
27	10	nnred 12232	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ ℝ)
28	26, 27	remulcld 11249	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℝ)
29	25, 28	remulcld 11249	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
30	29	renegcld 11646	. . . . . . . . . 10 ⊢ (𝜑 → -(𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
31	16, 17	absrpcld 15400	. . . . . . . . . 10 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ⁺)
32	3	nnzd 12590	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ ℤ)
33		pellex.xcg	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))
34		modmul1 13894	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
35	22, 23, 32, 31, 33, 34	syl221anc 1380	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
36	4	sqcld 14114	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
37	11	sqcld 14114	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
38	7, 37	mulcld 11239	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℂ)
39	36, 38	npcand 11580	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) = (𝐸↑2))
40	4	sqvald 14113	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
41	39, 40	eqtr2d 2772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 · 𝐸) = (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))))
42	41	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
43	23	resqcld 14095	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸↑2) ∈ ℝ)
44	27	resqcld 14095	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹↑2) ∈ ℝ)
45	25, 44	remulcld 11249	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℝ)
46	43, 45	resubcld 11647	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ)
47		0red 11222	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
48	16	abscld 15388	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ)
49	48	recnd 11247	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘𝐶) ∈ ℂ)
50	16, 17	absne0d 15399	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘𝐶) ≠ 0)
51	49, 50	dividd 11993	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) = 1)
52		1zzd 12598	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℤ)
53	51, 52	eqeltrd 2832	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ)
54		mod0 13846	. . . . . . . . . . . . . . . . 17 ⊢ (((abs‘𝐶) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
55	48, 31, 54	syl2anc 583	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
56	53, 55	mpbird 257	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘𝐶) mod (abs‘𝐶)) = 0)
57	15	zred 12671	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ℝ)
58		absmod0 15255	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
59	57, 31, 58	syl2anc 583	. . . . . . . . . . . . . . 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 7427	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (𝐶 mod (abs‘𝐶)))
63		0mod 13872	. . . . . . . . . . . . . . 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 13878	. . . . . . . . . . . . 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 1380	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
68	38	addlidd 11420	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐷 · (𝐹↑2)))
69	11	sqvald 14113	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
70	69	oveq2d 7428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) = (𝐷 · (𝐹 · 𝐹)))
71	7, 11, 11	mul12d 11428	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹 · 𝐹)) = (𝐹 · (𝐷 · 𝐹)))
72	68, 70, 71	3eqtrd 2775	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐹 · (𝐷 · 𝐹)))
73	72	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
74	42, 67, 73	3eqtrd 2775	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
75	6	nnzd 12590	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ ℤ)
76	10	nnzd 12590	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ ℤ)
77	75, 76	zmulcld 12677	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · 𝐹) ∈ ℤ)
78		pellex.ycg	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))
79	78	eqcomd 2737	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶)))
80		modmul1 13894	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐷 · 𝐹) ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶))) → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
81	27, 26, 77, 31, 79, 80	syl221anc 1380	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
82	9, 7, 11	mul12d 11428	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 · (𝐷 · 𝐹)) = (𝐷 · (𝐵 · 𝐹)))
83	82	oveq1d 7427	. . . . . . . . . . . 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 13878	. . . . . . . . . 10 ⊢ ((((𝐴 · 𝐸) ∈ ℝ ∧ (𝐷 · (𝐵 · 𝐹)) ∈ ℝ) ∧ (-(𝐷 · (𝐵 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
87	24, 29, 30, 31, 85, 86	syl221anc 1380	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
88	13	negidd 11566	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) = 0)
89	88	oveq1d 7427	. . . . . . . . 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 11647	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ)
93		absmod0 15255	. . . . . . . 8 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
94	92, 31, 93	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
95	91, 94	mpbid 231	. . . . . 6 ⊢ (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0)
96	14	abscld 15388	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ)
97		mod0 13846	. . . . . . 7 ⊢ (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
98	96, 31, 97	syl2anc 583	. . . . . 6 ⊢ (𝜑 → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
99	95, 98	mpbid 231	. . . . 5 ⊢ (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ)
100	18, 99	eqeltrd 2832	. . . 4 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ)
101	92, 57, 17	redivcld 12047	. . . . 5 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ)
102		absz 15263	. . . . 5 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
103	101, 102	syl 17	. . . 4 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
104	100, 103	mpbird 257	. . 3 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ)
105		0lt1 11741	. . . . . . . 8 ⊢ 0 < 1
106		0re 11221	. . . . . . . . 9 ⊢ 0 ∈ ℝ
107		1re 11219	. . . . . . . . 9 ⊢ 1 ∈ ℝ
108	106, 107	ltnlei 11340	. . . . . . . 8 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
109	105, 108	mpbi 229	. . . . . . 7 ⊢ ¬ 1 ≤ 0
110	9, 4	mulcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 · 𝐸) ∈ ℂ)
111	2, 11	mulcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐹) ∈ ℂ)
112	110, 111	subcld 11576	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℂ)
113	112, 16, 17	divcld 11995	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℂ)
114	113	abscld 15388	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℝ)
115	114	resqcld 14095	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) ∈ ℝ)
116	6	nnnn0d 12537	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ₀)
117	116	nn0ge0d 12540	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝐷)
118	114	sqge0d 14107	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
119	25, 115, 117, 118	mulge0d 11796	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
120	25, 115	remulcld 11249	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) ∈ ℝ)
121	47, 120	suble0d 11810	. . . . . . . . 9 ⊢ (𝜑 → ((0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0 ↔ 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
122	119, 121	mpbird 257	. . . . . . . 8 ⊢ (𝜑 → (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0)
123		breq1 5151	. . . . . . . 8 ⊢ (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → (1 ≤ 0 ↔ (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0))
124	122, 123	syl5ibrcom 246	. . . . . . 7 ⊢ (𝜑 → (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → 1 ≤ 0))
125	109, 124	mtoi 198	. . . . . 6 ⊢ (𝜑 → ¬ 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
126		absresq 15254	. . . . . . . . . . . 12 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
127	101, 126	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
128	14, 16, 17	sqdivd 14129	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)))
129	14	sqvald 14113	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) = (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))))
130	129	oveq1d 7427	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
131	127, 128, 130	3eqtrd 2775	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
132	26, 23	remulcld 11249	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 · 𝐸) ∈ ℝ)
133	22, 27	remulcld 11249	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 𝐹) ∈ ℝ)
134	132, 133	resubcld 11647	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ)
135	134, 57, 17	redivcld 12047	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ)
136		absresq 15254	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
137	135, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
138	112, 16, 17	sqdivd 14129	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
139	137, 138	eqtrd 2771	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
140	139	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
141	112	sqcld 14114	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) ∈ ℂ)
142	16	sqcld 14114	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
143		sqne0 14093	. . . . . . . . . . . . . 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 12030	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
147	112	sqvald 14113	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) = (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))
148	147	oveq2d 7428	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) = (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))))
149	148	oveq1d 7427	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
150	140, 146, 149	3eqtr2d 2777	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
151	131, 150	oveq12d 7430	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
152	14, 14	mulcld 11239	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
153	112, 112	mulcld 11239	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℂ)
154	7, 153	mulcld 11239	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) ∈ ℂ)
155	152, 154, 142, 145	divsubdird 12034	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
156	5, 13, 5, 13	mulsubd 11678	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))))
157	110, 111, 110, 111	mulsubd 11678	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) = ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
158	157	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
159	110, 110	mulcld 11239	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐵 · 𝐸)) ∈ ℂ)
160	111, 111	mulcld 11239	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐹) · (𝐴 · 𝐹)) ∈ ℂ)
161	159, 160	addcld 11238	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
162	110, 111	mulcld 11239	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐴 · 𝐹)) ∈ ℂ)
163	162, 162	addcld 11238	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
164	7, 161, 163	subdid 11675	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
165	7, 159, 160	adddid 11243	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
166	7, 162, 162	adddid 11243	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
167	165, 166	oveq12d 7430	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
168	158, 164, 167	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
169	156, 168	oveq12d 7430	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
170	169	oveq1d 7427	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)))
171	5, 13	mulcomd 11240	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)))
172	7, 12, 5	mulassd 11242	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)) = (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))))
173	2, 4	mulcomd 11240	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 · 𝐸) = (𝐸 · 𝐴))
174	173	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐹) · (𝐸 · 𝐴)))
175	9, 11, 4, 2	mul4d 11431	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐸 · 𝐴)) = ((𝐵 · 𝐸) · (𝐹 · 𝐴)))
176	11, 2	mulcomd 11240	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐹 · 𝐴) = (𝐴 · 𝐹))
177	176	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐹 · 𝐴)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
178	174, 175, 177	3eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
179	178	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
180	171, 172, 179	3eqtrd 2775	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
181	180, 180	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
182	181	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
183	182	oveq1d 7427	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
184	5, 5	mulcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐴 · 𝐸)) ∈ ℂ)
185	13, 13	mulcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
186	184, 185	addcld 11238	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
187	7, 159	mulcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) ∈ ℂ)
188	7, 160	mulcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
189	187, 188	addcld 11238	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) ∈ ℂ)
190	7, 162	mulcld 11239	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
191	190, 190	addcld 11238	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) ∈ ℂ)
192	186, 189, 191	nnncan2d 11611	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
193	184, 185, 187, 188	addsub4d 11623	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
194	5	sqvald 14113	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴 · 𝐸) · (𝐴 · 𝐸)))
195	110	sqvald 14113	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵 · 𝐸) · (𝐵 · 𝐸)))
196	195	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))))
197	194, 196	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))))
198	13	sqvald 14113	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))))
199	111	sqvald 14113	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴 · 𝐹) · (𝐴 · 𝐹)))
200	199	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))
201	198, 200	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
202	197, 201	oveq12d 7430	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
203	2, 4	sqmuld 14128	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴↑2) · (𝐸↑2)))
204	9, 4	sqmuld 14128	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵↑2) · (𝐸↑2)))
205	204	oveq2d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
206	9	sqcld 14114	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
207	7, 206, 36	mulassd 11242	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) · (𝐸↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
208	205, 207	eqtr4d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = ((𝐷 · (𝐵↑2)) · (𝐸↑2)))
209	203, 208	oveq12d 7430	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
210	7	sqvald 14113	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷↑2) = (𝐷 · 𝐷))
211	9, 11	sqmuld 14128	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹)↑2) = ((𝐵↑2) · (𝐹↑2)))
212	210, 211	oveq12d 7430	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷↑2) · ((𝐵 · 𝐹)↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
213	7, 12	sqmuld 14128	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷↑2) · ((𝐵 · 𝐹)↑2)))
214	7, 7	mulcld 11239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · 𝐷) ∈ ℂ)
215	214, 206, 37	mulassd 11242	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
216	212, 213, 215	3eqtr4d 2781	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)))
217	2, 11	sqmuld 14128	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴↑2) · (𝐹↑2)))
218	217	oveq2d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
219	2	sqcld 14114	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
220	7, 219, 37	mulassd 11242	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐴↑2)) · (𝐹↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
221	218, 220	eqtr4d 2774	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = ((𝐷 · (𝐴↑2)) · (𝐹↑2)))
222	216, 221	oveq12d 7430	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
223	209, 222	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))))
224	7, 206	mulcld 11239	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · (𝐵↑2)) ∈ ℂ)
225	219, 224, 36	subdird 11676	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
226		pellex.no1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)
227	226	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (𝐶 · (𝐸↑2)))
228	225, 227	eqtr3d 2773	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) = (𝐶 · (𝐸↑2)))
229	7, 7, 206	mulassd 11242	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) = (𝐷 · (𝐷 · (𝐵↑2))))
230	229	oveq1d 7427	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
231	230	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)))
232	214, 206	mulcld 11239	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) ∈ ℂ)
233	7, 219	mulcld 11239	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · (𝐴↑2)) ∈ ℂ)
234	232, 233, 37	subdird 11676	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
235		subdi 11652	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
236	235	eqcomd 2737	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
237	7, 224, 219, 236	syl3anc 1370	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
238		negsubdi2 11524	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = ((𝐷 · (𝐵↑2)) − (𝐴↑2)))
239	238	eqcomd 2737	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
240	219, 224, 239	syl2anc 583	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
241	226	negeqd 11459	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = -𝐶)
242	240, 241	eqtrd 2771	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -𝐶)
243	242	oveq2d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = (𝐷 · -𝐶))
244	7, 16	mulneg2d 11673	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · -𝐶) = -(𝐷 · 𝐶))
245	237, 243, 244	3eqtrd 2775	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = -(𝐷 · 𝐶))
246	245	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (-(𝐷 · 𝐶) · (𝐹↑2)))
247	231, 234, 246	3eqtr3d 2779	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))) = (-(𝐷 · 𝐶) · (𝐹↑2)))
248	228, 247	oveq12d 7430	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))))
249	7, 16	mulcld 11239	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · 𝐶) ∈ ℂ)
250	249, 37	mulneg1d 11672	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -((𝐷 · 𝐶) · (𝐹↑2)))
251	7, 16	mulcomd 11240	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐷 · 𝐶) = (𝐶 · 𝐷))
252	251	oveq1d 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = ((𝐶 · 𝐷) · (𝐹↑2)))
253	16, 7, 37	mulassd 11242	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐶 · 𝐷) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
254	252, 253	eqtrd 2771	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
255	254	negeqd 11459	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -((𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
256	250, 255	eqtrd 2771	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
257	256	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))))
258	16, 36	mulcld 11239	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · (𝐸↑2)) ∈ ℂ)
259	16, 38	mulcld 11239	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · (𝐷 · (𝐹↑2))) ∈ ℂ)
260	258, 259	negsubd 11582	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
261	61	oveq2d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = (𝐶 · 𝐶))
262		subdi 11652	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
263	262	eqcomd 2737	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
264	16, 36, 38, 263	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
265	16	sqvald 14113	. . . . . . . . . . . . . . . 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 7427	. . . . . . . . . 10 ⊢ (𝜑 → ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)) = ((𝐶↑2) / (𝐶↑2)))
272	142, 145	dividd 11993	. . . . . . . . . 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 7434	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = (abs‘(0 / 𝐶)))
278	16, 17	div0d 11994	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 / 𝐶) = 0)
279	278	abs00bd 15243	. . . . . . . . . . 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 14163	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = 0)
283	282	oveq1d 7427	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
284	275, 283	eqtr3d 2773	. . . . . 6 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
285	125, 284	mtand 813	. . . . 5 ⊢ (𝜑 → ¬ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
286	285	neqned 2946	. . . 4 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ≠ 0)
287	14, 16, 286, 17	divne0d 12011	. . 3 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0)
288		nnabscl 15277	. . 3 ⊢ (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ∧ (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
289	104, 287, 288	syl2anc 583	. 2 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
290	112, 16, 17	absdivd 15407	. . . . 5 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) = ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)))
291		negsub 11513	. . . . . . . . . . . 12 ⊢ (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) + -(𝐴 · 𝐹)) = ((𝐵 · 𝐸) − (𝐴 · 𝐹)))
292	291	eqcomd 2737	. . . . . . . . . . 11 ⊢ (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
293	110, 111, 292	syl2anc 583	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
294	293	oveq1d 7427	. . . . . . . . 9 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
295	133	renegcld 11646	. . . . . . . . . 10 ⊢ (𝜑 → -(𝐴 · 𝐹) ∈ ℝ)
296	11, 4	mulcomd 11240	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 · 𝐸) = (𝐸 · 𝐹))
297	296	oveq1d 7427	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
298		modmul1 13894	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℝ ∧ 𝐹 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
299	26, 27, 32, 31, 78, 298	syl221anc 1380	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
300		modmul1 13894	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐹 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
301	22, 23, 76, 31, 33, 300	syl221anc 1380	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
302	297, 299, 301	3eqtr4d 2781	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶)))
303		modadd1 13878	. . . . . . . . . 10 ⊢ ((((𝐵 · 𝐸) ∈ ℝ ∧ (𝐴 · 𝐹) ∈ ℝ) ∧ (-(𝐴 · 𝐹) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶))) → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
304	132, 133, 295, 31, 302, 303	syl221anc 1380	. . . . . . . . 9 ⊢ (𝜑 → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
305	111	negidd 11566	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐹) + -(𝐴 · 𝐹)) = 0)
306	305	oveq1d 7427	. . . . . . . . 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 15255	. . . . . . . 8 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
310	134, 31, 309	syl2anc 583	. . . . . . 7 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
311	308, 310	mpbid 231	. . . . . 6 ⊢ (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0)
312	112	abscld 15388	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ)
313		mod0 13846	. . . . . . 7 ⊢ (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
314	312, 31, 313	syl2anc 583	. . . . . 6 ⊢ (𝜑 → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
315	311, 314	mpbid 231	. . . . 5 ⊢ (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ)
316	290, 315	eqeltrd 2832	. . . 4 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ)
317		absz 15263	. . . . 5 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
318	135, 317	syl 17	. . . 4 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
319	316, 318	mpbird 257	. . 3 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ)
320		pellex.neq	. . . . . . 7 ⊢ (𝜑 → ¬ (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))
321	10	nnne0d 12267	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ≠ 0)
322	3	nnne0d 12267	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ≠ 0)
323	9, 11, 2, 4, 321, 322	divmuleqd 12041	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) ↔ (𝐵 · 𝐸) = (𝐴 · 𝐹)))
324	61	adantr 480	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
325	324	eqcomd 2737	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐸↑2) − (𝐷 · (𝐹↑2))))
326	325	oveq2d 7428	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
327	9, 11, 321	divcld 11995	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / 𝐹) ∈ ℂ)
328	327	sqcld 14114	. . . . . . . . . . . . . . 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 11675	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))))
333		oveq1 7419	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 / 𝐹) = (𝐴 / 𝐸) → ((𝐵 / 𝐹)↑2) = ((𝐴 / 𝐸)↑2))
334	333	oveq1d 7427	. . . . . . . . . . . . . . . 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 14129	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐴 / 𝐸)↑2) = ((𝐴↑2) / (𝐸↑2)))
340	339	oveq1d 7427	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴 / 𝐸)↑2) · (𝐸↑2)) = (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)))
341	219	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴↑2) ∈ ℂ)
342		sqne0 14093	. . . . . . . . . . . . . . . . . . 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 11996	. . . . . . . . . . . . . . 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 11428	. . . . . . . . . . . . . . 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 14129	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = ((𝐵↑2) / (𝐹↑2)))
355	354	oveq1d 7427	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐹↑2)) = (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)))
356	355	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))) = (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))))
357	206	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐵↑2) ∈ ℂ)
358		sqne0 14093	. . . . . . . . . . . . . . . . . . . 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 11996	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)) = (𝐵↑2))
363	362	oveq2d 7428	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
364	350, 356, 363	3eqtrd 2775	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
365	347, 364	oveq12d 7430	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
366	326, 332, 365	3eqtrd 2775	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
367	226	eqcomd 2737	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
368	367	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
369	366, 368	oveq12d 7430	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))))
370	16	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ∈ ℂ)
371	17	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ≠ 0)
372	329, 370, 371	divcan4d 12001	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = ((𝐵 / 𝐹)↑2))
373	226, 226	oveq12d 7430	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = (𝐶 / 𝐶))
374	16, 17	dividd 11993	. . . . . . . . . . . . 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 12047	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / 𝐹) ∈ ℝ)
379	8	nnnn0d 12537	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℕ₀)
380	379	nn0ge0d 12540	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 𝐵)
381	10	nngt0d 12266	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝐹)
382		divge0 12088	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ (𝐹 ∈ ℝ ∧ 0 < 𝐹)) → 0 ≤ (𝐵 / 𝐹))
383	26, 380, 27, 381, 382	syl22anc 836	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ (𝐵 / 𝐹))
384	378, 383	sqrtsqd 15371	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (√‘((𝐵 / 𝐹)↑2)) = (𝐵 / 𝐹))
385	384	eqcomd 2737	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
386	385	ad2antrr 723	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
387		fveq2 6891	. . . . . . . . . . . . . 14 ⊢ (((𝐵 / 𝐹)↑2) = 1 → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
388	387	adantl 481	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
389		sqrt1 15223	. . . . . . . . . . . . . 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 766	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = (𝐴 / 𝐸))
394		simpr 484	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = 1)
395	393, 394	eqtr3d 2773	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 / 𝐸) = 1)
396	395	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = (1 · 𝐸))
397	2, 4, 322	divcan1d 11996	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
398	397	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
399	4	mullidd 11237	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
400	399	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐸) = 𝐸)
401	396, 398, 400	3eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐴 = 𝐸)
402	394	oveq1d 7427	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = (1 · 𝐹))
403	9, 11, 321	divcan1d 11996	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
404	403	ad2antrr 723	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
405	11	mullidd 11237	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · 𝐹) = 𝐹)
406	405	ad2antrr 723	. . . . . . . . . . . . . 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 197	. . . . . 6 ⊢ (𝜑 → ¬ (𝐵 · 𝐸) = (𝐴 · 𝐹))
415	414	neqned 2946	. . . . 5 ⊢ (𝜑 → (𝐵 · 𝐸) ≠ (𝐴 · 𝐹))
416	110, 111, 415	subne0d 11585	. . . 4 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ≠ 0)
417	112, 16, 416, 17	divne0d 12011	. . 3 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0)
418		nnabscl 15277	. . 3 ⊢ (((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ∧ (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0) → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
419	319, 417, 418	syl2anc 583	. 2 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
420		oveq1 7419	. . . . 5 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (𝑎↑2) = ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2))
421	420	oveq1d 7427	. . . 4 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))))
422	421	eqeq1d 2733	. . 3 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1))
423		oveq1 7419	. . . . . 6 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝑏↑2) = ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
424	423	oveq2d 7428	. . . . 5 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝐷 · (𝑏↑2)) = (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
425	424	oveq2d 7428	. . . 4 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
426	425	eqeq1d 2733	. . 3 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → ((((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1))
427	422, 426	rspc2ev 3624	. 2 ⊢ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ ∧ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ ∧ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
428	289, 419, 274, 427	syl3anc 1370	1 ⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2105 ≠ wne 2939 ∃wrex 3069 class class class wbr 5148 ‘cfv 6543 (class class class)co 7412 ℂcc 11112 ℝcr 11113 0cc0 11114 1c1 11115 + caddc 11117 · cmul 11119 < clt 11253 ≤ cle 11254 − cmin 11449 -cneg 11450 / cdiv 11876 ℕcn 12217 2c2 12272 ℤcz 12563 ℚcq 12937 ℝ⁺crp 12979 mod cmo 13839 ↑cexp 14032 √csqrt 15185 abscabs 15186

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 ax-cnex 11170 ax-resscn 11171 ax-1cn 11172 ax-icn 11173 ax-addcl 11174 ax-addrcl 11175 ax-mulcl 11176 ax-mulrcl 11177 ax-mulcom 11178 ax-addass 11179 ax-mulass 11180 ax-distr 11181 ax-i2m1 11182 ax-1ne0 11183 ax-1rid 11184 ax-rnegex 11185 ax-rrecex 11186 ax-cnre 11187 ax-pre-lttri 11188 ax-pre-lttrn 11189 ax-pre-ltadd 11190 ax-pre-mulgt0 11191 ax-pre-sup 11192

This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-nel 3046 df-ral 3061 df-rex 3070 df-rmo 3375 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6300 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-riota 7368 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7860 df-2nd 7980 df-frecs 8270 df-wrecs 8301 df-recs 8375 df-rdg 8414 df-er 8707 df-en 8944 df-dom 8945 df-sdom 8946 df-sup 9441 df-inf 9442 df-pnf 11255 df-mnf 11256 df-xr 11257 df-ltxr 11258 df-le 11259 df-sub 11451 df-neg 11452 df-div 11877 df-nn 12218 df-2 12280 df-3 12281 df-n0 12478 df-z 12564 df-uz 12828 df-rp 12980 df-fl 13762 df-mod 13840 df-seq 13972 df-exp 14033 df-cj 15051 df-re 15052 df-im 15053 df-sqrt 15187 df-abs 15188

This theorem is referenced by: pellex 41876

W3C validator