Metamath Proof Explorer

Theorem 2sqlem4

Description: Lemma for 2sqlem5 . (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2sqlem5.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2sqlem5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2sqlem4.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
2sqlem4.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
2sqlem4.5 ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
2sqlem4.6 ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
2sqlem4.7 ⊢ ( 𝜑 → ( 𝑁 · 𝑃 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
2sqlem4.8 ⊢ ( 𝜑 → 𝑃 = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
Assertion 2sqlem4 ( 𝜑 → 𝑁 ∈ 𝑆 )

Proof

Step Hyp Ref Expression
1 2sq.1 ⊢ 𝑆 = ran ( 𝑤 ∈ ℤ[i] ↦ ( ( abs ‘ 𝑤 ) ↑ 2 ) )
2 2sqlem5.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
3 2sqlem5.2 ⊢ ( 𝜑 → 𝑃 ∈ ℙ )
4 2sqlem4.3 ⊢ ( 𝜑 → 𝐴 ∈ ℤ )
5 2sqlem4.4 ⊢ ( 𝜑 → 𝐵 ∈ ℤ )
6 2sqlem4.5 ⊢ ( 𝜑 → 𝐶 ∈ ℤ )
7 2sqlem4.6 ⊢ ( 𝜑 → 𝐷 ∈ ℤ )
8 2sqlem4.7 ⊢ ( 𝜑 → ( 𝑁 · 𝑃 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
9 2sqlem4.8 ⊢ ( 𝜑 → 𝑃 = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
10 2 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ) → 𝑁 ∈ ℕ )
11 3 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ) → 𝑃 ∈ ℙ )
12 4 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ) → 𝐴 ∈ ℤ )
13 5 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ) → 𝐵 ∈ ℤ )
14 6 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ) → 𝐶 ∈ ℤ )
15 7 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ) → 𝐷 ∈ ℤ )
16 8 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ) → ( 𝑁 · 𝑃 ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
17 9 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ) → 𝑃 = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ) → 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) )
19 1 10 11 12 13 14 15 16 17 18 2sqlem3 ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ) → 𝑁 ∈ 𝑆 )
20 2 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) → 𝑁 ∈ ℕ )
21 3 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) → 𝑃 ∈ ℙ )
22 4 znegcld ⊢ ( 𝜑 → - 𝐴 ∈ ℤ )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) → - 𝐴 ∈ ℤ )
24 5 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) → 𝐵 ∈ ℤ )
25 6 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) → 𝐶 ∈ ℤ )
26 7 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) → 𝐷 ∈ ℤ )
27 4 zcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
28 sqneg ⊢ ( 𝐴 ∈ ℂ → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
29 27 28 syl ⊢ ( 𝜑 → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
30 29 oveq1d ⊢ ( 𝜑 → ( ( - 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
31 8 30 eqtr4d ⊢ ( 𝜑 → ( 𝑁 · 𝑃 ) = ( ( - 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) → ( 𝑁 · 𝑃 ) = ( ( - 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
33 9 adantr ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) → 𝑃 = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
34 7 zcnd ⊢ ( 𝜑 → 𝐷 ∈ ℂ )
35 27 34 mulneg1d ⊢ ( 𝜑 → ( - 𝐴 · 𝐷 ) = - ( 𝐴 · 𝐷 ) )
36 35 oveq2d ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) + ( - 𝐴 · 𝐷 ) ) = ( ( 𝐶 · 𝐵 ) + - ( 𝐴 · 𝐷 ) ) )
37 6 5 zmulcld ⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℤ )
38 37 zcnd ⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℂ )
39 4 7 zmulcld ⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℤ )
40 39 zcnd ⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℂ )
41 38 40 negsubd ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) + - ( 𝐴 · 𝐷 ) ) = ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) )
42 36 41 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) + ( - 𝐴 · 𝐷 ) ) = ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) )
43 42 breq2d ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( - 𝐴 · 𝐷 ) ) ↔ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) )
44 43 biimpar ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) → 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( - 𝐴 · 𝐷 ) ) )
45 1 20 21 23 24 25 26 32 33 44 2sqlem3 ⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) → 𝑁 ∈ 𝑆 )
46 prmz ⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
47 3 46 syl ⊢ ( 𝜑 → 𝑃 ∈ ℤ )
48 zsqcl ⊢ ( 𝐶 ∈ ℤ → ( 𝐶 ↑ 2 ) ∈ ℤ )
49 6 48 syl ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℤ )
50 2 nnzd ⊢ ( 𝜑 → 𝑁 ∈ ℤ )
51 49 50 zmulcld ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) · 𝑁 ) ∈ ℤ )
52 zsqcl ⊢ ( 𝐴 ∈ ℤ → ( 𝐴 ↑ 2 ) ∈ ℤ )
53 4 52 syl ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℤ )
54 51 53 zsubcld ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) · 𝑁 ) − ( 𝐴 ↑ 2 ) ) ∈ ℤ )
55 dvdsmul1 ⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( ( 𝐶 ↑ 2 ) · 𝑁 ) − ( 𝐴 ↑ 2 ) ) ∈ ℤ ) → 𝑃 ∥ ( 𝑃 · ( ( ( 𝐶 ↑ 2 ) · 𝑁 ) − ( 𝐴 ↑ 2 ) ) ) )
56 47 54 55 syl2anc ⊢ ( 𝜑 → 𝑃 ∥ ( 𝑃 · ( ( ( 𝐶 ↑ 2 ) · 𝑁 ) − ( 𝐴 ↑ 2 ) ) ) )
57 6 4 zmulcld ⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ∈ ℤ )
58 57 zcnd ⊢ ( 𝜑 → ( 𝐶 · 𝐴 ) ∈ ℂ )
59 58 sqcld ⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) ↑ 2 ) ∈ ℂ )
60 38 sqcld ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) ↑ 2 ) ∈ ℂ )
61 40 sqcld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) ↑ 2 ) ∈ ℂ )
62 59 60 61 pnpcand ⊢ ( 𝜑 → ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) − ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) ) = ( ( ( 𝐶 · 𝐵 ) ↑ 2 ) − ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) )
63 6 zcnd ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
64 63 27 sqmuld ⊢ ( 𝜑 → ( ( 𝐶 · 𝐴 ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
65 5 zcnd ⊢ ( 𝜑 → 𝐵 ∈ ℂ )
66 63 65 sqmuld ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
67 64 66 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
68 63 sqcld ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
69 53 zcnd ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
70 65 sqcld ⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
71 68 69 70 adddid ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐶 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) + ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
72 67 71 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) )
73 2 nncnd ⊢ ( 𝜑 → 𝑁 ∈ ℂ )
74 47 zcnd ⊢ ( 𝜑 → 𝑃 ∈ ℂ )
75 73 74 mulcomd ⊢ ( 𝜑 → ( 𝑁 · 𝑃 ) = ( 𝑃 · 𝑁 ) )
76 8 75 eqtr3d ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( 𝑃 · 𝑁 ) )
77 76 oveq2d ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( ( 𝐶 ↑ 2 ) · ( 𝑃 · 𝑁 ) ) )
78 68 74 73 mul12d ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) · ( 𝑃 · 𝑁 ) ) = ( 𝑃 · ( ( 𝐶 ↑ 2 ) · 𝑁 ) ) )
79 77 78 eqtrd ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) · ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) ) = ( 𝑃 · ( ( 𝐶 ↑ 2 ) · 𝑁 ) ) )
80 72 79 eqtrd ⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) = ( 𝑃 · ( ( 𝐶 ↑ 2 ) · 𝑁 ) ) )
81 27 34 sqmuld ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) )
82 34 sqcld ⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
83 69 82 mulcomd ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) = ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
84 81 83 eqtrd ⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) ↑ 2 ) = ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) )
85 64 84 oveq12d ⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
86 49 zcnd ⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
87 86 82 69 adddird ⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) + ( ( 𝐷 ↑ 2 ) · ( 𝐴 ↑ 2 ) ) ) )
88 85 87 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( 𝐴 ↑ 2 ) ) )
89 9 oveq1d ⊢ ( 𝜑 → ( 𝑃 · ( 𝐴 ↑ 2 ) ) = ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) · ( 𝐴 ↑ 2 ) ) )
90 88 89 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) = ( 𝑃 · ( 𝐴 ↑ 2 ) ) )
91 80 90 oveq12d ⊢ ( 𝜑 → ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) − ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) ) = ( ( 𝑃 · ( ( 𝐶 ↑ 2 ) · 𝑁 ) ) − ( 𝑃 · ( 𝐴 ↑ 2 ) ) ) )
92 51 zcnd ⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) · 𝑁 ) ∈ ℂ )
93 74 92 69 subdid ⊢ ( 𝜑 → ( 𝑃 · ( ( ( 𝐶 ↑ 2 ) · 𝑁 ) − ( 𝐴 ↑ 2 ) ) ) = ( ( 𝑃 · ( ( 𝐶 ↑ 2 ) · 𝑁 ) ) − ( 𝑃 · ( 𝐴 ↑ 2 ) ) ) )
94 91 93 eqtr4d ⊢ ( 𝜑 → ( ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) − ( ( ( 𝐶 · 𝐴 ) ↑ 2 ) + ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) ) = ( 𝑃 · ( ( ( 𝐶 ↑ 2 ) · 𝑁 ) − ( 𝐴 ↑ 2 ) ) ) )
95 62 94 eqtr3d ⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐵 ) ↑ 2 ) − ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) = ( 𝑃 · ( ( ( 𝐶 ↑ 2 ) · 𝑁 ) − ( 𝐴 ↑ 2 ) ) ) )
96 subsq ⊢ ( ( ( 𝐶 · 𝐵 ) ∈ ℂ ∧ ( 𝐴 · 𝐷 ) ∈ ℂ ) → ( ( ( 𝐶 · 𝐵 ) ↑ 2 ) − ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) = ( ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) · ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) )
97 38 40 96 syl2anc ⊢ ( 𝜑 → ( ( ( 𝐶 · 𝐵 ) ↑ 2 ) − ( ( 𝐴 · 𝐷 ) ↑ 2 ) ) = ( ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) · ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) )
98 95 97 eqtr3d ⊢ ( 𝜑 → ( 𝑃 · ( ( ( 𝐶 ↑ 2 ) · 𝑁 ) − ( 𝐴 ↑ 2 ) ) ) = ( ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) · ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) )
99 56 98 breqtrd ⊢ ( 𝜑 → 𝑃 ∥ ( ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) · ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) )
100 37 39 zaddcld ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ∈ ℤ )
101 37 39 zsubcld ⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ∈ ℤ )
102 euclemma ⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ∈ ℤ ∧ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) · ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) ↔ ( 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ∨ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) ) )
103 3 100 101 102 syl3anc ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) · ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) ↔ ( 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ∨ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) ) )
104 99 103 mpbid ⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐶 · 𝐵 ) + ( 𝐴 · 𝐷 ) ) ∨ 𝑃 ∥ ( ( 𝐶 · 𝐵 ) − ( 𝐴 · 𝐷 ) ) ) )
105 19 45 104 mpjaodan ⊢ ( 𝜑 → 𝑁 ∈ 𝑆 )