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 ( ( 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ) → ∃ 𝑥 ∈ ℕ ∃ 𝑦 ∈ ℤ ( 𝐴 gcd 𝐵 ) = ( ( 𝐴 · 𝑥 ) + ( 𝐵 · 𝑦 ) ) )

Proof

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