Odd powers of 2 equal to 1 and even powers equal to −1 modulo p

Let p ≥ 5 be prime and t the order of 2 in ZMod p. There is an odd j ≤ p − 4 with 2^j = 1, or an even j ≤ p − 3 with 2^j = −1, iff t ≢ 2 (mod 4).

Main results

• ConjeturaC.euler_n3: the equivalence above.

theorem ConjeturaC.natCast_ne_zero_of_lt {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (hk0 : 0 < k) (hk : k < p) : ↑k ≠ 0

theorem ConjeturaC.euler_n3 {p : ℕ} [hp : Fact (Nat.Prime p)] (h5 : 5 ≤ p) : ((∃ (j : ℕ), Odd j ∧ j ≤ p - 4 ∧ 2 ^ j = 1) ∨ ∃ (j : ℕ), Even j ∧ j ≤ p - 3 ∧ 2 ^ j = -1) ↔ ¬orderOf 2 % 4 = 2