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 )