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	⊢ ( 𝜑 → 𝑁 ∈ 𝑆 )