Metamath Proof Explorer

Theorem pellexlem6

Description: Lemma for pellex . 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)

Ref Expression
Hypotheses 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 pellexlem6 ( 𝜑 → ∃ 𝑎 ∈ ℕ ∃ 𝑏 ∈ ℕ ( ( 𝑎 ↑ 2 ) − ( 𝐷 · ( 𝑏 ↑ 2 ) ) ) = 1 )

Proof

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