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 43841

Description: Lemma for pellex 43842. 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 12351	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		pellex.enn	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ ℕ)
4	3	nncnd 12351	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ℂ)
5	2, 4	mulcld 11329	. . . . . . 7 ⊢ (𝜑 → (𝐴 · 𝐸) ∈ ℂ)
6		pellex.dnn	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℕ)
7	6	nncnd 12351	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℂ)
8		pellex.bnn	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℕ)
9	8	nncnd 12351	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℂ)
10		pellex.fnn	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℕ)
11	10	nncnd 12351	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ℂ)
12	9, 11	mulcld 11329	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℂ)
13	7, 12	mulcld 11329	. . . . . . 7 ⊢ (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℂ)
14	5, 13	subcld 11669	. . . . . 6 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
15		pellex.cz	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℤ)
16	15	zcnd 12804	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ℂ)
17		pellex.cn0	. . . . . 6 ⊢ (𝜑 → 𝐶 ≠ 0)
18	14, 16, 17	absdivd 15625	. . . . 5 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)))
19	5, 13	negsubd 11675	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))))
20	19	eqcomd 2766	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))))
21	20	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
22	1	nnred 12350	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
23	3	nnred 12350	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℝ)
24	22, 23	remulcld 11339	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · 𝐸) ∈ ℝ)
25	6	nnred 12350	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
26	8	nnred 12350	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ)
27	10	nnred 12350	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ ℝ)
28	26, 27	remulcld 11339	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℝ)
29	25, 28	remulcld 11339	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
30	29	renegcld 11743	. . . . . . . . . 10 ⊢ (𝜑 → -(𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
31	16, 17	absrpcld 15618	. . . . . . . . . 10 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ⁺)
32	3	nnzd 12719	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ ℤ)
33		pellex.xcg	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))
34		modmul1 14067	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
35	22, 23, 32, 31, 33, 34	syl221anc 1408	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
36	4	sqcld 14287	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
37	11	sqcld 14287	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
38	7, 37	mulcld 11329	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℂ)
39	36, 38	npcand 11673	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) = (𝐸↑2))
40	4	sqvald 14286	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
41	39, 40	eqtr2d 2796	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 · 𝐸) = (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))))
42	41	oveq1d 7435	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
43	23	resqcld 14268	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸↑2) ∈ ℝ)
44	27	resqcld 14268	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹↑2) ∈ ℝ)
45	25, 44	remulcld 11339	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℝ)
46	43, 45	resubcld 11744	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ)
47		0red 11311	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
48	16	abscld 15606	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ)
49	48	recnd 11337	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘𝐶) ∈ ℂ)
50	16, 17	absne0d 15617	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘𝐶) ≠ 0)
51	49, 50	dividd 12091	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) = 1)
52		1zzd 12727	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℤ)
53	51, 52	eqeltrd 2860	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ)
54		mod0 14016	. . . . . . . . . . . . . . . . 17 ⊢ (((abs‘𝐶) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
55	48, 31, 54	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
56	53, 55	mpbird 260	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘𝐶) mod (abs‘𝐶)) = 0)
57	15	zred 12803	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ℝ)
58		absmod0 15470	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
59	57, 31, 58	syl2anc 596	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
60	56, 59	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 mod (abs‘𝐶)) = 0)
61		pellex.no2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
62	61	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (𝐶 mod (abs‘𝐶)))
63		0mod 14042	. . . . . . . . . . . . . . 15 ⊢ ((abs‘𝐶) ∈ ℝ⁺ → (0 mod (abs‘𝐶)) = 0)
64	31, 63	syl 18	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 mod (abs‘𝐶)) = 0)
65	60, 62, 64	3eqtr4d 2805	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
66		modadd1 14048	. . . . . . . . . . . . 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 1408	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
68	38	addlidd 11511	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐷 · (𝐹↑2)))
69	11	sqvald 14286	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
70	69	oveq2d 7436	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) = (𝐷 · (𝐹 · 𝐹)))
71	7, 11, 11	mul12d 11519	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹 · 𝐹)) = (𝐹 · (𝐷 · 𝐹)))
72	68, 70, 71	3eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐹 · (𝐷 · 𝐹)))
73	72	oveq1d 7435	. . . . . . . . . . . 12 ⊢ (𝜑 → ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
74	42, 67, 73	3eqtrd 2799	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
75	6	nnzd 12719	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ ℤ)
76	10	nnzd 12719	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ ℤ)
77	75, 76	zmulcld 12809	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · 𝐹) ∈ ℤ)
78		pellex.ycg	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))
79	78	eqcomd 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶)))
80		modmul1 14067	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐷 · 𝐹) ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶))) → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
81	27, 26, 77, 31, 79, 80	syl221anc 1408	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
82	9, 7, 11	mul12d 11519	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 · (𝐷 · 𝐹)) = (𝐷 · (𝐵 · 𝐹)))
83	82	oveq1d 7435	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
84	81, 83	eqtrd 2795	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
85	35, 74, 84	3eqtrd 2799	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
86		modadd1 14048	. . . . . . . . . 10 ⊢ ((((𝐴 · 𝐸) ∈ ℝ ∧ (𝐷 · (𝐵 · 𝐹)) ∈ ℝ) ∧ ( -(𝐷 · (𝐵 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
87	24, 29, 30, 31, 85, 86	syl221anc 1408	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
88	13	negidd 11659	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) = 0)
89	88	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
90	21, 87, 89	3eqtrd 2799	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
91	90, 64	eqtrd 2795	. . . . . . 7 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0)
92	24, 29	resubcld 11744	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ)
93		absmod0 15470	. . . . . . . 8 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
94	92, 31, 93	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
95	91, 94	mpbid 235	. . . . . 6 ⊢ (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0)
96	14	abscld 15606	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ)
97		mod0 14016	. . . . . . 7 ⊢ (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
98	96, 31, 97	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
99	95, 98	mpbid 235	. . . . 5 ⊢ (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ)
100	18, 99	eqeltrd 2860	. . . 4 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ)
101	92, 57, 17	redivcld 12145	. . . . 5 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ)
102		absz 15478	. . . . 5 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
103	101, 102	syl 18	. . . 4 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
104	100, 103	mpbird 260	. . 3 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ)
105		0lt1 11838	. . . . . . . 8 ⊢ 0 < 1
106		0re 11310	. . . . . . . . 9 ⊢ 0 ∈ ℝ
107		1re 11308	. . . . . . . . 9 ⊢ 1 ∈ ℝ
108	106, 107	ltnlei 11431	. . . . . . . 8 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
109	105, 108	mpbi 233	. . . . . . 7 ⊢ ¬ 1 ≤ 0
110	9, 4	mulcld 11329	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 · 𝐸) ∈ ℂ)
111	2, 11	mulcld 11329	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐹) ∈ ℂ)
112	110, 111	subcld 11669	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℂ)
113	112, 16, 17	divcld 12093	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℂ)
114	113	abscld 15606	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℝ)
115	114	resqcld 14268	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) ∈ ℝ)
116	6	nnnn0d 12667	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ₀)
117	116	nn0ge0d 12670	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝐷)
118	114	sqge0d 14280	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
119	25, 115, 117, 118	mulge0d 11893	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
120	25, 115	remulcld 11339	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) ∈ ℝ)
121	47, 120	suble0d 11907	. . . . . . . . 9 ⊢ (𝜑 → ((0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0 ↔ 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
122	119, 121	mpbird 260	. . . . . . . 8 ⊢ (𝜑 → (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0)
123		breq1 5105	. . . . . . . 8 ⊢ (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → (1 ≤ 0 ↔ (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0))
124	122, 123	syl5ibrcom 250	. . . . . . 7 ⊢ (𝜑 → (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → 1 ≤ 0))
125	109, 124	mtoi 202	. . . . . 6 ⊢ (𝜑 → ¬ 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
126		absresq 15469	. . . . . . . . . . . 12 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
127	101, 126	syl 18	. . . . . . . . . . 11 ⊢ (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
128	14, 16, 17	sqdivd 14302	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)))
129	14	sqvald 14286	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) = (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))))
130	129	oveq1d 7435	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
131	127, 128, 130	3eqtrd 2799	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
132	26, 23	remulcld 11339	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 · 𝐸) ∈ ℝ)
133	22, 27	remulcld 11339	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 𝐹) ∈ ℝ)
134	132, 133	resubcld 11744	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ)
135	134, 57, 17	redivcld 12145	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ)
136		absresq 15469	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
137	135, 136	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
138	112, 16, 17	sqdivd 14302	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
139	137, 138	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
140	139	oveq2d 7436	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
141	112	sqcld 14287	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) ∈ ℂ)
142	16	sqcld 14287	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
143		sqne0 14266	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ ℂ → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
144	16, 143	syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
145	17, 144	mpbird 260	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶↑2) ≠ 0)
146	7, 141, 142, 145	divassd 12128	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
147	112	sqvald 14286	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) = (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))
148	147	oveq2d 7436	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) = (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))))
149	148	oveq1d 7435	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
150	140, 146, 149	3eqtr2d 2801	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
151	131, 150	oveq12d 7438	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
152	14, 14	mulcld 11329	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
153	112, 112	mulcld 11329	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℂ)
154	7, 153	mulcld 11329	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) ∈ ℂ)
155	152, 154, 142, 145	divsubdird 12132	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
156	5, 13, 5, 13	mulsubd 11775	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))))
157	110, 111, 110, 111	mulsubd 11775	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) = ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
158	157	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
159	110, 110	mulcld 11329	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐵 · 𝐸)) ∈ ℂ)
160	111, 111	mulcld 11329	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐹) · (𝐴 · 𝐹)) ∈ ℂ)
161	159, 160	addcld 11328	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
162	110, 111	mulcld 11329	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐴 · 𝐹)) ∈ ℂ)
163	162, 162	addcld 11328	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
164	7, 161, 163	subdid 11772	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
165	7, 159, 160	adddid 11333	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
166	7, 162, 162	adddid 11333	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
167	165, 166	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
168	158, 164, 167	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
169	156, 168	oveq12d 7438	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
170	169	oveq1d 7435	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)))
171	5, 13	mulcomd 11330	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)))
172	7, 12, 5	mulassd 11332	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)) = (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))))
173	2, 4	mulcomd 11330	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 · 𝐸) = (𝐸 · 𝐴))
174	173	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐹) · (𝐸 · 𝐴)))
175	9, 11, 4, 2	mul4d 11522	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐸 · 𝐴)) = ((𝐵 · 𝐸) · (𝐹 · 𝐴)))
176	11, 2	mulcomd 11330	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐹 · 𝐴) = (𝐴 · 𝐹))
177	176	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐹 · 𝐴)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
178	174, 175, 177	3eqtrd 2799	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
179	178	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
180	171, 172, 179	3eqtrd 2799	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
181	180, 180	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
182	181	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
183	182	oveq1d 7435	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
184	5, 5	mulcld 11329	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐴 · 𝐸)) ∈ ℂ)
185	13, 13	mulcld 11329	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
186	184, 185	addcld 11328	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
187	7, 159	mulcld 11329	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) ∈ ℂ)
188	7, 160	mulcld 11329	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
189	187, 188	addcld 11328	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) ∈ ℂ)
190	7, 162	mulcld 11329	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
191	190, 190	addcld 11328	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) ∈ ℂ)
192	186, 189, 191	nnncan2d 11704	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
193	184, 185, 187, 188	addsub4d 11716	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
194	5	sqvald 14286	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴 · 𝐸) · (𝐴 · 𝐸)))
195	110	sqvald 14286	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵 · 𝐸) · (𝐵 · 𝐸)))
196	195	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))))
197	194, 196	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))))
198	13	sqvald 14286	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))))
199	111	sqvald 14286	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴 · 𝐹) · (𝐴 · 𝐹)))
200	199	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))
201	198, 200	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
202	197, 201	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
203	2, 4	sqmuld 14301	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴↑2) · (𝐸↑2)))
204	9, 4	sqmuld 14301	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵↑2) · (𝐸↑2)))
205	204	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
206	9	sqcld 14287	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
207	7, 206, 36	mulassd 11332	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) · (𝐸↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
208	205, 207	eqtr4d 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = ((𝐷 · (𝐵↑2)) · (𝐸↑2)))
209	203, 208	oveq12d 7438	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
210	7	sqvald 14286	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷↑2) = (𝐷 · 𝐷))
211	9, 11	sqmuld 14301	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹)↑2) = ((𝐵↑2) · (𝐹↑2)))
212	210, 211	oveq12d 7438	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷↑2) · ((𝐵 · 𝐹)↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
213	7, 12	sqmuld 14301	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷↑2) · ((𝐵 · 𝐹)↑2)))
214	7, 7	mulcld 11329	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · 𝐷) ∈ ℂ)
215	214, 206, 37	mulassd 11332	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
216	212, 213, 215	3eqtr4d 2805	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)))
217	2, 11	sqmuld 14301	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴↑2) · (𝐹↑2)))
218	217	oveq2d 7436	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
219	2	sqcld 14287	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
220	7, 219, 37	mulassd 11332	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐴↑2)) · (𝐹↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
221	218, 220	eqtr4d 2798	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = ((𝐷 · (𝐴↑2)) · (𝐹↑2)))
222	216, 221	oveq12d 7438	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
223	209, 222	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))))
224	7, 206	mulcld 11329	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · (𝐵↑2)) ∈ ℂ)
225	219, 224, 36	subdird 11773	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
226		pellex.no1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)
227	226	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (𝐶 · (𝐸↑2)))
228	225, 227	eqtr3d 2797	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) = (𝐶 · (𝐸↑2)))
229	7, 7, 206	mulassd 11332	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) = (𝐷 · (𝐷 · (𝐵↑2))))
230	229	oveq1d 7435	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
231	230	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)))
232	214, 206	mulcld 11329	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) ∈ ℂ)
233	7, 219	mulcld 11329	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · (𝐴↑2)) ∈ ℂ)
234	232, 233, 37	subdird 11773	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
235		subdi 11749	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
236	235	eqcomd 2766	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
237	7, 224, 219, 236	syl3anc 1398	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
238		negsubdi2 11617	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = ((𝐷 · (𝐵↑2)) − (𝐴↑2)))
239	238	eqcomd 2766	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
240	219, 224, 239	syl2anc 596	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
241	226	negeqd 11551	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = -𝐶)
242	240, 241	eqtrd 2795	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -𝐶)
243	242	oveq2d 7436	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = (𝐷 · -𝐶))
244	7, 16	mulneg2d 11770	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · -𝐶) = -(𝐷 · 𝐶))
245	237, 243, 244	3eqtrd 2799	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = -(𝐷 · 𝐶))
246	245	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = ( -(𝐷 · 𝐶) · (𝐹↑2)))
247	231, 234, 246	3eqtr3d 2803	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))) = ( -(𝐷 · 𝐶) · (𝐹↑2)))
248	228, 247	oveq12d 7438	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) + ( -(𝐷 · 𝐶) · (𝐹↑2))))
249	7, 16	mulcld 11329	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · 𝐶) ∈ ℂ)
250	249, 37	mulneg1d 11769	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ( -(𝐷 · 𝐶) · (𝐹↑2)) = -((𝐷 · 𝐶) · (𝐹↑2)))
251	7, 16	mulcomd 11330	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐷 · 𝐶) = (𝐶 · 𝐷))
252	251	oveq1d 7435	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = ((𝐶 · 𝐷) · (𝐹↑2)))
253	16, 7, 37	mulassd 11332	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐶 · 𝐷) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
254	252, 253	eqtrd 2795	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
255	254	negeqd 11551	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -((𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
256	250, 255	eqtrd 2795	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ( -(𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
257	256	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + ( -(𝐷 · 𝐶) · (𝐹↑2))) = ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))))
258	16, 36	mulcld 11329	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · (𝐸↑2)) ∈ ℂ)
259	16, 38	mulcld 11329	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · (𝐷 · (𝐹↑2))) ∈ ℂ)
260	258, 259	negsubd 11675	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
261	61	oveq2d 7436	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = (𝐶 · 𝐶))
262		subdi 11749	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
263	262	eqcomd 2766	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
264	16, 36, 38, 263	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
265	16	sqvald 14286	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶↑2) = (𝐶 · 𝐶))
266	261, 264, 265	3eqtr4d 2805	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶↑2))
267	257, 260, 266	3eqtrd 2799	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + ( -(𝐷 · 𝐶) · (𝐹↑2))) = (𝐶↑2))
268	223, 248, 267	3eqtrd 2799	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = (𝐶↑2))
269	193, 202, 268	3eqtr2d 2801	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = (𝐶↑2))
270	183, 192, 269	3eqtrd 2799	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (𝐶↑2))
271	270	oveq1d 7435	. . . . . . . . . 10 ⊢ (𝜑 → ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)) = ((𝐶↑2) / (𝐶↑2)))
272	142, 145	dividd 12091	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑2) / (𝐶↑2)) = 1)
273	170, 271, 272	3eqtrd 2799	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = 1)
274	151, 155, 273	3eqtr2d 2801	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
275	274	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
276		simpr 490	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
277	276	fvoveq1d 7442	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = (abs‘(0 / 𝐶)))
278	16, 17	div0d 12092	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 / 𝐶) = 0)
279	278	abs00bd 15458	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(0 / 𝐶)) = 0)
280	279	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(0 / 𝐶)) = 0)
281	277, 280	eqtrd 2795	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = 0)
282	281	sq0id 14337	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = 0)
283	282	oveq1d 7435	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
284	275, 283	eqtr3d 2797	. . . . . 6 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
285	125, 284	mtand 828	. . . . 5 ⊢ (𝜑 → ¬ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
286	285	neqned 2962	. . . 4 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ≠ 0)
287	14, 16, 286, 17	divne0d 12109	. . 3 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0)
288		nnabscl 15493	. . 3 ⊢ (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ∧ (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
289	104, 287, 288	syl2anc 596	. 2 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
290	112, 16, 17	absdivd 15625	. . . . 5 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) = ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)))
291		negsub 11606	. . . . . . . . . . . 12 ⊢ (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) + -(𝐴 · 𝐹)) = ((𝐵 · 𝐸) − (𝐴 · 𝐹)))
292	291	eqcomd 2766	. . . . . . . . . . 11 ⊢ (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
293	110, 111, 292	syl2anc 596	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
294	293	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
295	133	renegcld 11743	. . . . . . . . . 10 ⊢ (𝜑 → -(𝐴 · 𝐹) ∈ ℝ)
296	11, 4	mulcomd 11330	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 · 𝐸) = (𝐸 · 𝐹))
297	296	oveq1d 7435	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
298		modmul1 14067	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℝ ∧ 𝐹 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
299	26, 27, 32, 31, 78, 298	syl221anc 1408	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
300		modmul1 14067	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐹 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
301	22, 23, 76, 31, 33, 300	syl221anc 1408	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
302	297, 299, 301	3eqtr4d 2805	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶)))
303		modadd1 14048	. . . . . . . . . 10 ⊢ ((((𝐵 · 𝐸) ∈ ℝ ∧ (𝐴 · 𝐹) ∈ ℝ) ∧ ( -(𝐴 · 𝐹) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶))) → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
304	132, 133, 295, 31, 302, 303	syl221anc 1408	. . . . . . . . 9 ⊢ (𝜑 → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
305	111	negidd 11659	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐹) + -(𝐴 · 𝐹)) = 0)
306	305	oveq1d 7435	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
307	294, 304, 306	3eqtrd 2799	. . . . . . . 8 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
308	307, 64	eqtrd 2795	. . . . . . 7 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0)
309		absmod0 15470	. . . . . . . 8 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
310	134, 31, 309	syl2anc 596	. . . . . . 7 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
311	308, 310	mpbid 235	. . . . . 6 ⊢ (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0)
312	112	abscld 15606	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ)
313		mod0 14016	. . . . . . 7 ⊢ (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
314	312, 31, 313	syl2anc 596	. . . . . 6 ⊢ (𝜑 → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
315	311, 314	mpbid 235	. . . . 5 ⊢ (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ)
316	290, 315	eqeltrd 2860	. . . 4 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ)
317		absz 15478	. . . . 5 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
318	135, 317	syl 18	. . . 4 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
319	316, 318	mpbird 260	. . 3 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ)
320		pellex.neq	. . . . . . 7 ⊢ (𝜑 → ¬ (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))
321	10	nnne0d 12388	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ≠ 0)
322	3	nnne0d 12388	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ≠ 0)
323	9, 11, 2, 4, 321, 322	divmuleqd 12139	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) ↔ (𝐵 · 𝐸) = (𝐴 · 𝐹)))
324	61	adantr 486	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
325	324	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐸↑2) − (𝐷 · (𝐹↑2))))
326	325	oveq2d 7436	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
327	9, 11, 321	divcld 12093	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / 𝐹) ∈ ℂ)
328	327	sqcld 14287	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐹)↑2) ∈ ℂ)
329	328	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) ∈ ℂ)
330	36	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ∈ ℂ)
331	38	adantr 486	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (𝐹↑2)) ∈ ℂ)
332	329, 330, 331	subdid 11772	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))))
333		oveq1 7427	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 / 𝐹) = (𝐴 / 𝐸) → ((𝐵 / 𝐹)↑2) = ((𝐴 / 𝐸)↑2))
334	333	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
335	334	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
336	2	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐴 ∈ ℂ)
337	4	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ∈ ℂ)
338	322	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ≠ 0)
339	336, 337, 338	sqdivd 14302	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐴 / 𝐸)↑2) = ((𝐴↑2) / (𝐸↑2)))
340	339	oveq1d 7435	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴 / 𝐸)↑2) · (𝐸↑2)) = (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)))
341	219	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴↑2) ∈ ℂ)
342		sqne0 14266	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐸 ∈ ℂ → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
343	4, 342	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
344	322, 343	mpbird 260	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸↑2) ≠ 0)
345	344	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ≠ 0)
346	341, 330, 345	divcan1d 12094	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)) = (𝐴↑2))
347	335, 340, 346	3eqtrd 2799	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (𝐴↑2))
348	7	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐷 ∈ ℂ)
349	37	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ∈ ℂ)
350	329, 348, 349	mul12d 11519	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))))
351	9	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐵 ∈ ℂ)
352	11	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ∈ ℂ)
353	321	adantr 486	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ≠ 0)
354	351, 352, 353	sqdivd 14302	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = ((𝐵↑2) / (𝐹↑2)))
355	354	oveq1d 7435	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐹↑2)) = (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)))
356	355	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))) = (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))))
357	206	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐵↑2) ∈ ℂ)
358		sqne0 14266	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 ∈ ℂ → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
359	11, 358	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
360	321, 359	mpbird 260	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹↑2) ≠ 0)
361	360	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ≠ 0)
362	357, 349, 361	divcan1d 12094	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)) = (𝐵↑2))
363	362	oveq2d 7436	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
364	350, 356, 363	3eqtrd 2799	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
365	347, 364	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
366	326, 332, 365	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
367	226	eqcomd 2766	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
368	367	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
369	366, 368	oveq12d 7438	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))))
370	16	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ∈ ℂ)
371	17	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ≠ 0)
372	329, 370, 371	divcan4d 12099	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = ((𝐵 / 𝐹)↑2))
373	226, 226	oveq12d 7438	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = (𝐶 / 𝐶))
374	16, 17	dividd 12091	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 / 𝐶) = 1)
375	373, 374	eqtrd 2795	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
376	375	adantr 486	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
377	369, 372, 376	3eqtr3d 2803	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = 1)
378	26, 27, 321	redivcld 12145	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / 𝐹) ∈ ℝ)
379	8	nnnn0d 12667	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℕ₀)
380	379	nn0ge0d 12670	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 𝐵)
381	10	nngt0d 12387	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝐹)
382		divge0 12186	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ (𝐹 ∈ ℝ ∧ 0 < 𝐹)) → 0 ≤ (𝐵 / 𝐹))
383	26, 380, 27, 381, 382	syl22anc 852	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ (𝐵 / 𝐹))
384	378, 383	sqrtsqd 15587	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (√‘((𝐵 / 𝐹)↑2)) = (𝐵 / 𝐹))
385	384	eqcomd 2766	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
386	385	ad2antrr 739	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
387		fveq2 6885	. . . . . . . . . . . . . 14 ⊢ (((𝐵 / 𝐹)↑2) = 1 → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
388	387	adantl 487	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
389		sqrt1 15438	. . . . . . . . . . . . . 14 ⊢ (√‘1) = 1
390	389	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘1) = 1)
391	386, 388, 390	3eqtrd 2799	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = 1)
392	391	ex 418	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐵 / 𝐹) = 1))
393		simplr 781	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = (𝐴 / 𝐸))
394		simpr 490	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = 1)
395	393, 394	eqtr3d 2797	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 / 𝐸) = 1)
396	395	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = (1 · 𝐸))
397	2, 4, 322	divcan1d 12094	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
398	397	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
399	4	mullidd 11327	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
400	399	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐸) = 𝐸)
401	396, 398, 400	3eqtr3d 2803	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐴 = 𝐸)
402	394	oveq1d 7435	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = (1 · 𝐹))
403	9, 11, 321	divcan1d 12094	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
404	403	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
405	11	mullidd 11327	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · 𝐹) = 𝐹)
406	405	ad2antrr 739	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐹) = 𝐹)
407	402, 404, 406	3eqtr3d 2803	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐵 = 𝐹)
408	401, 407	jca 521	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))
409	408	ex 418	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹) = 1 → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
410	392, 409	syld 48	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
411	377, 410	mpd 16	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))
412	411	ex 418	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
413	323, 412	sylbird 263	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · 𝐸) = (𝐴 · 𝐹) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
414	320, 413	mtod 201	. . . . . 6 ⊢ (𝜑 → ¬ (𝐵 · 𝐸) = (𝐴 · 𝐹))
415	414	neqned 2962	. . . . 5 ⊢ (𝜑 → (𝐵 · 𝐸) ≠ (𝐴 · 𝐹))
416	110, 111, 415	subne0d 11679	. . . 4 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ≠ 0)
417	112, 16, 416, 17	divne0d 12109	. . 3 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0)
418		nnabscl 15493	. . 3 ⊢ (((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ∧ (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0) → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
419	319, 417, 418	syl2anc 596	. 2 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
420		oveq1 7427	. . . . 5 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (𝑎↑2) = ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2))
421	420	oveq1d 7435	. . . 4 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))))
422	421	eqeq1d 2762	. . 3 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1))
423		oveq1 7427	. . . . . 6 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝑏↑2) = ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
424	423	oveq2d 7436	. . . . 5 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝐷 · (𝑏↑2)) = (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
425	424	oveq2d 7436	. . . 4 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
426	425	eqeq1d 2762	. . 3 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → ((((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1))
427	422, 426	rspc2ev 3588	. 2 ⊢ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ ∧ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ ∧ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
428	289, 419, 274, 427	syl3anc 1398	1 ⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ≠ wne 2955 ∃wrex 3086 class class class wbr 5102 ‘cfv 6538 (class class class)co 7420 ℂcc 11198 ℝcr 11199 0cc0 11200 1c1 11201 + caddc 11203 · cmul 11205 < clt 11343 ≤ cle 11344 − cmin 11541 -cneg 11542 / cdiv 11973 ℕcn 12335 2c2 12397 ℤcz 12693 ℚcq 13075 ℝ⁺crp 13120 mod cmo 14009 ↑cexp 14204 √csqrt 15400 abscabs 15401

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7751 ax-cnex 11256 ax-resscn 11257 ax-1cn 11258 ax-icn 11259 ax-addcl 11260 ax-addrcl 11261 ax-mulcl 11262 ax-mulrcl 11263 ax-mulcom 11264 ax-addass 11265 ax-mulass 11266 ax-distr 11267 ax-i2m1 11268 ax-1ne0 11269 ax-1rid 11270 ax-rnegex 11271 ax-rrecex 11272 ax-cnre 11273 ax-pre-lttri 11274 ax-pre-lttrn 11275 ax-pre-ltadd 11276 ax-pre-mulgt0 11277 ax-pre-sup 11278

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4584 df-pr 4586 df-op 4590 df-uni 4867 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-riota 7377 df-ov 7423 df-oprab 7424 df-mpo 7425 df-om 7878 df-2nd 8002 df-frecs 8299 df-wrecs 8330 df-recs 8379 df-rdg 8418 df-er 8717 df-en 8974 df-dom 8975 df-sdom 8976 df-sup 9434 df-inf 9435 df-pnf 11345 df-mnf 11346 df-xr 11347 df-ltxr 11348 df-le 11349 df-sub 11543 df-neg 11544 df-div 11974 df-nn 12336 df-2 12405 df-3 12406 df-n0 12607 df-z 12694 df-uz 12966 df-rp 13121 df-fl 13932 df-mod 14010 df-seq 14145 df-exp 14205 df-cj 15266 df-re 15267 df-im 15268 df-sqrt 15402 df-abs 15403

This theorem is used by: pellex 43842

W3C validator