Step | Hyp | Ref
| Expression |
1 | | oveq2 7285 |
. . . . . . . . 9
⊢ (𝑚 = 𝑁 → (𝑥 gcd 𝑚) = (𝑥 gcd 𝑁)) |
2 | 1 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑚 = 𝑁 → ((𝑥 gcd 𝑚) = 1 ↔ (𝑥 gcd 𝑁) = 1)) |
3 | 2 | rabbidv 3413 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑚) = 1} = {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑁) = 1}) |
4 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑛 = 𝑥 → (𝑛 gcd 𝑁) = (𝑥 gcd 𝑁)) |
5 | 4 | eqeq1d 2740 |
. . . . . . . 8
⊢ (𝑛 = 𝑥 → ((𝑛 gcd 𝑁) = 1 ↔ (𝑥 gcd 𝑁) = 1)) |
6 | 5 | cbvrabv 3425 |
. . . . . . 7
⊢ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} = {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑁) = 1} |
7 | 3, 6 | eqtr4di 2796 |
. . . . . 6
⊢ (𝑚 = 𝑁 → {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑚) = 1} = {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1}) |
8 | | breq1 5079 |
. . . . . . . 8
⊢ (𝑚 = 𝑁 → (𝑚 ∥ ((𝑥↑𝑛) − 1) ↔ 𝑁 ∥ ((𝑥↑𝑛) − 1))) |
9 | 8 | rabbidv 3413 |
. . . . . . 7
⊢ (𝑚 = 𝑁 → {𝑛 ∈ ℕ ∣ 𝑚 ∥ ((𝑥↑𝑛) − 1)} = {𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}) |
10 | 9 | infeq1d 9234 |
. . . . . 6
⊢ (𝑚 = 𝑁 → inf({𝑛 ∈ ℕ ∣ 𝑚 ∥ ((𝑥↑𝑛) − 1)}, ℝ, < ) = inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}, ℝ, <
)) |
11 | 7, 10 | mpteq12dv 5167 |
. . . . 5
⊢ (𝑚 = 𝑁 → (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑚) = 1} ↦ inf({𝑛 ∈ ℕ ∣ 𝑚 ∥ ((𝑥↑𝑛) − 1)}, ℝ, < )) = (𝑥 ∈ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} ↦ inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}, ℝ, <
))) |
12 | | df-odz 16464 |
. . . . 5
⊢
odℤ = (𝑚 ∈ ℕ ↦ (𝑥 ∈ {𝑥 ∈ ℤ ∣ (𝑥 gcd 𝑚) = 1} ↦ inf({𝑛 ∈ ℕ ∣ 𝑚 ∥ ((𝑥↑𝑛) − 1)}, ℝ, <
))) |
13 | | zex 12326 |
. . . . . 6
⊢ ℤ
∈ V |
14 | 13 | mptrabex 7103 |
. . . . 5
⊢ (𝑥 ∈ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} ↦ inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}, ℝ, < )) ∈
V |
15 | 11, 12, 14 | fvmpt 6877 |
. . . 4
⊢ (𝑁 ∈ ℕ →
(odℤ‘𝑁) = (𝑥 ∈ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} ↦ inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}, ℝ, <
))) |
16 | 15 | fveq1d 6778 |
. . 3
⊢ (𝑁 ∈ ℕ →
((odℤ‘𝑁)‘𝐴) = ((𝑥 ∈ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} ↦ inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}, ℝ, < ))‘𝐴)) |
17 | | oveq1 7284 |
. . . . . 6
⊢ (𝑛 = 𝐴 → (𝑛 gcd 𝑁) = (𝐴 gcd 𝑁)) |
18 | 17 | eqeq1d 2740 |
. . . . 5
⊢ (𝑛 = 𝐴 → ((𝑛 gcd 𝑁) = 1 ↔ (𝐴 gcd 𝑁) = 1)) |
19 | 18 | elrab 3625 |
. . . 4
⊢ (𝐴 ∈ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} ↔ (𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) |
20 | | oveq1 7284 |
. . . . . . . . 9
⊢ (𝑥 = 𝐴 → (𝑥↑𝑛) = (𝐴↑𝑛)) |
21 | 20 | oveq1d 7292 |
. . . . . . . 8
⊢ (𝑥 = 𝐴 → ((𝑥↑𝑛) − 1) = ((𝐴↑𝑛) − 1)) |
22 | 21 | breq2d 5088 |
. . . . . . 7
⊢ (𝑥 = 𝐴 → (𝑁 ∥ ((𝑥↑𝑛) − 1) ↔ 𝑁 ∥ ((𝐴↑𝑛) − 1))) |
23 | 22 | rabbidv 3413 |
. . . . . 6
⊢ (𝑥 = 𝐴 → {𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)} = {𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴↑𝑛) − 1)}) |
24 | 23 | infeq1d 9234 |
. . . . 5
⊢ (𝑥 = 𝐴 → inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}, ℝ, < ) = inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴↑𝑛) − 1)}, ℝ, <
)) |
25 | | eqid 2738 |
. . . . 5
⊢ (𝑥 ∈ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} ↦ inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}, ℝ, < )) = (𝑥 ∈ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} ↦ inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}, ℝ, <
)) |
26 | | ltso 11053 |
. . . . . 6
⊢ < Or
ℝ |
27 | 26 | infex 9250 |
. . . . 5
⊢
inf({𝑛 ∈
ℕ ∣ 𝑁 ∥
((𝐴↑𝑛) − 1)}, ℝ, < ) ∈
V |
28 | 24, 25, 27 | fvmpt 6877 |
. . . 4
⊢ (𝐴 ∈ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} → ((𝑥 ∈ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} ↦ inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}, ℝ, < ))‘𝐴) = inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴↑𝑛) − 1)}, ℝ, <
)) |
29 | 19, 28 | sylbir 234 |
. . 3
⊢ ((𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → ((𝑥 ∈ {𝑛 ∈ ℤ ∣ (𝑛 gcd 𝑁) = 1} ↦ inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝑥↑𝑛) − 1)}, ℝ, < ))‘𝐴) = inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴↑𝑛) − 1)}, ℝ, <
)) |
30 | 16, 29 | sylan9eq 2798 |
. 2
⊢ ((𝑁 ∈ ℕ ∧ (𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1)) →
((odℤ‘𝑁)‘𝐴) = inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴↑𝑛) − 1)}, ℝ, <
)) |
31 | 30 | 3impb 1114 |
1
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) →
((odℤ‘𝑁)‘𝐴) = inf({𝑛 ∈ ℕ ∣ 𝑁 ∥ ((𝐴↑𝑛) − 1)}, ℝ, <
)) |