This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem flt4lem5a

Description: Part 1 of Equation 1 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 flt4lem5a ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 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 1 pythagtriplem11 ⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → 𝑀 ∈ ℕ )
31 29 30 syl ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
32 31 nnsqcld ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℕ )
33 32 nncnd ⊢ ( 𝜑 → ( 𝑀 ↑ 2 ) ∈ ℂ )
34 2 pythagtriplem13 ⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → 𝑁 ∈ ℕ )
35 29 34 syl ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
36 35 nnsqcld ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℕ )
37 36 nncnd ⊢ ( 𝜑 → ( 𝑁 ↑ 2 ) ∈ ℂ )
38 1 2 pythagtriplem15 ⊢ ( ( ( ( 𝐴 ↑ 2 ) ∈ ℕ ∧ ( 𝐵 ↑ 2 ) ∈ ℕ ∧ 𝐶 ∈ ℕ ) ∧ ( ( ( 𝐴 ↑ 2 ) ↑ 2 ) + ( ( 𝐵 ↑ 2 ) ↑ 2 ) ) = ( 𝐶 ↑ 2 ) ∧ ( ( ( 𝐴 ↑ 2 ) gcd ( 𝐵 ↑ 2 ) ) = 1 ∧ ¬ 2 ∥ ( 𝐴 ↑ 2 ) ) ) → ( 𝐴 ↑ 2 ) = ( ( 𝑀 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) )
39 29 38 syl ⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = ( ( 𝑀 ↑ 2 ) − ( 𝑁 ↑ 2 ) ) )
40 33 37 39 mvrrsubd ⊢ ( 𝜑 → ( ( 𝐴 ↑ 2 ) + ( 𝑁 ↑ 2 ) ) = ( 𝑀 ↑ 2 ) )