Step | Hyp | Ref
| Expression |
1 | | fltaccoprm.1 |
. . . 4
⊢ (𝜑 → (𝐴 gcd 𝐵) = 1) |
2 | | fltabcoprmex.a |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℕ) |
3 | | fltabcoprmex.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℕ) |
4 | | coprmgcdb 16354 |
. . . . 5
⊢ ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) →
(∀𝑖 ∈ ℕ
((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) ↔ (𝐴 gcd 𝐵) = 1)) |
5 | 2, 3, 4 | syl2anc 584 |
. . . 4
⊢ (𝜑 → (∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) ↔ (𝐴 gcd 𝐵) = 1)) |
6 | 1, 5 | mpbird 256 |
. . 3
⊢ (𝜑 → ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1)) |
7 | | simprl 768 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → 𝑖 ∥ 𝐴) |
8 | | simpr 485 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℕ) |
9 | 8 | nnzd 12425 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑖 ∈ ℤ) |
10 | | fltabcoprmex.c |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ∈ ℕ) |
11 | 10 | nnzd 12425 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈ ℤ) |
12 | 11 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐶 ∈ ℤ) |
13 | | fltabcoprmex.n |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
14 | 13 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝑁 ∈
ℕ0) |
15 | | dvdsexpim 40328 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ℤ ∧ 𝐶 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝑖 ∥ 𝐶 → (𝑖↑𝑁) ∥ (𝐶↑𝑁))) |
16 | 9, 12, 14, 15 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑖 ∥ 𝐶 → (𝑖↑𝑁) ∥ (𝐶↑𝑁))) |
17 | 2 | nnzd 12425 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℤ) |
18 | 17 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → 𝐴 ∈ ℤ) |
19 | | dvdsexpim 40328 |
. . . . . . . . . . . . . 14
⊢ ((𝑖 ∈ ℤ ∧ 𝐴 ∈ ℤ ∧ 𝑁 ∈ ℕ0)
→ (𝑖 ∥ 𝐴 → (𝑖↑𝑁) ∥ (𝐴↑𝑁))) |
20 | 9, 18, 14, 19 | syl3anc 1370 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑖 ∥ 𝐴 → (𝑖↑𝑁) ∥ (𝐴↑𝑁))) |
21 | 16, 20 | anim12d 609 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑖 ∥ 𝐶 ∧ 𝑖 ∥ 𝐴) → ((𝑖↑𝑁) ∥ (𝐶↑𝑁) ∧ (𝑖↑𝑁) ∥ (𝐴↑𝑁)))) |
22 | 21 | ancomsd 466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶) → ((𝑖↑𝑁) ∥ (𝐶↑𝑁) ∧ (𝑖↑𝑁) ∥ (𝐴↑𝑁)))) |
23 | 22 | imp 407 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → ((𝑖↑𝑁) ∥ (𝐶↑𝑁) ∧ (𝑖↑𝑁) ∥ (𝐴↑𝑁))) |
24 | 8, 14 | nnexpcld 13960 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑖↑𝑁) ∈ ℕ) |
25 | 24 | nnzd 12425 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (𝑖↑𝑁) ∈ ℤ) |
26 | 25 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → (𝑖↑𝑁) ∈ ℤ) |
27 | 10, 13 | nnexpcld 13960 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐶↑𝑁) ∈ ℕ) |
28 | 27 | nnzd 12425 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐶↑𝑁) ∈ ℤ) |
29 | 28 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → (𝐶↑𝑁) ∈ ℤ) |
30 | 2, 13 | nnexpcld 13960 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴↑𝑁) ∈ ℕ) |
31 | 30 | nnzd 12425 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐴↑𝑁) ∈ ℤ) |
32 | 31 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → (𝐴↑𝑁) ∈ ℤ) |
33 | | dvds2sub 16000 |
. . . . . . . . . . 11
⊢ (((𝑖↑𝑁) ∈ ℤ ∧ (𝐶↑𝑁) ∈ ℤ ∧ (𝐴↑𝑁) ∈ ℤ) → (((𝑖↑𝑁) ∥ (𝐶↑𝑁) ∧ (𝑖↑𝑁) ∥ (𝐴↑𝑁)) → (𝑖↑𝑁) ∥ ((𝐶↑𝑁) − (𝐴↑𝑁)))) |
34 | 26, 29, 32, 33 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → (((𝑖↑𝑁) ∥ (𝐶↑𝑁) ∧ (𝑖↑𝑁) ∥ (𝐴↑𝑁)) → (𝑖↑𝑁) ∥ ((𝐶↑𝑁) − (𝐴↑𝑁)))) |
35 | 23, 34 | mpd 15 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → (𝑖↑𝑁) ∥ ((𝐶↑𝑁) − (𝐴↑𝑁))) |
36 | 2 | nncnd 11989 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ ℂ) |
37 | 36, 13 | expcld 13864 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐴↑𝑁) ∈ ℂ) |
38 | 3 | nncnd 11989 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐵 ∈ ℂ) |
39 | 38, 13 | expcld 13864 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐵↑𝑁) ∈ ℂ) |
40 | | fltabcoprmex.1 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁)) |
41 | 37, 39, 40 | laddrotrd 40304 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐶↑𝑁) − (𝐴↑𝑁)) = (𝐵↑𝑁)) |
42 | 41 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → ((𝐶↑𝑁) − (𝐴↑𝑁)) = (𝐵↑𝑁)) |
43 | 35, 42 | breqtrd 5100 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → (𝑖↑𝑁) ∥ (𝐵↑𝑁)) |
44 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → 𝑖 ∈ ℕ) |
45 | 3 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → 𝐵 ∈ ℕ) |
46 | 10 | nncnd 11989 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ ℂ) |
47 | 36, 38, 46, 13, 40 | flt0 40474 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑁 ∈ ℕ) |
48 | 47 | ad2antrr 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → 𝑁 ∈ ℕ) |
49 | | dvdsexpnn 40340 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝑁 ∈ ℕ) → (𝑖 ∥ 𝐵 ↔ (𝑖↑𝑁) ∥ (𝐵↑𝑁))) |
50 | 44, 45, 48, 49 | syl3anc 1370 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → (𝑖 ∥ 𝐵 ↔ (𝑖↑𝑁) ∥ (𝐵↑𝑁))) |
51 | 43, 50 | mpbird 256 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → 𝑖 ∥ 𝐵) |
52 | 7, 51 | jca 512 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑖 ∈ ℕ) ∧ (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶)) → (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵)) |
53 | 52 | ex 413 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶) → (𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵))) |
54 | 53 | imim1d 82 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ℕ) → (((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) → ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶) → 𝑖 = 1))) |
55 | 54 | ralimdva 3108 |
. . 3
⊢ (𝜑 → (∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐵) → 𝑖 = 1) → ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶) → 𝑖 = 1))) |
56 | 6, 55 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶) → 𝑖 = 1)) |
57 | | coprmgcdb 16354 |
. . 3
⊢ ((𝐴 ∈ ℕ ∧ 𝐶 ∈ ℕ) →
(∀𝑖 ∈ ℕ
((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶) → 𝑖 = 1) ↔ (𝐴 gcd 𝐶) = 1)) |
58 | 2, 10, 57 | syl2anc 584 |
. 2
⊢ (𝜑 → (∀𝑖 ∈ ℕ ((𝑖 ∥ 𝐴 ∧ 𝑖 ∥ 𝐶) → 𝑖 = 1) ↔ (𝐴 gcd 𝐶) = 1)) |
59 | 56, 58 | mpbid 231 |
1
⊢ (𝜑 → (𝐴 gcd 𝐶) = 1) |