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	$⊢ (N \in ℝ \land 1 < N) \to 1 \mod N = 1$

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

Metamath Proof Explorer