lgsfle1

Description: The function F has magnitude less or equal to 1 . (Contributed by Mario Carneiro, 4-Feb-2015)

		Ref	Expression
	Hypothesis	lgsval.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, {if (n = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1)}^{n pCnt N}, 1))$
	Assertion	lgsfle1	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land M \in ℕ) \to \|F (M)\| \leq 1$

Step	Hyp	Ref	Expression
1		lgsval.1	$⊢ F = (n \in ℕ ⟼ if (n \in ℙ, {if (n = 2, if (2 ∥ A, 0, if (A \mod 8 \in \{1, 7\}, 1, - 1)), ((A^{\frac{n - 1}{2}} + 1) \mod n) - 1)}^{n pCnt N}, 1))$
2		eqid	$⊢ \{x \in ℤ \| \|x\| \leq 1\} = \{x \in ℤ \| \|x\| \leq 1\}$
3	1 2	lgsfcl2	$⊢ (A \in ℤ \land N \in ℤ \land N \neq 0) \to F : ℕ ⟶ \{x \in ℤ \| \|x\| \leq 1\}$
4	3	ffvelcdmda	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land M \in ℕ) \to F (M) \in \{x \in ℤ \| \|x\| \leq 1\}$
5		fveq2	$⊢ x = F (M) \to \|x\| = \|F (M)\|$
6	5	breq1d	$⊢ x = F (M) \to (\|x\| \leq 1 \leftrightarrow \|F (M)\| \leq 1)$
7	6	elrab	$⊢ F (M) \in \{x \in ℤ \| \|x\| \leq 1\} \leftrightarrow (F (M) \in ℤ \land \|F (M)\| \leq 1)$
8	7	simprbi	$⊢ F (M) \in \{x \in ℤ \| \|x\| \leq 1\} \to \|F (M)\| \leq 1$
9	4 8	syl	$⊢ ((A \in ℤ \land N \in ℤ \land N \neq 0) \land M \in ℕ) \to \|F (M)\| \leq 1$

Metamath Proof Explorer