Theorem 2sqmod

Description: Given two decompositions of a prime as a sum of two squares, show that they are equal. (Contributed by Thierry Arnoux, 2-Feb-2020)

	Ref	Expression
Hypotheses	2sqmod.1	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	2sqmod.2	⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
	2sqmod.3	⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
	2sqmod.4	⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
	2sqmod.5	⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
	2sqmod.6	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
	2sqmod.7	⊢ ( 𝜑 → 𝐶 ≤ 𝐷 )
	2sqmod.8	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 )
	2sqmod.9	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) = 𝑃 )
Assertion	2sqmod	⊢ ( 𝜑 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		2sqmod.1	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
2		2sqmod.2	⊢ ( 𝜑 → 𝐴 ∈ ℕ0 )
3		2sqmod.3	⊢ ( 𝜑 → 𝐵 ∈ ℕ0 )
4		2sqmod.4	⊢ ( 𝜑 → 𝐶 ∈ ℕ0 )
5		2sqmod.5	⊢ ( 𝜑 → 𝐷 ∈ ℕ0 )
6		2sqmod.6	⊢ ( 𝜑 → 𝐴 ≤ 𝐵 )
7		2sqmod.7	⊢ ( 𝜑 → 𝐶 ≤ 𝐷 )
8		2sqmod.8	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = 𝑃 )
9		2sqmod.9	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) = 𝑃 )
10	6	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ≤ 𝐵 )
11	4	nn0red	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐶 ∈ ℝ )
13	3	nn0red	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∈ ℝ )
15	4	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 𝐶 )
16	15	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐶 )
17	3	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 𝐵 )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐵 )
19	4	nn0cnd	⊢ ( 𝜑 → 𝐶 ∈ ℂ )
20	19	sqcld	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℂ )
21	20	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐶 ↑ 2 ) ∈ ℂ )
22	3	nn0cnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
23	22	sqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℂ )
24	23	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
25	2	nn0cnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
26	25	sqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
27	5	nn0cnd	⊢ ( 𝜑 → 𝐷 ∈ ℂ )
28	27	sqcld	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℂ )
29	8 9	eqtr4d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
30	26 23 20 28 29	subaddeqd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
32	2	nn0zd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
33	4	nn0zd	⊢ ( 𝜑 → 𝐶 ∈ ℤ )
34		dvdsmul1	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → 𝐴 ∥ ( 𝐴 · 𝐶 ) )
35	32 33 34	syl2anc	⊢ ( 𝜑 → 𝐴 ∥ ( 𝐴 · 𝐶 ) )
36	35	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ∥ ( 𝐴 · 𝐶 ) )
37	25 19	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℂ )
38	37	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐶 ) ∈ ℂ )
39	22 27	mulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐷 ) ∈ ℂ )
40	39	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 · 𝐷 ) ∈ ℂ )
41	2	nn0red	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
42	41 11	remulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℝ )
43	5	nn0red	⊢ ( 𝜑 → 𝐷 ∈ ℝ )
44	13 43	remulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐷 ) ∈ ℝ )
45	42 44	resubcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ∈ ℝ )
46	45	recnd	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ∈ ℂ )
47	46	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ∈ ℂ )
48	45	sqge0d	⊢ ( 𝜑 → 0 ≤ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) )
49	3	nn0zd	⊢ ( 𝜑 → 𝐵 ∈ ℤ )
50	1 32 49 8	2sqn0	⊢ ( 𝜑 → 𝐴 ≠ 0 )
51		elnnne0	⊢ ( 𝐴 ∈ ℕ ↔ ( 𝐴 ∈ ℕ0 ∧ 𝐴 ≠ 0 ) )
52	2 50 51	sylanbrc	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
53	5	nn0zd	⊢ ( 𝜑 → 𝐷 ∈ ℤ )
54	28 20	addcomd	⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) )
55	54 9	eqtrd	⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) + ( 𝐶 ↑ 2 ) ) = 𝑃 )
56	1 53 33 55	2sqn0	⊢ ( 𝜑 → 𝐷 ≠ 0 )
57		elnnne0	⊢ ( 𝐷 ∈ ℕ ↔ ( 𝐷 ∈ ℕ0 ∧ 𝐷 ≠ 0 ) )
58	5 56 57	sylanbrc	⊢ ( 𝜑 → 𝐷 ∈ ℕ )
59	52 58	nnmulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℕ )
60	1 33 53 9	2sqn0	⊢ ( 𝜑 → 𝐶 ≠ 0 )
61		elnnne0	⊢ ( 𝐶 ∈ ℕ ↔ ( 𝐶 ∈ ℕ0 ∧ 𝐶 ≠ 0 ) )
62	4 60 61	sylanbrc	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
63	23 26	addcomd	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) )
64	63 8	eqtrd	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = 𝑃 )
65	1 49 32 64	2sqn0	⊢ ( 𝜑 → 𝐵 ≠ 0 )
66		elnnne0	⊢ ( 𝐵 ∈ ℕ ↔ ( 𝐵 ∈ ℕ0 ∧ 𝐵 ≠ 0 ) )
67	3 65 66	sylanbrc	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
68	62 67	nnmulcld	⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℕ )
69	59 68	nnaddcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℕ )
70	69	nnsqcld	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℕ )
71	70	nnred	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℝ )
72	45	resqcld	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) ∈ ℝ )
73	71 72	addge02d	⊢ ( 𝜑 → ( 0 ≤ ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) ↔ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) ) )
74	48 73	mpbid	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
75	8 9	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( 𝑃 · 𝑃 ) )
76		bhmafibid1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
77	41 13 11 43 76	syl22anc	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
78	75 77	eqtr3d	⊢ ( 𝜑 → ( 𝑃 · 𝑃 ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
79		prmz	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℤ )
80	1 79	syl	⊢ ( 𝜑 → 𝑃 ∈ ℤ )
81	80	zcnd	⊢ ( 𝜑 → 𝑃 ∈ ℂ )
82	81	sqvald	⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) = ( 𝑃 · 𝑃 ) )
83	19 22	mulcomd	⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) = ( 𝐵 · 𝐶 ) )
84	83	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) = ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) )
85	84	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) )
86	85	oveq2d	⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
87	78 82 86	3eqtr4d	⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
88	74 87	breqtrrd	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( 𝑃 ↑ 2 ) )
89	88	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( 𝑃 ↑ 2 ) )
90	32 53	zmulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℤ )
91	33 49	zmulcld	⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℤ )
92	90 91	zaddcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℤ )
93		dvdssqim	⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
94	80 92 93	syl2anc	⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
95		zsqcl	⊢ ( 𝑃 ∈ ℤ → ( 𝑃 ↑ 2 ) ∈ ℤ )
96	80 95	syl	⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℤ )
97		dvdsle	⊢ ( ( ( 𝑃 ↑ 2 ) ∈ ℤ ∧ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℕ ) → ( ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
98	96 70 97	syl2anc	⊢ ( 𝜑 → ( ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
99	94 98	syld	⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
100	99	imp	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
101	96	zred	⊢ ( 𝜑 → ( 𝑃 ↑ 2 ) ∈ ℝ )
102	71 101	letri3d	⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) = ( 𝑃 ↑ 2 ) ↔ ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( 𝑃 ↑ 2 ) ∧ ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) ) )
103	102	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) = ( 𝑃 ↑ 2 ) ↔ ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ≤ ( 𝑃 ↑ 2 ) ∧ ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) ) )
104	89 100 103	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) = ( 𝑃 ↑ 2 ) )
105	87	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 ↑ 2 ) = ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
106	104 105	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
107	71	recnd	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℂ )
108	72	recnd	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) ∈ ℂ )
109	107 107 108	subadd2d	⊢ ( 𝜑 → ( ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) − ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) ↔ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
110	109	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) − ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) ↔ ( ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
111	106 110	mpbird	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) − ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) )
112	107	subidd	⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) − ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = 0 )
113	112	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) − ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = 0 )
114	111 113	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) ↑ 2 ) = 0 )
115	47 114	sqeq0d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 · 𝐶 ) − ( 𝐵 · 𝐷 ) ) = 0 )
116	38 40 115	subeq0d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐶 ) = ( 𝐵 · 𝐷 ) )
117	36 116	breqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ∥ ( 𝐵 · 𝐷 ) )
118	1 32 49 8	2sqcoprm	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = 1 )
119	118	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 gcd 𝐵 ) = 1 )
120		coprmdvds	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → ( ( 𝐴 ∥ ( 𝐵 · 𝐷 ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐴 ∥ 𝐷 ) )
121	32 49 53 120	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 ∥ ( 𝐵 · 𝐷 ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐴 ∥ 𝐷 ) )
122	121	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 ∥ ( 𝐵 · 𝐷 ) ∧ ( 𝐴 gcd 𝐵 ) = 1 ) → 𝐴 ∥ 𝐷 ) )
123	117 119 122	mp2and	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ∥ 𝐷 )
124		dvdsle	⊢ ( ( 𝐴 ∈ ℤ ∧ 𝐷 ∈ ℕ ) → ( 𝐴 ∥ 𝐷 → 𝐴 ≤ 𝐷 ) )
125	32 58 124	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∥ 𝐷 → 𝐴 ≤ 𝐷 ) )
126	125	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 ∥ 𝐷 → 𝐴 ≤ 𝐷 ) )
127	123 126	mpd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ≤ 𝐷 )
128	52	nnrpd	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
129	128	rprege0d	⊢ ( 𝜑 → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
130	5	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 𝐷 )
131		le2sq	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝐷 ∈ ℝ ∧ 0 ≤ 𝐷 ) ) → ( 𝐴 ≤ 𝐷 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) ) )
132	129 43 130 131	syl12anc	⊢ ( 𝜑 → ( 𝐴 ≤ 𝐷 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) ) )
133	132	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 ≤ 𝐷 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) ) )
134	127 133	mpbid	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) )
135	52	nnsqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℕ )
136	135	nnred	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℝ )
137		zsqcl	⊢ ( 𝐷 ∈ ℤ → ( 𝐷 ↑ 2 ) ∈ ℤ )
138	53 137	syl	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℤ )
139	138	zred	⊢ ( 𝜑 → ( 𝐷 ↑ 2 ) ∈ ℝ )
140	136 139	suble0d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ≤ 0 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) ) )
141	140	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ≤ 0 ↔ ( 𝐴 ↑ 2 ) ≤ ( 𝐷 ↑ 2 ) ) )
142	134 141	mpbird	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ≤ 0 )
143	31 142	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ≤ 0 )
144		dvdsmul1	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐷 ∈ ℤ ) → 𝐵 ∥ ( 𝐵 · 𝐷 ) )
145	49 53 144	syl2anc	⊢ ( 𝜑 → 𝐵 ∥ ( 𝐵 · 𝐷 ) )
146	145	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∥ ( 𝐵 · 𝐷 ) )
147	146 116	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∥ ( 𝐴 · 𝐶 ) )
148	32 49	gcdcomd	⊢ ( 𝜑 → ( 𝐴 gcd 𝐵 ) = ( 𝐵 gcd 𝐴 ) )
149	148 118	eqtr3d	⊢ ( 𝜑 → ( 𝐵 gcd 𝐴 ) = 1 )
150	149	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 gcd 𝐴 ) = 1 )
151		coprmdvds	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝐶 ∈ ℤ ) → ( ( 𝐵 ∥ ( 𝐴 · 𝐶 ) ∧ ( 𝐵 gcd 𝐴 ) = 1 ) → 𝐵 ∥ 𝐶 ) )
152	49 32 33 151	syl3anc	⊢ ( 𝜑 → ( ( 𝐵 ∥ ( 𝐴 · 𝐶 ) ∧ ( 𝐵 gcd 𝐴 ) = 1 ) → 𝐵 ∥ 𝐶 ) )
153	152	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐵 ∥ ( 𝐴 · 𝐶 ) ∧ ( 𝐵 gcd 𝐴 ) = 1 ) → 𝐵 ∥ 𝐶 ) )
154	147 150 153	mp2and	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∥ 𝐶 )
155		dvdsle	⊢ ( ( 𝐵 ∈ ℤ ∧ 𝐶 ∈ ℕ ) → ( 𝐵 ∥ 𝐶 → 𝐵 ≤ 𝐶 ) )
156	49 62 155	syl2anc	⊢ ( 𝜑 → ( 𝐵 ∥ 𝐶 → 𝐵 ≤ 𝐶 ) )
157	156	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 ∥ 𝐶 → 𝐵 ≤ 𝐶 ) )
158	154 157	mpd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐵 ≤ 𝐶 )
159	13 11 17 15	le2sqd	⊢ ( 𝜑 → ( 𝐵 ≤ 𝐶 ↔ ( 𝐵 ↑ 2 ) ≤ ( 𝐶 ↑ 2 ) ) )
160	159	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 ≤ 𝐶 ↔ ( 𝐵 ↑ 2 ) ≤ ( 𝐶 ↑ 2 ) ) )
161	158 160	mpbid	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 ↑ 2 ) ≤ ( 𝐶 ↑ 2 ) )
162	11	resqcld	⊢ ( 𝜑 → ( 𝐶 ↑ 2 ) ∈ ℝ )
163		zsqcl	⊢ ( 𝐵 ∈ ℤ → ( 𝐵 ↑ 2 ) ∈ ℤ )
164	49 163	syl	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℤ )
165	164	zred	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℝ )
166	162 165	subge0d	⊢ ( 𝜑 → ( 0 ≤ ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ↔ ( 𝐵 ↑ 2 ) ≤ ( 𝐶 ↑ 2 ) ) )
167	166	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 0 ≤ ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ↔ ( 𝐵 ↑ 2 ) ≤ ( 𝐶 ↑ 2 ) ) )
168	161 167	mpbird	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) )
169	136 139	resubcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ∈ ℝ )
170	30 169	eqeltrrd	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℝ )
171		0red	⊢ ( 𝜑 → 0 ∈ ℝ )
172	170 171	letri3d	⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
173	172	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ↔ ( ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) ) )
174	143 168 173	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐶 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 )
175	21 24 174	subeq0d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐶 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
176	12 14 16 18 175	sq11d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐶 = 𝐵 )
177	10 176	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ≤ 𝐶 )
178	7	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐶 ≤ 𝐷 )
179	41	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 ∈ ℝ )
180	43	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐷 ∈ ℝ )
181	2	nn0ge0d	⊢ ( 𝜑 → 0 ≤ 𝐴 )
182	181	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐴 )
183	130	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐷 )
184	26	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 ↑ 2 ) ∈ ℂ )
185	28	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐷 ↑ 2 ) ∈ ℂ )
186	168 31	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 0 ≤ ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) )
187	169 171	letri3d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = 0 ↔ ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ) ) )
188	187	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = 0 ↔ ( ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ≤ 0 ∧ 0 ≤ ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) ) ) )
189	142 186 188	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 ↑ 2 ) − ( 𝐷 ↑ 2 ) ) = 0 )
190	184 185 189	subeq0d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 ↑ 2 ) = ( 𝐷 ↑ 2 ) )
191	179 180 182 183 190	sq11d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 = 𝐷 )
192	178 191	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐶 ≤ 𝐴 )
193	41 11	letri3d	⊢ ( 𝜑 → ( 𝐴 = 𝐶 ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) ) )
194	193	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 = 𝐶 ↔ ( 𝐴 ≤ 𝐶 ∧ 𝐶 ≤ 𝐴 ) ) )
195	177 192 194	mpbir2and	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ) → 𝐴 = 𝐶 )
196	25	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐴 ∈ ℂ )
197	19	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐶 ∈ ℂ )
198	22	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∈ ℂ )
199	65	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐵 ≠ 0 )
200	43	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐷 ∈ ℝ )
201	13	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐵 ∈ ℝ )
202	130	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐷 )
203	17	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 0 ≤ 𝐵 )
204	28	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐷 ↑ 2 ) ∈ ℂ )
205	23	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
206		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
207	1 206	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
208	207	nnne0d	⊢ ( 𝜑 → 𝑃 ≠ 0 )
209	208	neneqd	⊢ ( 𝜑 → ¬ 𝑃 = 0 )
210	209	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ¬ 𝑃 = 0 )
211	81 28 23	subdid	⊢ ( 𝜑 → ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = ( ( 𝑃 · ( 𝐷 ↑ 2 ) ) − ( 𝑃 · ( 𝐵 ↑ 2 ) ) ) )
212	81 28	mulcld	⊢ ( 𝜑 → ( 𝑃 · ( 𝐷 ↑ 2 ) ) ∈ ℂ )
213	26 28	mulcld	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ∈ ℂ )
214	81 23	mulcld	⊢ ( 𝜑 → ( 𝑃 · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
215	20 23	mulcld	⊢ ( 𝜑 → ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ∈ ℂ )
216	23 28	mulcomd	⊢ ( 𝜑 → ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) = ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
217	8	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐴 ↑ 2 ) ) = ( 𝑃 − ( 𝐴 ↑ 2 ) ) )
218	26 23	pncan2d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) − ( 𝐴 ↑ 2 ) ) = ( 𝐵 ↑ 2 ) )
219	217 218	eqtr3d	⊢ ( 𝜑 → ( 𝑃 − ( 𝐴 ↑ 2 ) ) = ( 𝐵 ↑ 2 ) )
220	219	oveq1d	⊢ ( 𝜑 → ( ( 𝑃 − ( 𝐴 ↑ 2 ) ) · ( 𝐷 ↑ 2 ) ) = ( ( 𝐵 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) )
221	9	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( 𝐶 ↑ 2 ) ) = ( 𝑃 − ( 𝐶 ↑ 2 ) ) )
222	20 28	pncan2d	⊢ ( 𝜑 → ( ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) − ( 𝐶 ↑ 2 ) ) = ( 𝐷 ↑ 2 ) )
223	221 222	eqtr3d	⊢ ( 𝜑 → ( 𝑃 − ( 𝐶 ↑ 2 ) ) = ( 𝐷 ↑ 2 ) )
224	223	oveq1d	⊢ ( 𝜑 → ( ( 𝑃 − ( 𝐶 ↑ 2 ) ) · ( 𝐵 ↑ 2 ) ) = ( ( 𝐷 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
225	216 220 224	3eqtr4d	⊢ ( 𝜑 → ( ( 𝑃 − ( 𝐴 ↑ 2 ) ) · ( 𝐷 ↑ 2 ) ) = ( ( 𝑃 − ( 𝐶 ↑ 2 ) ) · ( 𝐵 ↑ 2 ) ) )
226	81 26 28	subdird	⊢ ( 𝜑 → ( ( 𝑃 − ( 𝐴 ↑ 2 ) ) · ( 𝐷 ↑ 2 ) ) = ( ( 𝑃 · ( 𝐷 ↑ 2 ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) )
227	81 20 23	subdird	⊢ ( 𝜑 → ( ( 𝑃 − ( 𝐶 ↑ 2 ) ) · ( 𝐵 ↑ 2 ) ) = ( ( 𝑃 · ( 𝐵 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
228	225 226 227	3eqtr3d	⊢ ( 𝜑 → ( ( 𝑃 · ( 𝐷 ↑ 2 ) ) − ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) ) = ( ( 𝑃 · ( 𝐵 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
229	212 213 214 215 228	subeqxfrd	⊢ ( 𝜑 → ( ( 𝑃 · ( 𝐷 ↑ 2 ) ) − ( 𝑃 · ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
230	211 229	eqtrd	⊢ ( 𝜑 → ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
231	25 27	sqmuld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) ↑ 2 ) = ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) )
232	19 22	sqmuld	⊢ ( 𝜑 → ( ( 𝐶 · 𝐵 ) ↑ 2 ) = ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) )
233	231 232	oveq12d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) − ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 ↑ 2 ) · ( 𝐷 ↑ 2 ) ) − ( ( 𝐶 ↑ 2 ) · ( 𝐵 ↑ 2 ) ) ) )
234	25 27	mulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℂ )
235	19 22	mulcld	⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℂ )
236		subsq	⊢ ( ( ( 𝐴 · 𝐷 ) ∈ ℂ ∧ ( 𝐶 · 𝐵 ) ∈ ℂ ) → ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) − ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
237	234 235 236	syl2anc	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) ↑ 2 ) − ( ( 𝐶 · 𝐵 ) ↑ 2 ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
238	230 233 237	3eqtr2d	⊢ ( 𝜑 → ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
239	238	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
240	234	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
241		simpll	⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → 𝜑 )
242		simpr	⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) )
243	242	neqned	⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) )
244	90 91	zsubcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ∈ ℤ )
245		dvdssqim	⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
246	80 244 245	syl2anc	⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
247	246	imp	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
248	247	adantr	⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
249	96	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ∈ ℤ )
250	244	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ∈ ℤ )
251	234	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( 𝐴 · 𝐷 ) ∈ ℂ )
252	235	adantr	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
253		simpr	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) )
254	251 252 253	subne0d	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ≠ 0 )
255	250 254	znsqcld	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℕ )
256		dvdsle	⊢ ( ( ( 𝑃 ↑ 2 ) ∈ ℤ ∧ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℕ ) → ( ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
257	249 255 256	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) → ( ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
258	257	imp	⊢ ( ( ( 𝜑 ∧ ( 𝐴 · 𝐷 ) ≠ ( 𝐶 · 𝐵 ) ) ∧ ( 𝑃 ↑ 2 ) ∥ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
259	241 243 248 258	syl21anc	⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
260	41 43	remulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐷 ) ∈ ℝ )
261	11 13	remulcld	⊢ ( 𝜑 → ( 𝐶 · 𝐵 ) ∈ ℝ )
262	260 261	resubcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ∈ ℝ )
263	262	resqcld	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ∈ ℝ )
264	62	nnrpd	⊢ ( 𝜑 → 𝐶 ∈ ℝ+ )
265	128 264	rpmulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐶 ) ∈ ℝ+ )
266	67	nnrpd	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
267	58	nnrpd	⊢ ( 𝜑 → 𝐷 ∈ ℝ+ )
268	266 267	rpmulcld	⊢ ( 𝜑 → ( 𝐵 · 𝐷 ) ∈ ℝ+ )
269	265 268	rpaddcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ∈ ℝ+ )
270		2z	⊢ 2 ∈ ℤ
271	270	a1i	⊢ ( 𝜑 → 2 ∈ ℤ )
272	269 271	rpexpcld	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) ∈ ℝ+ )
273	263 272	ltaddrp2d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
274		bhmafibid2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) ∧ ( 𝐶 ∈ ℝ ∧ 𝐷 ∈ ℝ ) ) → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
275	41 13 11 43 274	syl22anc	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) + ( 𝐵 ↑ 2 ) ) · ( ( 𝐶 ↑ 2 ) + ( 𝐷 ↑ 2 ) ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
276	75 275	eqtr3d	⊢ ( 𝜑 → ( 𝑃 · 𝑃 ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
277	83	oveq2d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) = ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) )
278	277	oveq1d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) = ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) )
279	278	oveq2d	⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐵 · 𝐶 ) ) ↑ 2 ) ) )
280	276 279	eqtr4d	⊢ ( 𝜑 → ( 𝑃 · 𝑃 ) = ( ( ( ( 𝐴 · 𝐶 ) + ( 𝐵 · 𝐷 ) ) ↑ 2 ) + ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
281	273 280	breqtrrd	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( 𝑃 · 𝑃 ) )
282	281 82	breqtrrd	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( 𝑃 ↑ 2 ) )
283	241 282	syl	⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( 𝑃 ↑ 2 ) )
284	263 101	ltnled	⊢ ( 𝜑 → ( ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( 𝑃 ↑ 2 ) ↔ ¬ ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
285	241 284	syl	⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ( ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) < ( 𝑃 ↑ 2 ) ↔ ¬ ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) ) )
286	283 285	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ∧ ¬ ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) ) → ¬ ( 𝑃 ↑ 2 ) ≤ ( ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ↑ 2 ) )
287	259 286	condan	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐷 ) = ( 𝐶 · 𝐵 ) )
288	240 287	subeq0bd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) = 0 )
289	288	oveq2d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) = ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · 0 ) )
290	234 235	addcld	⊢ ( 𝜑 → ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℂ )
291	290	mul01d	⊢ ( 𝜑 → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · 0 ) = 0 )
292	291	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · 0 ) = 0 )
293	239 289 292	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = 0 )
294	28 23	subcld	⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℂ )
295	81 294	mul0ord	⊢ ( 𝜑 → ( ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = 0 ↔ ( 𝑃 = 0 ∨ ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ) ) )
296	295	adantr	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) = 0 ↔ ( 𝑃 = 0 ∨ ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ) ) )
297	293 296	mpbid	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝑃 = 0 ∨ ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ) )
298	297	ord	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ¬ 𝑃 = 0 → ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 ) )
299	210 298	mpd	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) = 0 )
300	204 205 299	subeq0d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐷 ↑ 2 ) = ( 𝐵 ↑ 2 ) )
301	200 201 202 203 300	sq11d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐷 = 𝐵 )
302	301	oveq2d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐷 ) = ( 𝐴 · 𝐵 ) )
303	302 287	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → ( 𝐴 · 𝐵 ) = ( 𝐶 · 𝐵 ) )
304	196 197 198 199 303	mulcan2ad	⊢ ( ( 𝜑 ∧ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) → 𝐴 = 𝐶 )
305	138 164	zsubcld	⊢ ( 𝜑 → ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℤ )
306		dvdsmul1	⊢ ( ( 𝑃 ∈ ℤ ∧ ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ∈ ℤ ) → 𝑃 ∥ ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
307	80 305 306	syl2anc	⊢ ( 𝜑 → 𝑃 ∥ ( 𝑃 · ( ( 𝐷 ↑ 2 ) − ( 𝐵 ↑ 2 ) ) ) )
308	307 238	breqtrd	⊢ ( 𝜑 → 𝑃 ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
309		euclemma	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∈ ℤ ∧ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ∈ ℤ ) → ( 𝑃 ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ↔ ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∨ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ) )
310	1 92 244 309	syl3anc	⊢ ( 𝜑 → ( 𝑃 ∥ ( ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) · ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ↔ ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∨ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) ) )
311	308 310	mpbid	⊢ ( 𝜑 → ( 𝑃 ∥ ( ( 𝐴 · 𝐷 ) + ( 𝐶 · 𝐵 ) ) ∨ 𝑃 ∥ ( ( 𝐴 · 𝐷 ) − ( 𝐶 · 𝐵 ) ) ) )
312	195 304 311	mpjaodan	⊢ ( 𝜑 → 𝐴 = 𝐶 )
313	312	oveq1d	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = ( 𝐶 ↑ 2 ) )
314	313	oveq2d	⊢ ( 𝜑 → ( 𝑃 − ( 𝐴 ↑ 2 ) ) = ( 𝑃 − ( 𝐶 ↑ 2 ) ) )
315	314 219 223	3eqtr3d	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) = ( 𝐷 ↑ 2 ) )
316	13 43 17 130 315	sq11d	⊢ ( 𝜑 → 𝐵 = 𝐷 )
317	312 316	jca	⊢ ( 𝜑 → ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐷 ) )