# Metamath Proof Explorer

## Theorem 1mod

Description: Special case: 1 modulo a real number greater than 1 is 1. (Contributed by Mario Carneiro, 18-Feb-2014)

Ref Expression
Assertion 1mod ${⊢}\left({N}\in ℝ\wedge 1<{N}\right)\to 1\mathrm{mod}{N}=1$

### Proof

Step Hyp Ref Expression
1 0lt1 ${⊢}0<1$
2 0re ${⊢}0\in ℝ$
3 1re ${⊢}1\in ℝ$
4 lttr ${⊢}\left(0\in ℝ\wedge 1\in ℝ\wedge {N}\in ℝ\right)\to \left(\left(0<1\wedge 1<{N}\right)\to 0<{N}\right)$
5 2 3 4 mp3an12 ${⊢}{N}\in ℝ\to \left(\left(0<1\wedge 1<{N}\right)\to 0<{N}\right)$
6 1 5 mpani ${⊢}{N}\in ℝ\to \left(1<{N}\to 0<{N}\right)$
7 6 imdistani ${⊢}\left({N}\in ℝ\wedge 1<{N}\right)\to \left({N}\in ℝ\wedge 0<{N}\right)$
8 elrp ${⊢}{N}\in {ℝ}^{+}↔\left({N}\in ℝ\wedge 0<{N}\right)$
9 7 8 sylibr ${⊢}\left({N}\in ℝ\wedge 1<{N}\right)\to {N}\in {ℝ}^{+}$
10 9 3 jctil ${⊢}\left({N}\in ℝ\wedge 1<{N}\right)\to \left(1\in ℝ\wedge {N}\in {ℝ}^{+}\right)$
11 simpr ${⊢}\left({N}\in ℝ\wedge 1<{N}\right)\to 1<{N}$
12 0le1 ${⊢}0\le 1$
13 11 12 jctil ${⊢}\left({N}\in ℝ\wedge 1<{N}\right)\to \left(0\le 1\wedge 1<{N}\right)$
14 modid ${⊢}\left(\left(1\in ℝ\wedge {N}\in {ℝ}^{+}\right)\wedge \left(0\le 1\wedge 1<{N}\right)\right)\to 1\mathrm{mod}{N}=1$
15 10 13 14 syl2anc ${⊢}\left({N}\in ℝ\wedge 1<{N}\right)\to 1\mathrm{mod}{N}=1$