Theorem flt4lem5c

Description: Part 2 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html . (Contributed by SN, 22-Aug-2024)

	Ref	Expression
Hypotheses	flt4lem5a.m	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
	flt4lem5a.n	⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
	flt4lem5a.r	⊢ 𝑅 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) + ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
	flt4lem5a.s	⊢ 𝑆 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) − ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
	flt4lem5a.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
	flt4lem5a.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
	flt4lem5a.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
	flt4lem5a.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
	flt4lem5a.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
	flt4lem5a.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 2 ) )
Assertion	flt4lem5c	⊢ ( 𝜑 → 𝑁 = ( 2 · ( 𝑅 · 𝑆 ) ) )

Proof

Step	Hyp	Ref	Expression
1		flt4lem5a.m	⊢ 𝑀 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) + ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
2		flt4lem5a.n	⊢ 𝑁 = ( ( ( √ ‘ ( 𝐶 + ( 𝐵 ↑ 2 ) ) ) − ( √ ‘ ( 𝐶 − ( 𝐵 ↑ 2 ) ) ) ) / 2 )
3		flt4lem5a.r	⊢ 𝑅 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) + ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
4		flt4lem5a.s	⊢ 𝑆 = ( ( ( √ ‘ ( 𝑀 + 𝑁 ) ) − ( √ ‘ ( 𝑀 − 𝑁 ) ) ) / 2 )
5		flt4lem5a.a	⊢ ( 𝜑 → 𝐴 ∈ ℕ )
6		flt4lem5a.b	⊢ ( 𝜑 → 𝐵 ∈ ℕ )
7		flt4lem5a.c	⊢ ( 𝜑 → 𝐶 ∈ ℕ )
8		flt4lem5a.1	⊢ ( 𝜑 → ¬ 2 ∥ 𝐴 )
9		flt4lem5a.2	⊢ ( 𝜑 → ( 𝐴 gcd 𝐶 ) = 1 )
10		flt4lem5a.3	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( 𝐶 ↑ 2 ) )
11	5	nnsqcld	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℕ )
12	6	nnsqcld	⊢ ( 𝜑 → ( 𝐵 ↑ 2 ) ∈ ℕ )
13		2prm	⊢ 2 ∈ ℙ
14	5	nnzd	⊢ ( 𝜑 → 𝐴 ∈ ℤ )
15		prmdvdssq	⊢ ( ( 2 ∈ ℙ ∧ 𝐴 ∈ ℤ ) → ( 2 ∥ 𝐴 ↔ 2 ∥ ( 𝐴 ↑ 2 ) ) )
16	13 14 15	sylancr	⊢ ( 𝜑 → ( 2 ∥ 𝐴 ↔ 2 ∥ ( 𝐴 ↑ 2 ) ) )
17	8 16	mtbid	⊢ ( 𝜑 → ¬ 2 ∥ ( 𝐴 ↑ 2 ) )
18		2nn	⊢ 2 ∈ ℕ
19	18	a1i	⊢ ( 𝜑 → 2 ∈ ℕ )
20		rplpwr	⊢ ( ( 𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ ∧ 2 ∈ ℕ ) → ( ( 𝐴 gcd 𝐶 ) = 1 → ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 ) )
21	5 7 19 20	syl3anc	⊢ ( 𝜑 → ( ( 𝐴 gcd 𝐶 ) = 1 → ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 ) )
22	9 21	mpd	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) gcd 𝐶 ) = 1 )
23	5	nncnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
24	23	flt4lem	⊢ ( 𝜑 → ( 𝐴 ↑ 4 ) = ( ( 𝐴 ↑ 2 ) ↑ 2 ) )
25	6	nncnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
26	25	flt4lem	⊢ ( 𝜑 → ( 𝐵 ↑ 4 ) = ( ( 𝐵 ↑ 2 ) ↑ 2 ) )
27	24 26	oveq12d	⊢ ( 𝜑 → ( ( 𝐴 ↑ 4 ) + ( 𝐵 ↑ 4 ) ) = ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) )
28	27 10	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) )
29	11 12 7 17 22 28	flt4lem1	⊢ ( 𝜑 → ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) )
30	2	pythagtriplem13	⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → 𝑁 ∈ ℕ )
31	29 30	syl	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
32	1	pythagtriplem11	⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → 𝑀 ∈ ℕ )
33	29 32	syl	⊢ ( 𝜑 → 𝑀 ∈ ℕ )
34	1 2 3 4 5 6 7 8 9 10	flt4lem5a	⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) )
35	31	nnzd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
36	14 35	gcdcomd	⊢ ( 𝜑 → ( 𝐴 gcd 𝑁 ) = ( 𝑁 gcd 𝐴 ) )
37	33	nnzd	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
38	35 37	gcdcomd	⊢ ( 𝜑 → ( 𝑁 gcd 𝑀 ) = ( 𝑀 gcd 𝑁 ) )
39	1 2	flt4lem5	⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → ( 𝑀 gcd 𝑁 ) = 1 )
40	29 39	syl	⊢ ( 𝜑 → ( 𝑀 gcd 𝑁 ) = 1 )
41	38 40	eqtrd	⊢ ( 𝜑 → ( 𝑁 gcd 𝑀 ) = 1 )
42	31	nnsqcld	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℕ )
43	42	nncnd	⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
44	11	nncnd	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) ∈ ℂ )
45	43 44	addcomd	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) )
46	45 34	eqtrd	⊢ ( 𝜑 → ( ( 𝑁 ↑ 2 ) + ( 𝐴 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) )
47	31 5 33 41 46	fltabcoprm	⊢ ( 𝜑 → ( 𝑁 gcd 𝐴 ) = 1 )
48	36 47	eqtrd	⊢ ( 𝜑 → ( 𝐴 gcd 𝑁 ) = 1 )
49	3 4	pythagtriplem16	⊢ ( ( ( 𝐴 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ∈ ℕ ) ∧ ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) ∧ ( ( 𝐴 gcd 𝑁 ) = 1 ∧ ¬ 2 ∥ 𝐴 ) ) → 𝑁 = ( 2 · ( 𝑅 · 𝑆 ) ) )
50	5 31 33 34 48 8 49	syl312anc	⊢ ( 𝜑 → 𝑁 = ( 2 · ( 𝑅 · 𝑆 ) ) )