Proof of Theorem jm2.27c
Step | Hyp | Ref
| Expression |
1 | | jm2.27c5 |
. . . 4
⊢ 𝐷 = (𝐴 Xrm 𝐵) |
2 | | jm2.27a1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈
(ℤ≥‘2)) |
3 | | jm2.27a2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ ℕ) |
4 | 3 | nnzd 11833 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℤ) |
5 | | frmx 38429 |
. . . . . 6
⊢
Xrm :((ℤ≥‘2) ×
ℤ)⟶ℕ0 |
6 | 5 | fovcl 7042 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (𝐴 Xrm 𝐵) ∈
ℕ0) |
7 | 2, 4, 6 | syl2anc 579 |
. . . 4
⊢ (𝜑 → (𝐴 Xrm 𝐵) ∈
ℕ0) |
8 | 1, 7 | syl5eqel 2862 |
. . 3
⊢ (𝜑 → 𝐷 ∈
ℕ0) |
9 | | jm2.27c7 |
. . . 4
⊢ 𝐸 = (𝐴 Yrm (2 · 𝑄)) |
10 | | 2z 11761 |
. . . . . . 7
⊢ 2 ∈
ℤ |
11 | | jm2.27c6 |
. . . . . . . 8
⊢ 𝑄 = (𝐵 · (𝐴 Yrm 𝐵)) |
12 | | jm2.27c4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 = (𝐴 Yrm 𝐵)) |
13 | | jm2.27a3 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℕ) |
14 | 13 | nnzd 11833 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐶 ∈ ℤ) |
15 | 12, 14 | eqeltrrd 2859 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 Yrm 𝐵) ∈ ℤ) |
16 | 4, 15 | zmulcld 11840 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∈ ℤ) |
17 | 11, 16 | syl5eqel 2862 |
. . . . . . 7
⊢ (𝜑 → 𝑄 ∈ ℤ) |
18 | | zmulcl 11778 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝑄
∈ ℤ) → (2 · 𝑄) ∈ ℤ) |
19 | 10, 17, 18 | sylancr 581 |
. . . . . 6
⊢ (𝜑 → (2 · 𝑄) ∈
ℤ) |
20 | | frmy 38430 |
. . . . . . 7
⊢
Yrm :((ℤ≥‘2) ×
ℤ)⟶ℤ |
21 | 20 | fovcl 7042 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Yrm (2 · 𝑄)) ∈
ℤ) |
22 | 2, 19, 21 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (𝐴 Yrm (2 · 𝑄)) ∈
ℤ) |
23 | | rmy0 38445 |
. . . . . . 7
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Yrm 0) = 0) |
24 | 2, 23 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐴 Yrm 0) = 0) |
25 | | 2nn 11448 |
. . . . . . . . . 10
⊢ 2 ∈
ℕ |
26 | 12, 13 | eqeltrrd 2859 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 Yrm 𝐵) ∈ ℕ) |
27 | 3, 26 | nnmulcld 11428 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∈ ℕ) |
28 | 11, 27 | syl5eqel 2862 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑄 ∈ ℕ) |
29 | | nnmulcl 11399 |
. . . . . . . . . 10
⊢ ((2
∈ ℕ ∧ 𝑄
∈ ℕ) → (2 · 𝑄) ∈ ℕ) |
30 | 25, 28, 29 | sylancr 581 |
. . . . . . . . 9
⊢ (𝜑 → (2 · 𝑄) ∈
ℕ) |
31 | 30 | nnnn0d 11702 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝑄) ∈
ℕ0) |
32 | 31 | nn0ge0d 11705 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ (2 · 𝑄)) |
33 | | 0zd 11740 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℤ) |
34 | | lermy 38473 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ (2 · 𝑄) ∈ ℤ) → (0 ≤
(2 · 𝑄) ↔
(𝐴 Yrm 0) ≤
(𝐴 Yrm (2
· 𝑄)))) |
35 | 2, 33, 19, 34 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → (0 ≤ (2 · 𝑄) ↔ (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄)))) |
36 | 32, 35 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → (𝐴 Yrm 0) ≤ (𝐴 Yrm (2 · 𝑄))) |
37 | 24, 36 | eqbrtrrd 4910 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐴 Yrm (2 · 𝑄))) |
38 | | elnn0z 11741 |
. . . . 5
⊢ ((𝐴 Yrm (2 ·
𝑄)) ∈
ℕ0 ↔ ((𝐴 Yrm (2 · 𝑄)) ∈ ℤ ∧ 0 ≤
(𝐴 Yrm (2
· 𝑄)))) |
39 | 22, 37, 38 | sylanbrc 578 |
. . . 4
⊢ (𝜑 → (𝐴 Yrm (2 · 𝑄)) ∈
ℕ0) |
40 | 9, 39 | syl5eqel 2862 |
. . 3
⊢ (𝜑 → 𝐸 ∈
ℕ0) |
41 | | jm2.27c8 |
. . . 4
⊢ 𝐹 = (𝐴 Xrm (2 · 𝑄)) |
42 | 5 | fovcl 7042 |
. . . . 5
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Xrm (2 · 𝑄)) ∈
ℕ0) |
43 | 2, 19, 42 | syl2anc 579 |
. . . 4
⊢ (𝜑 → (𝐴 Xrm (2 · 𝑄)) ∈
ℕ0) |
44 | 41, 43 | syl5eqel 2862 |
. . 3
⊢ (𝜑 → 𝐹 ∈
ℕ0) |
45 | 8, 40, 44 | 3jca 1119 |
. 2
⊢ (𝜑 → (𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0
∧ 𝐹 ∈
ℕ0)) |
46 | | 2nn0 11661 |
. . . 4
⊢ 2 ∈
ℕ0 |
47 | | jm2.27c9 |
. . . . 5
⊢ 𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) |
48 | 44 | nn0cnd 11704 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 ∈ ℂ) |
49 | 48 | sqvald 13324 |
. . . . . . . 8
⊢ (𝜑 → (𝐹↑2) = (𝐹 · 𝐹)) |
50 | 44, 44 | nn0mulcld 11707 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 · 𝐹) ∈
ℕ0) |
51 | 49, 50 | eqeltrd 2858 |
. . . . . . 7
⊢ (𝜑 → (𝐹↑2) ∈
ℕ0) |
52 | | eluz2nn 12032 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℕ) |
53 | 2, 52 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℕ) |
54 | 53 | nnnn0d 11702 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈
ℕ0) |
55 | 54 | nn0red 11703 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ ℝ) |
56 | 44 | nn0red 11703 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ∈ ℝ) |
57 | 56, 56 | remulcld 10407 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 · 𝐹) ∈ ℝ) |
58 | | rmx1 38442 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈
(ℤ≥‘2) → (𝐴 Xrm 1) = 𝐴) |
59 | 2, 58 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 Xrm 1) = 𝐴) |
60 | 30 | nnge1d 11423 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 1 ≤ (2 · 𝑄)) |
61 | | 1nn0 11660 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℕ0 |
62 | 61 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 1 ∈
ℕ0) |
63 | | lermxnn0 38468 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 1 ∈ ℕ0 ∧ (2
· 𝑄) ∈
ℕ0) → (1 ≤ (2 · 𝑄) ↔ (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄)))) |
64 | 2, 62, 31, 63 | syl3anc 1439 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (1 ≤ (2 · 𝑄) ↔ (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄)))) |
65 | 60, 64 | mpbid 224 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴 Xrm 1) ≤ (𝐴 Xrm (2 · 𝑄))) |
66 | 59, 65 | eqbrtrrd 4910 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ≤ (𝐴 Xrm (2 · 𝑄))) |
67 | 66, 41 | syl6breqr 4928 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ≤ 𝐹) |
68 | 44 | nn0ge0d 11705 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ 𝐹) |
69 | | rmxnn 38469 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (2 · 𝑄) ∈ ℤ) → (𝐴 Xrm (2 · 𝑄)) ∈
ℕ) |
70 | 2, 19, 69 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 Xrm (2 · 𝑄)) ∈
ℕ) |
71 | 41, 70 | syl5eqel 2862 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐹 ∈ ℕ) |
72 | 71 | nnge1d 11423 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ≤ 𝐹) |
73 | 56, 56, 68, 72 | lemulge12d 11316 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹 ≤ (𝐹 · 𝐹)) |
74 | 55, 56, 57, 67, 73 | letrd 10533 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ≤ (𝐹 · 𝐹)) |
75 | 74, 49 | breqtrrd 4914 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ≤ (𝐹↑2)) |
76 | | nn0sub 11694 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℕ0
∧ (𝐹↑2) ∈
ℕ0) → (𝐴 ≤ (𝐹↑2) ↔ ((𝐹↑2) − 𝐴) ∈
ℕ0)) |
77 | 54, 51, 76 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ≤ (𝐹↑2) ↔ ((𝐹↑2) − 𝐴) ∈
ℕ0)) |
78 | 75, 77 | mpbid 224 |
. . . . . . 7
⊢ (𝜑 → ((𝐹↑2) − 𝐴) ∈
ℕ0) |
79 | 51, 78 | nn0mulcld 11707 |
. . . . . 6
⊢ (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈
ℕ0) |
80 | | uzaddcl 12050 |
. . . . . 6
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℕ0) → (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) ∈
(ℤ≥‘2)) |
81 | 2, 79, 80 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) ∈
(ℤ≥‘2)) |
82 | 47, 81 | syl5eqel 2862 |
. . . 4
⊢ (𝜑 → 𝐺 ∈
(ℤ≥‘2)) |
83 | | eluznn0 12064 |
. . . 4
⊢ ((2
∈ ℕ0 ∧ 𝐺 ∈ (ℤ≥‘2))
→ 𝐺 ∈
ℕ0) |
84 | 46, 82, 83 | sylancr 581 |
. . 3
⊢ (𝜑 → 𝐺 ∈
ℕ0) |
85 | | jm2.27c10 |
. . . 4
⊢ 𝐻 = (𝐺 Yrm 𝐵) |
86 | 20 | fovcl 7042 |
. . . . . 6
⊢ ((𝐺 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (𝐺 Yrm 𝐵) ∈ ℤ) |
87 | 82, 4, 86 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → (𝐺 Yrm 𝐵) ∈ ℤ) |
88 | | rmy0 38445 |
. . . . . . 7
⊢ (𝐺 ∈
(ℤ≥‘2) → (𝐺 Yrm 0) = 0) |
89 | 82, 88 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝐺 Yrm 0) = 0) |
90 | 3 | nnnn0d 11702 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈
ℕ0) |
91 | 90 | nn0ge0d 11705 |
. . . . . . 7
⊢ (𝜑 → 0 ≤ 𝐵) |
92 | | lermy 38473 |
. . . . . . . 8
⊢ ((𝐺 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ 𝐵 ∈ ℤ) → (0 ≤ 𝐵 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵))) |
93 | 82, 33, 4, 92 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → (0 ≤ 𝐵 ↔ (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵))) |
94 | 91, 93 | mpbid 224 |
. . . . . 6
⊢ (𝜑 → (𝐺 Yrm 0) ≤ (𝐺 Yrm 𝐵)) |
95 | 89, 94 | eqbrtrrd 4910 |
. . . . 5
⊢ (𝜑 → 0 ≤ (𝐺 Yrm 𝐵)) |
96 | | elnn0z 11741 |
. . . . 5
⊢ ((𝐺 Yrm 𝐵) ∈ ℕ0
↔ ((𝐺 Yrm
𝐵) ∈ ℤ ∧ 0
≤ (𝐺 Yrm
𝐵))) |
97 | 87, 95, 96 | sylanbrc 578 |
. . . 4
⊢ (𝜑 → (𝐺 Yrm 𝐵) ∈
ℕ0) |
98 | 85, 97 | syl5eqel 2862 |
. . 3
⊢ (𝜑 → 𝐻 ∈
ℕ0) |
99 | | jm2.27c11 |
. . . 4
⊢ 𝐼 = (𝐺 Xrm 𝐵) |
100 | 5 | fovcl 7042 |
. . . . 5
⊢ ((𝐺 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (𝐺 Xrm 𝐵) ∈
ℕ0) |
101 | 82, 4, 100 | syl2anc 579 |
. . . 4
⊢ (𝜑 → (𝐺 Xrm 𝐵) ∈
ℕ0) |
102 | 99, 101 | syl5eqel 2862 |
. . 3
⊢ (𝜑 → 𝐼 ∈
ℕ0) |
103 | 84, 98, 102 | 3jca 1119 |
. 2
⊢ (𝜑 → (𝐺 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0
∧ 𝐼 ∈
ℕ0)) |
104 | | jm2.27c12 |
. . . 4
⊢ 𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1) |
105 | | iddvds 15402 |
. . . . . . . . . . . 12
⊢ ((𝐵 · (𝐴 Yrm 𝐵)) ∈ ℤ → (𝐵 · (𝐴 Yrm 𝐵)) ∥ (𝐵 · (𝐴 Yrm 𝐵))) |
106 | 16, 105 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∥ (𝐵 · (𝐴 Yrm 𝐵))) |
107 | 106, 11 | syl6breqr 4928 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄) |
108 | | jm2.20nn 38515 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑄 ∈ ℕ ∧ 𝐵 ∈ ℕ) → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄)) |
109 | 2, 28, 3, 108 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) ↔ (𝐵 · (𝐴 Yrm 𝐵)) ∥ 𝑄)) |
110 | 107, 109 | mpbird 249 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄)) |
111 | | zsqcl 13253 |
. . . . . . . . . . 11
⊢ ((𝐴 Yrm 𝐵) ∈ ℤ → ((𝐴 Yrm 𝐵)↑2) ∈
ℤ) |
112 | 15, 111 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐴 Yrm 𝐵)↑2) ∈ ℤ) |
113 | 20 | fovcl 7042 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Yrm 𝑄) ∈ ℤ) |
114 | 2, 17, 113 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 Yrm 𝑄) ∈ ℤ) |
115 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → 2 ∈
ℤ) |
116 | | dvdscmul 15415 |
. . . . . . . . . 10
⊢ ((((𝐴 Yrm 𝐵)↑2) ∈ ℤ ∧
(𝐴 Yrm 𝑄) ∈ ℤ ∧ 2 ∈
ℤ) → (((𝐴
Yrm 𝐵)↑2)
∥ (𝐴 Yrm
𝑄) → (2 ·
((𝐴 Yrm 𝐵)↑2)) ∥ (2 ·
(𝐴 Yrm 𝑄)))) |
117 | 112, 114,
115, 116 | syl3anc 1439 |
. . . . . . . . 9
⊢ (𝜑 → (((𝐴 Yrm 𝐵)↑2) ∥ (𝐴 Yrm 𝑄) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 · (𝐴 Yrm 𝑄)))) |
118 | 110, 117 | mpd 15 |
. . . . . . . 8
⊢ (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 ·
(𝐴 Yrm 𝑄))) |
119 | | zmulcl 11778 |
. . . . . . . . . . 11
⊢ ((2
∈ ℤ ∧ (𝐴
Yrm 𝑄) ∈
ℤ) → (2 · (𝐴 Yrm 𝑄)) ∈ ℤ) |
120 | 10, 114, 119 | sylancr 581 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∈
ℤ) |
121 | 5 | fovcl 7042 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Xrm 𝑄) ∈
ℕ0) |
122 | 2, 17, 121 | syl2anc 579 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∈
ℕ0) |
123 | 122 | nn0zd 11832 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∈ ℤ) |
124 | | dvdsmul1 15410 |
. . . . . . . . . 10
⊢ (((2
· (𝐴 Yrm
𝑄)) ∈ ℤ ∧
(𝐴 Xrm 𝑄) ∈ ℤ) → (2
· (𝐴 Yrm
𝑄)) ∥ ((2 ·
(𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄))) |
125 | 120, 123,
124 | syl2anc 579 |
. . . . . . . . 9
⊢ (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∥ ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄))) |
126 | | rmydbl 38456 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝑄 ∈ ℤ) → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄))) |
127 | 2, 17, 126 | syl2anc 579 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄))) |
128 | | 2cnd 11453 |
. . . . . . . . . . 11
⊢ (𝜑 → 2 ∈
ℂ) |
129 | 122 | nn0cnd 11704 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 Xrm 𝑄) ∈ ℂ) |
130 | 114 | zcnd 11835 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴 Yrm 𝑄) ∈ ℂ) |
131 | 128, 129,
130 | mul32d 10586 |
. . . . . . . . . 10
⊢ (𝜑 → ((2 · (𝐴 Xrm 𝑄)) · (𝐴 Yrm 𝑄)) = ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄))) |
132 | 127, 131 | eqtrd 2813 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 Yrm (2 · 𝑄)) = ((2 · (𝐴 Yrm 𝑄)) · (𝐴 Xrm 𝑄))) |
133 | 125, 132 | breqtrrd 4914 |
. . . . . . . 8
⊢ (𝜑 → (2 · (𝐴 Yrm 𝑄)) ∥ (𝐴 Yrm (2 · 𝑄))) |
134 | | zmulcl 11778 |
. . . . . . . . . 10
⊢ ((2
∈ ℤ ∧ ((𝐴
Yrm 𝐵)↑2)
∈ ℤ) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∈ ℤ) |
135 | 10, 112, 134 | sylancr 581 |
. . . . . . . . 9
⊢ (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∈
ℤ) |
136 | | dvdstr 15425 |
. . . . . . . . 9
⊢ (((2
· ((𝐴 Yrm
𝐵)↑2)) ∈ ℤ
∧ (2 · (𝐴
Yrm 𝑄)) ∈
ℤ ∧ (𝐴
Yrm (2 · 𝑄)) ∈ ℤ) → (((2 ·
((𝐴 Yrm 𝐵)↑2)) ∥ (2 ·
(𝐴 Yrm 𝑄)) ∧ (2 · (𝐴 Yrm 𝑄)) ∥ (𝐴 Yrm (2 · 𝑄))) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (𝐴 Yrm (2 ·
𝑄)))) |
137 | 135, 120,
22, 136 | syl3anc 1439 |
. . . . . . . 8
⊢ (𝜑 → (((2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (2 ·
(𝐴 Yrm 𝑄)) ∧ (2 · (𝐴 Yrm 𝑄)) ∥ (𝐴 Yrm (2 · 𝑄))) → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (𝐴 Yrm (2 ·
𝑄)))) |
138 | 118, 133,
137 | mp2and 689 |
. . . . . . 7
⊢ (𝜑 → (2 · ((𝐴 Yrm 𝐵)↑2)) ∥ (𝐴 Yrm (2 ·
𝑄))) |
139 | 12 | oveq1d 6937 |
. . . . . . . 8
⊢ (𝜑 → (𝐶↑2) = ((𝐴 Yrm 𝐵)↑2)) |
140 | 139 | oveq2d 6938 |
. . . . . . 7
⊢ (𝜑 → (2 · (𝐶↑2)) = (2 · ((𝐴 Yrm 𝐵)↑2))) |
141 | 9 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐸 = (𝐴 Yrm (2 · 𝑄))) |
142 | 138, 140,
141 | 3brtr4d 4918 |
. . . . . 6
⊢ (𝜑 → (2 · (𝐶↑2)) ∥ 𝐸) |
143 | 9, 22 | syl5eqel 2862 |
. . . . . . . 8
⊢ (𝜑 → 𝐸 ∈ ℤ) |
144 | 30 | nngt0d 11424 |
. . . . . . . . . 10
⊢ (𝜑 → 0 < (2 · 𝑄)) |
145 | | ltrmy 38470 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 0 ∈ ℤ ∧ (2 · 𝑄) ∈ ℤ) → (0 <
(2 · 𝑄) ↔
(𝐴 Yrm 0) <
(𝐴 Yrm (2
· 𝑄)))) |
146 | 2, 33, 19, 145 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → (0 < (2 · 𝑄) ↔ (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄)))) |
147 | 144, 146 | mpbid 224 |
. . . . . . . . 9
⊢ (𝜑 → (𝐴 Yrm 0) < (𝐴 Yrm (2 · 𝑄))) |
148 | 24 | eqcomd 2783 |
. . . . . . . . 9
⊢ (𝜑 → 0 = (𝐴 Yrm 0)) |
149 | 147, 148,
141 | 3brtr4d 4918 |
. . . . . . . 8
⊢ (𝜑 → 0 < 𝐸) |
150 | | elnnz 11738 |
. . . . . . . 8
⊢ (𝐸 ∈ ℕ ↔ (𝐸 ∈ ℤ ∧ 0 <
𝐸)) |
151 | 143, 149,
150 | sylanbrc 578 |
. . . . . . 7
⊢ (𝜑 → 𝐸 ∈ ℕ) |
152 | 13 | nnsqcld 13350 |
. . . . . . . 8
⊢ (𝜑 → (𝐶↑2) ∈ ℕ) |
153 | | nnmulcl 11399 |
. . . . . . . 8
⊢ ((2
∈ ℕ ∧ (𝐶↑2) ∈ ℕ) → (2 ·
(𝐶↑2)) ∈
ℕ) |
154 | 25, 152, 153 | sylancr 581 |
. . . . . . 7
⊢ (𝜑 → (2 · (𝐶↑2)) ∈
ℕ) |
155 | | nndivdvds 15396 |
. . . . . . 7
⊢ ((𝐸 ∈ ℕ ∧ (2
· (𝐶↑2)) ∈
ℕ) → ((2 · (𝐶↑2)) ∥ 𝐸 ↔ (𝐸 / (2 · (𝐶↑2))) ∈ ℕ)) |
156 | 151, 154,
155 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → ((2 · (𝐶↑2)) ∥ 𝐸 ↔ (𝐸 / (2 · (𝐶↑2))) ∈ ℕ)) |
157 | 142, 156 | mpbid 224 |
. . . . 5
⊢ (𝜑 → (𝐸 / (2 · (𝐶↑2))) ∈ ℕ) |
158 | | nnm1nn0 11685 |
. . . . 5
⊢ ((𝐸 / (2 · (𝐶↑2))) ∈ ℕ →
((𝐸 / (2 · (𝐶↑2))) − 1) ∈
ℕ0) |
159 | 157, 158 | syl 17 |
. . . 4
⊢ (𝜑 → ((𝐸 / (2 · (𝐶↑2))) − 1) ∈
ℕ0) |
160 | 104, 159 | syl5eqel 2862 |
. . 3
⊢ (𝜑 → 𝐽 ∈
ℕ0) |
161 | 1 | oveq1i 6932 |
. . . . . . . 8
⊢ (𝐷↑2) = ((𝐴 Xrm 𝐵)↑2) |
162 | 161 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝐷↑2) = ((𝐴 Xrm 𝐵)↑2)) |
163 | 139 | oveq2d 6938 |
. . . . . . 7
⊢ (𝜑 → (((𝐴↑2) − 1) · (𝐶↑2)) = (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))) |
164 | 162, 163 | oveq12d 6940 |
. . . . . 6
⊢ (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) ·
((𝐴 Yrm 𝐵)↑2)))) |
165 | | rmxynorm 38434 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))) =
1) |
166 | 2, 4, 165 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → (((𝐴 Xrm 𝐵)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝐵)↑2))) =
1) |
167 | 164, 166 | eqtrd 2813 |
. . . . 5
⊢ (𝜑 → ((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1) |
168 | 41 | oveq1i 6932 |
. . . . . . 7
⊢ (𝐹↑2) = ((𝐴 Xrm (2 · 𝑄))↑2) |
169 | 9 | oveq1i 6932 |
. . . . . . . 8
⊢ (𝐸↑2) = ((𝐴 Yrm (2 · 𝑄))↑2) |
170 | 169 | oveq2i 6933 |
. . . . . . 7
⊢ (((𝐴↑2) − 1) ·
(𝐸↑2)) = (((𝐴↑2) − 1) ·
((𝐴 Yrm (2
· 𝑄))↑2)) |
171 | 168, 170 | oveq12i 6934 |
. . . . . 6
⊢ ((𝐹↑2) − (((𝐴↑2) − 1) ·
(𝐸↑2))) = (((𝐴 Xrm (2 ·
𝑄))↑2) −
(((𝐴↑2) − 1)
· ((𝐴 Yrm
(2 · 𝑄))↑2))) |
172 | | rmxynorm 38434 |
. . . . . . 7
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ (2 · 𝑄) ∈ ℤ) → (((𝐴 Xrm (2 ·
𝑄))↑2) −
(((𝐴↑2) − 1)
· ((𝐴 Yrm
(2 · 𝑄))↑2))) =
1) |
173 | 2, 19, 172 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → (((𝐴 Xrm (2 · 𝑄))↑2) − (((𝐴↑2) − 1) ·
((𝐴 Yrm (2
· 𝑄))↑2))) =
1) |
174 | 171, 173 | syl5eq 2825 |
. . . . 5
⊢ (𝜑 → ((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1) |
175 | 167, 174,
82 | 3jca 1119 |
. . . 4
⊢ (𝜑 → (((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝐹↑2) − (((𝐴↑2) − 1) ·
(𝐸↑2))) = 1 ∧
𝐺 ∈
(ℤ≥‘2))) |
176 | 99 | oveq1i 6932 |
. . . . . . 7
⊢ (𝐼↑2) = ((𝐺 Xrm 𝐵)↑2) |
177 | 85 | oveq1i 6932 |
. . . . . . . 8
⊢ (𝐻↑2) = ((𝐺 Yrm 𝐵)↑2) |
178 | 177 | oveq2i 6933 |
. . . . . . 7
⊢ (((𝐺↑2) − 1) ·
(𝐻↑2)) = (((𝐺↑2) − 1) ·
((𝐺 Yrm 𝐵)↑2)) |
179 | 176, 178 | oveq12i 6934 |
. . . . . 6
⊢ ((𝐼↑2) − (((𝐺↑2) − 1) ·
(𝐻↑2))) = (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) ·
((𝐺 Yrm 𝐵)↑2))) |
180 | | rmxynorm 38434 |
. . . . . . 7
⊢ ((𝐺 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ ℤ) → (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))) =
1) |
181 | 82, 4, 180 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → (((𝐺 Xrm 𝐵)↑2) − (((𝐺↑2) − 1) · ((𝐺 Yrm 𝐵)↑2))) =
1) |
182 | 179, 181 | syl5eq 2825 |
. . . . 5
⊢ (𝜑 → ((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1) |
183 | 104 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 = ((𝐸 / (2 · (𝐶↑2))) − 1)) |
184 | 183 | oveq1d 6937 |
. . . . . . . 8
⊢ (𝜑 → (𝐽 + 1) = (((𝐸 / (2 · (𝐶↑2))) − 1) + 1)) |
185 | 143 | zcnd 11835 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐸 ∈ ℂ) |
186 | 154 | nncnd 11392 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · (𝐶↑2)) ∈
ℂ) |
187 | 154 | nnne0d 11425 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · (𝐶↑2)) ≠
0) |
188 | 185, 186,
187 | divcld 11151 |
. . . . . . . . 9
⊢ (𝜑 → (𝐸 / (2 · (𝐶↑2))) ∈ ℂ) |
189 | | ax-1cn 10330 |
. . . . . . . . 9
⊢ 1 ∈
ℂ |
190 | | npcan 10632 |
. . . . . . . . 9
⊢ (((𝐸 / (2 · (𝐶↑2))) ∈ ℂ ∧
1 ∈ ℂ) → (((𝐸 / (2 · (𝐶↑2))) − 1) + 1) = (𝐸 / (2 · (𝐶↑2)))) |
191 | 188, 189,
190 | sylancl 580 |
. . . . . . . 8
⊢ (𝜑 → (((𝐸 / (2 · (𝐶↑2))) − 1) + 1) = (𝐸 / (2 · (𝐶↑2)))) |
192 | 184, 191 | eqtrd 2813 |
. . . . . . 7
⊢ (𝜑 → (𝐽 + 1) = (𝐸 / (2 · (𝐶↑2)))) |
193 | 192 | oveq1d 6937 |
. . . . . 6
⊢ (𝜑 → ((𝐽 + 1) · (2 · (𝐶↑2))) = ((𝐸 / (2 · (𝐶↑2))) · (2 · (𝐶↑2)))) |
194 | 185, 186,
187 | divcan1d 11152 |
. . . . . 6
⊢ (𝜑 → ((𝐸 / (2 · (𝐶↑2))) · (2 · (𝐶↑2))) = 𝐸) |
195 | 193, 194 | eqtr2d 2814 |
. . . . 5
⊢ (𝜑 → 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2)))) |
196 | 44 | nn0zd 11832 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ ℤ) |
197 | 78 | nn0zd 11832 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℤ) |
198 | 196, 197 | zmulcld 11840 |
. . . . . . 7
⊢ (𝜑 → (𝐹 · ((𝐹↑2) − 𝐴)) ∈ ℤ) |
199 | | dvdsmul1 15410 |
. . . . . . 7
⊢ ((𝐹 ∈ ℤ ∧ (𝐹 · ((𝐹↑2) − 𝐴)) ∈ ℤ) → 𝐹 ∥ (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴)))) |
200 | 196, 198,
199 | syl2anc 579 |
. . . . . 6
⊢ (𝜑 → 𝐹 ∥ (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴)))) |
201 | 47 | oveq1i 6932 |
. . . . . . 7
⊢ (𝐺 − 𝐴) = ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴) |
202 | 54 | nn0cnd 11704 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) |
203 | 79 | nn0cnd 11704 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℂ) |
204 | 202, 203 | pncan2d 10736 |
. . . . . . . 8
⊢ (𝜑 → ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴) = ((𝐹↑2) · ((𝐹↑2) − 𝐴))) |
205 | 49 | oveq1d 6937 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) = ((𝐹 · 𝐹) · ((𝐹↑2) − 𝐴))) |
206 | 78 | nn0cnd 11704 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹↑2) − 𝐴) ∈ ℂ) |
207 | 48, 48, 206 | mulassd 10400 |
. . . . . . . 8
⊢ (𝜑 → ((𝐹 · 𝐹) · ((𝐹↑2) − 𝐴)) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴)))) |
208 | 204, 205,
207 | 3eqtrd 2817 |
. . . . . . 7
⊢ (𝜑 → ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − 𝐴) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴)))) |
209 | 201, 208 | syl5eq 2825 |
. . . . . 6
⊢ (𝜑 → (𝐺 − 𝐴) = (𝐹 · (𝐹 · ((𝐹↑2) − 𝐴)))) |
210 | 200, 209 | breqtrrd 4914 |
. . . . 5
⊢ (𝜑 → 𝐹 ∥ (𝐺 − 𝐴)) |
211 | 182, 195,
210 | 3jca 1119 |
. . . 4
⊢ (𝜑 → (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺 − 𝐴))) |
212 | | zmulcl 11778 |
. . . . . . . 8
⊢ ((2
∈ ℤ ∧ 𝐶
∈ ℤ) → (2 · 𝐶) ∈ ℤ) |
213 | 10, 14, 212 | sylancr 581 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐶) ∈
ℤ) |
214 | | eluzelz 12002 |
. . . . . . . 8
⊢ (𝐴 ∈
(ℤ≥‘2) → 𝐴 ∈ ℤ) |
215 | 2, 214 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℤ) |
216 | 79 | nn0zd 11832 |
. . . . . . 7
⊢ (𝜑 → ((𝐹↑2) · ((𝐹↑2) − 𝐴)) ∈ ℤ) |
217 | | 1z 11759 |
. . . . . . . 8
⊢ 1 ∈
ℤ |
218 | | zsubcl 11771 |
. . . . . . . . 9
⊢ ((1
∈ ℤ ∧ 𝐴
∈ ℤ) → (1 − 𝐴) ∈ ℤ) |
219 | 217, 215,
218 | sylancr 581 |
. . . . . . . 8
⊢ (𝜑 → (1 − 𝐴) ∈
ℤ) |
220 | | zmulcl 11778 |
. . . . . . . 8
⊢ ((1
∈ ℤ ∧ (1 − 𝐴) ∈ ℤ) → (1 · (1
− 𝐴)) ∈
ℤ) |
221 | 217, 219,
220 | sylancr 581 |
. . . . . . 7
⊢ (𝜑 → (1 · (1 −
𝐴)) ∈
ℤ) |
222 | | congid 38489 |
. . . . . . . 8
⊢ (((2
· 𝐶) ∈ ℤ
∧ 𝐴 ∈ ℤ)
→ (2 · 𝐶)
∥ (𝐴 − 𝐴)) |
223 | 213, 215,
222 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐴 − 𝐴)) |
224 | 51 | nn0zd 11832 |
. . . . . . . 8
⊢ (𝜑 → (𝐹↑2) ∈ ℤ) |
225 | 217 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℤ) |
226 | 13 | nncnd 11392 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ ℂ) |
227 | 128, 226,
226 | mulassd 10400 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((2 · 𝐶) · 𝐶) = (2 · (𝐶 · 𝐶))) |
228 | 226 | sqvald 13324 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝐶↑2) = (𝐶 · 𝐶)) |
229 | 228 | oveq2d 6938 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (2 · (𝐶↑2)) = (2 · (𝐶 · 𝐶))) |
230 | 227, 229 | eqtr4d 2816 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((2 · 𝐶) · 𝐶) = (2 · (𝐶↑2))) |
231 | 230, 142 | eqbrtrd 4908 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((2 · 𝐶) · 𝐶) ∥ 𝐸) |
232 | | muldvds1 15413 |
. . . . . . . . . . . . 13
⊢ (((2
· 𝐶) ∈ ℤ
∧ 𝐶 ∈ ℤ
∧ 𝐸 ∈ ℤ)
→ (((2 · 𝐶)
· 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ 𝐸)) |
233 | 213, 14, 143, 232 | syl3anc 1439 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((2 · 𝐶) · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ 𝐸)) |
234 | 231, 233 | mpd 15 |
. . . . . . . . . . 11
⊢ (𝜑 → (2 · 𝐶) ∥ 𝐸) |
235 | | zsqcl 13253 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ℤ → (𝐴↑2) ∈
ℤ) |
236 | 215, 235 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐴↑2) ∈ ℤ) |
237 | | peano2zm 11772 |
. . . . . . . . . . . . . 14
⊢ ((𝐴↑2) ∈ ℤ →
((𝐴↑2) − 1)
∈ ℤ) |
238 | 236, 237 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝐴↑2) − 1) ∈
ℤ) |
239 | 238, 143 | zmulcld 11840 |
. . . . . . . . . . . 12
⊢ (𝜑 → (((𝐴↑2) − 1) · 𝐸) ∈
ℤ) |
240 | | dvdsmultr2 15428 |
. . . . . . . . . . . 12
⊢ (((2
· 𝐶) ∈ ℤ
∧ (((𝐴↑2) −
1) · 𝐸) ∈
ℤ ∧ 𝐸 ∈
ℤ) → ((2 · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸))) |
241 | 213, 239,
143, 240 | syl3anc 1439 |
. . . . . . . . . . 11
⊢ (𝜑 → ((2 · 𝐶) ∥ 𝐸 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸))) |
242 | 234, 241 | mpd 15 |
. . . . . . . . . 10
⊢ (𝜑 → (2 · 𝐶) ∥ ((((𝐴↑2) − 1) · 𝐸) · 𝐸)) |
243 | 185 | sqvald 13324 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸↑2) = (𝐸 · 𝐸)) |
244 | 243 | oveq2d 6938 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) = (((𝐴↑2) − 1) · (𝐸 · 𝐸))) |
245 | 202 | sqcld 13325 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴↑2) ∈ ℂ) |
246 | | subcl 10621 |
. . . . . . . . . . . . 13
⊢ (((𝐴↑2) ∈ ℂ ∧ 1
∈ ℂ) → ((𝐴↑2) − 1) ∈
ℂ) |
247 | 245, 189,
246 | sylancl 580 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((𝐴↑2) − 1) ∈
ℂ) |
248 | 247, 185,
185 | mulassd 10400 |
. . . . . . . . . . 11
⊢ (𝜑 → ((((𝐴↑2) − 1) · 𝐸) · 𝐸) = (((𝐴↑2) − 1) · (𝐸 · 𝐸))) |
249 | 244, 248 | eqtr4d 2816 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) = ((((𝐴↑2) − 1) ·
𝐸) · 𝐸)) |
250 | 242, 249 | breqtrrd 4914 |
. . . . . . . . 9
⊢ (𝜑 → (2 · 𝐶) ∥ (((𝐴↑2) − 1) · (𝐸↑2))) |
251 | 48 | sqcld 13325 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹↑2) ∈ ℂ) |
252 | 185 | sqcld 13325 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐸↑2) ∈ ℂ) |
253 | 247, 252 | mulcld 10397 |
. . . . . . . . . . 11
⊢ (𝜑 → (((𝐴↑2) − 1) · (𝐸↑2)) ∈
ℂ) |
254 | 189 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → 1 ∈
ℂ) |
255 | | subsub23 10627 |
. . . . . . . . . . 11
⊢ (((𝐹↑2) ∈ ℂ ∧
(((𝐴↑2) − 1)
· (𝐸↑2)) ∈
ℂ ∧ 1 ∈ ℂ) → (((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ↔ ((𝐹↑2) − 1) = (((𝐴↑2) − 1) ·
(𝐸↑2)))) |
256 | 251, 253,
254, 255 | syl3anc 1439 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝐹↑2) − (((𝐴↑2) − 1) · (𝐸↑2))) = 1 ↔ ((𝐹↑2) − 1) = (((𝐴↑2) − 1) ·
(𝐸↑2)))) |
257 | 174, 256 | mpbid 224 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹↑2) − 1) = (((𝐴↑2) − 1) · (𝐸↑2))) |
258 | 250, 257 | breqtrrd 4914 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝐶) ∥ ((𝐹↑2) − 1)) |
259 | | congsub 38488 |
. . . . . . . . 9
⊢ ((((2
· 𝐶) ∈ ℤ
∧ (𝐹↑2) ∈
ℤ ∧ 1 ∈ ℤ) ∧ (𝐴 ∈ ℤ ∧ 𝐴 ∈ ℤ) ∧ ((2 · 𝐶) ∥ ((𝐹↑2) − 1) ∧ (2 · 𝐶) ∥ (𝐴 − 𝐴))) → (2 · 𝐶) ∥ (((𝐹↑2) − 𝐴) − (1 − 𝐴))) |
260 | 213, 224,
225, 215, 215, 258, 223, 259 | syl322anc 1466 |
. . . . . . . 8
⊢ (𝜑 → (2 · 𝐶) ∥ (((𝐹↑2) − 𝐴) − (1 − 𝐴))) |
261 | | congmul 38485 |
. . . . . . . 8
⊢ ((((2
· 𝐶) ∈ ℤ
∧ (𝐹↑2) ∈
ℤ ∧ 1 ∈ ℤ) ∧ (((𝐹↑2) − 𝐴) ∈ ℤ ∧ (1 − 𝐴) ∈ ℤ) ∧ ((2
· 𝐶) ∥ ((𝐹↑2) − 1) ∧ (2
· 𝐶) ∥
(((𝐹↑2) − 𝐴) − (1 − 𝐴)))) → (2 · 𝐶) ∥ (((𝐹↑2) · ((𝐹↑2) − 𝐴)) − (1 · (1 − 𝐴)))) |
262 | 213, 224,
225, 197, 219, 258, 260, 261 | syl322anc 1466 |
. . . . . . 7
⊢ (𝜑 → (2 · 𝐶) ∥ (((𝐹↑2) · ((𝐹↑2) − 𝐴)) − (1 · (1 − 𝐴)))) |
263 | | congadd 38484 |
. . . . . . 7
⊢ ((((2
· 𝐶) ∈ ℤ
∧ 𝐴 ∈ ℤ
∧ 𝐴 ∈ ℤ)
∧ (((𝐹↑2) ·
((𝐹↑2) − 𝐴)) ∈ ℤ ∧ (1
· (1 − 𝐴))
∈ ℤ) ∧ ((2 · 𝐶) ∥ (𝐴 − 𝐴) ∧ (2 · 𝐶) ∥ (((𝐹↑2) · ((𝐹↑2) − 𝐴)) − (1 · (1 − 𝐴))))) → (2 · 𝐶) ∥ ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − (𝐴 + (1 · (1 − 𝐴))))) |
264 | 213, 215,
215, 216, 221, 223, 262, 263 | syl322anc 1466 |
. . . . . 6
⊢ (𝜑 → (2 · 𝐶) ∥ ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − (𝐴 + (1 · (1 − 𝐴))))) |
265 | 47 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 𝐺 = (𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴)))) |
266 | 219 | zcnd 11835 |
. . . . . . . . . 10
⊢ (𝜑 → (1 − 𝐴) ∈
ℂ) |
267 | 266 | mulid2d 10395 |
. . . . . . . . 9
⊢ (𝜑 → (1 · (1 −
𝐴)) = (1 − 𝐴)) |
268 | 267 | oveq2d 6938 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 + (1 · (1 − 𝐴))) = (𝐴 + (1 − 𝐴))) |
269 | | pncan3 10630 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 1 ∈
ℂ) → (𝐴 + (1
− 𝐴)) =
1) |
270 | 202, 189,
269 | sylancl 580 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 + (1 − 𝐴)) = 1) |
271 | 268, 270 | eqtr2d 2814 |
. . . . . . 7
⊢ (𝜑 → 1 = (𝐴 + (1 · (1 − 𝐴)))) |
272 | 265, 271 | oveq12d 6940 |
. . . . . 6
⊢ (𝜑 → (𝐺 − 1) = ((𝐴 + ((𝐹↑2) · ((𝐹↑2) − 𝐴))) − (𝐴 + (1 · (1 − 𝐴))))) |
273 | 264, 272 | breqtrrd 4914 |
. . . . 5
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐺 − 1)) |
274 | | jm2.15nn0 38521 |
. . . . . . . 8
⊢ ((𝐺 ∈
(ℤ≥‘2) ∧ 𝐴 ∈ (ℤ≥‘2)
∧ 𝐵 ∈
ℕ0) → (𝐺 − 𝐴) ∥ ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵))) |
275 | 82, 2, 90, 274 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → (𝐺 − 𝐴) ∥ ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵))) |
276 | 85 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 = (𝐺 Yrm 𝐵)) |
277 | 276, 12 | oveq12d 6940 |
. . . . . . 7
⊢ (𝜑 → (𝐻 − 𝐶) = ((𝐺 Yrm 𝐵) − (𝐴 Yrm 𝐵))) |
278 | 275, 277 | breqtrrd 4914 |
. . . . . 6
⊢ (𝜑 → (𝐺 − 𝐴) ∥ (𝐻 − 𝐶)) |
279 | | eluzelz 12002 |
. . . . . . . . 9
⊢ (𝐺 ∈
(ℤ≥‘2) → 𝐺 ∈ ℤ) |
280 | 82, 279 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐺 ∈ ℤ) |
281 | 280, 215 | zsubcld 11839 |
. . . . . . 7
⊢ (𝜑 → (𝐺 − 𝐴) ∈ ℤ) |
282 | 85, 87 | syl5eqel 2862 |
. . . . . . . 8
⊢ (𝜑 → 𝐻 ∈ ℤ) |
283 | 282, 14 | zsubcld 11839 |
. . . . . . 7
⊢ (𝜑 → (𝐻 − 𝐶) ∈ ℤ) |
284 | | dvdstr 15425 |
. . . . . . 7
⊢ ((𝐹 ∈ ℤ ∧ (𝐺 − 𝐴) ∈ ℤ ∧ (𝐻 − 𝐶) ∈ ℤ) → ((𝐹 ∥ (𝐺 − 𝐴) ∧ (𝐺 − 𝐴) ∥ (𝐻 − 𝐶)) → 𝐹 ∥ (𝐻 − 𝐶))) |
285 | 196, 281,
283, 284 | syl3anc 1439 |
. . . . . 6
⊢ (𝜑 → ((𝐹 ∥ (𝐺 − 𝐴) ∧ (𝐺 − 𝐴) ∥ (𝐻 − 𝐶)) → 𝐹 ∥ (𝐻 − 𝐶))) |
286 | 210, 278,
285 | mp2and 689 |
. . . . 5
⊢ (𝜑 → 𝐹 ∥ (𝐻 − 𝐶)) |
287 | | jm2.16nn0 38522 |
. . . . . . . . 9
⊢ ((𝐺 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ ℕ0) → (𝐺 − 1) ∥ ((𝐺 Yrm 𝐵) − 𝐵)) |
288 | 82, 90, 287 | syl2anc 579 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 − 1) ∥ ((𝐺 Yrm 𝐵) − 𝐵)) |
289 | 85 | oveq1i 6932 |
. . . . . . . 8
⊢ (𝐻 − 𝐵) = ((𝐺 Yrm 𝐵) − 𝐵) |
290 | 288, 289 | syl6breqr 4928 |
. . . . . . 7
⊢ (𝜑 → (𝐺 − 1) ∥ (𝐻 − 𝐵)) |
291 | | peano2zm 11772 |
. . . . . . . . 9
⊢ (𝐺 ∈ ℤ → (𝐺 − 1) ∈
ℤ) |
292 | 280, 291 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → (𝐺 − 1) ∈ ℤ) |
293 | 282, 4 | zsubcld 11839 |
. . . . . . . 8
⊢ (𝜑 → (𝐻 − 𝐵) ∈ ℤ) |
294 | | dvdstr 15425 |
. . . . . . . 8
⊢ (((2
· 𝐶) ∈ ℤ
∧ (𝐺 − 1) ∈
ℤ ∧ (𝐻 −
𝐵) ∈ ℤ) →
(((2 · 𝐶) ∥
(𝐺 − 1) ∧ (𝐺 − 1) ∥ (𝐻 − 𝐵)) → (2 · 𝐶) ∥ (𝐻 − 𝐵))) |
295 | 213, 292,
293, 294 | syl3anc 1439 |
. . . . . . 7
⊢ (𝜑 → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ (𝐺 − 1) ∥ (𝐻 − 𝐵)) → (2 · 𝐶) ∥ (𝐻 − 𝐵))) |
296 | 273, 290,
295 | mp2and 689 |
. . . . . 6
⊢ (𝜑 → (2 · 𝐶) ∥ (𝐻 − 𝐵)) |
297 | | rmygeid 38482 |
. . . . . . . 8
⊢ ((𝐴 ∈
(ℤ≥‘2) ∧ 𝐵 ∈ ℕ0) → 𝐵 ≤ (𝐴 Yrm 𝐵)) |
298 | 2, 90, 297 | syl2anc 579 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ≤ (𝐴 Yrm 𝐵)) |
299 | 298, 12 | breqtrrd 4914 |
. . . . . 6
⊢ (𝜑 → 𝐵 ≤ 𝐶) |
300 | 296, 299 | jca 507 |
. . . . 5
⊢ (𝜑 → ((2 · 𝐶) ∥ (𝐻 − 𝐵) ∧ 𝐵 ≤ 𝐶)) |
301 | 273, 286,
300 | jca31 510 |
. . . 4
⊢ (𝜑 → (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻 − 𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻 − 𝐵) ∧ 𝐵 ≤ 𝐶))) |
302 | 175, 211,
301 | jca31 510 |
. . 3
⊢ (𝜑 → (((((𝐷↑2) − (((𝐴↑2) − 1) · (𝐶↑2))) = 1 ∧ ((𝐹↑2) − (((𝐴↑2) − 1) ·
(𝐸↑2))) = 1 ∧
𝐺 ∈
(ℤ≥‘2)) ∧ (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺 − 𝐴))) ∧ (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻 − 𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻 − 𝐵) ∧ 𝐵 ≤ 𝐶)))) |
303 | 160, 302 | jca 507 |
. 2
⊢ (𝜑 → (𝐽 ∈ ℕ0 ∧ (((((𝐷↑2) − (((𝐴↑2) − 1) ·
(𝐶↑2))) = 1 ∧
((𝐹↑2) −
(((𝐴↑2) − 1)
· (𝐸↑2))) = 1
∧ 𝐺 ∈
(ℤ≥‘2)) ∧ (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺 − 𝐴))) ∧ (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻 − 𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻 − 𝐵) ∧ 𝐵 ≤ 𝐶))))) |
304 | 45, 103, 303 | jca31 510 |
1
⊢ (𝜑 → (((𝐷 ∈ ℕ0 ∧ 𝐸 ∈ ℕ0
∧ 𝐹 ∈
ℕ0) ∧ (𝐺 ∈ ℕ0 ∧ 𝐻 ∈ ℕ0
∧ 𝐼 ∈
ℕ0)) ∧ (𝐽 ∈ ℕ0 ∧ (((((𝐷↑2) − (((𝐴↑2) − 1) ·
(𝐶↑2))) = 1 ∧
((𝐹↑2) −
(((𝐴↑2) − 1)
· (𝐸↑2))) = 1
∧ 𝐺 ∈
(ℤ≥‘2)) ∧ (((𝐼↑2) − (((𝐺↑2) − 1) · (𝐻↑2))) = 1 ∧ 𝐸 = ((𝐽 + 1) · (2 · (𝐶↑2))) ∧ 𝐹 ∥ (𝐺 − 𝐴))) ∧ (((2 · 𝐶) ∥ (𝐺 − 1) ∧ 𝐹 ∥ (𝐻 − 𝐶)) ∧ ((2 · 𝐶) ∥ (𝐻 − 𝐵) ∧ 𝐵 ≤ 𝐶)))))) |