2sqlem4

	Ref	Expression
Hypotheses	2sq.1	$⊢ S = ran (w \in ℤ [i] ⟼ {\|w\|}^{2})$
	2sqlem5.1	$⊢ φ \to N \in ℕ$
	2sqlem5.2	$⊢ φ \to P \in ℙ$
	2sqlem4.3	$⊢ φ \to A \in ℤ$
	2sqlem4.4	$⊢ φ \to B \in ℤ$
	2sqlem4.5	$⊢ φ \to C \in ℤ$
	2sqlem4.6	$⊢ φ \to D \in ℤ$
	2sqlem4.7	$⊢ φ \to N P = A^{2} + B^{2}$
	2sqlem4.8	$⊢ φ \to P = C^{2} + D^{2}$
Assertion	2sqlem4	$⊢ φ \to N \in S$

Proof

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

Metamath Proof Explorer

Theorem 2sqlem4

Proof