Metamath Proof Explorer

Theorem flt4lem5e

Description: Satisfy the hypotheses of flt4lem4 . EDITORIAL: This is not minimized! (Contributed by SN, 23-Aug-2024)

Ref Expression
Hypotheses flt4lem5a.m 
|- M = ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 )
flt4lem5a.n 
|- N = ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 )
flt4lem5a.r 
|- R = ( ( ( sqrt ` ( M + N ) ) + ( sqrt ` ( M - N ) ) ) / 2 )
flt4lem5a.s 
|- S = ( ( ( sqrt ` ( M + N ) ) - ( sqrt ` ( M - N ) ) ) / 2 )
flt4lem5a.a 
|- ( ph -> A e. NN )
flt4lem5a.b 
|- ( ph -> B e. NN )
flt4lem5a.c 
|- ( ph -> C e. NN )
flt4lem5a.1 
|- ( ph -> -. 2 || A )
flt4lem5a.2 
|- ( ph -> ( A gcd C ) = 1 )
flt4lem5a.3 
|- ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) )
Assertion flt4lem5e 
|- ( ph -> ( ( ( R gcd S ) = 1 /\ ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) /\ ( R e. NN /\ S e. NN /\ M e. NN ) /\ ( ( M x. ( R x. S ) ) = ( ( B / 2 ) ^ 2 ) /\ ( B / 2 ) e. NN ) ) )

Proof

Step Hyp Ref Expression
1 flt4lem5a.m 
 |-  M = ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) + ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 )
2 flt4lem5a.n 
 |-  N = ( ( ( sqrt ` ( C + ( B ^ 2 ) ) ) - ( sqrt ` ( C - ( B ^ 2 ) ) ) ) / 2 )
3 flt4lem5a.r 
 |-  R = ( ( ( sqrt ` ( M + N ) ) + ( sqrt ` ( M - N ) ) ) / 2 )
4 flt4lem5a.s 
 |-  S = ( ( ( sqrt ` ( M + N ) ) - ( sqrt ` ( M - N ) ) ) / 2 )
5 flt4lem5a.a 
 |-  ( ph -> A e. NN )
6 flt4lem5a.b 
 |-  ( ph -> B e. NN )
7 flt4lem5a.c 
 |-  ( ph -> C e. NN )
8 flt4lem5a.1 
 |-  ( ph -> -. 2 || A )
9 flt4lem5a.2 
 |-  ( ph -> ( A gcd C ) = 1 )
10 flt4lem5a.3 
 |-  ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( C ^ 2 ) )
11 5 nnsqcld 
 |-  ( ph -> ( A ^ 2 ) e. NN )
12 6 nnsqcld 
 |-  ( ph -> ( B ^ 2 ) e. NN )
13 2prm 
 |-  2 e. Prime
14 5 nnzd 
 |-  ( ph -> A e. ZZ )
15 prmdvdssq 
 |-  ( ( 2 e. Prime /\ A e. ZZ ) -> ( 2 || A <-> 2 || ( A ^ 2 ) ) )
16 13 14 15 sylancr 
 |-  ( ph -> ( 2 || A <-> 2 || ( A ^ 2 ) ) )
17 8 16 mtbid 
 |-  ( ph -> -. 2 || ( A ^ 2 ) )
18 2nn 
 |-  2 e. NN
19 18 a1i 
 |-  ( ph -> 2 e. NN )
20 rplpwr 
 |-  ( ( A e. NN /\ C e. NN /\ 2 e. NN ) -> ( ( A gcd C ) = 1 -> ( ( A ^ 2 ) gcd C ) = 1 ) )
21 5 7 19 20 syl3anc 
 |-  ( ph -> ( ( A gcd C ) = 1 -> ( ( A ^ 2 ) gcd C ) = 1 ) )
22 9 21 mpd 
 |-  ( ph -> ( ( A ^ 2 ) gcd C ) = 1 )
23 5 nncnd 
 |-  ( ph -> A e. CC )
24 23 flt4lem 
 |-  ( ph -> ( A ^ 4 ) = ( ( A ^ 2 ) ^ 2 ) )
25 6 nncnd 
 |-  ( ph -> B e. CC )
26 25 flt4lem 
 |-  ( ph -> ( B ^ 4 ) = ( ( B ^ 2 ) ^ 2 ) )
27 24 26 oveq12d 
 |-  ( ph -> ( ( A ^ 4 ) + ( B ^ 4 ) ) = ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) )
28 27 10 eqtr3d 
 |-  ( ph -> ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) )
29 11 12 7 17 22 28 flt4lem1 
 |-  ( ph -> ( ( ( A ^ 2 ) e. NN /\ ( B ^ 2 ) e. NN /\ C e. NN ) /\ ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) /\ ( ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 /\ -. 2 || ( A ^ 2 ) ) ) )
30 2 pythagtriplem13 
 |-  ( ( ( ( A ^ 2 ) e. NN /\ ( B ^ 2 ) e. NN /\ C e. NN ) /\ ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) /\ ( ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 /\ -. 2 || ( A ^ 2 ) ) ) -> N e. NN )
31 29 30 syl 
 |-  ( ph -> N e. NN )
32 1 pythagtriplem11 
 |-  ( ( ( ( A ^ 2 ) e. NN /\ ( B ^ 2 ) e. NN /\ C e. NN ) /\ ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) /\ ( ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 /\ -. 2 || ( A ^ 2 ) ) ) -> M e. NN )
33 29 32 syl 
 |-  ( ph -> M e. NN )
34 1 2 3 4 5 6 7 8 9 10 flt4lem5a 
 |-  ( ph -> ( ( A ^ 2 ) + ( N ^ 2 ) ) = ( M ^ 2 ) )
35 31 nnzd 
 |-  ( ph -> N e. ZZ )
36 14 35 gcdcomd 
 |-  ( ph -> ( A gcd N ) = ( N gcd A ) )
37 33 nnzd 
 |-  ( ph -> M e. ZZ )
38 35 37 gcdcomd 
 |-  ( ph -> ( N gcd M ) = ( M gcd N ) )
39 1 2 flt4lem5 
 |-  ( ( ( ( A ^ 2 ) e. NN /\ ( B ^ 2 ) e. NN /\ C e. NN ) /\ ( ( ( A ^ 2 ) ^ 2 ) + ( ( B ^ 2 ) ^ 2 ) ) = ( C ^ 2 ) /\ ( ( ( A ^ 2 ) gcd ( B ^ 2 ) ) = 1 /\ -. 2 || ( A ^ 2 ) ) ) -> ( M gcd N ) = 1 )
40 29 39 syl 
 |-  ( ph -> ( M gcd N ) = 1 )
41 38 40 eqtrd 
 |-  ( ph -> ( N gcd M ) = 1 )
42 31 nnsqcld 
 |-  ( ph -> ( N ^ 2 ) e. NN )
43 42 nncnd 
 |-  ( ph -> ( N ^ 2 ) e. CC )
44 11 nncnd 
 |-  ( ph -> ( A ^ 2 ) e. CC )
45 43 44 addcomd 
 |-  ( ph -> ( ( N ^ 2 ) + ( A ^ 2 ) ) = ( ( A ^ 2 ) + ( N ^ 2 ) ) )
46 45 34 eqtrd 
 |-  ( ph -> ( ( N ^ 2 ) + ( A ^ 2 ) ) = ( M ^ 2 ) )
47 31 5 33 41 46 fltabcoprm 
 |-  ( ph -> ( N gcd A ) = 1 )
48 36 47 eqtrd 
 |-  ( ph -> ( A gcd N ) = 1 )
49 3 4 flt4lem5 
 |-  ( ( ( A e. NN /\ N e. NN /\ M e. NN ) /\ ( ( A ^ 2 ) + ( N ^ 2 ) ) = ( M ^ 2 ) /\ ( ( A gcd N ) = 1 /\ -. 2 || A ) ) -> ( R gcd S ) = 1 )
50 5 31 33 34 48 8 49 syl312anc 
 |-  ( ph -> ( R gcd S ) = 1 )
51 3 pythagtriplem11 
 |-  ( ( ( A e. NN /\ N e. NN /\ M e. NN ) /\ ( ( A ^ 2 ) + ( N ^ 2 ) ) = ( M ^ 2 ) /\ ( ( A gcd N ) = 1 /\ -. 2 || A ) ) -> R e. NN )
52 5 31 33 34 48 8 51 syl312anc 
 |-  ( ph -> R e. NN )
53 4 pythagtriplem13 
 |-  ( ( ( A e. NN /\ N e. NN /\ M e. NN ) /\ ( ( A ^ 2 ) + ( N ^ 2 ) ) = ( M ^ 2 ) /\ ( ( A gcd N ) = 1 /\ -. 2 || A ) ) -> S e. NN )
54 5 31 33 34 48 8 53 syl312anc 
 |-  ( ph -> S e. NN )
55 1 2 3 4 5 6 7 8 9 10 flt4lem5d 
 |-  ( ph -> M = ( ( R ^ 2 ) + ( S ^ 2 ) ) )
56 33 52 54 55 50 flt4lem5elem 
 |-  ( ph -> ( ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) )
57 50 56 jca 
 |-  ( ph -> ( ( R gcd S ) = 1 /\ ( ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) ) )
58 3anass 
 |-  ( ( ( R gcd S ) = 1 /\ ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) <-> ( ( R gcd S ) = 1 /\ ( ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) ) )
59 57 58 sylibr 
 |-  ( ph -> ( ( R gcd S ) = 1 /\ ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) )
60 52 54 33 3jca 
 |-  ( ph -> ( R e. NN /\ S e. NN /\ M e. NN ) )
61 sq2 
 |-  ( 2 ^ 2 ) = 4
62 4cn 
 |-  4 e. CC
63 61 62 eqeltri 
 |-  ( 2 ^ 2 ) e. CC
64 63 a1i 
 |-  ( ph -> ( 2 ^ 2 ) e. CC )
65 52 54 nnmulcld 
 |-  ( ph -> ( R x. S ) e. NN )
66 33 65 nnmulcld 
 |-  ( ph -> ( M x. ( R x. S ) ) e. NN )
67 66 nncnd 
 |-  ( ph -> ( M x. ( R x. S ) ) e. CC )
68 4ne0 
 |-  4 =/= 0
69 61 68 eqnetri 
 |-  ( 2 ^ 2 ) =/= 0
70 69 a1i 
 |-  ( ph -> ( 2 ^ 2 ) =/= 0 )
71 2cn 
 |-  2 e. CC
72 71 sqvali 
 |-  ( 2 ^ 2 ) = ( 2 x. 2 )
73 72 oveq1i 
 |-  ( ( 2 ^ 2 ) x. ( M x. ( R x. S ) ) ) = ( ( 2 x. 2 ) x. ( M x. ( R x. S ) ) )
74 2cnd 
 |-  ( ph -> 2 e. CC )
75 33 nncnd 
 |-  ( ph -> M e. CC )
76 65 nncnd 
 |-  ( ph -> ( R x. S ) e. CC )
77 74 74 75 76 mul4d 
 |-  ( ph -> ( ( 2 x. 2 ) x. ( M x. ( R x. S ) ) ) = ( ( 2 x. M ) x. ( 2 x. ( R x. S ) ) ) )
78 1 2 3 4 5 6 7 8 9 10 flt4lem5c 
 |-  ( ph -> N = ( 2 x. ( R x. S ) ) )
79 78 eqcomd 
 |-  ( ph -> ( 2 x. ( R x. S ) ) = N )
80 79 31 eqeltrd 
 |-  ( ph -> ( 2 x. ( R x. S ) ) e. NN )
81 80 nncnd 
 |-  ( ph -> ( 2 x. ( R x. S ) ) e. CC )
82 74 75 81 mulassd 
 |-  ( ph -> ( ( 2 x. M ) x. ( 2 x. ( R x. S ) ) ) = ( 2 x. ( M x. ( 2 x. ( R x. S ) ) ) ) )
83 79 oveq2d 
 |-  ( ph -> ( M x. ( 2 x. ( R x. S ) ) ) = ( M x. N ) )
84 83 oveq2d 
 |-  ( ph -> ( 2 x. ( M x. ( 2 x. ( R x. S ) ) ) ) = ( 2 x. ( M x. N ) ) )
85 82 84 eqtrd 
 |-  ( ph -> ( ( 2 x. M ) x. ( 2 x. ( R x. S ) ) ) = ( 2 x. ( M x. N ) ) )
86 1 2 3 4 5 6 7 8 9 10 flt4lem5b 
 |-  ( ph -> ( 2 x. ( M x. N ) ) = ( B ^ 2 ) )
87 77 85 86 3eqtrd 
 |-  ( ph -> ( ( 2 x. 2 ) x. ( M x. ( R x. S ) ) ) = ( B ^ 2 ) )
88 73 87 syl5eq 
 |-  ( ph -> ( ( 2 ^ 2 ) x. ( M x. ( R x. S ) ) ) = ( B ^ 2 ) )
89 64 67 70 88 mvllmuld 
 |-  ( ph -> ( M x. ( R x. S ) ) = ( ( B ^ 2 ) / ( 2 ^ 2 ) ) )
90 2ne0 
 |-  2 =/= 0
91 90 a1i 
 |-  ( ph -> 2 =/= 0 )
92 25 74 91 sqdivd 
 |-  ( ph -> ( ( B / 2 ) ^ 2 ) = ( ( B ^ 2 ) / ( 2 ^ 2 ) ) )
93 89 92 eqtr4d 
 |-  ( ph -> ( M x. ( R x. S ) ) = ( ( B / 2 ) ^ 2 ) )
94 66 nnzd 
 |-  ( ph -> ( M x. ( R x. S ) ) e. ZZ )
95 93 94 eqeltrrd 
 |-  ( ph -> ( ( B / 2 ) ^ 2 ) e. ZZ )
96 6 nnzd 
 |-  ( ph -> B e. ZZ )
97 znq 
 |-  ( ( B e. ZZ /\ 2 e. NN ) -> ( B / 2 ) e. QQ )
98 96 18 97 sylancl 
 |-  ( ph -> ( B / 2 ) e. QQ )
99 6 nngt0d 
 |-  ( ph -> 0 < B )
100 6 nnred 
 |-  ( ph -> B e. RR )
101 halfpos2 
 |-  ( B e. RR -> ( 0 < B <-> 0 < ( B / 2 ) ) )
102 100 101 syl 
 |-  ( ph -> ( 0 < B <-> 0 < ( B / 2 ) ) )
103 99 102 mpbid 
 |-  ( ph -> 0 < ( B / 2 ) )
104 95 98 103 posqsqznn 
 |-  ( ph -> ( B / 2 ) e. NN )
105 93 104 jca 
 |-  ( ph -> ( ( M x. ( R x. S ) ) = ( ( B / 2 ) ^ 2 ) /\ ( B / 2 ) e. NN ) )
106 59 60 105 3jca 
 |-  ( ph -> ( ( ( R gcd S ) = 1 /\ ( R gcd M ) = 1 /\ ( S gcd M ) = 1 ) /\ ( R e. NN /\ S e. NN /\ M e. NN ) /\ ( ( M x. ( R x. S ) ) = ( ( B / 2 ) ^ 2 ) /\ ( B / 2 ) e. NN ) ) )