modirr

Description: A number modulo an irrational multiple of it is nonzero. (Contributed by NM, 11-Nov-2008)

		Ref	Expression
	Assertion	modirr	$⊢ (A \in ℝ \land B \in ℝ^{+} \land \frac{A}{B} \in (ℝ ∖ ℚ)) \to A \mod B \neq 0$

Proof

Step	Hyp	Ref	Expression
1		eldif	$⊢ \frac{A}{B} \in (ℝ ∖ ℚ) \leftrightarrow (\frac{A}{B} \in ℝ \land \neg \frac{A}{B} \in ℚ)$
2		modval	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \mod B = A - B ⌊\frac{A}{B}⌋$
3	2	eqeq1d	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B = 0 \leftrightarrow A - B ⌊\frac{A}{B}⌋ = 0)$
4		recn	$⊢ A \in ℝ \to A \in ℂ$
5	4	adantr	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to A \in ℂ$
6		rpre	$⊢ B \in ℝ^{+} \to B \in ℝ$
7	6	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B \in ℝ$
8		refldivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℝ$
9	7 8	remulcld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B ⌊\frac{A}{B}⌋ \in ℝ$
10	9	recnd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to B ⌊\frac{A}{B}⌋ \in ℂ$
11	5 10	subeq0ad	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A - B ⌊\frac{A}{B}⌋ = 0 \leftrightarrow A = B ⌊\frac{A}{B}⌋)$
12		rerpdivcl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to \frac{A}{B} \in ℝ$
13		reflcl	$⊢ \frac{A}{B} \in ℝ \to ⌊\frac{A}{B}⌋ \in ℝ$
14	13	recnd	$⊢ \frac{A}{B} \in ℝ \to ⌊\frac{A}{B}⌋ \in ℂ$
15	12 14	syl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ⌊\frac{A}{B}⌋ \in ℂ$
16		rpcnne0	$⊢ B \in ℝ^{+} \to (B \in ℂ \land B \neq 0)$
17	16	adantl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (B \in ℂ \land B \neq 0)$
18		divmul2	$⊢ (A \in ℂ \land ⌊\frac{A}{B}⌋ \in ℂ \land (B \in ℂ \land B \neq 0)) \to (\frac{A}{B} = ⌊\frac{A}{B}⌋ \leftrightarrow A = B ⌊\frac{A}{B}⌋)$
19	5 15 17 18	syl3anc	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (\frac{A}{B} = ⌊\frac{A}{B}⌋ \leftrightarrow A = B ⌊\frac{A}{B}⌋)$
20		eqcom	$⊢ \frac{A}{B} = ⌊\frac{A}{B}⌋ \leftrightarrow ⌊\frac{A}{B}⌋ = \frac{A}{B}$
21	19 20	bitr3di	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A = B ⌊\frac{A}{B}⌋ \leftrightarrow ⌊\frac{A}{B}⌋ = \frac{A}{B})$
22	3 11 21	3bitrd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B = 0 \leftrightarrow ⌊\frac{A}{B}⌋ = \frac{A}{B})$
23		flidz	$⊢ \frac{A}{B} \in ℝ \to (⌊\frac{A}{B}⌋ = \frac{A}{B} \leftrightarrow \frac{A}{B} \in ℤ)$
24		zq	$⊢ \frac{A}{B} \in ℤ \to \frac{A}{B} \in ℚ$
25	23 24	syl6bi	$⊢ \frac{A}{B} \in ℝ \to (⌊\frac{A}{B}⌋ = \frac{A}{B} \to \frac{A}{B} \in ℚ)$
26	12 25	syl	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (⌊\frac{A}{B}⌋ = \frac{A}{B} \to \frac{A}{B} \in ℚ)$
27	22 26	sylbid	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (A \mod B = 0 \to \frac{A}{B} \in ℚ)$
28	27	necon3bd	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (\neg \frac{A}{B} \in ℚ \to A \mod B \neq 0)$
29	28	adantld	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to ((\frac{A}{B} \in ℝ \land \neg \frac{A}{B} \in ℚ) \to A \mod B \neq 0)$
30	1 29	syl5bi	$⊢ (A \in ℝ \land B \in ℝ^{+}) \to (\frac{A}{B} \in (ℝ ∖ ℚ) \to A \mod B \neq 0)$
31	30	3impia	$⊢ (A \in ℝ \land B \in ℝ^{+} \land \frac{A}{B} \in (ℝ ∖ ℚ)) \to A \mod B \neq 0$

Metamath Proof Explorer

Theorem modirr

Proof