Metamath Proof Explorer

Theorem nprmdvdsfacm1lem2

Description: Lemma 2 for nprmdvdsfacm1 . (Contributed by AV, 7-Apr-2026)

Ref Expression
Assertion nprmdvdsfacm1lem2 
|- ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> 3 <_ A )

Proof

Step Hyp Ref Expression
1 eluz2 
 |-  ( N e. ( ZZ>= ` 6 ) <-> ( 6 e. ZZ /\ N e. ZZ /\ 6 <_ N ) )
2 breq2 
 |-  ( N = ( A ^ 2 ) -> ( 6 <_ N <-> 6 <_ ( A ^ 2 ) ) )
3 2 adantr 
 |-  ( ( N = ( A ^ 2 ) /\ A e. ( 2 ..^ N ) ) -> ( 6 <_ N <-> 6 <_ ( A ^ 2 ) ) )
4 elfzo2 
 |-  ( A e. ( 2 ..^ N ) <-> ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ A < N ) )
5 eluz2 
 |-  ( A e. ( ZZ>= ` 2 ) <-> ( 2 e. ZZ /\ A e. ZZ /\ 2 <_ A ) )
6 2re 
 |-  2 e. RR
7 6 a1i 
 |-  ( A e. ZZ -> 2 e. RR )
8 zre 
 |-  ( A e. ZZ -> A e. RR )
9 7 8 leloed 
 |-  ( A e. ZZ -> ( 2 <_ A <-> ( 2 < A \/ 2 = A ) ) )
10 df-3 
 |-  3 = ( 2 + 1 )
11 2z 
 |-  2 e. ZZ
12 11 a1i 
 |-  ( A e. ZZ -> 2 e. ZZ )
13 id 
 |-  ( A e. ZZ -> A e. ZZ )
14 12 13 zltp1led 
 |-  ( A e. ZZ -> ( 2 < A <-> ( 2 + 1 ) <_ A ) )
15 14 biimpa 
 |-  ( ( A e. ZZ /\ 2 < A ) -> ( 2 + 1 ) <_ A )
16 10 15 eqbrtrid 
 |-  ( ( A e. ZZ /\ 2 < A ) -> 3 <_ A )
17 16 a1d 
 |-  ( ( A e. ZZ /\ 2 < A ) -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) )
18 17 ex 
 |-  ( A e. ZZ -> ( 2 < A -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) ) )
19 oveq1 
 |-  ( 2 = A -> ( 2 ^ 2 ) = ( A ^ 2 ) )
20 19 breq2d 
 |-  ( 2 = A -> ( 6 <_ ( 2 ^ 2 ) <-> 6 <_ ( A ^ 2 ) ) )
21 sq2 
 |-  ( 2 ^ 2 ) = 4
22 21 breq2i 
 |-  ( 6 <_ ( 2 ^ 2 ) <-> 6 <_ 4 )
23 4lt6 
 |-  4 < 6
24 4re 
 |-  4 e. RR
25 6re 
 |-  6 e. RR
26 24 25 ltnlei 
 |-  ( 4 < 6 <-> -. 6 <_ 4 )
27 23 26 mpbi 
 |-  -. 6 <_ 4
28 27 pm2.21i 
 |-  ( 6 <_ 4 -> 3 <_ A )
29 22 28 sylbi 
 |-  ( 6 <_ ( 2 ^ 2 ) -> 3 <_ A )
30 20 29 biimtrrdi 
 |-  ( 2 = A -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) )
31 30 a1i 
 |-  ( A e. ZZ -> ( 2 = A -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) ) )
32 18 31 jaod 
 |-  ( A e. ZZ -> ( ( 2 < A \/ 2 = A ) -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) ) )
33 9 32 sylbid 
 |-  ( A e. ZZ -> ( 2 <_ A -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) ) )
34 33 a1i 
 |-  ( 2 e. ZZ -> ( A e. ZZ -> ( 2 <_ A -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) ) ) )
35 34 3imp 
 |-  ( ( 2 e. ZZ /\ A e. ZZ /\ 2 <_ A ) -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) )
36 5 35 sylbi 
 |-  ( A e. ( ZZ>= ` 2 ) -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) )
37 36 3ad2ant1 
 |-  ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ /\ A < N ) -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) )
38 4 37 sylbi 
 |-  ( A e. ( 2 ..^ N ) -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) )
39 38 adantl 
 |-  ( ( N = ( A ^ 2 ) /\ A e. ( 2 ..^ N ) ) -> ( 6 <_ ( A ^ 2 ) -> 3 <_ A ) )
40 3 39 sylbid 
 |-  ( ( N = ( A ^ 2 ) /\ A e. ( 2 ..^ N ) ) -> ( 6 <_ N -> 3 <_ A ) )
41 40 ex 
 |-  ( N = ( A ^ 2 ) -> ( A e. ( 2 ..^ N ) -> ( 6 <_ N -> 3 <_ A ) ) )
42 41 com13 
 |-  ( 6 <_ N -> ( A e. ( 2 ..^ N ) -> ( N = ( A ^ 2 ) -> 3 <_ A ) ) )
43 42 3ad2ant3 
 |-  ( ( 6 e. ZZ /\ N e. ZZ /\ 6 <_ N ) -> ( A e. ( 2 ..^ N ) -> ( N = ( A ^ 2 ) -> 3 <_ A ) ) )
44 1 43 sylbi 
 |-  ( N e. ( ZZ>= ` 6 ) -> ( A e. ( 2 ..^ N ) -> ( N = ( A ^ 2 ) -> 3 <_ A ) ) )
45 44 3imp 
 |-  ( ( N e. ( ZZ>= ` 6 ) /\ A e. ( 2 ..^ N ) /\ N = ( A ^ 2 ) ) -> 3 <_ A )