Metamath Proof Explorer


Theorem 4sqlem10

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 16-Jul-2014)

Ref Expression
Hypotheses 4sqlem5.2 ( 𝜑𝐴 ∈ ℤ )
4sqlem5.3 ( 𝜑𝑀 ∈ ℕ )
4sqlem5.4 𝐵 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
4sqlem10.5 ( ( 𝜑𝜓 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐵 ↑ 2 ) ) = 0 )
Assertion 4sqlem10 ( ( 𝜑𝜓 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )

Proof

Step Hyp Ref Expression
1 4sqlem5.2 ( 𝜑𝐴 ∈ ℤ )
2 4sqlem5.3 ( 𝜑𝑀 ∈ ℕ )
3 4sqlem5.4 𝐵 = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) )
4 4sqlem10.5 ( ( 𝜑𝜓 ) → ( ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) − ( 𝐵 ↑ 2 ) ) = 0 )
5 2 adantr ( ( 𝜑𝜓 ) → 𝑀 ∈ ℕ )
6 5 nnzd ( ( 𝜑𝜓 ) → 𝑀 ∈ ℤ )
7 zsqcl ( 𝑀 ∈ ℤ → ( 𝑀 ↑ 2 ) ∈ ℤ )
8 6 7 syl ( ( 𝜑𝜓 ) → ( 𝑀 ↑ 2 ) ∈ ℤ )
9 1 adantr ( ( 𝜑𝜓 ) → 𝐴 ∈ ℤ )
10 5 nnred ( ( 𝜑𝜓 ) → 𝑀 ∈ ℝ )
11 10 rehalfcld ( ( 𝜑𝜓 ) → ( 𝑀 / 2 ) ∈ ℝ )
12 11 recnd ( ( 𝜑𝜓 ) → ( 𝑀 / 2 ) ∈ ℂ )
13 12 negnegd ( ( 𝜑𝜓 ) → - - ( 𝑀 / 2 ) = ( 𝑀 / 2 ) )
14 1 2 3 4sqlem5 ( 𝜑 → ( 𝐵 ∈ ℤ ∧ ( ( 𝐴𝐵 ) / 𝑀 ) ∈ ℤ ) )
15 14 adantr ( ( 𝜑𝜓 ) → ( 𝐵 ∈ ℤ ∧ ( ( 𝐴𝐵 ) / 𝑀 ) ∈ ℤ ) )
16 15 simpld ( ( 𝜑𝜓 ) → 𝐵 ∈ ℤ )
17 16 zred ( ( 𝜑𝜓 ) → 𝐵 ∈ ℝ )
18 1 2 3 4sqlem6 ( 𝜑 → ( - ( 𝑀 / 2 ) ≤ 𝐵𝐵 < ( 𝑀 / 2 ) ) )
19 18 adantr ( ( 𝜑𝜓 ) → ( - ( 𝑀 / 2 ) ≤ 𝐵𝐵 < ( 𝑀 / 2 ) ) )
20 19 simprd ( ( 𝜑𝜓 ) → 𝐵 < ( 𝑀 / 2 ) )
21 17 20 ltned ( ( 𝜑𝜓 ) → 𝐵 ≠ ( 𝑀 / 2 ) )
22 21 neneqd ( ( 𝜑𝜓 ) → ¬ 𝐵 = ( 𝑀 / 2 ) )
23 2cnd ( ( 𝜑𝜓 ) → 2 ∈ ℂ )
24 23 sqvald ( ( 𝜑𝜓 ) → ( 2 ↑ 2 ) = ( 2 · 2 ) )
25 24 oveq2d ( ( 𝜑𝜓 ) → ( ( 𝑀 ↑ 2 ) / ( 2 ↑ 2 ) ) = ( ( 𝑀 ↑ 2 ) / ( 2 · 2 ) ) )
26 5 nncnd ( ( 𝜑𝜓 ) → 𝑀 ∈ ℂ )
27 2ne0 2 ≠ 0
28 27 a1i ( ( 𝜑𝜓 ) → 2 ≠ 0 )
29 26 23 28 sqdivd ( ( 𝜑𝜓 ) → ( ( 𝑀 / 2 ) ↑ 2 ) = ( ( 𝑀 ↑ 2 ) / ( 2 ↑ 2 ) ) )
30 26 sqcld ( ( 𝜑𝜓 ) → ( 𝑀 ↑ 2 ) ∈ ℂ )
31 30 23 23 28 28 divdiv1d ( ( 𝜑𝜓 ) → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) = ( ( 𝑀 ↑ 2 ) / ( 2 · 2 ) ) )
32 25 29 31 3eqtr4d ( ( 𝜑𝜓 ) → ( ( 𝑀 / 2 ) ↑ 2 ) = ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) )
33 30 halfcld ( ( 𝜑𝜓 ) → ( ( 𝑀 ↑ 2 ) / 2 ) ∈ ℂ )
34 33 halfcld ( ( 𝜑𝜓 ) → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ∈ ℂ )
35 16 zcnd ( ( 𝜑𝜓 ) → 𝐵 ∈ ℂ )
36 35 sqcld ( ( 𝜑𝜓 ) → ( 𝐵 ↑ 2 ) ∈ ℂ )
37 34 36 4 subeq0d ( ( 𝜑𝜓 ) → ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) = ( 𝐵 ↑ 2 ) )
38 32 37 eqtr2d ( ( 𝜑𝜓 ) → ( 𝐵 ↑ 2 ) = ( ( 𝑀 / 2 ) ↑ 2 ) )
39 sqeqor ( ( 𝐵 ∈ ℂ ∧ ( 𝑀 / 2 ) ∈ ℂ ) → ( ( 𝐵 ↑ 2 ) = ( ( 𝑀 / 2 ) ↑ 2 ) ↔ ( 𝐵 = ( 𝑀 / 2 ) ∨ 𝐵 = - ( 𝑀 / 2 ) ) ) )
40 35 12 39 syl2anc ( ( 𝜑𝜓 ) → ( ( 𝐵 ↑ 2 ) = ( ( 𝑀 / 2 ) ↑ 2 ) ↔ ( 𝐵 = ( 𝑀 / 2 ) ∨ 𝐵 = - ( 𝑀 / 2 ) ) ) )
41 38 40 mpbid ( ( 𝜑𝜓 ) → ( 𝐵 = ( 𝑀 / 2 ) ∨ 𝐵 = - ( 𝑀 / 2 ) ) )
42 41 ord ( ( 𝜑𝜓 ) → ( ¬ 𝐵 = ( 𝑀 / 2 ) → 𝐵 = - ( 𝑀 / 2 ) ) )
43 22 42 mpd ( ( 𝜑𝜓 ) → 𝐵 = - ( 𝑀 / 2 ) )
44 43 16 eqeltrrd ( ( 𝜑𝜓 ) → - ( 𝑀 / 2 ) ∈ ℤ )
45 44 znegcld ( ( 𝜑𝜓 ) → - - ( 𝑀 / 2 ) ∈ ℤ )
46 13 45 eqeltrrd ( ( 𝜑𝜓 ) → ( 𝑀 / 2 ) ∈ ℤ )
47 9 46 zaddcld ( ( 𝜑𝜓 ) → ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℤ )
48 zsqcl ( ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℤ → ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) ∈ ℤ )
49 47 48 syl ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) ∈ ℤ )
50 47 6 zmulcld ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ∈ ℤ )
51 47 zred ( ( 𝜑𝜓 ) → ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℝ )
52 5 nnrpd ( ( 𝜑𝜓 ) → 𝑀 ∈ ℝ+ )
53 51 52 modcld ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ∈ ℝ )
54 53 recnd ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ∈ ℂ )
55 0cnd ( ( 𝜑𝜓 ) → 0 ∈ ℂ )
56 df-neg - ( 𝑀 / 2 ) = ( 0 − ( 𝑀 / 2 ) )
57 43 3 56 3eqtr3g ( ( 𝜑𝜓 ) → ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) = ( 0 − ( 𝑀 / 2 ) ) )
58 54 55 12 57 subcan2d ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) = 0 )
59 dvdsval3 ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℤ ) → ( 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ↔ ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) = 0 ) )
60 5 47 59 syl2anc ( ( 𝜑𝜓 ) → ( 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ↔ ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) = 0 ) )
61 58 60 mpbird ( ( 𝜑𝜓 ) → 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) )
62 dvdssq ( ( 𝑀 ∈ ℤ ∧ ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℤ ) → ( 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ↔ ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) ) )
63 6 47 62 syl2anc ( ( 𝜑𝜓 ) → ( 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ↔ ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) ) )
64 61 63 mpbid ( ( 𝜑𝜓 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) )
65 26 sqvald ( ( 𝜑𝜓 ) → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
66 5 nnne0d ( ( 𝜑𝜓 ) → 𝑀 ≠ 0 )
67 dvdsmulcr ( ( 𝑀 ∈ ℤ ∧ ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ( ( 𝑀 · 𝑀 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ↔ 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ) )
68 6 47 6 66 67 syl112anc ( ( 𝜑𝜓 ) → ( ( 𝑀 · 𝑀 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ↔ 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ) )
69 61 68 mpbird ( ( 𝜑𝜓 ) → ( 𝑀 · 𝑀 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) )
70 65 69 eqbrtrd ( ( 𝜑𝜓 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) )
71 8 49 50 64 70 dvds2subd ( ( 𝜑𝜓 ) → ( 𝑀 ↑ 2 ) ∥ ( ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) − ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ) )
72 47 zcnd ( ( 𝜑𝜓 ) → ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℂ )
73 72 sqvald ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) = ( ( 𝐴 + ( 𝑀 / 2 ) ) · ( 𝐴 + ( 𝑀 / 2 ) ) ) )
74 73 oveq1d ( ( 𝜑𝜓 ) → ( ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) − ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ) = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) · ( 𝐴 + ( 𝑀 / 2 ) ) ) − ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ) )
75 72 72 26 subdid ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) · ( ( 𝐴 + ( 𝑀 / 2 ) ) − 𝑀 ) ) = ( ( ( 𝐴 + ( 𝑀 / 2 ) ) · ( 𝐴 + ( 𝑀 / 2 ) ) ) − ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ) )
76 26 2halvesd ( ( 𝜑𝜓 ) → ( ( 𝑀 / 2 ) + ( 𝑀 / 2 ) ) = 𝑀 )
77 76 oveq2d ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) − ( ( 𝑀 / 2 ) + ( 𝑀 / 2 ) ) ) = ( ( 𝐴 + ( 𝑀 / 2 ) ) − 𝑀 ) )
78 9 zcnd ( ( 𝜑𝜓 ) → 𝐴 ∈ ℂ )
79 78 12 12 pnpcan2d ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) − ( ( 𝑀 / 2 ) + ( 𝑀 / 2 ) ) ) = ( 𝐴 − ( 𝑀 / 2 ) ) )
80 77 79 eqtr3d ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) − 𝑀 ) = ( 𝐴 − ( 𝑀 / 2 ) ) )
81 80 oveq2d ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) · ( ( 𝐴 + ( 𝑀 / 2 ) ) − 𝑀 ) ) = ( ( 𝐴 + ( 𝑀 / 2 ) ) · ( 𝐴 − ( 𝑀 / 2 ) ) ) )
82 subsq ( ( 𝐴 ∈ ℂ ∧ ( 𝑀 / 2 ) ∈ ℂ ) → ( ( 𝐴 ↑ 2 ) − ( ( 𝑀 / 2 ) ↑ 2 ) ) = ( ( 𝐴 + ( 𝑀 / 2 ) ) · ( 𝐴 − ( 𝑀 / 2 ) ) ) )
83 78 12 82 syl2anc ( ( 𝜑𝜓 ) → ( ( 𝐴 ↑ 2 ) − ( ( 𝑀 / 2 ) ↑ 2 ) ) = ( ( 𝐴 + ( 𝑀 / 2 ) ) · ( 𝐴 − ( 𝑀 / 2 ) ) ) )
84 32 oveq2d ( ( 𝜑𝜓 ) → ( ( 𝐴 ↑ 2 ) − ( ( 𝑀 / 2 ) ↑ 2 ) ) = ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
85 81 83 84 3eqtr2d ( ( 𝜑𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) · ( ( 𝐴 + ( 𝑀 / 2 ) ) − 𝑀 ) ) = ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
86 74 75 85 3eqtr2d ( ( 𝜑𝜓 ) → ( ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) − ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ) = ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )
87 71 86 breqtrd ( ( 𝜑𝜓 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 ↑ 2 ) − ( ( ( 𝑀 ↑ 2 ) / 2 ) / 2 ) ) )