Step | Hyp | Ref
| Expression |
1 | | eulerth.1 |
. . . . . 6
⊢ (𝜑 → (𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) |
2 | 1 | simp1d 994 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈ ℕ) |
3 | 2 | phicld 12097 |
. . . 4
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℕ) |
4 | | elnnuz 9476 |
. . . 4
⊢
((ϕ‘𝑁)
∈ ℕ ↔ (ϕ‘𝑁) ∈
(ℤ≥‘1)) |
5 | 3, 4 | sylib 121 |
. . 3
⊢ (𝜑 → (ϕ‘𝑁) ∈
(ℤ≥‘1)) |
6 | | eluzfz2 9935 |
. . 3
⊢
((ϕ‘𝑁)
∈ (ℤ≥‘1) → (ϕ‘𝑁) ∈ (1...(ϕ‘𝑁))) |
7 | 5, 6 | syl 14 |
. 2
⊢ (𝜑 → (ϕ‘𝑁) ∈
(1...(ϕ‘𝑁))) |
8 | | oveq2 5833 |
. . . . . . 7
⊢ (𝑤 = 1 → (1...𝑤) = (1...1)) |
9 | 8 | prodeq1d 11465 |
. . . . . 6
⊢ (𝑤 = 1 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) |
10 | 9 | oveq2d 5841 |
. . . . 5
⊢ (𝑤 = 1 → (𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = (𝑁 gcd ∏𝑥 ∈ (1...1)(𝐹‘𝑥))) |
11 | 10 | eqeq1d 2166 |
. . . 4
⊢ (𝑤 = 1 → ((𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = 1 ↔ (𝑁 gcd ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) = 1)) |
12 | 11 | imbi2d 229 |
. . 3
⊢ (𝑤 = 1 → ((𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = 1) ↔ (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) = 1))) |
13 | | oveq2 5833 |
. . . . . . 7
⊢ (𝑤 = 𝑘 → (1...𝑤) = (1...𝑘)) |
14 | 13 | prodeq1d 11465 |
. . . . . 6
⊢ (𝑤 = 𝑘 → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) |
15 | 14 | oveq2d 5841 |
. . . . 5
⊢ (𝑤 = 𝑘 → (𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥))) |
16 | 15 | eqeq1d 2166 |
. . . 4
⊢ (𝑤 = 𝑘 → ((𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = 1 ↔ (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1)) |
17 | 16 | imbi2d 229 |
. . 3
⊢ (𝑤 = 𝑘 → ((𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = 1) ↔ (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1))) |
18 | | oveq2 5833 |
. . . . . . 7
⊢ (𝑤 = (𝑘 + 1) → (1...𝑤) = (1...(𝑘 + 1))) |
19 | 18 | prodeq1d 11465 |
. . . . . 6
⊢ (𝑤 = (𝑘 + 1) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) |
20 | 19 | oveq2d 5841 |
. . . . 5
⊢ (𝑤 = (𝑘 + 1) → (𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = (𝑁 gcd ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥))) |
21 | 20 | eqeq1d 2166 |
. . . 4
⊢ (𝑤 = (𝑘 + 1) → ((𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = 1 ↔ (𝑁 gcd ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = 1)) |
22 | 21 | imbi2d 229 |
. . 3
⊢ (𝑤 = (𝑘 + 1) → ((𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = 1) ↔ (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = 1))) |
23 | | oveq2 5833 |
. . . . . . 7
⊢ (𝑤 = (ϕ‘𝑁) → (1...𝑤) = (1...(ϕ‘𝑁))) |
24 | 23 | prodeq1d 11465 |
. . . . . 6
⊢ (𝑤 = (ϕ‘𝑁) → ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥) = ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) |
25 | 24 | oveq2d 5841 |
. . . . 5
⊢ (𝑤 = (ϕ‘𝑁) → (𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = (𝑁 gcd ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥))) |
26 | 25 | eqeq1d 2166 |
. . . 4
⊢ (𝑤 = (ϕ‘𝑁) → ((𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = 1 ↔ (𝑁 gcd ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) = 1)) |
27 | 26 | imbi2d 229 |
. . 3
⊢ (𝑤 = (ϕ‘𝑁) → ((𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...𝑤)(𝐹‘𝑥)) = 1) ↔ (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) = 1))) |
28 | | 1z 9194 |
. . . . . . 7
⊢ 1 ∈
ℤ |
29 | | eulerth.2 |
. . . . . . . . . . 11
⊢ 𝑆 = {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} |
30 | | ssrab2 3213 |
. . . . . . . . . . 11
⊢ {𝑦 ∈ (0..^𝑁) ∣ (𝑦 gcd 𝑁) = 1} ⊆ (0..^𝑁) |
31 | 29, 30 | eqsstri 3160 |
. . . . . . . . . 10
⊢ 𝑆 ⊆ (0..^𝑁) |
32 | | fzo0ssnn0 10118 |
. . . . . . . . . 10
⊢
(0..^𝑁) ⊆
ℕ0 |
33 | 31, 32 | sstri 3137 |
. . . . . . . . 9
⊢ 𝑆 ⊆
ℕ0 |
34 | | nn0sscn 9096 |
. . . . . . . . 9
⊢
ℕ0 ⊆ ℂ |
35 | 33, 34 | sstri 3137 |
. . . . . . . 8
⊢ 𝑆 ⊆
ℂ |
36 | | eulerth.4 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆) |
37 | | f1of 5415 |
. . . . . . . . . 10
⊢ (𝐹:(1...(ϕ‘𝑁))–1-1-onto→𝑆 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
38 | 36, 37 | syl 14 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
39 | 3 | nnge1d 8877 |
. . . . . . . . . 10
⊢ (𝜑 → 1 ≤ (ϕ‘𝑁)) |
40 | | uzid 9454 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℤ → 1 ∈ (ℤ≥‘1)) |
41 | 28, 40 | ax-mp 5 |
. . . . . . . . . . 11
⊢ 1 ∈
(ℤ≥‘1) |
42 | 3 | nnzd 9286 |
. . . . . . . . . . 11
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℤ) |
43 | | elfz5 9921 |
. . . . . . . . . . 11
⊢ ((1
∈ (ℤ≥‘1) ∧ (ϕ‘𝑁) ∈ ℤ) → (1 ∈
(1...(ϕ‘𝑁))
↔ 1 ≤ (ϕ‘𝑁))) |
44 | 41, 42, 43 | sylancr 411 |
. . . . . . . . . 10
⊢ (𝜑 → (1 ∈
(1...(ϕ‘𝑁))
↔ 1 ≤ (ϕ‘𝑁))) |
45 | 39, 44 | mpbird 166 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
(1...(ϕ‘𝑁))) |
46 | 38, 45 | ffvelrnd 5604 |
. . . . . . . 8
⊢ (𝜑 → (𝐹‘1) ∈ 𝑆) |
47 | 35, 46 | sseldi 3126 |
. . . . . . 7
⊢ (𝜑 → (𝐹‘1) ∈ ℂ) |
48 | | fveq2 5469 |
. . . . . . . 8
⊢ (𝑥 = 1 → (𝐹‘𝑥) = (𝐹‘1)) |
49 | 48 | fprod1 11495 |
. . . . . . 7
⊢ ((1
∈ ℤ ∧ (𝐹‘1) ∈ ℂ) →
∏𝑥 ∈
(1...1)(𝐹‘𝑥) = (𝐹‘1)) |
50 | 28, 47, 49 | sylancr 411 |
. . . . . 6
⊢ (𝜑 → ∏𝑥 ∈ (1...1)(𝐹‘𝑥) = (𝐹‘1)) |
51 | 50 | oveq2d 5841 |
. . . . 5
⊢ (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) = (𝑁 gcd (𝐹‘1))) |
52 | 2 | nnzd 9286 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℤ) |
53 | | nn0ssz 9186 |
. . . . . . . 8
⊢
ℕ0 ⊆ ℤ |
54 | 33, 53 | sstri 3137 |
. . . . . . 7
⊢ 𝑆 ⊆
ℤ |
55 | 54, 46 | sseldi 3126 |
. . . . . 6
⊢ (𝜑 → (𝐹‘1) ∈ ℤ) |
56 | | gcdcom 11861 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ (𝐹‘1) ∈ ℤ) →
(𝑁 gcd (𝐹‘1)) = ((𝐹‘1) gcd 𝑁)) |
57 | 52, 55, 56 | syl2anc 409 |
. . . . 5
⊢ (𝜑 → (𝑁 gcd (𝐹‘1)) = ((𝐹‘1) gcd 𝑁)) |
58 | | oveq1 5832 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘1) → (𝑦 gcd 𝑁) = ((𝐹‘1) gcd 𝑁)) |
59 | 58 | eqeq1d 2166 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘1) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘1) gcd 𝑁) = 1)) |
60 | 59, 29 | elrab2 2871 |
. . . . . . 7
⊢ ((𝐹‘1) ∈ 𝑆 ↔ ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1)) |
61 | 46, 60 | sylib 121 |
. . . . . 6
⊢ (𝜑 → ((𝐹‘1) ∈ (0..^𝑁) ∧ ((𝐹‘1) gcd 𝑁) = 1)) |
62 | 61 | simprd 113 |
. . . . 5
⊢ (𝜑 → ((𝐹‘1) gcd 𝑁) = 1) |
63 | 51, 57, 62 | 3eqtrd 2194 |
. . . 4
⊢ (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) = 1) |
64 | 63 | a1i 9 |
. . 3
⊢
((ϕ‘𝑁)
∈ (ℤ≥‘1) → (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...1)(𝐹‘𝑥)) = 1)) |
65 | | simpr 109 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1) → (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1) |
66 | 38 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
67 | | fzofzp1 10130 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁))) |
68 | 67 | adantl 275 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑘 + 1) ∈ (1...(ϕ‘𝑁))) |
69 | 66, 68 | ffvelrnd 5604 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ 𝑆) |
70 | 54, 69 | sseldi 3126 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝐹‘(𝑘 + 1)) ∈ ℤ) |
71 | 52 | adantr 274 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑁 ∈ ℤ) |
72 | | gcdcom 11861 |
. . . . . . . . . . 11
⊢ (((𝐹‘(𝑘 + 1)) ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐹‘(𝑘 + 1)) gcd 𝑁) = (𝑁 gcd (𝐹‘(𝑘 + 1)))) |
73 | 70, 71, 72 | syl2anc 409 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐹‘(𝑘 + 1)) gcd 𝑁) = (𝑁 gcd (𝐹‘(𝑘 + 1)))) |
74 | | oveq1 5832 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝐹‘(𝑘 + 1)) → (𝑦 gcd 𝑁) = ((𝐹‘(𝑘 + 1)) gcd 𝑁)) |
75 | 74 | eqeq1d 2166 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (𝐹‘(𝑘 + 1)) → ((𝑦 gcd 𝑁) = 1 ↔ ((𝐹‘(𝑘 + 1)) gcd 𝑁) = 1)) |
76 | 75, 29 | elrab2 2871 |
. . . . . . . . . . . 12
⊢ ((𝐹‘(𝑘 + 1)) ∈ 𝑆 ↔ ((𝐹‘(𝑘 + 1)) ∈ (0..^𝑁) ∧ ((𝐹‘(𝑘 + 1)) gcd 𝑁) = 1)) |
77 | 76 | simprbi 273 |
. . . . . . . . . . 11
⊢ ((𝐹‘(𝑘 + 1)) ∈ 𝑆 → ((𝐹‘(𝑘 + 1)) gcd 𝑁) = 1) |
78 | 69, 77 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝐹‘(𝑘 + 1)) gcd 𝑁) = 1) |
79 | 73, 78 | eqtr3d 2192 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑁 gcd (𝐹‘(𝑘 + 1))) = 1) |
80 | 79 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1) → (𝑁 gcd (𝐹‘(𝑘 + 1))) = 1) |
81 | 28 | a1i 9 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 1 ∈
ℤ) |
82 | | elfzoelz 10050 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈ ℤ) |
83 | 82 | adantl 275 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈ ℤ) |
84 | 81, 83 | fzfigd 10334 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (1...𝑘) ∈ Fin) |
85 | 38 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
86 | | elfznn 9957 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℕ) |
87 | 86 | nnred 8847 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈ ℝ) |
88 | 87 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ ℝ) |
89 | 3 | nnred 8847 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (ϕ‘𝑁) ∈
ℝ) |
90 | 89 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℝ) |
91 | 82 | ad2antlr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 ∈ ℤ) |
92 | 91 | zred 9287 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 ∈ ℝ) |
93 | | elfzle2 9931 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ≤ 𝑘) |
94 | 93 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ 𝑘) |
95 | | elfzolt2 10059 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 < (ϕ‘𝑁)) |
96 | 95 | ad2antlr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑘 < (ϕ‘𝑁)) |
97 | 88, 92, 90, 94, 96 | lelttrd 8001 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 < (ϕ‘𝑁)) |
98 | 88, 90, 97 | ltled 7995 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ≤ (ϕ‘𝑁)) |
99 | | elfzuz 9925 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...𝑘) → 𝑥 ∈
(ℤ≥‘1)) |
100 | 42 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (ϕ‘𝑁) ∈ ℤ) |
101 | | elfz5 9921 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈
(ℤ≥‘1) ∧ (ϕ‘𝑁) ∈ ℤ) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁))) |
102 | 99, 100, 101 | syl2an2 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁))) |
103 | 98, 102 | mpbird 166 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → 𝑥 ∈ (1...(ϕ‘𝑁))) |
104 | 85, 103 | ffvelrnd 5604 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ 𝑆) |
105 | 54, 104 | sseldi 3126 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...𝑘)) → (𝐹‘𝑥) ∈ ℤ) |
106 | 84, 105 | fprodzcl 11510 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) ∈ ℤ) |
107 | | rpmul 11979 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧
∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) ∈ ℤ ∧ (𝐹‘(𝑘 + 1)) ∈ ℤ) → (((𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑘 + 1))) = 1) → (𝑁 gcd (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))) = 1)) |
108 | 71, 106, 70, 107 | syl3anc 1220 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (((𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑘 + 1))) = 1) → (𝑁 gcd (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))) = 1)) |
109 | 108 | adantr 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1) → (((𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1 ∧ (𝑁 gcd (𝐹‘(𝑘 + 1))) = 1) → (𝑁 gcd (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))) = 1)) |
110 | 65, 80, 109 | mp2and 430 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1) → (𝑁 gcd (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))) = 1) |
111 | | elfzouz 10054 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → 𝑘 ∈
(ℤ≥‘1)) |
112 | 111 | adantl 275 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → 𝑘 ∈
(ℤ≥‘1)) |
113 | 38 | ad2antrr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝐹:(1...(ϕ‘𝑁))⟶𝑆) |
114 | | elfzelz 9929 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℤ) |
115 | 114 | zred 9287 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈ ℝ) |
116 | 115 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ ℝ) |
117 | 82 | ad2antlr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑘 ∈ ℤ) |
118 | 117 | peano2zd 9290 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ ℤ) |
119 | 118 | zred 9287 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ∈ ℝ) |
120 | 89 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈
ℝ) |
121 | | elfzle2 9931 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ≤ (𝑘 + 1)) |
122 | 121 | adantl 275 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (𝑘 + 1)) |
123 | | elfzle2 9931 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 + 1) ∈
(1...(ϕ‘𝑁))
→ (𝑘 + 1) ≤
(ϕ‘𝑁)) |
124 | 67, 123 | syl 14 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝑘 + 1) ≤ (ϕ‘𝑁)) |
125 | 124 | ad2antlr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑘 + 1) ≤ (ϕ‘𝑁)) |
126 | 116, 119,
120, 122, 125 | letrd 8000 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ≤ (ϕ‘𝑁)) |
127 | | elfzuz 9925 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1...(𝑘 + 1)) → 𝑥 ∈
(ℤ≥‘1)) |
128 | 42 | ad2antrr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (ϕ‘𝑁) ∈
ℤ) |
129 | 127, 128,
101 | syl2an2 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝑥 ∈ (1...(ϕ‘𝑁)) ↔ 𝑥 ≤ (ϕ‘𝑁))) |
130 | 126, 129 | mpbird 166 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → 𝑥 ∈ (1...(ϕ‘𝑁))) |
131 | 113, 130 | ffvelrnd 5604 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ 𝑆) |
132 | 35, 131 | sseldi 3126 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ 𝑥 ∈ (1...(𝑘 + 1))) → (𝐹‘𝑥) ∈ ℂ) |
133 | | fveq2 5469 |
. . . . . . . . . . 11
⊢ (𝑥 = (𝑘 + 1) → (𝐹‘𝑥) = (𝐹‘(𝑘 + 1))) |
134 | 112, 132,
133 | fprodp1 11501 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥) = (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))) |
135 | 134 | oveq2d 5841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → (𝑁 gcd ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = (𝑁 gcd (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1))))) |
136 | 135 | eqeq1d 2166 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝑁 gcd ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = 1 ↔ (𝑁 gcd (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))) = 1)) |
137 | 136 | adantr 274 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1) → ((𝑁 gcd ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = 1 ↔ (𝑁 gcd (∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥) · (𝐹‘(𝑘 + 1)))) = 1)) |
138 | 110, 137 | mpbird 166 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) ∧ (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1) → (𝑁 gcd ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = 1) |
139 | 138 | ex 114 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1..^(ϕ‘𝑁))) → ((𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1 → (𝑁 gcd ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = 1)) |
140 | 139 | expcom 115 |
. . . 4
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → (𝜑 → ((𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1 → (𝑁 gcd ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = 1))) |
141 | 140 | a2d 26 |
. . 3
⊢ (𝑘 ∈ (1..^(ϕ‘𝑁)) → ((𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...𝑘)(𝐹‘𝑥)) = 1) → (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...(𝑘 + 1))(𝐹‘𝑥)) = 1))) |
142 | 12, 17, 22, 27, 64, 141 | fzind2 10142 |
. 2
⊢
((ϕ‘𝑁)
∈ (1...(ϕ‘𝑁)) → (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) = 1)) |
143 | 7, 142 | mpcom 36 |
1
⊢ (𝜑 → (𝑁 gcd ∏𝑥 ∈ (1...(ϕ‘𝑁))(𝐹‘𝑥)) = 1) |