Proof of Theorem m1mod0mod1
| Step | Hyp | Ref
| Expression |
| 1 | | recn 11245 |
. . . . . . 7
⊢ (𝐴 ∈ ℝ → 𝐴 ∈
ℂ) |
| 2 | | npcan1 11688 |
. . . . . . . 8
⊢ (𝐴 ∈ ℂ → ((𝐴 − 1) + 1) = 𝐴) |
| 3 | 2 | eqcomd 2743 |
. . . . . . 7
⊢ (𝐴 ∈ ℂ → 𝐴 = ((𝐴 − 1) + 1)) |
| 4 | 1, 3 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ℝ → 𝐴 = ((𝐴 − 1) + 1)) |
| 5 | 4 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → 𝐴 = ((𝐴 − 1) + 1)) |
| 6 | 5 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → 𝐴 = ((𝐴 − 1) + 1)) |
| 7 | 6 | oveq1d 7446 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → (𝐴 mod 𝑁) = (((𝐴 − 1) + 1) mod 𝑁)) |
| 8 | | simpr 484 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → ((𝐴 − 1) mod 𝑁) = 0) |
| 9 | | 1mod 13943 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 1 <
𝑁) → (1 mod 𝑁) = 1) |
| 10 | 9 | 3adant1 1131 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → (1 mod 𝑁) = 1) |
| 11 | 10 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → (1 mod 𝑁) = 1) |
| 12 | 8, 11 | oveq12d 7449 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → (((𝐴 − 1) mod 𝑁) + (1 mod 𝑁)) = (0 + 1)) |
| 13 | 12 | oveq1d 7446 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → ((((𝐴 − 1) mod 𝑁) + (1 mod 𝑁)) mod 𝑁) = ((0 + 1) mod 𝑁)) |
| 14 | | peano2rem 11576 |
. . . . . . . 8
⊢ (𝐴 ∈ ℝ → (𝐴 − 1) ∈
ℝ) |
| 15 | 14 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → (𝐴 − 1) ∈
ℝ) |
| 16 | | 1red 11262 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → 1 ∈
ℝ) |
| 17 | | simpl 482 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 1 <
𝑁) → 𝑁 ∈ ℝ) |
| 18 | | 0lt1 11785 |
. . . . . . . . . . 11
⊢ 0 <
1 |
| 19 | | 0re 11263 |
. . . . . . . . . . . 12
⊢ 0 ∈
ℝ |
| 20 | | 1re 11261 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ |
| 21 | | lttr 11337 |
. . . . . . . . . . . 12
⊢ ((0
∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ) → ((0 < 1 ∧ 1
< 𝑁) → 0 < 𝑁)) |
| 22 | 19, 20, 21 | mp3an12 1453 |
. . . . . . . . . . 11
⊢ (𝑁 ∈ ℝ → ((0 <
1 ∧ 1 < 𝑁) → 0
< 𝑁)) |
| 23 | 18, 22 | mpani 696 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℝ → (1 <
𝑁 → 0 < 𝑁)) |
| 24 | 23 | imp 406 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 1 <
𝑁) → 0 < 𝑁) |
| 25 | 17, 24 | elrpd 13074 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 1 <
𝑁) → 𝑁 ∈
ℝ+) |
| 26 | 25 | 3adant1 1131 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → 𝑁 ∈
ℝ+) |
| 27 | 15, 16, 26 | 3jca 1129 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → ((𝐴 − 1) ∈ ℝ ∧
1 ∈ ℝ ∧ 𝑁
∈ ℝ+)) |
| 28 | 27 | adantr 480 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → ((𝐴 − 1) ∈ ℝ ∧
1 ∈ ℝ ∧ 𝑁
∈ ℝ+)) |
| 29 | | modaddabs 13949 |
. . . . 5
⊢ (((𝐴 − 1) ∈ ℝ ∧
1 ∈ ℝ ∧ 𝑁
∈ ℝ+) → ((((𝐴 − 1) mod 𝑁) + (1 mod 𝑁)) mod 𝑁) = (((𝐴 − 1) + 1) mod 𝑁)) |
| 30 | 28, 29 | syl 17 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → ((((𝐴 − 1) mod 𝑁) + (1 mod 𝑁)) mod 𝑁) = (((𝐴 − 1) + 1) mod 𝑁)) |
| 31 | | 0p1e1 12388 |
. . . . . . . 8
⊢ (0 + 1) =
1 |
| 32 | 31 | oveq1i 7441 |
. . . . . . 7
⊢ ((0 + 1)
mod 𝑁) = (1 mod 𝑁) |
| 33 | 32, 9 | eqtrid 2789 |
. . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ 1 <
𝑁) → ((0 + 1) mod
𝑁) = 1) |
| 34 | 33 | 3adant1 1131 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → ((0 + 1) mod
𝑁) = 1) |
| 35 | 34 | adantr 480 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → ((0 + 1) mod 𝑁) = 1) |
| 36 | 13, 30, 35 | 3eqtr3d 2785 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → (((𝐴 − 1) + 1) mod 𝑁) = 1) |
| 37 | 7, 36 | eqtrd 2777 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ ((𝐴 − 1) mod 𝑁) = 0) → (𝐴 mod 𝑁) = 1) |
| 38 | | simpr 484 |
. . . . . 6
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ (𝐴 mod 𝑁) = 1) → (𝐴 mod 𝑁) = 1) |
| 39 | 38 | eqcomd 2743 |
. . . . 5
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ (𝐴 mod 𝑁) = 1) → 1 = (𝐴 mod 𝑁)) |
| 40 | 39 | oveq2d 7447 |
. . . 4
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ (𝐴 mod 𝑁) = 1) → (𝐴 − 1) = (𝐴 − (𝐴 mod 𝑁))) |
| 41 | 40 | oveq1d 7446 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ (𝐴 mod 𝑁) = 1) → ((𝐴 − 1) mod 𝑁) = ((𝐴 − (𝐴 mod 𝑁)) mod 𝑁)) |
| 42 | | simp1 1137 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → 𝐴 ∈ ℝ) |
| 43 | 42, 26 | modcld 13915 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → (𝐴 mod 𝑁) ∈ ℝ) |
| 44 | 43 | recnd 11289 |
. . . . . . 7
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → (𝐴 mod 𝑁) ∈ ℂ) |
| 45 | 44 | subidd 11608 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → ((𝐴 mod 𝑁) − (𝐴 mod 𝑁)) = 0) |
| 46 | 45 | oveq1d 7446 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → (((𝐴 mod 𝑁) − (𝐴 mod 𝑁)) mod 𝑁) = (0 mod 𝑁)) |
| 47 | | modsubmod 13970 |
. . . . . 6
⊢ ((𝐴 ∈ ℝ ∧ (𝐴 mod 𝑁) ∈ ℝ ∧ 𝑁 ∈ ℝ+) → (((𝐴 mod 𝑁) − (𝐴 mod 𝑁)) mod 𝑁) = ((𝐴 − (𝐴 mod 𝑁)) mod 𝑁)) |
| 48 | 42, 43, 26, 47 | syl3anc 1373 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → (((𝐴 mod 𝑁) − (𝐴 mod 𝑁)) mod 𝑁) = ((𝐴 − (𝐴 mod 𝑁)) mod 𝑁)) |
| 49 | | 0mod 13942 |
. . . . . 6
⊢ (𝑁 ∈ ℝ+
→ (0 mod 𝑁) =
0) |
| 50 | 26, 49 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → (0 mod 𝑁) = 0) |
| 51 | 46, 48, 50 | 3eqtr3d 2785 |
. . . 4
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → ((𝐴 − (𝐴 mod 𝑁)) mod 𝑁) = 0) |
| 52 | 51 | adantr 480 |
. . 3
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ (𝐴 mod 𝑁) = 1) → ((𝐴 − (𝐴 mod 𝑁)) mod 𝑁) = 0) |
| 53 | 41, 52 | eqtrd 2777 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) ∧ (𝐴 mod 𝑁) = 1) → ((𝐴 − 1) mod 𝑁) = 0) |
| 54 | 37, 53 | impbida 801 |
1
⊢ ((𝐴 ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ 1 <
𝑁) → (((𝐴 − 1) mod 𝑁) = 0 ↔ (𝐴 mod 𝑁) = 1)) |