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 47 zred ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℝ )
49 5 nnrpd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∈ ℝ+ )
50 48 49 modcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ∈ ℝ )
51 50 recnd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) ∈ ℂ )
52 0cnd ⊢ ( ( 𝜑 ∧ 𝜓 ) → 0 ∈ ℂ )
53 df-neg ⊢ - ( 𝑀 / 2 ) = ( 0 − ( 𝑀 / 2 ) )
54 43 3 53 3eqtr3g ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) − ( 𝑀 / 2 ) ) = ( 0 − ( 𝑀 / 2 ) ) )
55 51 52 12 54 subcan2d ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) = 0 )
56 dvdsval3 ⊢ ( ( 𝑀 ∈ ℕ ∧ ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℤ ) → ( 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ↔ ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) = 0 ) )
57 5 47 56 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ↔ ( ( 𝐴 + ( 𝑀 / 2 ) ) mod 𝑀 ) = 0 ) )
58 55 57 mpbird ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) )
59 dvdssq ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℤ ) → ( 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ↔ ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) ) )
60 6 47 59 syl2anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ↔ ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) ) )
61 58 60 mpbid ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) )
62 26 sqvald ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 ↑ 2 ) = ( 𝑀 · 𝑀 ) )
63 5 nnne0d ⊢ ( ( 𝜑 ∧ 𝜓 ) → 𝑀 ≠ 0 )
64 dvdsmulcr ⊢ ( ( 𝑀 ∈ ℤ ∧ ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℤ ∧ ( 𝑀 ∈ ℤ ∧ 𝑀 ≠ 0 ) ) → ( ( 𝑀 · 𝑀 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ↔ 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ) )
65 6 47 6 63 64 syl112anc ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝑀 · 𝑀 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ↔ 𝑀 ∥ ( 𝐴 + ( 𝑀 / 2 ) ) ) )
66 58 65 mpbird ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 · 𝑀 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) )
67 62 66 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( 𝑀 ↑ 2 ) ∥ ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) )
68 zsqcl ⊢ ( ( 𝐴 + ( 𝑀 / 2 ) ) ∈ ℤ → ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) ∈ ℤ )
69 47 68 syl ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) ↑ 2 ) ∈ ℤ )
70 47 6 zmulcld ⊢ ( ( 𝜑 ∧ 𝜓 ) → ( ( 𝐴 + ( 𝑀 / 2 ) ) · 𝑀 ) ∈ ℤ )
71 8 61 67 69 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 ) ) )