Metamath Proof Explorer

Theorem posbezout

Description: Bezout's identity restricted on positive integers in all but one variable. (Contributed by metakunt, 26-Apr-2025)

Ref Expression
Assertion posbezout 
|- ( ( A e. NN /\ B e. NN ) -> E. x e. NN E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) -> ( A x. x ) = ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) )
2 1 oveq1d 
 |-  ( x = ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) -> ( ( A x. x ) + ( B x. y ) ) = ( ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( B x. y ) ) )
3 2 eqeq2d 
 |-  ( x = ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) -> ( ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) <-> ( A gcd B ) = ( ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( B x. y ) ) ) )
4 oveq2 
 |-  ( y = ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) -> ( B x. y ) = ( B x. ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) )
5 4 oveq2d 
 |-  ( y = ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) -> ( ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( B x. y ) ) = ( ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( B x. ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) )
6 5 eqeq2d 
 |-  ( y = ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) -> ( ( A gcd B ) = ( ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( B x. y ) ) <-> ( A gcd B ) = ( ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( B x. ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) ) )
7 simplr 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> w e. ZZ )
8 simpllr 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> B e. NN )
9 8 nnzd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> B e. ZZ )
10 7 7 zmulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w x. w ) e. ZZ )
11 simpr 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> z e. ZZ )
12 11 11 zmulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( z x. z ) e. ZZ )
13 10 12 zaddcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( w x. w ) + ( z x. z ) ) e. ZZ )
14 2z 
 |-  2 e. ZZ
15 14 a1i 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 2 e. ZZ )
16 13 15 zaddcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( ( w x. w ) + ( z x. z ) ) + 2 ) e. ZZ )
17 9 16 zmulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) e. ZZ )
18 7 17 zaddcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) e. ZZ )
19 7 zred 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> w e. RR )
20 19 renegcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> -u w e. RR )
21 20 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> -u w e. RR )
22 0red 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> 0 e. RR )
23 17 zred 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) e. RR )
24 23 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) e. RR )
25 df-neg 
 |-  -u w = ( 0 - w )
26 25 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> -u w = ( 0 - w ) )
27 19 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> w e. RR )
28 22 leidd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> 0 <_ 0 )
29 simpr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> 0 <_ w )
30 22 27 28 29 addge0d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> 0 <_ ( 0 + w ) )
31 22 27 22 lesubaddd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> ( ( 0 - w ) <_ 0 <-> 0 <_ ( 0 + w ) ) )
32 30 31 mpbird 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> ( 0 - w ) <_ 0 )
33 26 32 eqbrtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> -u w <_ 0 )
34 8 nnred 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> B e. RR )
35 16 zred 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( ( w x. w ) + ( z x. z ) ) + 2 ) e. RR )
36 8 nngt0d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 < B )
37 0red 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 e. RR )
38 2re 
 |-  2 e. RR
39 38 a1i 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 2 e. RR )
40 37 39 readdcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( 0 + 2 ) e. RR )
41 2pos 
 |-  0 < 2
42 eqid 
 |-  2 = 2
43 2cn 
 |-  2 e. CC
44 43 addlidi 
 |-  ( 0 + 2 ) = 2
45 42 44 eqtr4i 
 |-  2 = ( 0 + 2 )
46 41 45 breqtri 
 |-  0 < ( 0 + 2 )
47 46 a1i 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 < ( 0 + 2 ) )
48 13 zred 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( w x. w ) + ( z x. z ) ) e. RR )
49 19 19 remulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w x. w ) e. RR )
50 12 zred 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( z x. z ) e. RR )
51 19 msqge0d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 <_ ( w x. w ) )
52 11 zred 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> z e. RR )
53 52 msqge0d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 <_ ( z x. z ) )
54 49 50 51 53 addge0d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 <_ ( ( w x. w ) + ( z x. z ) ) )
55 39 leidd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 2 <_ 2 )
56 37 39 48 39 54 55 le2addd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( 0 + 2 ) <_ ( ( ( w x. w ) + ( z x. z ) ) + 2 ) )
57 37 40 35 47 56 ltletrd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 < ( ( ( w x. w ) + ( z x. z ) ) + 2 ) )
58 34 35 36 57 mulgt0d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) )
59 58 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> 0 < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) )
60 21 22 24 33 59 lelttrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 0 <_ w ) -> -u w < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) )
61 25 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> -u w = ( 0 - w ) )
62 37 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 e. RR )
63 34 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> B e. RR )
64 52 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> z e. RR )
65 64 64 remulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( z x. z ) e. RR )
66 63 65 remulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( B x. ( z x. z ) ) e. RR )
67 19 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> w e. RR )
68 67 67 remulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( w x. w ) e. RR )
69 38 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 2 e. RR )
70 68 69 readdcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( w x. w ) + 2 ) e. RR )
71 63 70 remulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( B x. ( ( w x. w ) + 2 ) ) e. RR )
72 71 67 readdcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( B x. ( ( w x. w ) + 2 ) ) + w ) e. RR )
73 66 72 readdcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( B x. ( z x. z ) ) + ( ( B x. ( ( w x. w ) + 2 ) ) + w ) ) e. RR )
74 8 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> B e. NN )
75 74 nnnn0d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> B e. NN0 )
76 75 nn0ge0d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 <_ B )
77 64 msqge0d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 <_ ( z x. z ) )
78 63 65 76 77 mulge0d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 <_ ( B x. ( z x. z ) ) )
79 63 recnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> B e. CC )
80 64 recnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> z e. CC )
81 80 80 mulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( z x. z ) e. CC )
82 79 81 mulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( B x. ( z x. z ) ) e. CC )
83 82 subidd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( B x. ( z x. z ) ) - ( B x. ( z x. z ) ) ) = 0 )
84 1red 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 1 e. RR )
85 84 70 remulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( 1 x. ( ( w x. w ) + 2 ) ) e. RR )
86 85 67 readdcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( 1 x. ( ( w x. w ) + 2 ) ) + w ) e. RR )
87 20 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> -u w e. RR )
88 19 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> w e. RR )
89 88 88 remulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( w x. w ) e. RR )
90 38 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> 2 e. RR )
91 89 90 readdcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( w x. w ) + 2 ) e. RR )
92 37 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> 0 e. RR )
93 87 87 remulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( -u w x. -u w ) e. RR )
94 93 90 readdcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( -u w x. -u w ) + 2 ) e. RR )
95 1red 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 1 e. RR )
96 95 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> 1 e. RR )
97 0le1 
 |-  0 <_ 1
98 97 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> 0 <_ 1 )
99 simpr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> 1 <_ -u w )
100 92 96 87 98 99 letrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> 0 <_ -u w )
101 87 87 100 99 lemulge11d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> -u w <_ ( -u w x. -u w ) )
102 93 92 readdcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( -u w x. -u w ) + 0 ) e. RR )
103 93 leidd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( -u w x. -u w ) <_ ( -u w x. -u w ) )
104 88 recnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> w e. CC )
105 104 negcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> -u w e. CC )
106 105 105 mulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( -u w x. -u w ) e. CC )
107 106 addridd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( -u w x. -u w ) + 0 ) = ( -u w x. -u w ) )
108 107 eqcomd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( -u w x. -u w ) = ( ( -u w x. -u w ) + 0 ) )
109 103 108 breqtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( -u w x. -u w ) <_ ( ( -u w x. -u w ) + 0 ) )
110 41 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> 0 < 2 )
111 92 90 93 110 ltadd2dd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( -u w x. -u w ) + 0 ) < ( ( -u w x. -u w ) + 2 ) )
112 93 102 94 109 111 lelttrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( -u w x. -u w ) < ( ( -u w x. -u w ) + 2 ) )
113 87 93 94 101 112 lelttrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> -u w < ( ( -u w x. -u w ) + 2 ) )
114 104 104 mul2negd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( -u w x. -u w ) = ( w x. w ) )
115 114 oveq1d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( -u w x. -u w ) + 2 ) = ( ( w x. w ) + 2 ) )
116 113 115 breqtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> -u w < ( ( w x. w ) + 2 ) )
117 91 recnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( w x. w ) + 2 ) e. CC )
118 117 subid1d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( ( w x. w ) + 2 ) - 0 ) = ( ( w x. w ) + 2 ) )
119 118 eqcomd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( w x. w ) + 2 ) = ( ( ( w x. w ) + 2 ) - 0 ) )
120 116 119 breqtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> -u w < ( ( ( w x. w ) + 2 ) - 0 ) )
121 87 91 92 120 ltsub13d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> 0 < ( ( ( w x. w ) + 2 ) - -u w ) )
122 7 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> w e. ZZ )
123 122 zcnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> w e. CC )
124 123 123 mulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( w x. w ) e. CC )
125 2cnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> 2 e. CC )
126 124 125 addcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( w x. w ) + 2 ) e. CC )
127 126 123 subnegd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> ( ( ( w x. w ) + 2 ) - -u w ) = ( ( ( w x. w ) + 2 ) + w ) )
128 121 127 breqtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ 1 <_ -u w ) -> 0 < ( ( ( w x. w ) + 2 ) + w ) )
129 128 ex 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( 1 <_ -u w -> 0 < ( ( ( w x. w ) + 2 ) + w ) ) )
130 0zd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 e. ZZ )
131 7 130 zltlem1d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w < 0 <-> w <_ ( 0 - 1 ) ) )
132 df-neg 
 |-  -u 1 = ( 0 - 1 )
133 132 eqcomi 
 |-  ( 0 - 1 ) = -u 1
134 133 a1i 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( 0 - 1 ) = -u 1 )
135 134 breq2d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w <_ ( 0 - 1 ) <-> w <_ -u 1 ) )
136 131 135 bitrd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w < 0 <-> w <_ -u 1 ) )
137 95 renegcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> -u 1 e. RR )
138 19 137 lenegd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w <_ -u 1 <-> -u -u 1 <_ -u w ) )
139 136 138 bitrd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w < 0 <-> -u -u 1 <_ -u w ) )
140 1cnd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 1 e. CC )
141 140 negnegd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> -u -u 1 = 1 )
142 141 breq1d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( -u -u 1 <_ -u w <-> 1 <_ -u w ) )
143 139 142 bitrd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w < 0 <-> 1 <_ -u w ) )
144 143 biimpd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w < 0 -> 1 <_ -u w ) )
145 144 imim1d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( 1 <_ -u w -> 0 < ( ( ( w x. w ) + 2 ) + w ) ) -> ( w < 0 -> 0 < ( ( ( w x. w ) + 2 ) + w ) ) ) )
146 129 145 mpd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w < 0 -> 0 < ( ( ( w x. w ) + 2 ) + w ) ) )
147 146 imp 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 < ( ( ( w x. w ) + 2 ) + w ) )
148 70 recnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( w x. w ) + 2 ) e. CC )
149 148 mullidd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( 1 x. ( ( w x. w ) + 2 ) ) = ( ( w x. w ) + 2 ) )
150 149 eqcomd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( w x. w ) + 2 ) = ( 1 x. ( ( w x. w ) + 2 ) ) )
151 150 oveq1d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( ( w x. w ) + 2 ) + w ) = ( ( 1 x. ( ( w x. w ) + 2 ) ) + w ) )
152 147 151 breqtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 < ( ( 1 x. ( ( w x. w ) + 2 ) ) + w ) )
153 40 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( 0 + 2 ) e. RR )
154 62 leidd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 <_ 0 )
155 0le2 
 |-  0 <_ 2
156 155 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 <_ 2 )
157 62 69 154 156 addge0d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 <_ ( 0 + 2 ) )
158 51 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 <_ ( w x. w ) )
159 62 68 69 158 leadd1dd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( 0 + 2 ) <_ ( ( w x. w ) + 2 ) )
160 62 153 70 157 159 letrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 <_ ( ( w x. w ) + 2 ) )
161 74 nnge1d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 1 <_ B )
162 84 63 70 160 161 lemul1ad 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( 1 x. ( ( w x. w ) + 2 ) ) <_ ( B x. ( ( w x. w ) + 2 ) ) )
163 85 71 67 162 leadd1dd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( 1 x. ( ( w x. w ) + 2 ) ) + w ) <_ ( ( B x. ( ( w x. w ) + 2 ) ) + w ) )
164 62 86 72 152 163 ltletrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 < ( ( B x. ( ( w x. w ) + 2 ) ) + w ) )
165 83 164 eqbrtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( B x. ( z x. z ) ) - ( B x. ( z x. z ) ) ) < ( ( B x. ( ( w x. w ) + 2 ) ) + w ) )
166 66 66 72 ltsubadd2d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( ( B x. ( z x. z ) ) - ( B x. ( z x. z ) ) ) < ( ( B x. ( ( w x. w ) + 2 ) ) + w ) <-> ( B x. ( z x. z ) ) < ( ( B x. ( z x. z ) ) + ( ( B x. ( ( w x. w ) + 2 ) ) + w ) ) ) )
167 165 166 mpbid 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( B x. ( z x. z ) ) < ( ( B x. ( z x. z ) ) + ( ( B x. ( ( w x. w ) + 2 ) ) + w ) ) )
168 62 66 73 78 167 lelttrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 < ( ( B x. ( z x. z ) ) + ( ( B x. ( ( w x. w ) + 2 ) ) + w ) ) )
169 74 nncnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> B e. CC )
170 11 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> z e. ZZ )
171 170 zcnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> z e. CC )
172 171 171 mulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( z x. z ) e. CC )
173 169 172 mulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( B x. ( z x. z ) ) e. CC )
174 67 recnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> w e. CC )
175 174 174 mulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( w x. w ) e. CC )
176 2cnd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 2 e. CC )
177 175 176 addcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( w x. w ) + 2 ) e. CC )
178 169 177 mulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( B x. ( ( w x. w ) + 2 ) ) e. CC )
179 173 178 174 addassd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( ( B x. ( z x. z ) ) + ( B x. ( ( w x. w ) + 2 ) ) ) + w ) = ( ( B x. ( z x. z ) ) + ( ( B x. ( ( w x. w ) + 2 ) ) + w ) ) )
180 179 eqcomd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( B x. ( z x. z ) ) + ( ( B x. ( ( w x. w ) + 2 ) ) + w ) ) = ( ( ( B x. ( z x. z ) ) + ( B x. ( ( w x. w ) + 2 ) ) ) + w ) )
181 169 172 177 adddid 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( B x. ( ( z x. z ) + ( ( w x. w ) + 2 ) ) ) = ( ( B x. ( z x. z ) ) + ( B x. ( ( w x. w ) + 2 ) ) ) )
182 181 eqcomd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( B x. ( z x. z ) ) + ( B x. ( ( w x. w ) + 2 ) ) ) = ( B x. ( ( z x. z ) + ( ( w x. w ) + 2 ) ) ) )
183 182 oveq1d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( ( B x. ( z x. z ) ) + ( B x. ( ( w x. w ) + 2 ) ) ) + w ) = ( ( B x. ( ( z x. z ) + ( ( w x. w ) + 2 ) ) ) + w ) )
184 180 183 eqtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( B x. ( z x. z ) ) + ( ( B x. ( ( w x. w ) + 2 ) ) + w ) ) = ( ( B x. ( ( z x. z ) + ( ( w x. w ) + 2 ) ) ) + w ) )
185 43 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 2 e. CC )
186 172 175 185 addassd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( ( z x. z ) + ( w x. w ) ) + 2 ) = ( ( z x. z ) + ( ( w x. w ) + 2 ) ) )
187 186 eqcomd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( z x. z ) + ( ( w x. w ) + 2 ) ) = ( ( ( z x. z ) + ( w x. w ) ) + 2 ) )
188 172 175 addcomd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( z x. z ) + ( w x. w ) ) = ( ( w x. w ) + ( z x. z ) ) )
189 188 oveq1d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( ( z x. z ) + ( w x. w ) ) + 2 ) = ( ( ( w x. w ) + ( z x. z ) ) + 2 ) )
190 187 189 eqtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( z x. z ) + ( ( w x. w ) + 2 ) ) = ( ( ( w x. w ) + ( z x. z ) ) + 2 ) )
191 190 oveq2d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( B x. ( ( z x. z ) + ( ( w x. w ) + 2 ) ) ) = ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) )
192 191 oveq1d 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( B x. ( ( z x. z ) + ( ( w x. w ) + 2 ) ) ) + w ) = ( ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) + w ) )
193 184 192 eqtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( B x. ( z x. z ) ) + ( ( B x. ( ( w x. w ) + 2 ) ) + w ) ) = ( ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) + w ) )
194 168 193 breqtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> 0 < ( ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) + w ) )
195 23 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) e. RR )
196 62 67 195 ltsubaddd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( ( 0 - w ) < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) <-> 0 < ( ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) + w ) ) )
197 194 196 mpbird 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> ( 0 - w ) < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) )
198 61 197 eqbrtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ w < 0 ) -> -u w < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) )
199 198 ex 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w < 0 -> -u w < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) )
200 19 37 ltnled 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w < 0 <-> -. 0 <_ w ) )
201 200 bicomd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( -. 0 <_ w <-> w < 0 ) )
202 201 biimpd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( -. 0 <_ w -> w < 0 ) )
203 202 imim1d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( w < 0 -> -u w < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) -> ( -. 0 <_ w -> -u w < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) )
204 199 203 mpd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( -. 0 <_ w -> -u w < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) )
205 204 imp 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ -. 0 <_ w ) -> -u w < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) )
206 60 205 pm2.61dan 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> -u w < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) )
207 20 23 posdifd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( -u w < ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) <-> 0 < ( ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) - -u w ) ) )
208 206 207 mpbid 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 < ( ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) - -u w ) )
209 17 zcnd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) e. CC )
210 7 zcnd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> w e. CC )
211 209 210 subnegd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) - -u w ) = ( ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) + w ) )
212 209 210 addcomd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) + w ) = ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) )
213 211 212 eqtrd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) - -u w ) = ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) )
214 208 213 breqtrd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 0 < ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) )
215 18 214 jca 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) e. ZZ /\ 0 < ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) )
216 elnnz 
 |-  ( ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) e. NN <-> ( ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) e. ZZ /\ 0 < ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) )
217 215 216 sylibr 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) e. NN )
218 217 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) e. NN )
219 simplr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> z e. ZZ )
220 simp-4l 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> A e. NN )
221 220 nnzd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> A e. ZZ )
222 simpllr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> w e. ZZ )
223 222 222 zmulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> ( w x. w ) e. ZZ )
224 219 219 zmulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> ( z x. z ) e. ZZ )
225 223 224 zaddcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> ( ( w x. w ) + ( z x. z ) ) e. ZZ )
226 14 a1i 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> 2 e. ZZ )
227 225 226 zaddcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> ( ( ( w x. w ) + ( z x. z ) ) + 2 ) e. ZZ )
228 221 227 zmulcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) e. ZZ )
229 219 228 zsubcld 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) e. ZZ )
230 simpr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) )
231 simplll 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> A e. NN )
232 231 nncnd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> A e. CC )
233 232 210 mulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( A x. w ) e. CC )
234 8 nncnd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> B e. CC )
235 210 210 mulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( w x. w ) e. CC )
236 11 zcnd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> z e. CC )
237 236 236 mulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( z x. z ) e. CC )
238 235 237 addcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( w x. w ) + ( z x. z ) ) e. CC )
239 2cnd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> 2 e. CC )
240 238 239 addcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( ( w x. w ) + ( z x. z ) ) + 2 ) e. CC )
241 234 240 mulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) e. CC )
242 232 241 mulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) e. CC )
243 234 236 mulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( B x. z ) e. CC )
244 233 242 243 ppncand 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( ( A x. w ) + ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( ( B x. z ) - ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) = ( ( A x. w ) + ( B x. z ) ) )
245 eqidd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( A x. w ) + ( B x. z ) ) = ( ( A x. w ) + ( B x. z ) ) )
246 244 245 eqtr2d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( A x. w ) + ( B x. z ) ) = ( ( ( A x. w ) + ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( ( B x. z ) - ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) )
247 16 zcnd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( ( w x. w ) + ( z x. z ) ) + 2 ) e. CC )
248 232 234 247 mul12d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) = ( B x. ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) )
249 248 oveq2d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( B x. z ) - ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) = ( ( B x. z ) - ( B x. ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) )
250 249 oveq2d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( ( A x. w ) + ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( ( B x. z ) - ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) = ( ( ( A x. w ) + ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( ( B x. z ) - ( B x. ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) )
251 246 250 eqtrd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( A x. w ) + ( B x. z ) ) = ( ( ( A x. w ) + ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( ( B x. z ) - ( B x. ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) )
252 232 210 209 adddid 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) = ( ( A x. w ) + ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) )
253 252 eqcomd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( A x. w ) + ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) = ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) )
254 232 240 mulcld 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) e. CC )
255 234 236 254 subdid 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( B x. ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) = ( ( B x. z ) - ( B x. ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) )
256 255 eqcomd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( B x. z ) - ( B x. ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) = ( B x. ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) )
257 253 256 oveq12d 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( ( A x. w ) + ( A x. ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( ( B x. z ) - ( B x. ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) = ( ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( B x. ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) )
258 251 257 eqtrd 
 |-  ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) -> ( ( A x. w ) + ( B x. z ) ) = ( ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( B x. ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) )
259 258 adantr 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> ( ( A x. w ) + ( B x. z ) ) = ( ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( B x. ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) )
260 230 259 eqtrd 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> ( A gcd B ) = ( ( A x. ( w + ( B x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) + ( B x. ( z - ( A x. ( ( ( w x. w ) + ( z x. z ) ) + 2 ) ) ) ) ) )
261 3 6 218 229 260 2rspcedvdw 
 |-  ( ( ( ( ( A e. NN /\ B e. NN ) /\ w e. ZZ ) /\ z e. ZZ ) /\ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) ) -> E. x e. NN E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) )
262 nnz 
 |-  ( A e. NN -> A e. ZZ )
263 262 adantr 
 |-  ( ( A e. NN /\ B e. NN ) -> A e. ZZ )
264 nnz 
 |-  ( B e. NN -> B e. ZZ )
265 264 adantl 
 |-  ( ( A e. NN /\ B e. NN ) -> B e. ZZ )
266 263 265 jca 
 |-  ( ( A e. NN /\ B e. NN ) -> ( A e. ZZ /\ B e. ZZ ) )
267 bezout 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> E. w e. ZZ E. z e. ZZ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) )
268 266 267 syl 
 |-  ( ( A e. NN /\ B e. NN ) -> E. w e. ZZ E. z e. ZZ ( A gcd B ) = ( ( A x. w ) + ( B x. z ) ) )
269 261 268 r19.29vva 
 |-  ( ( A e. NN /\ B e. NN ) -> E. x e. NN E. y e. ZZ ( A gcd B ) = ( ( A x. x ) + ( B x. y ) ) )