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 39437

Description: Lemma for pellex 39438. 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 11657	. . . . . . . 8 ⊢ (𝜑 → 𝐴 ∈ ℂ)
3		pellex.enn	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ ℕ)
4	3	nncnd 11657	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ ℂ)
5	2, 4	mulcld 10664	. . . . . . 7 ⊢ (𝜑 → (𝐴 · 𝐸) ∈ ℂ)
6		pellex.dnn	. . . . . . . . 9 ⊢ (𝜑 → 𝐷 ∈ ℕ)
7	6	nncnd 11657	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ ℂ)
8		pellex.bnn	. . . . . . . . . 10 ⊢ (𝜑 → 𝐵 ∈ ℕ)
9	8	nncnd 11657	. . . . . . . . 9 ⊢ (𝜑 → 𝐵 ∈ ℂ)
10		pellex.fnn	. . . . . . . . . 10 ⊢ (𝜑 → 𝐹 ∈ ℕ)
11	10	nncnd 11657	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ∈ ℂ)
12	9, 11	mulcld 10664	. . . . . . . 8 ⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℂ)
13	7, 12	mulcld 10664	. . . . . . 7 ⊢ (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℂ)
14	5, 13	subcld 11000	. . . . . 6 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
15		pellex.cz	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ ℤ)
16	15	zcnd 12091	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ ℂ)
17		pellex.cn0	. . . . . 6 ⊢ (𝜑 → 𝐶 ≠ 0)
18	14, 16, 17	absdivd 14818	. . . . 5 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)))
19	5, 13	negsubd 11006	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))))
20	19	eqcomd 2830	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = ((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))))
21	20	oveq1d 7174	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
22	1	nnred 11656	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐴 ∈ ℝ)
23	3	nnred 11656	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐸 ∈ ℝ)
24	22, 23	remulcld 10674	. . . . . . . . . 10 ⊢ (𝜑 → (𝐴 · 𝐸) ∈ ℝ)
25	6	nnred 11656	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℝ)
26	8	nnred 11656	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐵 ∈ ℝ)
27	10	nnred 11656	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ ℝ)
28	26, 27	remulcld 10674	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐵 · 𝐹) ∈ ℝ)
29	25, 28	remulcld 10674	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
30	29	renegcld 11070	. . . . . . . . . 10 ⊢ (𝜑 → -(𝐷 · (𝐵 · 𝐹)) ∈ ℝ)
31	16, 17	absrpcld 14811	. . . . . . . . . 10 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ⁺)
32	3	nnzd 12089	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ ℤ)
33		pellex.xcg	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶)))
34		modmul1 13295	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
35	22, 23, 32, 31, 33, 34	syl221anc 1377	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐸) mod (abs‘𝐶)))
36	4	sqcld 13511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐸↑2) ∈ ℂ)
37	11	sqcld 13511	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐹↑2) ∈ ℂ)
38	7, 37	mulcld 10664	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℂ)
39	36, 38	npcand 11004	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) = (𝐸↑2))
40	4	sqvald 13510	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸↑2) = (𝐸 · 𝐸))
41	39, 40	eqtr2d 2860	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐸 · 𝐸) = (((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))))
42	41	oveq1d 7174	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
43	23	resqcld 13614	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐸↑2) ∈ ℝ)
44	27	resqcld 13614	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹↑2) ∈ ℝ)
45	25, 44	remulcld 10674	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) ∈ ℝ)
46	43, 45	resubcld 11071	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) ∈ ℝ)
47		0red 10647	. . . . . . . . . . . . 13 ⊢ (𝜑 → 0 ∈ ℝ)
48	16	abscld 14799	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (abs‘𝐶) ∈ ℝ)
49	48	recnd 10672	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘𝐶) ∈ ℂ)
50	16, 17	absne0d 14810	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (abs‘𝐶) ≠ 0)
51	49, 50	dividd 11417	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) = 1)
52		1zzd 12016	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ ℤ)
53	51, 52	eqeltrd 2916	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ)
54		mod0 13247	. . . . . . . . . . . . . . . . 17 ⊢ (((abs‘𝐶) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
55	48, 31, 54	syl2anc 586	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((abs‘𝐶) mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) / (abs‘𝐶)) ∈ ℤ))
56	53, 55	mpbird 259	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((abs‘𝐶) mod (abs‘𝐶)) = 0)
57	15	zred 12090	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝐶 ∈ ℝ)
58		absmod0 14666	. . . . . . . . . . . . . . . 16 ⊢ ((𝐶 ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
59	57, 31, 58	syl2anc 586	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 mod (abs‘𝐶)) = 0 ↔ ((abs‘𝐶) mod (abs‘𝐶)) = 0))
60	56, 59	mpbird 259	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐶 mod (abs‘𝐶)) = 0)
61		pellex.no2	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
62	61	oveq1d 7174	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (𝐶 mod (abs‘𝐶)))
63		0mod 13273	. . . . . . . . . . . . . . 15 ⊢ ((abs‘𝐶) ∈ ℝ⁺ → (0 mod (abs‘𝐶)) = 0)
64	31, 63	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 mod (abs‘𝐶)) = 0)
65	60, 62, 64	3eqtr4d 2869	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐸↑2) − (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
66		modadd1 13279	. . . . . . . . . . . . 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 1377	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐸↑2) − (𝐷 · (𝐹↑2))) + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)))
68	38	addid2d 10844	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐷 · (𝐹↑2)))
69	11	sqvald 13510	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹↑2) = (𝐹 · 𝐹))
70	69	oveq2d 7175	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹↑2)) = (𝐷 · (𝐹 · 𝐹)))
71	7, 11, 11	mul12d 10852	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (𝐹 · 𝐹)) = (𝐹 · (𝐷 · 𝐹)))
72	68, 70, 71	3eqtrd 2863	. . . . . . . . . . . . 13 ⊢ (𝜑 → (0 + (𝐷 · (𝐹↑2))) = (𝐹 · (𝐷 · 𝐹)))
73	72	oveq1d 7174	. . . . . . . . . . . 12 ⊢ (𝜑 → ((0 + (𝐷 · (𝐹↑2))) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
74	42, 67, 73	3eqtrd 2863	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
75	6	nnzd 12089	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐷 ∈ ℤ)
76	10	nnzd 12089	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐹 ∈ ℤ)
77	75, 76	zmulcld 12096	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · 𝐹) ∈ ℤ)
78		pellex.ycg	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶)))
79	78	eqcomd 2830	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶)))
80		modmul1 13295	. . . . . . . . . . . . 13 ⊢ (((𝐹 ∈ ℝ ∧ 𝐵 ∈ ℝ) ∧ ((𝐷 · 𝐹) ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐹 mod (abs‘𝐶)) = (𝐵 mod (abs‘𝐶))) → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
81	27, 26, 77, 31, 79, 80	syl221anc 1377	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)))
82	9, 7, 11	mul12d 10852	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐵 · (𝐷 · 𝐹)) = (𝐷 · (𝐵 · 𝐹)))
83	82	oveq1d 7174	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐵 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
84	81, 83	eqtrd 2859	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 · (𝐷 · 𝐹)) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
85	35, 74, 84	3eqtrd 2863	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶)))
86		modadd1 13279	. . . . . . . . . 10 ⊢ ((((𝐴 · 𝐸) ∈ ℝ ∧ (𝐷 · (𝐵 · 𝐹)) ∈ ℝ) ∧ (-(𝐷 · (𝐵 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ ((𝐴 · 𝐸) mod (abs‘𝐶)) = ((𝐷 · (𝐵 · 𝐹)) mod (abs‘𝐶))) → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
87	24, 29, 30, 31, 85, 86	syl221anc 1377	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐸) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)))
88	13	negidd 10990	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) = 0)
89	88	oveq1d 7174	. . . . . . . . 9 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹)) + -(𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
90	21, 87, 89	3eqtrd 2863	. . . . . . . 8 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
91	90, 64	eqtrd 2859	. . . . . . 7 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0)
92	24, 29	resubcld 11071	. . . . . . . 8 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ)
93		absmod0 14666	. . . . . . . 8 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
94	92, 31, 93	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0))
95	91, 94	mpbid 234	. . . . . 6 ⊢ (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0)
96	14	abscld 14799	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ)
97		mod0 13247	. . . . . . 7 ⊢ (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
98	96, 31, 97	syl2anc 586	. . . . . 6 ⊢ (𝜑 → (((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ))
99	95, 98	mpbid 234	. . . . 5 ⊢ (𝜑 → ((abs‘((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (abs‘𝐶)) ∈ ℤ)
100	18, 99	eqeltrd 2916	. . . 4 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ)
101	92, 57, 17	redivcld 11471	. . . . 5 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ)
102		absz 14674	. . . . 5 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
103	101, 102	syl 17	. . . 4 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℤ))
104	100, 103	mpbird 259	. . 3 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ)
105		0lt1 11165	. . . . . . . 8 ⊢ 0 < 1
106		0re 10646	. . . . . . . . 9 ⊢ 0 ∈ ℝ
107		1re 10644	. . . . . . . . 9 ⊢ 1 ∈ ℝ
108	106, 107	ltnlei 10764	. . . . . . . 8 ⊢ (0 < 1 ↔ ¬ 1 ≤ 0)
109	105, 108	mpbi 232	. . . . . . 7 ⊢ ¬ 1 ≤ 0
110	9, 4	mulcld 10664	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 · 𝐸) ∈ ℂ)
111	2, 11	mulcld 10664	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐴 · 𝐹) ∈ ℂ)
112	110, 111	subcld 11000	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℂ)
113	112, 16, 17	divcld 11419	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℂ)
114	113	abscld 14799	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℝ)
115	114	resqcld 13614	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) ∈ ℝ)
116	6	nnnn0d 11958	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐷 ∈ ℕ₀)
117	116	nn0ge0d 11961	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ 𝐷)
118	114	sqge0d 13615	. . . . . . . . . 10 ⊢ (𝜑 → 0 ≤ ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
119	25, 115, 117, 118	mulge0d 11220	. . . . . . . . 9 ⊢ (𝜑 → 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
120	25, 115	remulcld 10674	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) ∈ ℝ)
121	47, 120	suble0d 11234	. . . . . . . . 9 ⊢ (𝜑 → ((0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0 ↔ 0 ≤ (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
122	119, 121	mpbird 259	. . . . . . . 8 ⊢ (𝜑 → (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0)
123		breq1 5072	. . . . . . . 8 ⊢ (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → (1 ≤ 0 ↔ (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) ≤ 0))
124	122, 123	syl5ibrcom 249	. . . . . . 7 ⊢ (𝜑 → (1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) → 1 ≤ 0))
125	109, 124	mtoi 201	. . . . . 6 ⊢ (𝜑 → ¬ 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
126		absresq 14665	. . . . . . . . . . . 12 ⊢ ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℝ → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
127	101, 126	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2))
128	14, 16, 17	sqdivd 13526	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)))
129	14	sqvald 13510	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) = (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))))
130	129	oveq1d 7174	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))↑2) / (𝐶↑2)) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
131	127, 128, 130	3eqtrd 2863	. . . . . . . . . 10 ⊢ (𝜑 → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)))
132	26, 23	remulcld 10674	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 · 𝐸) ∈ ℝ)
133	22, 27	remulcld 10674	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐴 · 𝐹) ∈ ℝ)
134	132, 133	resubcld 11071	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ)
135	134, 57, 17	redivcld 11471	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ)
136		absresq 14665	. . . . . . . . . . . . . 14 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
137	135, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2))
138	112, 16, 17	sqdivd 13526	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
139	137, 138	eqtrd 2859	. . . . . . . . . . . 12 ⊢ (𝜑 → ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2) = ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2)))
140	139	oveq2d 7175	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
141	112	sqcld 13511	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) ∈ ℂ)
142	16	sqcld 13511	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶↑2) ∈ ℂ)
143		sqne0 13492	. . . . . . . . . . . . . 14 ⊢ (𝐶 ∈ ℂ → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
144	16, 143	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐶↑2) ≠ 0 ↔ 𝐶 ≠ 0))
145	17, 144	mpbird 259	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐶↑2) ≠ 0)
146	7, 141, 142, 145	divassd 11454	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = (𝐷 · ((((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) / (𝐶↑2))))
147	112	sqvald 13510	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2) = (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))
148	147	oveq2d 7175	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) = (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))))
149	148	oveq1d 7174	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹))↑2)) / (𝐶↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
150	140, 146, 149	3eqtr2d 2865	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)) = ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2)))
151	131, 150	oveq12d 7177	. . . . . . . . 9 ⊢ (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
152	14, 14	mulcld 10664	. . . . . . . . . 10 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
153	112, 112	mulcld 10664	. . . . . . . . . . 11 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℂ)
154	7, 153	mulcld 10664	. . . . . . . . . 10 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) ∈ ℂ)
155	152, 154, 142, 145	divsubdird 11458	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) / (𝐶↑2)) − ((𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) / (𝐶↑2))))
156	5, 13, 5, 13	mulsubd 11102	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))))
157	110, 111, 110, 111	mulsubd 11102	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))) = ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
158	157	oveq2d 7175	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
159	110, 110	mulcld 10664	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐵 · 𝐸)) ∈ ℂ)
160	111, 111	mulcld 10664	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐹) · (𝐴 · 𝐹)) ∈ ℂ)
161	159, 160	addcld 10663	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
162	110, 111	mulcld 10664	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐴 · 𝐹)) ∈ ℂ)
163	162, 162	addcld 10663	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
164	7, 161, 163	subdid 11099	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐷 · ((((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹))) − (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
165	7, 159, 160	adddid 10668	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
166	7, 162, 162	adddid 10668	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
167	165, 166	oveq12d 7177	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · (((𝐵 · 𝐸) · (𝐵 · 𝐸)) + ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) · (𝐴 · 𝐹)) + ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
168	158, 164, 167	3eqtrd 2863	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹)))) = (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
169	156, 168	oveq12d 7177	. . . . . . . . . . 11 ⊢ (𝜑 → ((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
170	169	oveq1d 7174	. . . . . . . . . 10 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)))
171	5, 13	mulcomd 10665	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)))
172	7, 12, 5	mulassd 10667	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐴 · 𝐸)) = (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))))
173	2, 4	mulcomd 10665	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐴 · 𝐸) = (𝐸 · 𝐴))
174	173	oveq2d 7175	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐹) · (𝐸 · 𝐴)))
175	9, 11, 4, 2	mul4d 10855	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐸 · 𝐴)) = ((𝐵 · 𝐸) · (𝐹 · 𝐴)))
176	11, 2	mulcomd 10665	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → (𝐹 · 𝐴) = (𝐴 · 𝐹))
177	176	oveq2d 7175	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐸) · (𝐹 · 𝐴)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
178	174, 175, 177	3eqtrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐵 · 𝐹) · (𝐴 · 𝐸)) = ((𝐵 · 𝐸) · (𝐴 · 𝐹)))
179	178	oveq2d 7175	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐹) · (𝐴 · 𝐸))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
180	171, 172, 179	3eqtrd 2863	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) = (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))
181	180, 180	oveq12d 7177	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹)))) = ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))
182	181	oveq2d 7175	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))))
183	182	oveq1d 7174	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))))
184	5, 5	mulcld 10664	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐴 · 𝐸) · (𝐴 · 𝐸)) ∈ ℂ)
185	13, 13	mulcld 10664	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) ∈ ℂ)
186	184, 185	addcld 10663	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) ∈ ℂ)
187	7, 159	mulcld 10664	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) ∈ ℂ)
188	7, 160	mulcld 10664	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))) ∈ ℂ)
189	187, 188	addcld 10663	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) ∈ ℂ)
190	7, 162	mulcld 10664	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) ∈ ℂ)
191	190, 190	addcld 10663	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))) ∈ ℂ)
192	186, 189, 191	nnncan2d 11035	. . . . . . . . . . . 12 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
193	184, 185, 187, 188	addsub4d 11047	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
194	5	sqvald 13510	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴 · 𝐸) · (𝐴 · 𝐸)))
195	110	sqvald 13510	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵 · 𝐸) · (𝐵 · 𝐸)))
196	195	oveq2d 7175	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))))
197	194, 196	oveq12d 7177	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))))
198	13	sqvald 13510	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))))
199	111	sqvald 13510	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴 · 𝐹) · (𝐴 · 𝐹)))
200	199	oveq2d 7175	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))
201	198, 200	oveq12d 7177	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))))
202	197, 201	oveq12d 7177	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) − (𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸)))) + (((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹))) − (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))))
203	2, 4	sqmuld 13525	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐴 · 𝐸)↑2) = ((𝐴↑2) · (𝐸↑2)))
204	9, 4	sqmuld 13525	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐸)↑2) = ((𝐵↑2) · (𝐸↑2)))
205	204	oveq2d 7175	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
206	9	sqcld 13511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐵↑2) ∈ ℂ)
207	7, 206, 36	mulassd 10667	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) · (𝐸↑2)) = (𝐷 · ((𝐵↑2) · (𝐸↑2))))
208	205, 207	eqtr4d 2862	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐵 · 𝐸)↑2)) = ((𝐷 · (𝐵↑2)) · (𝐸↑2)))
209	203, 208	oveq12d 7177	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
210	7	sqvald 13510	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷↑2) = (𝐷 · 𝐷))
211	9, 11	sqmuld 13525	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐵 · 𝐹)↑2) = ((𝐵↑2) · (𝐹↑2)))
212	210, 211	oveq12d 7177	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷↑2) · ((𝐵 · 𝐹)↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
213	7, 12	sqmuld 13525	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = ((𝐷↑2) · ((𝐵 · 𝐹)↑2)))
214	7, 7	mulcld 10664	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · 𝐷) ∈ ℂ)
215	214, 206, 37	mulassd 10667	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) = ((𝐷 · 𝐷) · ((𝐵↑2) · (𝐹↑2))))
216	212, 213, 215	3eqtr4d 2869	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐷 · (𝐵 · 𝐹))↑2) = (((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)))
217	2, 11	sqmuld 13525	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐴 · 𝐹)↑2) = ((𝐴↑2) · (𝐹↑2)))
218	217	oveq2d 7175	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
219	2	sqcld 13511	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐴↑2) ∈ ℂ)
220	7, 219, 37	mulassd 10667	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐴↑2)) · (𝐹↑2)) = (𝐷 · ((𝐴↑2) · (𝐹↑2))))
221	218, 220	eqtr4d 2862	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐷 · ((𝐴 · 𝐹)↑2)) = ((𝐷 · (𝐴↑2)) · (𝐹↑2)))
222	216, 221	oveq12d 7177	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2))) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
223	209, 222	oveq12d 7177	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))))
224	7, 206	mulcld 10664	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · (𝐵↑2)) ∈ ℂ)
225	219, 224, 36	subdird 11100	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))))
226		pellex.no1	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶)
227	226	oveq1d 7174	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) · (𝐸↑2)) = (𝐶 · (𝐸↑2)))
228	225, 227	eqtr3d 2861	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) = (𝐶 · (𝐸↑2)))
229	7, 7, 206	mulassd 10667	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) = (𝐷 · (𝐷 · (𝐵↑2))))
230	229	oveq1d 7174	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
231	230	oveq1d 7174	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)))
232	214, 206	mulcld 10664	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · 𝐷) · (𝐵↑2)) ∈ ℂ)
233	7, 219	mulcld 10664	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐷 · (𝐴↑2)) ∈ ℂ)
234	232, 233, 37	subdird 11100	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))))
235		subdi 11076	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))))
236	235	eqcomd 2830	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐷 ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ ∧ (𝐴↑2) ∈ ℂ) → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
237	7, 224, 219, 236	syl3anc 1367	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))))
238		negsubdi2 10948	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = ((𝐷 · (𝐵↑2)) − (𝐴↑2)))
239	238	eqcomd 2830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((𝐴↑2) ∈ ℂ ∧ (𝐷 · (𝐵↑2)) ∈ ℂ) → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
240	219, 224, 239	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -((𝐴↑2) − (𝐷 · (𝐵↑2))))
241	226	negeqd 10883	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → -((𝐴↑2) − (𝐷 · (𝐵↑2))) = -𝐶)
242	240, 241	eqtrd 2859	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐷 · (𝐵↑2)) − (𝐴↑2)) = -𝐶)
243	242	oveq2d 7175	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · ((𝐷 · (𝐵↑2)) − (𝐴↑2))) = (𝐷 · -𝐶))
244	7, 16	mulneg2d 11097	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · -𝐶) = -(𝐷 · 𝐶))
245	237, 243, 244	3eqtrd 2863	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) = -(𝐷 · 𝐶))
246	245	oveq1d 7174	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (((𝐷 · (𝐷 · (𝐵↑2))) − (𝐷 · (𝐴↑2))) · (𝐹↑2)) = (-(𝐷 · 𝐶) · (𝐹↑2)))
247	231, 234, 246	3eqtr3d 2867	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2))) = (-(𝐷 · 𝐶) · (𝐹↑2)))
248	228, 247	oveq12d 7177	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((((𝐴↑2) · (𝐸↑2)) − ((𝐷 · (𝐵↑2)) · (𝐸↑2))) + ((((𝐷 · 𝐷) · (𝐵↑2)) · (𝐹↑2)) − ((𝐷 · (𝐴↑2)) · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))))
249	7, 16	mulcld 10664	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐷 · 𝐶) ∈ ℂ)
250	249, 37	mulneg1d 11096	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -((𝐷 · 𝐶) · (𝐹↑2)))
251	7, 16	mulcomd 10665	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝜑 → (𝐷 · 𝐶) = (𝐶 · 𝐷))
252	251	oveq1d 7174	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = ((𝐶 · 𝐷) · (𝐹↑2)))
253	16, 7, 37	mulassd 10667	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐶 · 𝐷) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
254	252, 253	eqtrd 2859	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐷 · 𝐶) · (𝐹↑2)) = (𝐶 · (𝐷 · (𝐹↑2))))
255	254	negeqd 10883	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → -((𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
256	250, 255	eqtrd 2859	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (-(𝐷 · 𝐶) · (𝐹↑2)) = -(𝐶 · (𝐷 · (𝐹↑2))))
257	256	oveq2d 7175	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))))
258	16, 36	mulcld 10664	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · (𝐸↑2)) ∈ ℂ)
259	16, 38	mulcld 10664	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · (𝐷 · (𝐹↑2))) ∈ ℂ)
260	258, 259	negsubd 11006	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + -(𝐶 · (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
261	61	oveq2d 7175	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = (𝐶 · 𝐶))
262		subdi 11076	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))))
263	262	eqcomd 2830	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ℂ ∧ (𝐸↑2) ∈ ℂ ∧ (𝐷 · (𝐹↑2)) ∈ ℂ) → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
264	16, 36, 38, 263	syl3anc 1367	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶 · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
265	16	sqvald 13510	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶↑2) = (𝐶 · 𝐶))
266	261, 264, 265	3eqtr4d 2869	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) − (𝐶 · (𝐷 · (𝐹↑2)))) = (𝐶↑2))
267	257, 260, 266	3eqtrd 2863	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐶 · (𝐸↑2)) + (-(𝐷 · 𝐶) · (𝐹↑2))) = (𝐶↑2))
268	223, 248, 267	3eqtrd 2863	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((((𝐴 · 𝐸)↑2) − (𝐷 · ((𝐵 · 𝐸)↑2))) + (((𝐷 · (𝐵 · 𝐹))↑2) − (𝐷 · ((𝐴 · 𝐹)↑2)))) = (𝐶↑2))
269	193, 202, 268	3eqtr2d 2865	. . . . . . . . . . . 12 ⊢ (𝜑 → ((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹))))) = (𝐶↑2))
270	183, 192, 269	3eqtrd 2863	. . . . . . . . . . 11 ⊢ (𝜑 → (((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) = (𝐶↑2))
271	270	oveq1d 7174	. . . . . . . . . 10 ⊢ (𝜑 → ((((((𝐴 · 𝐸) · (𝐴 · 𝐸)) + ((𝐷 · (𝐵 · 𝐹)) · (𝐷 · (𝐵 · 𝐹)))) − (((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))) + ((𝐴 · 𝐸) · (𝐷 · (𝐵 · 𝐹))))) − (((𝐷 · ((𝐵 · 𝐸) · (𝐵 · 𝐸))) + (𝐷 · ((𝐴 · 𝐹) · (𝐴 · 𝐹)))) − ((𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹))) + (𝐷 · ((𝐵 · 𝐸) · (𝐴 · 𝐹)))))) / (𝐶↑2)) = ((𝐶↑2) / (𝐶↑2)))
272	142, 145	dividd 11417	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐶↑2) / (𝐶↑2)) = 1)
273	170, 271, 272	3eqtrd 2863	. . . . . . . . 9 ⊢ (𝜑 → (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) · ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹)))) − (𝐷 · (((𝐵 · 𝐸) − (𝐴 · 𝐹)) · ((𝐵 · 𝐸) − (𝐴 · 𝐹))))) / (𝐶↑2)) = 1)
274	151, 155, 273	3eqtr2d 2865	. . . . . . . 8 ⊢ (𝜑 → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
275	274	adantr 483	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1)
276		simpr 487	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
277	276	fvoveq1d 7181	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = (abs‘(0 / 𝐶)))
278	16, 17	div0d 11418	. . . . . . . . . . . 12 ⊢ (𝜑 → (0 / 𝐶) = 0)
279	278	abs00bd 14654	. . . . . . . . . . 11 ⊢ (𝜑 → (abs‘(0 / 𝐶)) = 0)
280	279	adantr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(0 / 𝐶)) = 0)
281	277, 280	eqtrd 2859	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) = 0)
282	281	sq0id 13560	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) = 0)
283	282	oveq1d 7174	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
284	275, 283	eqtr3d 2861	. . . . . 6 ⊢ ((𝜑 ∧ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0) → 1 = (0 − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
285	125, 284	mtand 814	. . . . 5 ⊢ (𝜑 → ¬ ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) = 0)
286	285	neqned 3026	. . . 4 ⊢ (𝜑 → ((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) ≠ 0)
287	14, 16, 286, 17	divne0d 11435	. . 3 ⊢ (𝜑 → (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0)
288		nnabscl 14688	. . 3 ⊢ (((((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ∈ ℤ ∧ (((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶) ≠ 0) → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
289	104, 287, 288	syl2anc 586	. 2 ⊢ (𝜑 → (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ)
290	112, 16, 17	absdivd 14818	. . . . 5 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) = ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)))
291		negsub 10937	. . . . . . . . . . . 12 ⊢ (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) + -(𝐴 · 𝐹)) = ((𝐵 · 𝐸) − (𝐴 · 𝐹)))
292	291	eqcomd 2830	. . . . . . . . . . 11 ⊢ (((𝐵 · 𝐸) ∈ ℂ ∧ (𝐴 · 𝐹) ∈ ℂ) → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
293	110, 111, 292	syl2anc 586	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) = ((𝐵 · 𝐸) + -(𝐴 · 𝐹)))
294	293	oveq1d 7174	. . . . . . . . 9 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
295	133	renegcld 11070	. . . . . . . . . 10 ⊢ (𝜑 → -(𝐴 · 𝐹) ∈ ℝ)
296	11, 4	mulcomd 10665	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 · 𝐸) = (𝐸 · 𝐹))
297	296	oveq1d 7174	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 · 𝐸) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
298		modmul1 13295	. . . . . . . . . . . 12 ⊢ (((𝐵 ∈ ℝ ∧ 𝐹 ∈ ℝ) ∧ (𝐸 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
299	26, 27, 32, 31, 78, 298	syl221anc 1377	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐹 · 𝐸) mod (abs‘𝐶)))
300		modmul1 13295	. . . . . . . . . . . 12 ⊢ (((𝐴 ∈ ℝ ∧ 𝐸 ∈ ℝ) ∧ (𝐹 ∈ ℤ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
301	22, 23, 76, 31, 33, 300	syl221anc 1377	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐴 · 𝐹) mod (abs‘𝐶)) = ((𝐸 · 𝐹) mod (abs‘𝐶)))
302	297, 299, 301	3eqtr4d 2869	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶)))
303		modadd1 13279	. . . . . . . . . 10 ⊢ ((((𝐵 · 𝐸) ∈ ℝ ∧ (𝐴 · 𝐹) ∈ ℝ) ∧ (-(𝐴 · 𝐹) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) ∧ ((𝐵 · 𝐸) mod (abs‘𝐶)) = ((𝐴 · 𝐹) mod (abs‘𝐶))) → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
304	132, 133, 295, 31, 302, 303	syl221anc 1377	. . . . . . . . 9 ⊢ (𝜑 → (((𝐵 · 𝐸) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)))
305	111	negidd 10990	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐴 · 𝐹) + -(𝐴 · 𝐹)) = 0)
306	305	oveq1d 7174	. . . . . . . . 9 ⊢ (𝜑 → (((𝐴 · 𝐹) + -(𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
307	294, 304, 306	3eqtrd 2863	. . . . . . . 8 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = (0 mod (abs‘𝐶)))
308	307, 64	eqtrd 2859	. . . . . . 7 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0)
309		absmod0 14666	. . . . . . . 8 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
310	134, 31, 309	syl2anc 586	. . . . . . 7 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0))
311	308, 310	mpbid 234	. . . . . 6 ⊢ (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0)
312	112	abscld 14799	. . . . . . 7 ⊢ (𝜑 → (abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ)
313		mod0 13247	. . . . . . 7 ⊢ (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) ∈ ℝ ∧ (abs‘𝐶) ∈ ℝ⁺) → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
314	312, 31, 313	syl2anc 586	. . . . . 6 ⊢ (𝜑 → (((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) mod (abs‘𝐶)) = 0 ↔ ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ))
315	311, 314	mpbid 234	. . . . 5 ⊢ (𝜑 → ((abs‘((𝐵 · 𝐸) − (𝐴 · 𝐹))) / (abs‘𝐶)) ∈ ℤ)
316	290, 315	eqeltrd 2916	. . . 4 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ)
317		absz 14674	. . . . 5 ⊢ ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℝ → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
318	135, 317	syl 17	. . . 4 ⊢ (𝜑 → ((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ↔ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℤ))
319	316, 318	mpbird 259	. . 3 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ)
320		pellex.neq	. . . . . . 7 ⊢ (𝜑 → ¬ (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))
321	10	nnne0d 11690	. . . . . . . . 9 ⊢ (𝜑 → 𝐹 ≠ 0)
322	3	nnne0d 11690	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ≠ 0)
323	9, 11, 2, 4, 321, 322	divmuleqd 11465	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) ↔ (𝐵 · 𝐸) = (𝐴 · 𝐹)))
324	61	adantr 483	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶)
325	324	eqcomd 2830	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐸↑2) − (𝐷 · (𝐹↑2))))
326	325	oveq2d 7175	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))))
327	9, 11, 321	divcld 11419	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / 𝐹) ∈ ℂ)
328	327	sqcld 13511	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐹)↑2) ∈ ℂ)
329	328	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) ∈ ℂ)
330	36	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ∈ ℂ)
331	38	adantr 483	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (𝐹↑2)) ∈ ℂ)
332	329, 330, 331	subdid 11099	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · ((𝐸↑2) − (𝐷 · (𝐹↑2)))) = ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))))
333		oveq1 7166	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐵 / 𝐹) = (𝐴 / 𝐸) → ((𝐵 / 𝐹)↑2) = ((𝐴 / 𝐸)↑2))
334	333	oveq1d 7174	. . . . . . . . . . . . . . . 16 ⊢ ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
335	334	adantl 484	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (((𝐴 / 𝐸)↑2) · (𝐸↑2)))
336	2	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐴 ∈ ℂ)
337	4	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ∈ ℂ)
338	322	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐸 ≠ 0)
339	336, 337, 338	sqdivd 13526	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐴 / 𝐸)↑2) = ((𝐴↑2) / (𝐸↑2)))
340	339	oveq1d 7174	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴 / 𝐸)↑2) · (𝐸↑2)) = (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)))
341	219	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴↑2) ∈ ℂ)
342		sqne0 13492	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐸 ∈ ℂ → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
343	4, 342	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝐸↑2) ≠ 0 ↔ 𝐸 ≠ 0))
344	322, 343	mpbird 259	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐸↑2) ≠ 0)
345	344	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐸↑2) ≠ 0)
346	341, 330, 345	divcan1d 11420	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) / (𝐸↑2)) · (𝐸↑2)) = (𝐴↑2))
347	335, 340, 346	3eqtrd 2863	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐸↑2)) = (𝐴↑2))
348	7	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐷 ∈ ℂ)
349	37	adantr 483	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ∈ ℂ)
350	329, 348, 349	mul12d 10852	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))))
351	9	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐵 ∈ ℂ)
352	11	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ∈ ℂ)
353	321	adantr 483	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐹 ≠ 0)
354	351, 352, 353	sqdivd 13526	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = ((𝐵↑2) / (𝐹↑2)))
355	354	oveq1d 7174	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐹↑2)) = (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)))
356	355	oveq2d 7175	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵 / 𝐹)↑2) · (𝐹↑2))) = (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))))
357	206	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐵↑2) ∈ ℂ)
358		sqne0 13492	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐹 ∈ ℂ → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
359	11, 358	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → ((𝐹↑2) ≠ 0 ↔ 𝐹 ≠ 0))
360	321, 359	mpbird 259	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹↑2) ≠ 0)
361	360	adantr 483	. . . . . . . . . . . . . . . . 17 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐹↑2) ≠ 0)
362	357, 349, 361	divcan1d 11420	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2)) = (𝐵↑2))
363	362	oveq2d 7175	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐷 · (((𝐵↑2) / (𝐹↑2)) · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
364	350, 356, 363	3eqtrd 2863	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2))) = (𝐷 · (𝐵↑2)))
365	347, 364	oveq12d 7177	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · (𝐸↑2)) − (((𝐵 / 𝐹)↑2) · (𝐷 · (𝐹↑2)))) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
366	326, 332, 365	3eqtrd 2863	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) · 𝐶) = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
367	226	eqcomd 2830	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
368	367	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 = ((𝐴↑2) − (𝐷 · (𝐵↑2))))
369	366, 368	oveq12d 7177	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))))
370	16	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ∈ ℂ)
371	17	adantr 483	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → 𝐶 ≠ 0)
372	329, 370, 371	divcan4d 11425	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((((𝐵 / 𝐹)↑2) · 𝐶) / 𝐶) = ((𝐵 / 𝐹)↑2))
373	226, 226	oveq12d 7177	. . . . . . . . . . . . 13 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = (𝐶 / 𝐶))
374	16, 17	dividd 11417	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝐶 / 𝐶) = 1)
375	373, 374	eqtrd 2859	. . . . . . . . . . . 12 ⊢ (𝜑 → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
376	375	adantr 483	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐴↑2) − (𝐷 · (𝐵↑2))) / ((𝐴↑2) − (𝐷 · (𝐵↑2)))) = 1)
377	369, 372, 376	3eqtr3d 2867	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹)↑2) = 1)
378	26, 27, 321	redivcld 11471	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐵 / 𝐹) ∈ ℝ)
379	8	nnnn0d 11958	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → 𝐵 ∈ ℕ₀)
380	379	nn0ge0d 11961	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 ≤ 𝐵)
381	10	nngt0d 11689	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 0 < 𝐹)
382		divge0 11512	. . . . . . . . . . . . . . . . 17 ⊢ (((𝐵 ∈ ℝ ∧ 0 ≤ 𝐵) ∧ (𝐹 ∈ ℝ ∧ 0 < 𝐹)) → 0 ≤ (𝐵 / 𝐹))
383	26, 380, 27, 381, 382	syl22anc 836	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 0 ≤ (𝐵 / 𝐹))
384	378, 383	sqrtsqd 14782	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (√‘((𝐵 / 𝐹)↑2)) = (𝐵 / 𝐹))
385	384	eqcomd 2830	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
386	385	ad2antrr 724	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = (√‘((𝐵 / 𝐹)↑2)))
387		fveq2 6673	. . . . . . . . . . . . . 14 ⊢ (((𝐵 / 𝐹)↑2) = 1 → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
388	387	adantl 484	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘((𝐵 / 𝐹)↑2)) = (√‘1))
389		sqrt1 14634	. . . . . . . . . . . . . 14 ⊢ (√‘1) = 1
390	389	a1i 11	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (√‘1) = 1)
391	386, 388, 390	3eqtrd 2863	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ ((𝐵 / 𝐹)↑2) = 1) → (𝐵 / 𝐹) = 1)
392	391	ex 415	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐵 / 𝐹) = 1))
393		simplr 767	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = (𝐴 / 𝐸))
394		simpr 487	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐵 / 𝐹) = 1)
395	393, 394	eqtr3d 2861	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 / 𝐸) = 1)
396	395	oveq1d 7174	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = (1 · 𝐸))
397	2, 4, 322	divcan1d 11420	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
398	397	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐴 / 𝐸) · 𝐸) = 𝐴)
399	4	mulid2d 10662	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · 𝐸) = 𝐸)
400	399	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐸) = 𝐸)
401	396, 398, 400	3eqtr3d 2867	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐴 = 𝐸)
402	394	oveq1d 7174	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = (1 · 𝐹))
403	9, 11, 321	divcan1d 11420	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
404	403	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → ((𝐵 / 𝐹) · 𝐹) = 𝐵)
405	11	mulid2d 10662	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (1 · 𝐹) = 𝐹)
406	405	ad2antrr 724	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (1 · 𝐹) = 𝐹)
407	402, 404, 406	3eqtr3d 2867	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → 𝐵 = 𝐹)
408	401, 407	jca 514	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) ∧ (𝐵 / 𝐹) = 1) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))
409	408	ex 415	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → ((𝐵 / 𝐹) = 1 → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
410	392, 409	syld 47	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (((𝐵 / 𝐹)↑2) = 1 → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
411	377, 410	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝐵 / 𝐹) = (𝐴 / 𝐸)) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹))
412	411	ex 415	. . . . . . . 8 ⊢ (𝜑 → ((𝐵 / 𝐹) = (𝐴 / 𝐸) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
413	323, 412	sylbird 262	. . . . . . 7 ⊢ (𝜑 → ((𝐵 · 𝐸) = (𝐴 · 𝐹) → (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)))
414	320, 413	mtod 200	. . . . . 6 ⊢ (𝜑 → ¬ (𝐵 · 𝐸) = (𝐴 · 𝐹))
415	414	neqned 3026	. . . . 5 ⊢ (𝜑 → (𝐵 · 𝐸) ≠ (𝐴 · 𝐹))
416	110, 111, 415	subne0d 11009	. . . 4 ⊢ (𝜑 → ((𝐵 · 𝐸) − (𝐴 · 𝐹)) ≠ 0)
417	112, 16, 416, 17	divne0d 11435	. . 3 ⊢ (𝜑 → (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0)
418		nnabscl 14688	. . 3 ⊢ (((((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ∈ ℤ ∧ (((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶) ≠ 0) → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
419	319, 417, 418	syl2anc 586	. 2 ⊢ (𝜑 → (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ)
420		oveq1 7166	. . . . 5 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (𝑎↑2) = ((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2))
421	420	oveq1d 7174	. . . 4 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → ((𝑎↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))))
422	421	eqeq1d 2826	. . 3 ⊢ (𝑎 = (abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) → (((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1))
423		oveq1 7166	. . . . . 6 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝑏↑2) = ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))
424	423	oveq2d 7175	. . . . 5 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (𝐷 · (𝑏↑2)) = (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2)))
425	424	oveq2d 7175	. . . 4 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))))
426	425	eqeq1d 2826	. . 3 ⊢ (𝑏 = (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) → ((((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · (𝑏↑2))) = 1 ↔ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1))
427	422, 426	rspc2ev 3638	. 2 ⊢ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶)) ∈ ℕ ∧ (abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶)) ∈ ℕ ∧ (((abs‘(((𝐴 · 𝐸) − (𝐷 · (𝐵 · 𝐹))) / 𝐶))↑2) − (𝐷 · ((abs‘(((𝐵 · 𝐸) − (𝐴 · 𝐹)) / 𝐶))↑2))) = 1) → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)
428	289, 419, 274, 427	syl3anc 1367	1 ⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∧ w3a 1083 = wceq 1536 ∈ wcel 2113 ≠ wne 3019 ∃wrex 3142 class class class wbr 5069 ‘cfv 6358 (class class class)co 7159 ℂcc 10538 ℝcr 10539 0cc0 10540 1c1 10541 + caddc 10543 · cmul 10545 < clt 10678 ≤ cle 10679 − cmin 10873 -cneg 10874 / cdiv 11300 ℕcn 11641 2c2 11695 ℤcz 11984 ℚcq 12351 ℝ⁺crp 12392 mod cmo 13240 ↑cexp 13432 √csqrt 14595 abscabs 14596

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 ax-sep 5206 ax-nul 5213 ax-pow 5269 ax-pr 5333 ax-un 7464 ax-cnex 10596 ax-resscn 10597 ax-1cn 10598 ax-icn 10599 ax-addcl 10600 ax-addrcl 10601 ax-mulcl 10602 ax-mulrcl 10603 ax-mulcom 10604 ax-addass 10605 ax-mulass 10606 ax-distr 10607 ax-i2m1 10608 ax-1ne0 10609 ax-1rid 10610 ax-rnegex 10611 ax-rrecex 10612 ax-cnre 10613 ax-pre-lttri 10614 ax-pre-lttrn 10615 ax-pre-ltadd 10616 ax-pre-mulgt0 10617 ax-pre-sup 10618

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-ne 3020 df-nel 3127 df-ral 3146 df-rex 3147 df-reu 3148 df-rmo 3149 df-rab 3150 df-v 3499 df-sbc 3776 df-csb 3887 df-dif 3942 df-un 3944 df-in 3946 df-ss 3955 df-pss 3957 df-nul 4295 df-if 4471 df-pw 4544 df-sn 4571 df-pr 4573 df-tp 4575 df-op 4577 df-uni 4842 df-iun 4924 df-br 5070 df-opab 5132 df-mpt 5150 df-tr 5176 df-id 5463 df-eprel 5468 df-po 5477 df-so 5478 df-fr 5517 df-we 5519 df-xp 5564 df-rel 5565 df-cnv 5566 df-co 5567 df-dm 5568 df-rn 5569 df-res 5570 df-ima 5571 df-pred 6151 df-ord 6197 df-on 6198 df-lim 6199 df-suc 6200 df-iota 6317 df-fun 6360 df-fn 6361 df-f 6362 df-f1 6363 df-fo 6364 df-f1o 6365 df-fv 6366 df-riota 7117 df-ov 7162 df-oprab 7163 df-mpo 7164 df-om 7584 df-2nd 7693 df-wrecs 7950 df-recs 8011 df-rdg 8049 df-er 8292 df-en 8513 df-dom 8514 df-sdom 8515 df-sup 8909 df-inf 8910 df-pnf 10680 df-mnf 10681 df-xr 10682 df-ltxr 10683 df-le 10684 df-sub 10875 df-neg 10876 df-div 11301 df-nn 11642 df-2 11703 df-3 11704 df-n0 11901 df-z 11985 df-uz 12247 df-rp 12393 df-fl 13165 df-mod 13241 df-seq 13373 df-exp 13433 df-cj 14461 df-re 14462 df-im 14463 df-sqrt 14597 df-abs 14598

This theorem is referenced by: pellex 39438

W3C validator