Theorem hashscontpow1

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

	Ref	Expression
Hypotheses	hashscontpow1.1	|- ( ph -> N e. NN )
	hashscontpow1.2	|- ( ph -> A e. ( 1 ... ( ( odZ ` R ) ` N ) ) )
	hashscontpow1.3	|- ( ph -> B e. ( 1 ... ( ( odZ ` R ) ` N ) ) )
	hashscontpow1.4	|- ( ph -> R e. NN )
	hashscontpow1.5	|- ( ph -> ( N gcd R ) = 1 )
	hashscontpow1.6	|- L = ( ZRHom ` Y )
	hashscontpow1.7	|- Y = ( Z/nZ ` R )
	hashscontpow1.8	|- ( ph -> A < B )
Assertion	hashscontpow1	|- ( ph -> ( L ` ( N ^ A ) ) =/= ( L ` ( N ^ B ) ) )

Proof

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