This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( 1 mod 𝑁 ) = 1 )

Proof

Step Hyp Ref Expression
1 0lt1 ⊢ 0 < 1
2 0re ⊢ 0 ∈ ℝ
3 1re ⊢ 1 ∈ ℝ
4 lttr ⊢ ( ( 0 ∈ ℝ ∧ 1 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( ( 0 < 1 ∧ 1 < 𝑁 ) → 0 < 𝑁 ) )
5 2 3 4 mp3an12 ⊢ ( 𝑁 ∈ ℝ → ( ( 0 < 1 ∧ 1 < 𝑁 ) → 0 < 𝑁 ) )
6 1 5 mpani ⊢ ( 𝑁 ∈ ℝ → ( 1 < 𝑁 → 0 < 𝑁 ) )
7 6 imdistani ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
8 elrp ⊢ ( 𝑁 ∈ ℝ+ ↔ ( 𝑁 ∈ ℝ ∧ 0 < 𝑁 ) )
9 7 8 sylibr ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → 𝑁 ∈ ℝ+ )
10 9 3 jctil ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) )
11 simpr ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → 1 < 𝑁 )
12 0le1 ⊢ 0 ≤ 1
13 11 12 jctil ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( 0 ≤ 1 ∧ 1 < 𝑁 ) )
14 modid ⊢ ( ( ( 1 ∈ ℝ ∧ 𝑁 ∈ ℝ+ ) ∧ ( 0 ≤ 1 ∧ 1 < 𝑁 ) ) → ( 1 mod 𝑁 ) = 1 )
15 10 13 14 syl2anc ⊢ ( ( 𝑁 ∈ ℝ ∧ 1 < 𝑁 ) → ( 1 mod 𝑁 ) = 1 )