hashscontpow1

Description: Helper lemma for to prove inequality in Zr. (Contributed by metakunt, 28-Apr-2025)

	Ref	Expression
Hypotheses	hashscontpow1.1	$⊢ φ \to N \in ℕ$
	hashscontpow1.2	$⊢ φ \to A \in (1 \dots {od}_{ℤ} (R) (N))$
	hashscontpow1.3	$⊢ φ \to B \in (1 \dots {od}_{ℤ} (R) (N))$
	hashscontpow1.4	$⊢ φ \to R \in ℕ$
	hashscontpow1.5	$⊢ φ \to N \gcd R = 1$
	hashscontpow1.6	$⊢ L = ℤRHom (Y)$
	hashscontpow1.7	$⊢ Y = ℤ / R ℤ$
	hashscontpow1.8	$⊢ φ \to A < B$
Assertion	hashscontpow1	$⊢ φ \to L (N^{A}) \neq L (N^{B})$

Proof

Step	Hyp	Ref	Expression
1		hashscontpow1.1	$⊢ φ \to N \in ℕ$
2		hashscontpow1.2	$⊢ φ \to A \in (1 \dots {od}_{ℤ} (R) (N))$
3		hashscontpow1.3	$⊢ φ \to B \in (1 \dots {od}_{ℤ} (R) (N))$
4		hashscontpow1.4	$⊢ φ \to R \in ℕ$
5		hashscontpow1.5	$⊢ φ \to N \gcd R = 1$
6		hashscontpow1.6	$⊢ L = ℤRHom (Y)$
7		hashscontpow1.7	$⊢ Y = ℤ / R ℤ$
8		hashscontpow1.8	$⊢ φ \to A < B$
9	3	elfzelzd	$⊢ φ \to B \in ℤ$
10	9	zred	$⊢ φ \to B \in ℝ$
11	2	elfzelzd	$⊢ φ \to A \in ℤ$
12	11	zred	$⊢ φ \to A \in ℝ$
13	10 12	resubcld	$⊢ φ \to B - A \in ℝ$
14	1	nnzd	$⊢ φ \to N \in ℤ$
15		odzcl	$⊢ (R \in ℕ \land N \in ℤ \land N \gcd R = 1) \to {od}_{ℤ} (R) (N) \in ℕ$
16	4 14 5 15	syl3anc	$⊢ φ \to {od}_{ℤ} (R) (N) \in ℕ$
17	16	nnred	$⊢ φ \to {od}_{ℤ} (R) (N) \in ℝ$
18		elfznn	$⊢ A \in (1 \dots {od}_{ℤ} (R) (N)) \to A \in ℕ$
19	2 18	syl	$⊢ φ \to A \in ℕ$
20	19	nnrpd	$⊢ φ \to A \in ℝ^{+}$
21	10 20	ltsubrpd	$⊢ φ \to B - A < B$
22		elfzle2	$⊢ B \in (1 \dots {od}_{ℤ} (R) (N)) \to B \leq {od}_{ℤ} (R) (N)$
23	3 22	syl	$⊢ φ \to B \leq {od}_{ℤ} (R) (N)$
24	13 10 17 21 23	ltletrd	$⊢ φ \to B - A < {od}_{ℤ} (R) (N)$
25	24	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to B - A < {od}_{ℤ} (R) (N)$
26		odzval	$⊢ (R \in ℕ \land N \in ℤ \land N \gcd R = 1) \to {od}_{ℤ} (R) (N) = inf (\{i \in ℕ \| R ∥ (N^{i} - 1)\} ℝ <)$
27	4 14 5 26	syl3anc	$⊢ φ \to {od}_{ℤ} (R) (N) = inf (\{i \in ℕ \| R ∥ (N^{i} - 1)\} ℝ <)$
28	27	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to {od}_{ℤ} (R) (N) = inf (\{i \in ℕ \| R ∥ (N^{i} - 1)\} ℝ <)$
29		elrabi	$⊢ j \in \{i \in ℕ \| R ∥ (N^{i} - 1)\} \to j \in ℕ$
30	29	adantl	$⊢ (φ \land j \in \{i \in ℕ \| R ∥ (N^{i} - 1)\}) \to j \in ℕ$
31	30	nnred	$⊢ (φ \land j \in \{i \in ℕ \| R ∥ (N^{i} - 1)\}) \to j \in ℝ$
32	31	ex	$⊢ φ \to (j \in \{i \in ℕ \| R ∥ (N^{i} - 1)\} \to j \in ℝ)$
33	32	ssrdv	$⊢ φ \to \{i \in ℕ \| R ∥ (N^{i} - 1)\} \subseteq ℝ$
34	33	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to \{i \in ℕ \| R ∥ (N^{i} - 1)\} \subseteq ℝ$
35		1red	$⊢ φ \to 1 \in ℝ$
36		simpr	$⊢ (φ \land x = 1) \to x = 1$
37	36	breq1d	$⊢ (φ \land x = 1) \to (x \leq y \leftrightarrow 1 \leq y)$
38	37	ralbidv	$⊢ (φ \land x = 1) \to (\forall y \in \{i \in ℕ \| R ∥ (N^{i} - 1)\} x \leq y \leftrightarrow \forall y \in \{i \in ℕ \| R ∥ (N^{i} - 1)\} 1 \leq y)$
39		elrabi	$⊢ y \in \{i \in ℕ \| R ∥ (N^{i} - 1)\} \to y \in ℕ$
40	39	adantl	$⊢ (φ \land y \in \{i \in ℕ \| R ∥ (N^{i} - 1)\}) \to y \in ℕ$
41	40	nnge1d	$⊢ (φ \land y \in \{i \in ℕ \| R ∥ (N^{i} - 1)\}) \to 1 \leq y$
42	41	ralrimiva	$⊢ φ \to \forall y \in \{i \in ℕ \| R ∥ (N^{i} - 1)\} 1 \leq y$
43	35 38 42	rspcedvd	$⊢ φ \to \exists x \in ℝ \forall y \in \{i \in ℕ \| R ∥ (N^{i} - 1)\} x \leq y$
44	43	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to \exists x \in ℝ \forall y \in \{i \in ℕ \| R ∥ (N^{i} - 1)\} x \leq y$
45		oveq2	$⊢ i = B - A \to N^{i} = N^{B - A}$
46	45	oveq1d	$⊢ i = B - A \to N^{i} - 1 = N^{B - A} - 1$
47	46	breq2d	$⊢ i = B - A \to (R ∥ (N^{i} - 1) \leftrightarrow R ∥ (N^{B - A} - 1))$
48	9	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to B \in ℤ$
49	11	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to A \in ℤ$
50	48 49	zsubcld	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to B - A \in ℤ$
51	12 10	posdifd	$⊢ φ \to (A < B \leftrightarrow 0 < B - A)$
52	8 51	mpbid	$⊢ φ \to 0 < B - A$
53	52	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to 0 < B - A$
54	50 53	jca	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to (B - A \in ℤ \land 0 < B - A)$
55		elnnz	$⊢ B - A \in ℕ \leftrightarrow (B - A \in ℤ \land 0 < B - A)$
56	54 55	sylibr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to B - A \in ℕ$
57	4	nnzd	$⊢ φ \to R \in ℤ$
58	57	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to R \in ℤ$
59	14	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to N \in ℤ$
60	19	nnnn0d	$⊢ φ \to A \in ℕ_{0}$
61	60	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to A \in ℕ_{0}$
62	59 61	zexpcld	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to N^{A} \in ℤ$
63	56	nnnn0d	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to B - A \in ℕ_{0}$
64	59 63	zexpcld	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to N^{B - A} \in ℤ$
65		1zzd	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to 1 \in ℤ$
66	64 65	zsubcld	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to N^{B - A} - 1 \in ℤ$
67	58 62 66	3jca	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to (R \in ℤ \land N^{A} \in ℤ \land N^{B - A} - 1 \in ℤ)$
68		simpr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to L (N^{A}) = L (N^{B})$
69	68	eqcomd	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to L (N^{B}) = L (N^{A})$
70	4	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
71	70	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to R \in ℕ_{0}$
72		elfznn	$⊢ B \in (1 \dots {od}_{ℤ} (R) (N)) \to B \in ℕ$
73	3 72	syl	$⊢ φ \to B \in ℕ$
74	73	nnnn0d	$⊢ φ \to B \in ℕ_{0}$
75	14 74	zexpcld	$⊢ φ \to N^{B} \in ℤ$
76	75	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to N^{B} \in ℤ$
77	7 6	zndvds	$⊢ (R \in ℕ_{0} \land N^{B} \in ℤ \land N^{A} \in ℤ) \to (L (N^{B}) = L (N^{A}) \leftrightarrow R ∥ (N^{B} - N^{A}))$
78	71 76 62 77	syl3anc	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to (L (N^{B}) = L (N^{A}) \leftrightarrow R ∥ (N^{B} - N^{A}))$
79	69 78	mpbid	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to R ∥ (N^{B} - N^{A})$
80	14 60	zexpcld	$⊢ φ \to N^{A} \in ℤ$
81	80	zcnd	$⊢ φ \to N^{A} \in ℂ$
82	9 11	zsubcld	$⊢ φ \to B - A \in ℤ$
83		0red	$⊢ φ \to 0 \in ℝ$
84	83 13 52	ltled	$⊢ φ \to 0 \leq B - A$
85	82 84	jca	$⊢ φ \to (B - A \in ℤ \land 0 \leq B - A)$
86		elnn0z	$⊢ B - A \in ℕ_{0} \leftrightarrow (B - A \in ℤ \land 0 \leq B - A)$
87	85 86	sylibr	$⊢ φ \to B - A \in ℕ_{0}$
88	14 87	zexpcld	$⊢ φ \to N^{B - A} \in ℤ$
89	88	zcnd	$⊢ φ \to N^{B - A} \in ℂ$
90		1cnd	$⊢ φ \to 1 \in ℂ$
91	81 89 90	subdid	$⊢ φ \to N^{A} (N^{B - A} - 1) = N^{A} N^{B - A} - N^{A} \cdot 1$
92	12	recnd	$⊢ φ \to A \in ℂ$
93	10	recnd	$⊢ φ \to B \in ℂ$
94	92 93	pncan3d	$⊢ φ \to A + B - A = B$
95	94	eqcomd	$⊢ φ \to B = A + B - A$
96	95	oveq2d	$⊢ φ \to N^{B} = N^{A + B - A}$
97	1	nncnd	$⊢ φ \to N \in ℂ$
98	97 87 60	expaddd	$⊢ φ \to N^{A + B - A} = N^{A} N^{B - A}$
99	96 98	eqtrd	$⊢ φ \to N^{B} = N^{A} N^{B - A}$
100	99	eqcomd	$⊢ φ \to N^{A} N^{B - A} = N^{B}$
101	81	mulridd	$⊢ φ \to N^{A} \cdot 1 = N^{A}$
102	100 101	oveq12d	$⊢ φ \to N^{A} N^{B - A} - N^{A} \cdot 1 = N^{B} - N^{A}$
103	91 102	eqtr2d	$⊢ φ \to N^{B} - N^{A} = N^{A} (N^{B - A} - 1)$
104	103	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to N^{B} - N^{A} = N^{A} (N^{B - A} - 1)$
105	79 104	breqtrd	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to R ∥ N^{A} (N^{B - A} - 1)$
106	57 80	gcdcomd	$⊢ φ \to R \gcd N^{A} = N^{A} \gcd R$
107		rpexp	$⊢ (N \in ℤ \land R \in ℤ \land A \in ℕ) \to (N^{A} \gcd R = 1 \leftrightarrow N \gcd R = 1)$
108	14 57 19 107	syl3anc	$⊢ φ \to (N^{A} \gcd R = 1 \leftrightarrow N \gcd R = 1)$
109	5 108	mpbird	$⊢ φ \to N^{A} \gcd R = 1$
110	106 109	eqtrd	$⊢ φ \to R \gcd N^{A} = 1$
111	110	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to R \gcd N^{A} = 1$
112	105 111	jca	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to (R ∥ N^{A} (N^{B - A} - 1) \land R \gcd N^{A} = 1)$
113		coprmdvds	$⊢ (R \in ℤ \land N^{A} \in ℤ \land N^{B - A} - 1 \in ℤ) \to ((R ∥ N^{A} (N^{B - A} - 1) \land R \gcd N^{A} = 1) \to R ∥ (N^{B - A} - 1))$
114	113	imp	$⊢ ((R \in ℤ \land N^{A} \in ℤ \land N^{B - A} - 1 \in ℤ) \land (R ∥ N^{A} (N^{B - A} - 1) \land R \gcd N^{A} = 1)) \to R ∥ (N^{B - A} - 1)$
115	67 112 114	syl2anc	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to R ∥ (N^{B - A} - 1)$
116	47 56 115	elrabd	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to B - A \in \{i \in ℕ \| R ∥ (N^{i} - 1)\}$
117		infrelb	$⊢ (\{i \in ℕ \| R ∥ (N^{i} - 1)\} \subseteq ℝ \land \exists x \in ℝ \forall y \in \{i \in ℕ \| R ∥ (N^{i} - 1)\} x \leq y \land B - A \in \{i \in ℕ \| R ∥ (N^{i} - 1)\}) \to inf (\{i \in ℕ \| R ∥ (N^{i} - 1)\} ℝ <) \leq B - A$
118	34 44 116 117	syl3anc	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to inf (\{i \in ℕ \| R ∥ (N^{i} - 1)\} ℝ <) \leq B - A$
119	28 118	eqbrtrd	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to {od}_{ℤ} (R) (N) \leq B - A$
120	16	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to {od}_{ℤ} (R) (N) \in ℕ$
121	120	nnred	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to {od}_{ℤ} (R) (N) \in ℝ$
122	13	adantr	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to B - A \in ℝ$
123	121 122	lenltd	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to ({od}_{ℤ} (R) (N) \leq B - A \leftrightarrow \neg B - A < {od}_{ℤ} (R) (N))$
124	119 123	mpbid	$⊢ (φ \land L (N^{A}) = L (N^{B})) \to \neg B - A < {od}_{ℤ} (R) (N)$
125	25 124	pm2.65da	$⊢ φ \to \neg L (N^{A}) = L (N^{B})$
126	125	neqned	$⊢ φ \to L (N^{A}) \neq L (N^{B})$

Metamath Proof Explorer

Theorem hashscontpow1

Proof