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	$⊢ φ \to P \in ℙ$
	2sqmod.2	$⊢ φ \to A \in ℕ_{0}$
	2sqmod.3	$⊢ φ \to B \in ℕ_{0}$
	2sqmod.4	$⊢ φ \to C \in ℕ_{0}$
	2sqmod.5	$⊢ φ \to D \in ℕ_{0}$
	2sqmod.6	$⊢ φ \to A \leq B$
	2sqmod.7	$⊢ φ \to C \leq D$
	2sqmod.8	$⊢ φ \to A^{2} + B^{2} = P$
	2sqmod.9	$⊢ φ \to C^{2} + D^{2} = P$
Assertion	2sqmod	$⊢ φ \to (A = C \land B = D)$

Proof

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

Metamath Proof Explorer

Theorem 2sqmod

Proof