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		gcdcom	$⊢ (A \in ℤ \land B \in ℤ) \to A \gcd B = B \gcd A$
149	32 49 148	syl2anc	$⊢ φ \to A \gcd B = B \gcd A$
150	149 118	eqtr3d	$⊢ φ \to B \gcd A = 1$
151	150	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to B \gcd A = 1$
152		coprmdvds	$⊢ (B \in ℤ \land A \in ℤ \land C \in ℤ) \to ((B ∥ A C \land B \gcd A = 1) \to B ∥ C)$
153	49 32 33 152	syl3anc	$⊢ φ \to ((B ∥ A C \land B \gcd A = 1) \to B ∥ C)$
154	153	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to ((B ∥ A C \land B \gcd A = 1) \to B ∥ C)$
155	147 151 154	mp2and	$⊢ (φ \land P ∥ (A D + C B)) \to B ∥ C$
156		dvdsle	$⊢ (B \in ℤ \land C \in ℕ) \to (B ∥ C \to B \leq C)$
157	49 62 156	syl2anc	$⊢ φ \to (B ∥ C \to B \leq C)$
158	157	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to (B ∥ C \to B \leq C)$
159	155 158	mpd	$⊢ (φ \land P ∥ (A D + C B)) \to B \leq C$
160	13 11 17 15	le2sqd	$⊢ φ \to (B \leq C \leftrightarrow B^{2} \leq C^{2})$
161	160	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to (B \leq C \leftrightarrow B^{2} \leq C^{2})$
162	159 161	mpbid	$⊢ (φ \land P ∥ (A D + C B)) \to B^{2} \leq C^{2}$
163	11	resqcld	$⊢ φ \to C^{2} \in ℝ$
164		zsqcl	$⊢ B \in ℤ \to B^{2} \in ℤ$
165	49 164	syl	$⊢ φ \to B^{2} \in ℤ$
166	165	zred	$⊢ φ \to B^{2} \in ℝ$
167	163 166	subge0d	$⊢ φ \to (0 \leq C^{2} - B^{2} \leftrightarrow B^{2} \leq C^{2})$
168	167	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to (0 \leq C^{2} - B^{2} \leftrightarrow B^{2} \leq C^{2})$
169	162 168	mpbird	$⊢ (φ \land P ∥ (A D + C B)) \to 0 \leq C^{2} - B^{2}$
170	136 139	resubcld	$⊢ φ \to A^{2} - D^{2} \in ℝ$
171	30 170	eqeltrrd	$⊢ φ \to C^{2} - B^{2} \in ℝ$
172		0red	$⊢ φ \to 0 \in ℝ$
173	171 172	letri3d	$⊢ φ \to (C^{2} - B^{2} = 0 \leftrightarrow (C^{2} - B^{2} \leq 0 \land 0 \leq C^{2} - B^{2}))$
174	173	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}))$
175	143 169 174	mpbir2and	$⊢ (φ \land P ∥ (A D + C B)) \to C^{2} - B^{2} = 0$
176	21 24 175	subeq0d	$⊢ (φ \land P ∥ (A D + C B)) \to C^{2} = B^{2}$
177	12 14 16 18 176	sq11d	$⊢ (φ \land P ∥ (A D + C B)) \to C = B$
178	10 177	breqtrrd	$⊢ (φ \land P ∥ (A D + C B)) \to A \leq C$
179	7	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to C \leq D$
180	41	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to A \in ℝ$
181	43	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to D \in ℝ$
182	2	nn0ge0d	$⊢ φ \to 0 \leq A$
183	182	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to 0 \leq A$
184	130	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to 0 \leq D$
185	26	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to A^{2} \in ℂ$
186	28	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to D^{2} \in ℂ$
187	169 31	breqtrrd	$⊢ (φ \land P ∥ (A D + C B)) \to 0 \leq A^{2} - D^{2}$
188	170 172	letri3d	$⊢ φ \to (A^{2} - D^{2} = 0 \leftrightarrow (A^{2} - D^{2} \leq 0 \land 0 \leq A^{2} - D^{2}))$
189	188	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}))$
190	142 187 189	mpbir2and	$⊢ (φ \land P ∥ (A D + C B)) \to A^{2} - D^{2} = 0$
191	185 186 190	subeq0d	$⊢ (φ \land P ∥ (A D + C B)) \to A^{2} = D^{2}$
192	180 181 183 184 191	sq11d	$⊢ (φ \land P ∥ (A D + C B)) \to A = D$
193	179 192	breqtrrd	$⊢ (φ \land P ∥ (A D + C B)) \to C \leq A$
194	41 11	letri3d	$⊢ φ \to (A = C \leftrightarrow (A \leq C \land C \leq A))$
195	194	adantr	$⊢ (φ \land P ∥ (A D + C B)) \to (A = C \leftrightarrow (A \leq C \land C \leq A))$
196	178 193 195	mpbir2and	$⊢ (φ \land P ∥ (A D + C B)) \to A = C$
197	25	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to A \in ℂ$
198	19	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to C \in ℂ$
199	22	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to B \in ℂ$
200	65	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to B \neq 0$
201	43	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to D \in ℝ$
202	13	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to B \in ℝ$
203	130	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to 0 \leq D$
204	17	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to 0 \leq B$
205	28	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to D^{2} \in ℂ$
206	23	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to B^{2} \in ℂ$
207		prmnn	$⊢ P \in ℙ \to P \in ℕ$
208	1 207	syl	$⊢ φ \to P \in ℕ$
209	208	nnne0d	$⊢ φ \to P \neq 0$
210	209	neneqd	$⊢ φ \to \neg P = 0$
211	210	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to \neg P = 0$
212	81 28 23	subdid	$⊢ φ \to P (D^{2} - B^{2}) = P D^{2} - P B^{2}$
213	81 28	mulcld	$⊢ φ \to P D^{2} \in ℂ$
214	26 28	mulcld	$⊢ φ \to A^{2} D^{2} \in ℂ$
215	81 23	mulcld	$⊢ φ \to P B^{2} \in ℂ$
216	20 23	mulcld	$⊢ φ \to C^{2} B^{2} \in ℂ$
217	23 28	mulcomd	$⊢ φ \to B^{2} D^{2} = D^{2} B^{2}$
218	8	oveq1d	$⊢ φ \to A^{2} + B^{2} - A^{2} = P - A^{2}$
219	26 23	pncan2d	$⊢ φ \to A^{2} + B^{2} - A^{2} = B^{2}$
220	218 219	eqtr3d	$⊢ φ \to P - A^{2} = B^{2}$
221	220	oveq1d	$⊢ φ \to (P - A^{2}) D^{2} = B^{2} D^{2}$
222	9	oveq1d	$⊢ φ \to C^{2} + D^{2} - C^{2} = P - C^{2}$
223	20 28	pncan2d	$⊢ φ \to C^{2} + D^{2} - C^{2} = D^{2}$
224	222 223	eqtr3d	$⊢ φ \to P - C^{2} = D^{2}$
225	224	oveq1d	$⊢ φ \to (P - C^{2}) B^{2} = D^{2} B^{2}$
226	217 221 225	3eqtr4d	$⊢ φ \to (P - A^{2}) D^{2} = (P - C^{2}) B^{2}$
227	81 26 28	subdird	$⊢ φ \to (P - A^{2}) D^{2} = P D^{2} - A^{2} D^{2}$
228	81 20 23	subdird	$⊢ φ \to (P - C^{2}) B^{2} = P B^{2} - C^{2} B^{2}$
229	226 227 228	3eqtr3d	$⊢ φ \to P D^{2} - A^{2} D^{2} = P B^{2} - C^{2} B^{2}$
230	213 214 215 216 229	subeqxfrd	$⊢ φ \to P D^{2} - P B^{2} = A^{2} D^{2} - C^{2} B^{2}$
231	212 230	eqtrd	$⊢ φ \to P (D^{2} - B^{2}) = A^{2} D^{2} - C^{2} B^{2}$
232	25 27	sqmuld	$⊢ φ \to {A D}^{2} = A^{2} D^{2}$
233	19 22	sqmuld	$⊢ φ \to {C B}^{2} = C^{2} B^{2}$
234	232 233	oveq12d	$⊢ φ \to {A D}^{2} - {C B}^{2} = A^{2} D^{2} - C^{2} B^{2}$
235	25 27	mulcld	$⊢ φ \to A D \in ℂ$
236	19 22	mulcld	$⊢ φ \to C B \in ℂ$
237		subsq	$⊢ (A D \in ℂ \land C B \in ℂ) \to {A D}^{2} - {C B}^{2} = (A D + C B) (A D - C B)$
238	235 236 237	syl2anc	$⊢ φ \to {A D}^{2} - {C B}^{2} = (A D + C B) (A D - C B)$
239	231 234 238	3eqtr2d	$⊢ φ \to P (D^{2} - B^{2}) = (A D + C B) (A D - C B)$
240	239	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to P (D^{2} - B^{2}) = (A D + C B) (A D - C B)$
241	235	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to A D \in ℂ$
242		simpll	$⊢ ((φ \land P ∥ (A D - C B)) \land \neg A D = C B) \to φ$
243		simpr	$⊢ ((φ \land P ∥ (A D - C B)) \land \neg A D = C B) \to \neg A D = C B$
244	243	neqned	$⊢ ((φ \land P ∥ (A D - C B)) \land \neg A D = C B) \to A D \neq C B$
245	90 91	zsubcld	$⊢ φ \to A D - C B \in ℤ$
246		dvdssqim	$⊢ (P \in ℤ \land A D - C B \in ℤ) \to (P ∥ (A D - C B) \to P^{2} ∥ {(A D - C B)}^{2})$
247	80 245 246	syl2anc	$⊢ φ \to (P ∥ (A D - C B) \to P^{2} ∥ {(A D - C B)}^{2})$
248	247	imp	$⊢ (φ \land P ∥ (A D - C B)) \to P^{2} ∥ {(A D - C B)}^{2}$
249	248	adantr	$⊢ ((φ \land P ∥ (A D - C B)) \land \neg A D = C B) \to P^{2} ∥ {(A D - C B)}^{2}$
250	96	adantr	$⊢ (φ \land A D \neq C B) \to P^{2} \in ℤ$
251	245	adantr	$⊢ (φ \land A D \neq C B) \to A D - C B \in ℤ$
252	235	adantr	$⊢ (φ \land A D \neq C B) \to A D \in ℂ$
253	236	adantr	$⊢ (φ \land A D \neq C B) \to C B \in ℂ$
254		simpr	$⊢ (φ \land A D \neq C B) \to A D \neq C B$
255	252 253 254	subne0d	$⊢ (φ \land A D \neq C B) \to A D - C B \neq 0$
256	251 255	znsqcld	$⊢ (φ \land A D \neq C B) \to {(A D - C B)}^{2} \in ℕ$
257		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})$
258	250 256 257	syl2anc	$⊢ (φ \land A D \neq C B) \to (P^{2} ∥ {(A D - C B)}^{2} \to P^{2} \leq {(A D - C B)}^{2})$
259	258	imp	$⊢ ((φ \land A D \neq C B) \land P^{2} ∥ {(A D - C B)}^{2}) \to P^{2} \leq {(A D - C B)}^{2}$
260	242 244 249 259	syl21anc	$⊢ ((φ \land P ∥ (A D - C B)) \land \neg A D = C B) \to P^{2} \leq {(A D - C B)}^{2}$
261	41 43	remulcld	$⊢ φ \to A D \in ℝ$
262	11 13	remulcld	$⊢ φ \to C B \in ℝ$
263	261 262	resubcld	$⊢ φ \to A D - C B \in ℝ$
264	263	resqcld	$⊢ φ \to {(A D - C B)}^{2} \in ℝ$
265	62	nnrpd	$⊢ φ \to C \in ℝ^{+}$
266	128 265	rpmulcld	$⊢ φ \to A C \in ℝ^{+}$
267	67	nnrpd	$⊢ φ \to B \in ℝ^{+}$
268	58	nnrpd	$⊢ φ \to D \in ℝ^{+}$
269	267 268	rpmulcld	$⊢ φ \to B D \in ℝ^{+}$
270	266 269	rpaddcld	$⊢ φ \to A C + B D \in ℝ^{+}$
271		2z	$⊢ 2 \in ℤ$
272	271	a1i	$⊢ φ \to 2 \in ℤ$
273	270 272	rpexpcld	$⊢ φ \to {(A C + B D)}^{2} \in ℝ^{+}$
274	264 273	ltaddrp2d	$⊢ φ \to {(A D - C B)}^{2} < {(A C + B D)}^{2} + {(A D - C B)}^{2}$
275		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}$
276	41 13 11 43 275	syl22anc	$⊢ φ \to (A^{2} + B^{2}) (C^{2} + D^{2}) = {(A C + B D)}^{2} + {(A D - B C)}^{2}$
277	75 276	eqtr3d	$⊢ φ \to P P = {(A C + B D)}^{2} + {(A D - B C)}^{2}$
278	83	oveq2d	$⊢ φ \to A D - C B = A D - B C$
279	278	oveq1d	$⊢ φ \to {(A D - C B)}^{2} = {(A D - B C)}^{2}$
280	279	oveq2d	$⊢ φ \to {(A C + B D)}^{2} + {(A D - C B)}^{2} = {(A C + B D)}^{2} + {(A D - B C)}^{2}$
281	277 280	eqtr4d	$⊢ φ \to P P = {(A C + B D)}^{2} + {(A D - C B)}^{2}$
282	274 281	breqtrrd	$⊢ φ \to {(A D - C B)}^{2} < P P$
283	282 82	breqtrrd	$⊢ φ \to {(A D - C B)}^{2} < P^{2}$
284	242 283	syl	$⊢ ((φ \land P ∥ (A D - C B)) \land \neg A D = C B) \to {(A D - C B)}^{2} < P^{2}$
285	264 101	ltnled	$⊢ φ \to ({(A D - C B)}^{2} < P^{2} \leftrightarrow \neg P^{2} \leq {(A D - C B)}^{2})$
286	242 285	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})$
287	284 286	mpbid	$⊢ ((φ \land P ∥ (A D - C B)) \land \neg A D = C B) \to \neg P^{2} \leq {(A D - C B)}^{2}$
288	260 287	condan	$⊢ (φ \land P ∥ (A D - C B)) \to A D = C B$
289	241 288	subeq0bd	$⊢ (φ \land P ∥ (A D - C B)) \to A D - C B = 0$
290	289	oveq2d	$⊢ (φ \land P ∥ (A D - C B)) \to (A D + C B) (A D - C B) = (A D + C B) \cdot 0$
291	235 236	addcld	$⊢ φ \to A D + C B \in ℂ$
292	291	mul01d	$⊢ φ \to (A D + C B) \cdot 0 = 0$
293	292	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to (A D + C B) \cdot 0 = 0$
294	240 290 293	3eqtrd	$⊢ (φ \land P ∥ (A D - C B)) \to P (D^{2} - B^{2}) = 0$
295	28 23	subcld	$⊢ φ \to D^{2} - B^{2} \in ℂ$
296	81 295	mul0ord	$⊢ φ \to (P (D^{2} - B^{2}) = 0 \leftrightarrow (P = 0 \lor D^{2} - B^{2} = 0))$
297	296	adantr	$⊢ (φ \land P ∥ (A D - C B)) \to (P (D^{2} - B^{2}) = 0 \leftrightarrow (P = 0 \lor D^{2} - B^{2} = 0))$
298	294 297	mpbid	$⊢ (φ \land P ∥ (A D - C B)) \to (P = 0 \lor D^{2} - B^{2} = 0)$
299	298	ord	$⊢ (φ \land P ∥ (A D - C B)) \to (\neg P = 0 \to D^{2} - B^{2} = 0)$
300	211 299	mpd	$⊢ (φ \land P ∥ (A D - C B)) \to D^{2} - B^{2} = 0$
301	205 206 300	subeq0d	$⊢ (φ \land P ∥ (A D - C B)) \to D^{2} = B^{2}$
302	201 202 203 204 301	sq11d	$⊢ (φ \land P ∥ (A D - C B)) \to D = B$
303	302	oveq2d	$⊢ (φ \land P ∥ (A D - C B)) \to A D = A B$
304	303 288	eqtr3d	$⊢ (φ \land P ∥ (A D - C B)) \to A B = C B$
305	197 198 199 200 304	mulcan2ad	$⊢ (φ \land P ∥ (A D - C B)) \to A = C$
306	138 165	zsubcld	$⊢ φ \to D^{2} - B^{2} \in ℤ$
307		dvdsmul1	$⊢ (P \in ℤ \land D^{2} - B^{2} \in ℤ) \to P ∥ P (D^{2} - B^{2})$
308	80 306 307	syl2anc	$⊢ φ \to P ∥ P (D^{2} - B^{2})$
309	308 239	breqtrd	$⊢ φ \to P ∥ (A D + C B) (A D - C B)$
310		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)))$
311	1 92 245 310	syl3anc	$⊢ φ \to (P ∥ (A D + C B) (A D - C B) \leftrightarrow (P ∥ (A D + C B) \lor P ∥ (A D - C B)))$
312	309 311	mpbid	$⊢ φ \to (P ∥ (A D + C B) \lor P ∥ (A D - C B))$
313	196 305 312	mpjaodan	$⊢ φ \to A = C$
314	313	oveq1d	$⊢ φ \to A^{2} = C^{2}$
315	314	oveq2d	$⊢ φ \to P - A^{2} = P - C^{2}$
316	315 220 224	3eqtr3d	$⊢ φ \to B^{2} = D^{2}$
317	13 43 17 130 316	sq11d	$⊢ φ \to B = D$
318	313 317	jca	$⊢ φ \to (A = C \land B = D)$

Metamath Proof Explorer

Theorem 2sqmod

Proof