Proof of Theorem odadd1
Step | Hyp | Ref
| Expression |
1 | | ablgrp 19175 |
. . . . . . . . 9
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
2 | | odadd1.2 |
. . . . . . . . . 10
⊢ 𝑋 = (Base‘𝐺) |
3 | | odadd1.3 |
. . . . . . . . . 10
⊢ + =
(+g‘𝐺) |
4 | 2, 3 | grpcl 18373 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + 𝐵) ∈ 𝑋) |
5 | 1, 4 | syl3an1 1165 |
. . . . . . . 8
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 + 𝐵) ∈ 𝑋) |
6 | | odadd1.1 |
. . . . . . . . 9
⊢ 𝑂 = (od‘𝐺) |
7 | 2, 6 | odcl 18928 |
. . . . . . . 8
⊢ ((𝐴 + 𝐵) ∈ 𝑋 → (𝑂‘(𝐴 + 𝐵)) ∈
ℕ0) |
8 | 5, 7 | syl 17 |
. . . . . . 7
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑂‘(𝐴 + 𝐵)) ∈
ℕ0) |
9 | 8 | nn0zd 12280 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑂‘(𝐴 + 𝐵)) ∈ ℤ) |
10 | 2, 6 | odcl 18928 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝑋 → (𝑂‘𝐴) ∈
ℕ0) |
11 | 10 | 3ad2ant2 1136 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑂‘𝐴) ∈
ℕ0) |
12 | 11 | nn0zd 12280 |
. . . . . . . 8
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑂‘𝐴) ∈ ℤ) |
13 | 2, 6 | odcl 18928 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑋 → (𝑂‘𝐵) ∈
ℕ0) |
14 | 13 | 3ad2ant3 1137 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑂‘𝐵) ∈
ℕ0) |
15 | 14 | nn0zd 12280 |
. . . . . . . 8
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝑂‘𝐵) ∈ ℤ) |
16 | 12, 15 | gcdcld 16067 |
. . . . . . 7
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∈
ℕ0) |
17 | 16 | nn0zd 12280 |
. . . . . 6
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∈ ℤ) |
18 | 9, 17 | zmulcld 12288 |
. . . . 5
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ) |
19 | 18 | adantr 484 |
. . . 4
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) = 0) → ((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ) |
20 | | dvds0 15833 |
. . . 4
⊢ (((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ → ((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∥ 0) |
21 | 19, 20 | syl 17 |
. . 3
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) = 0) → ((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∥ 0) |
22 | | gcdeq0 16076 |
. . . . . 6
⊢ (((𝑂‘𝐴) ∈ ℤ ∧ (𝑂‘𝐵) ∈ ℤ) → (((𝑂‘𝐴) gcd (𝑂‘𝐵)) = 0 ↔ ((𝑂‘𝐴) = 0 ∧ (𝑂‘𝐵) = 0))) |
23 | 12, 15, 22 | syl2anc 587 |
. . . . 5
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑂‘𝐴) gcd (𝑂‘𝐵)) = 0 ↔ ((𝑂‘𝐴) = 0 ∧ (𝑂‘𝐵) = 0))) |
24 | 23 | biimpa 480 |
. . . 4
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) = 0) → ((𝑂‘𝐴) = 0 ∧ (𝑂‘𝐵) = 0)) |
25 | | oveq12 7222 |
. . . . 5
⊢ (((𝑂‘𝐴) = 0 ∧ (𝑂‘𝐵) = 0) → ((𝑂‘𝐴) · (𝑂‘𝐵)) = (0 · 0)) |
26 | | 0cn 10825 |
. . . . . 6
⊢ 0 ∈
ℂ |
27 | 26 | mul01i 11022 |
. . . . 5
⊢ (0
· 0) = 0 |
28 | 25, 27 | eqtrdi 2794 |
. . . 4
⊢ (((𝑂‘𝐴) = 0 ∧ (𝑂‘𝐵) = 0) → ((𝑂‘𝐴) · (𝑂‘𝐵)) = 0) |
29 | 24, 28 | syl 17 |
. . 3
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) = 0) → ((𝑂‘𝐴) · (𝑂‘𝐵)) = 0) |
30 | 21, 29 | breqtrrd 5081 |
. 2
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) = 0) → ((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∥ ((𝑂‘𝐴) · (𝑂‘𝐵))) |
31 | | simpl1 1193 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → 𝐺 ∈ Abel) |
32 | 17 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∈ ℤ) |
33 | 12 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝑂‘𝐴) ∈ ℤ) |
34 | 15 | adantr 484 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝑂‘𝐵) ∈ ℤ) |
35 | | gcddvds 16062 |
. . . . . . . . . . 11
⊢ (((𝑂‘𝐴) ∈ ℤ ∧ (𝑂‘𝐵) ∈ ℤ) → (((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ (𝑂‘𝐴) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ (𝑂‘𝐵))) |
36 | 33, 34, 35 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ (𝑂‘𝐴) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ (𝑂‘𝐵))) |
37 | 36 | simpld 498 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ (𝑂‘𝐴)) |
38 | 32, 33, 34, 37 | dvdsmultr1d 15858 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ ((𝑂‘𝐴) · (𝑂‘𝐵))) |
39 | | simpr 488 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) |
40 | 33, 34 | zmulcld 12288 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) · (𝑂‘𝐵)) ∈ ℤ) |
41 | | dvdsval2 15818 |
. . . . . . . . 9
⊢ ((((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∈ ℤ ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0 ∧ ((𝑂‘𝐴) · (𝑂‘𝐵)) ∈ ℤ) → (((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ ((𝑂‘𝐴) · (𝑂‘𝐵)) ↔ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ)) |
42 | 32, 39, 40, 41 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ ((𝑂‘𝐴) · (𝑂‘𝐵)) ↔ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ)) |
43 | 38, 42 | mpbid 235 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ) |
44 | | simpl2 1194 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → 𝐴 ∈ 𝑋) |
45 | | simpl3 1195 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → 𝐵 ∈ 𝑋) |
46 | | eqid 2737 |
. . . . . . . 8
⊢
(.g‘𝐺) = (.g‘𝐺) |
47 | 2, 46, 3 | mulgdi 19212 |
. . . . . . 7
⊢ ((𝐺 ∈ Abel ∧ ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)(𝐴 + 𝐵)) = (((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐴) + ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐵))) |
48 | 31, 43, 44, 45, 47 | syl13anc 1374 |
. . . . . 6
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)(𝐴 + 𝐵)) = (((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐴) + ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐵))) |
49 | 36 | simprd 499 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ (𝑂‘𝐵)) |
50 | | dvdsval2 15818 |
. . . . . . . . . . . 12
⊢ ((((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∈ ℤ ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0 ∧ (𝑂‘𝐵) ∈ ℤ) → (((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ (𝑂‘𝐵) ↔ ((𝑂‘𝐵) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ)) |
51 | 32, 39, 34, 50 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ (𝑂‘𝐵) ↔ ((𝑂‘𝐵) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ)) |
52 | 49, 51 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐵) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ) |
53 | | dvdsmul1 15839 |
. . . . . . . . . 10
⊢ (((𝑂‘𝐴) ∈ ℤ ∧ ((𝑂‘𝐵) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ) → (𝑂‘𝐴) ∥ ((𝑂‘𝐴) · ((𝑂‘𝐵) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))))) |
54 | 33, 52, 53 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝑂‘𝐴) ∥ ((𝑂‘𝐴) · ((𝑂‘𝐵) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))))) |
55 | 33 | zcnd 12283 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝑂‘𝐴) ∈ ℂ) |
56 | 34 | zcnd 12283 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝑂‘𝐵) ∈ ℂ) |
57 | 32 | zcnd 12283 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∈ ℂ) |
58 | 55, 56, 57, 39 | divassd 11643 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) = ((𝑂‘𝐴) · ((𝑂‘𝐵) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))))) |
59 | 54, 58 | breqtrrd 5081 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝑂‘𝐴) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))) |
60 | 31, 1 | syl 17 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → 𝐺 ∈ Grp) |
61 | | eqid 2737 |
. . . . . . . . . 10
⊢
(0g‘𝐺) = (0g‘𝐺) |
62 | 2, 6, 46, 61 | oddvds 18939 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐴 ∈ 𝑋 ∧ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ) → ((𝑂‘𝐴) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ↔ ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐴) = (0g‘𝐺))) |
63 | 60, 44, 43, 62 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ↔ ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐴) = (0g‘𝐺))) |
64 | 59, 63 | mpbid 235 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐴) = (0g‘𝐺)) |
65 | | dvdsval2 15818 |
. . . . . . . . . . . 12
⊢ ((((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∈ ℤ ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0 ∧ (𝑂‘𝐴) ∈ ℤ) → (((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ (𝑂‘𝐴) ↔ ((𝑂‘𝐴) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ)) |
66 | 32, 39, 33, 65 | syl3anc 1373 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∥ (𝑂‘𝐴) ↔ ((𝑂‘𝐴) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ)) |
67 | 37, 66 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ) |
68 | | dvdsmul1 15839 |
. . . . . . . . . 10
⊢ (((𝑂‘𝐵) ∈ ℤ ∧ ((𝑂‘𝐴) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ) → (𝑂‘𝐵) ∥ ((𝑂‘𝐵) · ((𝑂‘𝐴) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))))) |
69 | 34, 67, 68 | syl2anc 587 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝑂‘𝐵) ∥ ((𝑂‘𝐵) · ((𝑂‘𝐴) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))))) |
70 | 55, 56 | mulcomd 10854 |
. . . . . . . . . . 11
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) · (𝑂‘𝐵)) = ((𝑂‘𝐵) · (𝑂‘𝐴))) |
71 | 70 | oveq1d 7228 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) = (((𝑂‘𝐵) · (𝑂‘𝐴)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))) |
72 | 56, 55, 57, 39 | divassd 11643 |
. . . . . . . . . 10
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((𝑂‘𝐵) · (𝑂‘𝐴)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) = ((𝑂‘𝐵) · ((𝑂‘𝐴) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))))) |
73 | 71, 72 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) = ((𝑂‘𝐵) · ((𝑂‘𝐴) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))))) |
74 | 69, 73 | breqtrrd 5081 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝑂‘𝐵) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))) |
75 | 2, 6, 46, 61 | oddvds 18939 |
. . . . . . . . 9
⊢ ((𝐺 ∈ Grp ∧ 𝐵 ∈ 𝑋 ∧ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ) → ((𝑂‘𝐵) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ↔ ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐵) = (0g‘𝐺))) |
76 | 60, 45, 43, 75 | syl3anc 1373 |
. . . . . . . 8
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐵) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ↔ ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐵) = (0g‘𝐺))) |
77 | 74, 76 | mpbid 235 |
. . . . . . 7
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐵) = (0g‘𝐺)) |
78 | 64, 77 | oveq12d 7231 |
. . . . . 6
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐴) + ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)𝐵)) = ((0g‘𝐺) + (0g‘𝐺))) |
79 | 2, 61 | grpidcl 18395 |
. . . . . . 7
⊢ (𝐺 ∈ Grp →
(0g‘𝐺)
∈ 𝑋) |
80 | 2, 3, 61 | grplid 18397 |
. . . . . . 7
⊢ ((𝐺 ∈ Grp ∧
(0g‘𝐺)
∈ 𝑋) →
((0g‘𝐺)
+
(0g‘𝐺)) =
(0g‘𝐺)) |
81 | 60, 79, 80 | syl2anc2 588 |
. . . . . 6
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) →
((0g‘𝐺)
+
(0g‘𝐺)) =
(0g‘𝐺)) |
82 | 48, 78, 81 | 3eqtrd 2781 |
. . . . 5
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)(𝐴 + 𝐵)) = (0g‘𝐺)) |
83 | 5 | adantr 484 |
. . . . . 6
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝐴 + 𝐵) ∈ 𝑋) |
84 | 2, 6, 46, 61 | oddvds 18939 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ (𝐴 + 𝐵) ∈ 𝑋 ∧ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ) → ((𝑂‘(𝐴 + 𝐵)) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ↔ ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)(𝐴 + 𝐵)) = (0g‘𝐺))) |
85 | 60, 83, 43, 84 | syl3anc 1373 |
. . . . 5
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘(𝐴 + 𝐵)) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ↔ ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))(.g‘𝐺)(𝐴 + 𝐵)) = (0g‘𝐺))) |
86 | 82, 85 | mpbird 260 |
. . . 4
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝑂‘(𝐴 + 𝐵)) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵)))) |
87 | 9 | adantr 484 |
. . . . 5
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (𝑂‘(𝐴 + 𝐵)) ∈ ℤ) |
88 | | dvdsmulcr 15847 |
. . . . 5
⊢ (((𝑂‘(𝐴 + 𝐵)) ∈ ℤ ∧ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∈ ℤ ∧ (((𝑂‘𝐴) gcd (𝑂‘𝐵)) ∈ ℤ ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0)) → (((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∥ ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ↔ (𝑂‘(𝐴 + 𝐵)) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))))) |
89 | 87, 43, 32, 39, 88 | syl112anc 1376 |
. . . 4
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → (((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∥ ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ↔ (𝑂‘(𝐴 + 𝐵)) ∥ (((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))))) |
90 | 86, 89 | mpbird 260 |
. . 3
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∥ ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) · ((𝑂‘𝐴) gcd (𝑂‘𝐵)))) |
91 | 40 | zcnd 12283 |
. . . 4
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘𝐴) · (𝑂‘𝐵)) ∈ ℂ) |
92 | 91, 57, 39 | divcan1d 11609 |
. . 3
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((((𝑂‘𝐴) · (𝑂‘𝐵)) / ((𝑂‘𝐴) gcd (𝑂‘𝐵))) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) = ((𝑂‘𝐴) · (𝑂‘𝐵))) |
93 | 90, 92 | breqtrd 5079 |
. 2
⊢ (((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) ∧ ((𝑂‘𝐴) gcd (𝑂‘𝐵)) ≠ 0) → ((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∥ ((𝑂‘𝐴) · (𝑂‘𝐵))) |
94 | 30, 93 | pm2.61dane 3029 |
1
⊢ ((𝐺 ∈ Abel ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((𝑂‘(𝐴 + 𝐵)) · ((𝑂‘𝐴) gcd (𝑂‘𝐵))) ∥ ((𝑂‘𝐴) · (𝑂‘𝐵))) |