Metamath Proof Explorer

Theorem hgt749d

Description: A deduction version of ax-hgt749 . (Contributed by Thierry Arnoux, 15-Dec-2021)

Ref Expression
Hypotheses hgt749d.o 
|- O = { z e. ZZ | -. 2 || z }
hgt749d.n 
|- ( ph -> N e. O )
hgt749d.1 
|- ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N )
Assertion hgt749d 
|- ( ph -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) )

Proof

Step Hyp Ref Expression
1 hgt749d.o 
 |-  O = { z e. ZZ | -. 2 || z }
2 hgt749d.n 
 |-  ( ph -> N e. O )
3 hgt749d.1 
 |-  ( ph -> ( ; 1 0 ^ ; 2 7 ) <_ N )
4 breq2 
 |-  ( n = N -> ( ( ; 1 0 ^ ; 2 7 ) <_ n <-> ( ; 1 0 ^ ; 2 7 ) <_ N ) )
5 oveq1 
 |-  ( n = N -> ( n ^ 2 ) = ( N ^ 2 ) )
6 5 oveq2d 
 |-  ( n = N -> ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) = ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) )
7 oveq2 
 |-  ( n = N -> ( ( Lam oF x. h ) vts n ) = ( ( Lam oF x. h ) vts N ) )
8 7 fveq1d 
 |-  ( n = N -> ( ( ( Lam oF x. h ) vts n ) ` x ) = ( ( ( Lam oF x. h ) vts N ) ` x ) )
9 oveq2 
 |-  ( n = N -> ( ( Lam oF x. k ) vts n ) = ( ( Lam oF x. k ) vts N ) )
10 9 fveq1d 
 |-  ( n = N -> ( ( ( Lam oF x. k ) vts n ) ` x ) = ( ( ( Lam oF x. k ) vts N ) ` x ) )
11 10 oveq1d 
 |-  ( n = N -> ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) = ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) )
12 8 11 oveq12d 
 |-  ( n = N -> ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) = ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) )
13 negeq 
 |-  ( n = N -> -u n = -u N )
14 13 oveq1d 
 |-  ( n = N -> ( -u n x. x ) = ( -u N x. x ) )
15 14 oveq2d 
 |-  ( n = N -> ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) = ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) )
16 15 fveq2d 
 |-  ( n = N -> ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) = ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) )
17 12 16 oveq12d 
 |-  ( n = N -> ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) = ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) )
18 17 adantr 
 |-  ( ( n = N /\ x e. ( 0 (,) 1 ) ) -> ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) = ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) )
19 18 itgeq2dv 
 |-  ( n = N -> S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x = S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x )
20 6 19 breq12d 
 |-  ( n = N -> ( ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x <-> ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) )
21 20 3anbi3d 
 |-  ( n = N -> ( ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) <-> ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) )
22 21 rexbidv 
 |-  ( n = N -> ( E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) <-> E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) )
23 22 rexbidv 
 |-  ( n = N -> ( E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) <-> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) )
24 4 23 imbi12d 
 |-  ( n = N -> ( ( ( ; 1 0 ^ ; 2 7 ) <_ n -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) ) <-> ( ( ; 1 0 ^ ; 2 7 ) <_ N -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) ) )
25 ax-hgt749 
 |-  A. n e. { z e. ZZ | -. 2 || z } ( ( ; 1 0 ^ ; 2 7 ) <_ n -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) )
26 25 a1i 
 |-  ( ph -> A. n e. { z e. ZZ | -. 2 || z } ( ( ; 1 0 ^ ; 2 7 ) <_ n -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( n ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts n ) ` x ) x. ( ( ( ( Lam oF x. k ) vts n ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u n x. x ) ) ) ) _d x ) ) )
27 2 1 eleqtrdi 
 |-  ( ph -> N e. { z e. ZZ | -. 2 || z } )
28 24 26 27 rspcdva 
 |-  ( ph -> ( ( ; 1 0 ^ ; 2 7 ) <_ N -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) ) )
29 3 28 mpd 
 |-  ( ph -> E. h e. ( ( 0 [,) +oo ) ^m NN ) E. k e. ( ( 0 [,) +oo ) ^m NN ) ( A. m e. NN ( k ` m ) <_ ( 1 . _ 0 _ 7 _ 9 _ 9 _ 5 5 ) /\ A. m e. NN ( h ` m ) <_ ( 1 . _ 4 _ 1 4 ) /\ ( ( 0 . _ 0 _ 0 _ 0 _ 4 _ 2 _ 2 _ 4 8 ) x. ( N ^ 2 ) ) <_ S. ( 0 (,) 1 ) ( ( ( ( ( Lam oF x. h ) vts N ) ` x ) x. ( ( ( ( Lam oF x. k ) vts N ) ` x ) ^ 2 ) ) x. ( exp ` ( ( _i x. ( 2 x. _pi ) ) x. ( -u N x. x ) ) ) ) _d x ) )