Proof of Theorem 4sqlem10
Step | Hyp | Ref
| Expression |
1 | | 4sqlem5.2 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ ℤ) |
2 | 1 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ ℤ) |
3 | | 4sqlem5.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑀 ∈ ℕ) |
4 | 3 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℕ) |
5 | 4 | nnred 11035 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℝ) |
6 | 5 | rehalfcld 11279 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → (𝑀 / 2) ∈ ℝ) |
7 | 6 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑀 / 2) ∈ ℂ) |
8 | 7 | negnegd 10383 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → --(𝑀 / 2) = (𝑀 / 2)) |
9 | | 4sqlem5.4 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐵 = (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) |
10 | 1, 3, 9 | 4sqlem5 15646 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ)) |
11 | 10 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → (𝐵 ∈ ℤ ∧ ((𝐴 − 𝐵) / 𝑀) ∈ ℤ)) |
12 | 11 | simpld 475 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ ℤ) |
13 | 12 | zred 11482 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ ℝ) |
14 | 1, 3, 9 | 4sqlem6 15647 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2))) |
15 | 14 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → (-(𝑀 / 2) ≤ 𝐵 ∧ 𝐵 < (𝑀 / 2))) |
16 | 15 | simprd 479 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → 𝐵 < (𝑀 / 2)) |
17 | 13, 16 | ltned 10173 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → 𝐵 ≠ (𝑀 / 2)) |
18 | 17 | neneqd 2799 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → ¬ 𝐵 = (𝑀 / 2)) |
19 | | 2cnd 11093 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝜓) → 2 ∈ ℂ) |
20 | 19 | sqvald 13005 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜓) → (2↑2) = (2 ·
2)) |
21 | 20 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → ((𝑀↑2) / (2↑2)) = ((𝑀↑2) / (2 · 2))) |
22 | 4 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℂ) |
23 | | 2ne0 11113 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 2 ≠
0 |
24 | 23 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜓) → 2 ≠ 0) |
25 | 22, 19, 24 | sqdivd 13021 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → ((𝑀 / 2)↑2) = ((𝑀↑2) / (2↑2))) |
26 | 22 | sqcld 13006 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∈ ℂ) |
27 | 26, 19, 19, 24, 24 | divdiv1d 10832 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → (((𝑀↑2) / 2) / 2) = ((𝑀↑2) / (2 · 2))) |
28 | 21, 25, 27 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → ((𝑀 / 2)↑2) = (((𝑀↑2) / 2) / 2)) |
29 | 26 | halfcld 11277 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜓) → ((𝑀↑2) / 2) ∈
ℂ) |
30 | 29 | halfcld 11277 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → (((𝑀↑2) / 2) / 2) ∈
ℂ) |
31 | 12 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝜓) → 𝐵 ∈ ℂ) |
32 | 31 | sqcld 13006 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) ∈ ℂ) |
33 | | 4sqlem10.5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝜓) → ((((𝑀↑2) / 2) / 2) − (𝐵↑2)) = 0) |
34 | 30, 32, 33 | subeq0d 10400 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝜓) → (((𝑀↑2) / 2) / 2) = (𝐵↑2)) |
35 | 28, 34 | eqtr2d 2657 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → (𝐵↑2) = ((𝑀 / 2)↑2)) |
36 | | sqeqor 12978 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐵 ∈ ℂ ∧ (𝑀 / 2) ∈ ℂ) →
((𝐵↑2) = ((𝑀 / 2)↑2) ↔ (𝐵 = (𝑀 / 2) ∨ 𝐵 = -(𝑀 / 2)))) |
37 | 31, 7, 36 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝜓) → ((𝐵↑2) = ((𝑀 / 2)↑2) ↔ (𝐵 = (𝑀 / 2) ∨ 𝐵 = -(𝑀 / 2)))) |
38 | 35, 37 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝜓) → (𝐵 = (𝑀 / 2) ∨ 𝐵 = -(𝑀 / 2))) |
39 | 38 | ord 392 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝜓) → (¬ 𝐵 = (𝑀 / 2) → 𝐵 = -(𝑀 / 2))) |
40 | 18, 39 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝜓) → 𝐵 = -(𝑀 / 2)) |
41 | 40, 12 | eqeltrrd 2702 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → -(𝑀 / 2) ∈ ℤ) |
42 | 41 | znegcld 11484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → --(𝑀 / 2) ∈ ℤ) |
43 | 8, 42 | eqeltrrd 2702 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑀 / 2) ∈ ℤ) |
44 | 2, 43 | zaddcld 11486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝐴 + (𝑀 / 2)) ∈ ℤ) |
45 | 44 | zred 11482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → (𝐴 + (𝑀 / 2)) ∈ ℝ) |
46 | 4 | nnrpd 11870 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈
ℝ+) |
47 | 45, 46 | modcld 12674 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) mod 𝑀) ∈ ℝ) |
48 | 47 | recnd 10068 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) mod 𝑀) ∈ ℂ) |
49 | | 0cnd 10033 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 0 ∈ ℂ) |
50 | | df-neg 10269 |
. . . . . . 7
⊢ -(𝑀 / 2) = (0 − (𝑀 / 2)) |
51 | 40, 9, 50 | 3eqtr3g 2679 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → (((𝐴 + (𝑀 / 2)) mod 𝑀) − (𝑀 / 2)) = (0 − (𝑀 / 2))) |
52 | 48, 49, 7, 51 | subcan2d 10434 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) mod 𝑀) = 0) |
53 | | dvdsval3 14987 |
. . . . . 6
⊢ ((𝑀 ∈ ℕ ∧ (𝐴 + (𝑀 / 2)) ∈ ℤ) → (𝑀 ∥ (𝐴 + (𝑀 / 2)) ↔ ((𝐴 + (𝑀 / 2)) mod 𝑀) = 0)) |
54 | 4, 44, 53 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝑀 ∥ (𝐴 + (𝑀 / 2)) ↔ ((𝐴 + (𝑀 / 2)) mod 𝑀) = 0)) |
55 | 52, 54 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∥ (𝐴 + (𝑀 / 2))) |
56 | 4 | nnzd 11481 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → 𝑀 ∈ ℤ) |
57 | | dvdssq 15280 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ (𝐴 + (𝑀 / 2)) ∈ ℤ) → (𝑀 ∥ (𝐴 + (𝑀 / 2)) ↔ (𝑀↑2) ∥ ((𝐴 + (𝑀 / 2))↑2))) |
58 | 56, 44, 57 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑀 ∥ (𝐴 + (𝑀 / 2)) ↔ (𝑀↑2) ∥ ((𝐴 + (𝑀 / 2))↑2))) |
59 | 55, 58 | mpbid 222 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴 + (𝑀 / 2))↑2)) |
60 | 22 | sqvald 13005 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) = (𝑀 · 𝑀)) |
61 | 4 | nnne0d 11065 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → 𝑀 ≠ 0) |
62 | | dvdsmulcr 15011 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ (𝐴 + (𝑀 / 2)) ∈ ℤ ∧ (𝑀 ∈ ℤ ∧ 𝑀 ≠ 0)) → ((𝑀 · 𝑀) ∥ ((𝐴 + (𝑀 / 2)) · 𝑀) ↔ 𝑀 ∥ (𝐴 + (𝑀 / 2)))) |
63 | 56, 44, 56, 61, 62 | syl112anc 1330 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝑀 · 𝑀) ∥ ((𝐴 + (𝑀 / 2)) · 𝑀) ↔ 𝑀 ∥ (𝐴 + (𝑀 / 2)))) |
64 | 55, 63 | mpbird 247 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑀 · 𝑀) ∥ ((𝐴 + (𝑀 / 2)) · 𝑀)) |
65 | 60, 64 | eqbrtrd 4675 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴 + (𝑀 / 2)) · 𝑀)) |
66 | | zsqcl 12934 |
. . . . 5
⊢ (𝑀 ∈ ℤ → (𝑀↑2) ∈
ℤ) |
67 | 56, 66 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∈ ℤ) |
68 | | zsqcl 12934 |
. . . . 5
⊢ ((𝐴 + (𝑀 / 2)) ∈ ℤ → ((𝐴 + (𝑀 / 2))↑2) ∈
ℤ) |
69 | 44, 68 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2))↑2) ∈
ℤ) |
70 | 44, 56 | zmulcld 11488 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) · 𝑀) ∈ ℤ) |
71 | | dvds2sub 15016 |
. . . 4
⊢ (((𝑀↑2) ∈ ℤ ∧
((𝐴 + (𝑀 / 2))↑2) ∈ ℤ ∧ ((𝐴 + (𝑀 / 2)) · 𝑀) ∈ ℤ) → (((𝑀↑2) ∥ ((𝐴 + (𝑀 / 2))↑2) ∧ (𝑀↑2) ∥ ((𝐴 + (𝑀 / 2)) · 𝑀)) → (𝑀↑2) ∥ (((𝐴 + (𝑀 / 2))↑2) − ((𝐴 + (𝑀 / 2)) · 𝑀)))) |
72 | 67, 69, 70, 71 | syl3anc 1326 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (((𝑀↑2) ∥ ((𝐴 + (𝑀 / 2))↑2) ∧ (𝑀↑2) ∥ ((𝐴 + (𝑀 / 2)) · 𝑀)) → (𝑀↑2) ∥ (((𝐴 + (𝑀 / 2))↑2) − ((𝐴 + (𝑀 / 2)) · 𝑀)))) |
73 | 59, 65, 72 | mp2and 715 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ (((𝐴 + (𝑀 / 2))↑2) − ((𝐴 + (𝑀 / 2)) · 𝑀))) |
74 | 44 | zcnd 11483 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → (𝐴 + (𝑀 / 2)) ∈ ℂ) |
75 | 74 | sqvald 13005 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2))↑2) = ((𝐴 + (𝑀 / 2)) · (𝐴 + (𝑀 / 2)))) |
76 | 75 | oveq1d 6665 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → (((𝐴 + (𝑀 / 2))↑2) − ((𝐴 + (𝑀 / 2)) · 𝑀)) = (((𝐴 + (𝑀 / 2)) · (𝐴 + (𝑀 / 2))) − ((𝐴 + (𝑀 / 2)) · 𝑀))) |
77 | 74, 74, 22 | subdid 10486 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) · ((𝐴 + (𝑀 / 2)) − 𝑀)) = (((𝐴 + (𝑀 / 2)) · (𝐴 + (𝑀 / 2))) − ((𝐴 + (𝑀 / 2)) · 𝑀))) |
78 | 22 | 2halvesd 11278 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → ((𝑀 / 2) + (𝑀 / 2)) = 𝑀) |
79 | 78 | oveq2d 6666 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) − ((𝑀 / 2) + (𝑀 / 2))) = ((𝐴 + (𝑀 / 2)) − 𝑀)) |
80 | 2 | zcnd 11483 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝜓) → 𝐴 ∈ ℂ) |
81 | 80, 7, 7 | pnpcan2d 10430 |
. . . . . 6
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) − ((𝑀 / 2) + (𝑀 / 2))) = (𝐴 − (𝑀 / 2))) |
82 | 79, 81 | eqtr3d 2658 |
. . . . 5
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) − 𝑀) = (𝐴 − (𝑀 / 2))) |
83 | 82 | oveq2d 6666 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) · ((𝐴 + (𝑀 / 2)) − 𝑀)) = ((𝐴 + (𝑀 / 2)) · (𝐴 − (𝑀 / 2)))) |
84 | | subsq 12972 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ (𝑀 / 2) ∈ ℂ) →
((𝐴↑2) − ((𝑀 / 2)↑2)) = ((𝐴 + (𝑀 / 2)) · (𝐴 − (𝑀 / 2)))) |
85 | 80, 7, 84 | syl2anc 693 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝐴↑2) − ((𝑀 / 2)↑2)) = ((𝐴 + (𝑀 / 2)) · (𝐴 − (𝑀 / 2)))) |
86 | 28 | oveq2d 6666 |
. . . 4
⊢ ((𝜑 ∧ 𝜓) → ((𝐴↑2) − ((𝑀 / 2)↑2)) = ((𝐴↑2) − (((𝑀↑2) / 2) / 2))) |
87 | 83, 85, 86 | 3eqtr2d 2662 |
. . 3
⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + (𝑀 / 2)) · ((𝐴 + (𝑀 / 2)) − 𝑀)) = ((𝐴↑2) − (((𝑀↑2) / 2) / 2))) |
88 | 76, 77, 87 | 3eqtr2d 2662 |
. 2
⊢ ((𝜑 ∧ 𝜓) → (((𝐴 + (𝑀 / 2))↑2) − ((𝐴 + (𝑀 / 2)) · 𝑀)) = ((𝐴↑2) − (((𝑀↑2) / 2) / 2))) |
89 | 73, 88 | breqtrd 4679 |
1
⊢ ((𝜑 ∧ 𝜓) → (𝑀↑2) ∥ ((𝐴↑2) − (((𝑀↑2) / 2) / 2))) |